Releases · goblint/analyzer

02 Aug 11:43

sim642

2.4.0 Latest

Latest

CHANGES:

Remove unmaintained analyses: spec, file (#1281).
Add linear two-variable equalities analysis (#1297, #1412, #1466).
Add callstring, loopfree callstring and context gas analyses (#1038, #1340, #1379, #1427, #1439).
Add non-relational thread-modular value analyses with thread IDs (#1366, #1398, #1399).
Add NULL byte array domain (#1076).
Fix spurious overflow warnings from internal evaluations (#1406, #1411, #1511).
Refactor non-definite mutex handling to fix unsoundness (#1430, #1500, #1503, #1409).
Fix non-relational thread-modular value analysis unsoundness with ambiguous points-to sets (#1457, #1458).
Fix mutex type analysis unsoundness and enable it by default (#1414, #1416, #1510).
Add points-to set refinement on mutex path splitting (#1287, #1343, #1374, #1396, #1407).
Improve narrowing operators (#1502, #1540, #1543).
Extract automatic configuration tuning for soundness (#1369).
Fix many locations in witnesses (#1355, #1372, #1400, #1403).
Improve output readability (#1294, #1312, #1405, #1497).
Refactor logging (#1117).
Modernize all library function specifications (#1029, #688, #1174, #1289, #1447, #1487).
Remove OCaml 4.10, 4.11, 4.12 and 4.13 support (#1448).

Assets 3

24 Nov 21:18

sim642

2.3.0

CHANGES:

Functionally equivalent to Goblint in SV-COMP 2024.

Add termination analysis for loops (#1093).
Add memory out-of-bounds analysis (#1094, #1197).
Add memory leak analysis (#1127, #1241, #1246).
Add SV-COMP termination, valid-memsafety and valid-memcleanup properties support (#1220, #1228, #1201, #1199, #1259, #1262).
Add YAML witness version 2.0 support (#1238, #1240, #1217, #1226, #1225, #1248).
Add final warnings about unsound results (#1190, #1191).
Add many library function specifications (#1167, #1174, #1203, #1205, #1212, #1220, #1239, #1242, #1244, #1254, #1269).
Adapt automatic configuration tuning (#912, #921, #987, #1168, #1214, #1234).

Assets 3

24 Nov 13:52

sim642

SV-COMP 2024

Goblint version tags/svcomp24-0-gc2e9465a7 for SV-COMP 2024.

The verifier archive containing the Ubuntu 22.04 binary and auxiliary files is attached below.

Assets 3

13 Sep 14:03

sim642

2.2.1

CHANGES:

Assets 3

13 Sep 11:31

sim642

2.2.0

CHANGES:

Add setjmp/longjmp analysis (#887, #970, #1015, #1019).
Refactor race analysis to lazy distribution (#1084, #1089, #1136, #1016).
Add thread-unsafe library function call analysis (#723, #1082).
Add mutex type analysis and mutex API analysis (#800, #839, #1073).
Add interval set domain and string literals domain (#901, #966, #994, #1048).
Add affine equalities analysis (#592).
Add use-after-free analysis (#1050, #1114).
Add dead code elimination transformation (#850, #979).
Add taint analysis for partial contexts (#553, #952).
Add YAML witness validation via unassume (#796, #977, #1044, #1045, #1124).
Add incremental analysis rename detection (#774, #777).
Fix address sets unsoundness (#822, #967, #564, #1032, #998, #1031).
Fix thread escape analysis unsoundness (#939, #984, #1074, #1078).
Fix many incremental analysis issues (#627, #836, #835, #841, #932, #678, #942, #949, #950, #957, #955, #954, #960, #959, #1004, #558, #1010, #1091).
Fix server mode for abstract debugging (#983, #990, #997, #1000, #1001, #1013, #1018, #1017, #1026, #1027).
Add documentation for configuration JSON schema and OCaml API (#999, #1054, #1055, #1053).
Add many library function specifications (#962, #996, #1028, #1079, #1121, #1135, #1138).
Add OCaml 5.0 support (#1003, #945, #1162).