Non-deterministic non-termination of ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-43_2a-drivers--scsi--device_handler--scsi_dh_rdac.ko-entry_point.cil.out.i #1942
Description
While benchmarking #1940 at 7881999 I encountered something strange with one SV-COMP benchmark:
./goblint --conf conf/svcomp26/common.json --conf conf/svcomp26/verify.json --conf conf/svcomp26/level01.json --sets ana.specification /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp --sets exp.architecture 64bit /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-43_2a-drivers--scsi--device_handler--scsi_dh_rdac.ko-entry_point.cil.out.i
At 3127a30, the analysis runs out of 1GB of memory after 50s. With #1940 it succeeds with the correct verdict after 5s.
While trying to run the new version locally to understand the single improvement, it again didn't terminate quickly and started consuming lots of memory.
Killing it revealed the following call stack:
Details
Raised at Stdlib__Sys.catch_break.(fun) in file "stdlib/sys.ml.in", line 115, characters 46-57
Called from GoblintCil__Cil.plainCilPrinterClass#pOnlyType in file "src/cil.ml", line 4678, characters 11-22
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Pretty.seq.loop in file "src/ocamlutil/pretty.ml", line 140, characters 17-23
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Cil.plainCilPrinterClass#pOnlyType in file "src/cil.ml", line 4672, characters 19-329
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Pretty.seq.loop in file "src/ocamlutil/pretty.ml", line 140, characters 17-23
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Cil.plainCilPrinterClass#pOnlyType in file "src/cil.ml", line 4672, characters 19-329
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Pretty.seq.loop in file "src/ocamlutil/pretty.ml", line 140, characters 17-23
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Cil.plainCilPrinterClass#pOnlyType in file "src/cil.ml", line 4672, characters 19-329
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Pretty.seq.loop in file "src/ocamlutil/pretty.ml", line 140, characters 17-23
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Cil.plainCilPrinterClass#pOnlyType in file "src/cil.ml", line 4672, characters 19-329
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Pretty.seq in file "src/ocamlutil/pretty.ml", line 146, characters 15-21
Called from GoblintCil__Cil.plainCilPrinterClass#pOnlyType in file "src/cil.ml", line 4659, characters 14-188
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Pretty.seq.loop in file "src/ocamlutil/pretty.ml", line 140, characters 17-23
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Cil.plainCilPrinterClass#pOnlyType in file "src/cil.ml", line 4672, characters 19-329
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Pretty.seq.loop in file "src/ocamlutil/pretty.ml", line 140, characters 17-23
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Cil.plainCilPrinterClass#pOnlyType in file "src/cil.ml", line 4672, characters 19-329
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Pretty.seq in file "src/ocamlutil/pretty.ml", line 146, characters 15-21
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Cil.plainCilPrinterClass#pOnlyType in file "src/cil.ml", line 4672, characters 19-329
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Pretty.seq.loop in file "src/ocamlutil/pretty.ml", line 140, characters 17-23
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Cil.plainCilPrinterClass#pOnlyType in file "src/cil.ml", line 4672, characters 19-329
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Pretty.seq.loop in file "src/ocamlutil/pretty.ml", line 140, characters 17-23
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Cil.plainCilPrinterClass#pOnlyType in file "src/cil.ml", line 4672, characters 19-329
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Pretty.seq.loop in file "src/ocamlutil/pretty.ml", line 140, characters 17-23
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Cil.plainCilPrinterClass#pOnlyType in file "src/cil.ml", line 4672, characters 19-329
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Pretty.seq in file "src/ocamlutil/pretty.ml", line 146, characters 15-21
Called from GoblintCil__Cil.plainCilPrinterClass#pOnlyType in file "src/cil.ml", line 4659, characters 14-188
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Pretty.seq.loop in file "src/ocamlutil/pretty.ml", line 140, characters 17-23
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Cil.plainCilPrinterClass#pOnlyType in file "src/cil.ml", line 4672, characters 19-329
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Pretty.seq.loop in file "src/ocamlutil/pretty.ml", line 140, characters 17-23
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Cil.plainCilPrinterClass#pOnlyType in file "src/cil.ml", line 4672, characters 19-329
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Pretty.seq.loop in file "src/ocamlutil/pretty.ml", line 140, characters 17-23
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Cil.plainCilPrinterClass#pOnlyType in file "src/cil.ml", line 4672, characters 19-329
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Pretty.seq.loop in file "src/ocamlutil/pretty.ml", line 140, characters 17-23
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Cil.plainCilPrinterClass#pOnlyType in file "src/cil.ml", line 4672, characters 19-329
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Pretty.seq.loop in file "src/ocamlutil/pretty.ml", line 140, characters 17-23
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Cil.plainCilPrinterClass#pOnlyType in file "src/cil.ml", line 4672, characters 19-329
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Pretty.seq.loop in file "src/ocamlutil/pretty.ml", line 140, characters 17-23
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Cil.plainCilPrinterClass#pOnlyType in file "src/cil.ml", line 4672, characters 19-329
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Pretty.seq.loop in file "src/ocamlutil/pretty.ml", line 140, characters 17-23
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Cil.plainCilPrinterClass#pOnlyType in file "src/cil.ml", line 4672, characters 19-329
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Pretty.seq.loop in file "src/ocamlutil/pretty.ml", line 140, characters 17-23
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Cil.plainCilPrinterClass#pOnlyType in file "src/cil.ml", line 4672, characters 19-329
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Pretty.seq.loop in file "src/ocamlutil/pretty.ml", line 140, characters 17-23
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Cil.plainCilPrinterClass#pOnlyType in file "src/cil.ml", line 4672, characters 19-329
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Pretty.seq in file "src/ocamlutil/pretty.ml", line 146, characters 15-21
Called from GoblintCil__Cil.plainCilPrinterClass#pOnlyType in file "src/cil.ml", line 4659, characters 14-188
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Pretty.seq.loop in file "src/ocamlutil/pretty.ml", line 140, characters 17-23
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Cil.plainCilPrinterClass#pOnlyType in file "src/cil.ml", line 4672, characters 19-329
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Pretty.seq.loop in file "src/ocamlutil/pretty.ml", line 140, characters 17-23
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Cil.plainCilPrinterClass#pOnlyType in file "src/cil.ml", line 4672, characters 19-329
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Pretty.seq.loop in file "src/ocamlutil/pretty.ml", line 140, characters 17-23
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Cil.plainCilPrinterClass#pOnlyType in file "src/cil.ml", line 4672, characters 19-329
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Pretty.seq in file "src/ocamlutil/pretty.ml", line 146, characters 15-21
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Cil.plainCilPrinterClass#pOnlyType in file "src/cil.ml", line 4672, characters 19-329
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Pretty.seq.loop in file "src/ocamlutil/pretty.ml", line 140, characters 17-23
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Cil.plainCilPrinterClass#pOnlyType in file "src/cil.ml", line 4672, characters 19-329
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Pretty.seq.loop in file "src/ocamlutil/pretty.ml", line 140, characters 17-23
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Cil.plainCilPrinterClass#pOnlyType in file "src/cil.ml", line 4672, characters 19-329
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Pretty.seq in file "src/ocamlutil/pretty.ml", line 146, characters 15-21
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Cil.plainCilPrinterClass#pOnlyType in file "src/cil.ml", line 4672, characters 19-329
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Pretty.seq.loop in file "src/ocamlutil/pretty.ml", line 140, characters 17-23
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Cil.plainCilPrinterClass#pOnlyType in file "src/cil.ml", line 4672, characters 19-329
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Pretty.seq.loop in file "src/ocamlutil/pretty.ml", line 140, characters 17-23
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Cil.plainCilPrinterClass#pOnlyType in file "src/cil.ml", line 4672, characters 19-329
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Pretty.seq.loop in file "src/ocamlutil/pretty.ml", line 140, characters 17-23
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Cil.plainCilPrinterClass#pOnlyType in file "src/cil.ml", line 4672, characters 19-329
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Pretty.seq.loop in file "src/ocamlutil/pretty.ml", line 140, characters 17-23
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Cil.plainCilPrinterClass#pOnlyType in file "src/cil.ml", line 4672, characters 19-329
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Pretty.seq.loop in file "src/ocamlutil/pretty.ml", line 140, characters 17-23
Called from GoblintCil__Cil.plainCilPrinterClass#pOnlyType in file "src/cil.ml", line 4659, characters 14-188
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Pretty.seq in file "src/ocamlutil/pretty.ml", line 146, characters 15-21
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Cil.plainCilPrinterClass#pOnlyType in file "src/cil.ml", line 4672, characters 19-329
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Pretty.seq.loop in file "src/ocamlutil/pretty.ml", line 140, characters 17-23
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Cil.plainCilPrinterClass#pOnlyType in file "src/cil.ml", line 4672, characters 19-329
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Pretty.seq.loop in file "src/ocamlutil/pretty.ml", line 140, characters 17-23
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Cil.plainCilPrinterClass#pOnlyType in file "src/cil.ml", line 4672, characters 19-329
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Pretty.seq.loop in file "src/ocamlutil/pretty.ml", line 140, characters 17-23
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Cil.plainCilPrinterClass#pOnlyType in file "src/cil.ml", line 4672, characters 19-329
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Pretty.seq.loop in file "src/ocamlutil/pretty.ml", line 140, characters 17-23
Called from GoblintCil__Cil.plainCilPrinterClass#pOnlyType in file "src/cil.ml", line 4659, characters 14-188
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Pretty.seq in file "src/ocamlutil/pretty.ml", line 146, characters 15-21
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Cil.plainCilPrinterClass#pOnlyType in file "src/cil.ml", line 4672, characters 19-329
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Pretty.seq.loop in file "src/ocamlutil/pretty.ml", line 140, characters 17-23
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Cil.plainCilPrinterClass#pOnlyType in file "src/cil.ml", line 4672, characters 19-329
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Pretty.seq in file "src/ocamlutil/pretty.ml", line 146, characters 15-21
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Cil.plainCilPrinterClass#pOnlyType in file "src/cil.ml", line 4672, characters 19-329
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Pretty.seq.loop in file "src/ocamlutil/pretty.ml", line 140, characters 17-23
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Cil.plainCilPrinterClass#pOnlyType in file "src/cil.ml", line 4672, characters 19-329
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Pretty.seq.loop in file "src/ocamlutil/pretty.ml", line 140, characters 17-23
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Cil.plainCilPrinterClass#pOnlyType in file "src/cil.ml", line 4672, characters 19-329
Called from GoblintCil__Cil.plainCilPrinterClass#pExp in file "src/cil.ml", line 4747, characters 24-44
Called from GoblintCil__Cil.d_plainexp in file "src/cil.ml" (inlined), line 4802, characters 22-47
Called from Goblint_lib__SharedFunctions.pp_unsupported_cilExp.__2.(fun) in file "src/cdomains/apron/sharedFunctions.apron.ml", line 59, characters 94-115
Called from Stdlib__Format.kasprintf.k in file "format.ml", line 1391, characters 4-22
Called from Goblint_lib__SharedFunctions.ApronOfCil.texpr1_expr_of_cil_exp in file "src/cdomains/apron/sharedFunctions.apron.ml", line 222, characters 58-86
This is odd because the analysis was still going and no output was being printed. My two theories are:
- There's some infinite recursion still in
plainCilPrinterClass. - It's an instance of Avoid eager string conversions during analysis #1795, in which case Replace eager
showwith lazyprettyduring analysis #1797 could help.
Who knows how much SV-COMP timeouts/OOMs are similar, having nothing to do with the analysis itself but some silly unnecessary internal stringification.