-
Notifications
You must be signed in to change notification settings - Fork 88
Open
Labels
relationalRelational analyses (Apron, affeq, lin2var)Relational analyses (Apron, affeq, lin2var)sv-compSV-COMP (analyses, results), witnessesSV-COMP (analyses, results), witnesses
Milestone
Description
While working on the dashboard paper, @karoliineh noticed that Goblint has a lot of crashes in SV-COMP NoOverflows.
A huge chunk of these is Fatal error: exception Invalid_argument("Option.get") which comes from the affeq analysis:
Fatal error: exception Invalid_argument("Option.get")
Marked with transfer function at ../sv-benchmarks/c/Juliet_Test/CWE190_Integer_Overflow__int64_t_max_add_01_bad.i:1555:9-1555:34
Marked with transfer function at ../sv-benchmarks/c/Juliet_Test/CWE190_Integer_Overflow__int64_t_max_add_01_bad.i:1562:5-1562:54
Raised at BatOption.get_exn in file "src/batOption.ml" (inlined), line 96, characters 14-21
Called from BatOption.get in file "src/batOption.ml", line 103, characters 12-53
Called from Goblint_lib__AffineEqualityDomain.D.forget_vars in file "src/cdomains/apron/affineEqualityDomain.apron.ml", line 328, characters 14-28
Called from Goblint_lib__AffineEqualityDomain.D.assign_exp in file "src/cdomains/apron/affineEqualityDomain.apron.ml", line 385, characters 30-49
Called from Goblint_lib__RelationAnalysis.SpecFunctor.assign_from_globals_wrapper in file "src/analyses/apron/relationAnalysis.apron.ml", line 128, characters 15-24
Called from Stdlib__List.fold_left in file "list.ml", line 121, characters 24-34
Called from Goblint_lib__RelationAnalysis.SpecFunctor.make_callee_rel in file "src/analyses/apron/relationAnalysis.apron.ml", line 320, characters 8-258
Called from Goblint_lib__RelationAnalysis.SpecFunctor.enter in file "src/analyses/apron/relationAnalysis.apron.ml", line 338, characters 20-60
Called from Goblint_lib__MCP.MCP2.enter.f in file "src/analyses/mCP.ml", line 536, characters 63-81
Called from BatList.map.loop in file "src/batList.ml", line 244, characters 28-33
Called from BatList.map in file "src/batList.ml", line 247, characters 4-12
Called from Goblint_lib__MCP.MCP2.enter in file "src/analyses/mCP.ml", line 538, characters 14-42
[...]
and can be replicated with
./goblint --conf conf/svcomp26/verify.json --conf conf/svcomp26/common.json --conf conf/svcomp26/level02.json --sets ana.specification sv-benchmarks/c/properties/no-overflow.prp --sets exp.architecture 64bit sv-benchmarks/c/Juliet_Test/CWE190_Integer_Overflow__int64_t_max_add_01_bad.i -v
Reactions are currently unavailable
Metadata
Metadata
Assignees
Labels
relationalRelational analyses (Apron, affeq, lin2var)Relational analyses (Apron, affeq, lin2var)sv-compSV-COMP (analyses, results), witnessesSV-COMP (analyses, results), witnesses