Fatal error: exception Not_found
Raised at Stdlib__Hashtbl.MakeSeeded.find in file "hashtbl.ml", line 393, characters 21-36
Called from Goblint_lib__Control.AnalyzeCFG.analyze.solve_and_postprocess.ask.(fun) in file "src/framework/control.ml", line 582, characters 50-83
Called from Goblint_lib__Constraints.DeadBranchLifter.conv.(fun) in file "src/framework/constraints.ml", line 1095, characters 29-49
Called from Goblint_lib__MCP.MCP2.inner_ctx.(fun) in file "src/analyses/mCP.ml", line 341, characters 30-51
Called from Goblint_lib__Base.MainFunctor.priv_getg in file "src/analyses/base.ml", line 70, characters 32-49
Called from Goblint_lib__BasePriv.TracingPriv.read_global.getg in file "src/analyses/basePriv.ml", line 1654, characters 14-20
Called from Goblint_lib__BasePriv.PrecisionDumpPriv.read_global in file "src/analyses/basePriv.ml", line 1625, characters 12-42
Called from Goblint_lib__BasePriv.TracingPriv.read_global in file "src/analyses/basePriv.ml", line 1658, characters 12-42
Called from Goblint_lib__ValueDomain.ValueInvariant.deref_invariant in file "src/cdomains/valueDomain.ml", line 1295, characters 12-19
Called from Goblint_lib__ValueDomain.ValueInvariant.ad_invariant.(fun) in file "src/cdomains/valueDomain.ml", line 1249, characters 28-85
Called from Stdlib__Map.Make.fold in file "map.ml", line 321, characters 19-42
Called from Goblint_lib__ValueDomain.ValueInvariant.ad_invariant in file "src/cdomains/valueDomain.ml", line 1225, characters 16-1023
Called from Goblint_lib__Base.MainFunctor.query_invariant.(fun) in file "src/analyses/base.ml", line 1166, characters 32-47
Called from Stdlib__Map.Make.fold in file "map.ml", line 321, characters 19-42
Called from Stdlib__Map.Make.fold in file "map.ml", line 321, characters 26-41
Called from Goblint_lib__Base.MainFunctor.query_invariant in file "src/analyses/base.ml", line 1164, characters 10-195
Called from Goblint_lib__MCP.MCP2.query'.f in file "src/analyses/mCP.ml", line 262, characters 29-43
Called from Stdlib__List.fold_left in file "list.ml", line 121, characters 24-34
Called from Goblint_lib__MCP.MCP2.query' in file "src/analyses/mCP.ml", line 287, characters 20-75
Called from Goblint_lib__Constraints.PathSensitive2.query.(fun) in file "src/framework/constraints.ml", line 1027, characters 60-65
Called from Goblint_lib__Constraints.PathSensitive2.fold'.k in file "src/framework/constraints.ml", line 1000, characters 10-37
Called from BatSet.Concrete.fold in file "src/batSet.ml", line 310, characters 35-56
Called from Goblint_lib__Constraints.DeadCodeLifter.lift_fun in file "src/framework/constraints.ml", line 410, characters 13-29
Called from Goblint_lib__EvalAssert.EvalAssert.visitor#vstmt.make_assert in file "src/transform/evalAssert.ml", line 58, characters 14-53
Called from Goblint_lib__EvalAssert.EvalAssert.visitor#vstmt.instrument_instructions.instrument_instructions in file "src/transform/evalAssert.ml", line 94, characters 17-35
Called from Goblint_lib__EvalAssert.EvalAssert.visitor#vstmt.instrument_instructions in file "src/transform/evalAssert.ml", line 101, characters 8-34
Called from GoblintCil__Cil.visitCilStmt in file "src/cil.ml", line 5318, characters 12-64
Called from GoblintCil__Cil.mapNoCopy.aux in file "src/cil.ml", line 5121, characters 15-18
Called from GoblintCil__Cil.childrenBlock in file "src/cil.ml", line 5398, characters 15-39
Called from GoblintCil__Cil.childrenStmt.(fun).fBlock in file "src/cil.ml" (inlined), line 5334, characters 17-36
Called from GoblintCil__Cil.childrenStmt.(fun) in file "src/cil.ml", line 5371, characters 17-25
Called from GoblintCil__Cil.doVisit in file "src/cil.ml", line 5113, characters 40-60
Called from GoblintCil__Cil.visitCilStmt in file "src/cil.ml", line 5318, characters 12-64
Called from GoblintCil__Cil.mapNoCopy.aux in file "src/cil.ml", line 5121, characters 15-18
Called from GoblintCil__Cil.childrenBlock in file "src/cil.ml", line 5398, characters 15-39
Called from GoblintCil__Cil.childrenStmt.(fun).fBlock in file "src/cil.ml" (inlined), line 5334, characters 17-36
Called from GoblintCil__Cil.childrenStmt.(fun) in file "src/cil.ml", line 5347, characters 17-25
Called from GoblintCil__Cil.doVisit in file "src/cil.ml", line 5113, characters 40-60
Called from GoblintCil__Cil.visitCilStmt in file "src/cil.ml", line 5318, characters 12-64
Called from GoblintCil__Cil.mapNoCopy.aux in file "src/cil.ml", line 5121, characters 15-18
Called from GoblintCil__Cil.childrenBlock in file "src/cil.ml", line 5398, characters 15-39
Called from GoblintCil__Cil.childrenStmt.(fun).fBlock in file "src/cil.ml" (inlined), line 5334, characters 17-36
Called from GoblintCil__Cil.childrenStmt.(fun) in file "src/cil.ml", line 5371, characters 17-25
Called from GoblintCil__Cil.doVisit in file "src/cil.ml", line 5113, characters 40-60
Called from GoblintCil__Cil.visitCilStmt in file "src/cil.ml", line 5318, characters 12-64
Called from GoblintCil__Cil.mapNoCopy.aux in file "src/cil.ml", line 5121, characters 15-18
Called from GoblintCil__Cil.childrenBlock in file "src/cil.ml", line 5398, characters 15-39
Called from GoblintCil__Cil.childrenStmt.(fun).fBlock in file "src/cil.ml" (inlined), line 5334, characters 17-36
Called from GoblintCil__Cil.childrenStmt.(fun) in file "src/cil.ml", line 5347, characters 17-25
Called from GoblintCil__Cil.doVisit in file "src/cil.ml", line 5113, characters 40-60
Called from GoblintCil__Cil.visitCilStmt in file "src/cil.ml", line 5318, characters 12-64
Called from GoblintCil__Cil.mapNoCopy.aux in file "src/cil.ml", line 5121, characters 15-18
Called from GoblintCil__Cil.childrenBlock in file "src/cil.ml", line 5398, characters 15-39
Called from GoblintCil__Cil.childrenStmt.(fun).fBlock in file "src/cil.ml" (inlined), line 5334, characters 17-36
Called from GoblintCil__Cil.childrenStmt.(fun) in file "src/cil.ml", line 5371, characters 17-25
Called from GoblintCil__Cil.doVisit in file "src/cil.ml", line 5113, characters 40-60
Called from GoblintCil__Cil.visitCilStmt in file "src/cil.ml", line 5318, characters 12-64
Called from GoblintCil__Cil.mapNoCopy.aux in file "src/cil.ml", line 5121, characters 15-18
Called from GoblintCil__Cil.childrenBlock in file "src/cil.ml", line 5398, characters 15-39
Called from GoblintCil__Cil.childrenFunction in file "src/cil.ml", line 5561, characters 13-38
Called from GoblintCil__Cil.visitCilFunction in file "src/cil.ml", line 5541, characters 10-54
Called from GoblintCil__Cil.childrenGlobal in file "src/cil.ml", line 5577, characters 15-37
Called from GoblintCil__Cil.doVisitList in file "src/cil.ml", line 5145, characters 19-36
Called from GoblintCil__Cil.visitCilGlobal in file "src/cil.ml", line 5571, characters 12-58
Called from GoblintCil__Cil.visitCilFile.fGlob in file "src/cil.ml", line 5702, characters 16-36
Called from GoblintCil__Cil.visitCilFile in file "src/cil.ml", line 5709, characters 2-19
Called from Goblint_lib__EvalAssert.EvalAssert.transform in file "src/transform/evalAssert.ml", line 142, characters 4-39
Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15
Called from Goblint_lib__Control.AnalyzeCFG.analyze.solve_and_postprocess in file "src/framework/control.ml", line 592, characters 8-82
Called from Goblint_lib__Timeout.Unix.timeout in file "src/util/timeout.ml", line 6, characters 14-19
Called from Goblint_lib__Control.AnalyzeCFG.analyze in file "src/framework/control.ml", line 610, characters 17-100
Called from Goblint_lib__Control.analyze_loop.(fun) in file "src/framework/control.ml", line 686, characters 4-21
Called from Goblint_lib__Maingoblint.do_analyze.control_analyze in file "src/maingoblint.ml", line 442, characters 10-46
Re-raised at Goblint_lib__Maingoblint.do_analyze.control_analyze in file "src/maingoblint.ml", line 451, characters 8-49
Called from Goblint_timing.Make.wrap in file "src/util/timing/goblint_timing.ml", line 140, characters 10-13
Re-raised at Goblint_timing.Make.wrap in file "src/util/timing/goblint_timing.ml", line 146, characters 6-13
Called from Dune__exe__Goblint.main in file "src/goblint.ml", line 62, characters 6-35
Called from Stdlib.at_exit.new_exit in file "stdlib.ml", line 560, characters 59-63
Called from Stdlib.do_at_exit in file "stdlib.ml" (inlined), line 566, characters 20-61
Called from Std_exit in file "std_exit.ml", line 18, characters 8-20
When activating the
EvalAsserttransformation, goblint crashes on some programs when the transformation is performed.In particular, this happens on all of the
bench/coreutilprograms. Example command-line:Goblint will crash with the following stack trace (on
master, b4c0057):Stack trace