Regression from #1427: Calls to top () where that is unsupported

[michael-schwarz]

It seems that #1427 causes calls to top () where these are unsupported (most likely when creating initial value-based contexts that are then discarded)

./goblint --conf conf/svcomp.json --sets ana.specification /home/goblint/sv-benchmarks/c/properties/unreach-call.prp --sets exp.architecture 64bit /home/goblint/sv-benchmarks/c/busybox-1.22.0/cut-4.i


--------------------------------------------------------------------------------


�[0;33m[Warning] --sets is deprecated, use --set instead.�[0;0;00m
�[0;33m[Warning] --sets is deprecated, use --set instead.�[0;0;00m
[Info] unrolling loop at /home/goblint/sv-benchmarks/c/busybox-1.22.0/cut-4.i:2252:3-2273:18 with factor 3
[Info] unrolling loop at /home/goblint/sv-benchmarks/c/busybox-1.22.0/cut-4.i:2383:9-2393:9 with factor 8
[Info] unrolling loop at /home/goblint/sv-benchmarks/c/busybox-1.22.0/cut-4.i:2401:9-2419:9 with factor 3
[Info] unrolling loop at /home/goblint/sv-benchmarks/c/busybox-1.22.0/cut-4.i:2442:11-2455:26 with factor 5
[Info] unrolling loop at /home/goblint/sv-benchmarks/c/busybox-1.22.0/cut-4.i:2536:3-2576:18 with factor 1
[Info] unrolling loop at /home/goblint/sv-benchmarks/c/busybox-1.22.0/cut-4.i:2586:3-2599:43 with factor 4
[Info] unrolling loop at /home/goblint/sv-benchmarks/c/busybox-1.22.0/cut-4.i:2663:3-2674:3 with factor 5
[Info] unrolling loop at /home/goblint/sv-benchmarks/c/busybox-1.22.0/cut-4.i:2696:3-2697:5 with factor 25
[Info] unrolling loop at /home/goblint/sv-benchmarks/c/busybox-1.22.0/cut-4.i:2723:7-2729:22 with factor 25
[Info] unrolling loop at /home/goblint/sv-benchmarks/c/busybox-1.22.0/cut-4.i:2741:5-2747:5 with factor 6
[Info] unrolling loop at /home/goblint/sv-benchmarks/c/busybox-1.22.0/cut-4.i:2754:5-2771:20 with factor 2
[Info] unrolling loop at /home/goblint/sv-benchmarks/c/busybox-1.22.0/cut-4.i:2778:9-2781:9 with factor 25
[Info] unrolling loop at /home/goblint/sv-benchmarks/c/busybox-1.22.0/cut-4.i:2863:13-2866:13 with factor 25
[Info] unrolling loop at /home/goblint/sv-benchmarks/c/busybox-1.22.0/cut-4.i:2951:25-2957:23 with factor 12
[Info] unrolling loop at /home/goblint/sv-benchmarks/c/busybox-1.22.0/cut-4.i:2979:5-2998:5 with factor 2
[Info] unrolling loop at /home/goblint/sv-benchmarks/c/busybox-1.22.0/cut-4.i:3008:5-3011:5 with factor 25
[Info] unrolling loop at /home/goblint/sv-benchmarks/c/busybox-1.22.0/cut-4.i:3037:3-3046:3 with factor 25
[Info] unrolling loop at /home/goblint/sv-benchmarks/c/busybox-1.22.0/cut-4.i:3080:3-3081:5 with factor 25
[Info] unrolling loop at /home/goblint/sv-benchmarks/c/busybox-1.22.0/cut-4.i:3091:3-3099:35 with factor 4
[Info] unrolling loop at /home/goblint/sv-benchmarks/c/busybox-1.22.0/cut-4.i:3201:11-3215:11 with factor 5
[Info] unrolling loop at /home/goblint/sv-benchmarks/c/busybox-1.22.0/cut-4.i:3261:3-3262:53 with factor 8
[Info] unrolling loop at /home/goblint/sv-benchmarks/c/busybox-1.22.0/cut-4.i:3263:3-3264:53 with factor 8
[Info] unrolling loop at /home/goblint/sv-benchmarks/c/busybox-1.22.0/cut-4.i:3315:3-3316:3 with factor 6
[Info] unrolling loop at /home/goblint/sv-benchmarks/c/busybox-1.22.0/cut-4.i:3322:3-3328:3 with factor 8
[Info] unrolling loop at /home/goblint/sv-benchmarks/c/busybox-1.22.0/cut-4.i:3342:3-3343:34 with factor 8
[Info] unrolling loop at /home/goblint/sv-benchmarks/c/busybox-1.22.0/cut-4.i:3357:5-3358:42 with factor 8
[Info] unrolling loop at /home/goblint/sv-benchmarks/c/busybox-1.22.0/cut-4.i:3352:3-3359:3 with factor 1
[Info] unrolling loop at /home/goblint/sv-benchmarks/c/busybox-1.22.0/cut-4.i:3361:3-3362:23 with factor 12
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:10:5-12:5 with factor 12
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:21:9-27:9 with factor 4
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:40:3-45:3 with factor 6
[Info] longjmp -> enabling longjmp analyses "activeLongjmp, activeSetjmp, taintPartialContexts, modifiedSinceSetjmp, poisonVariables, expsplit, vla"
[Info] no thread creation -> disabling thread analyses "race, deadlock, maylocks, symb_locks, thread, threadid, threadJoins, threadreturn, mhp, region"
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Error][Analyzer] About to crash!

Fatal error: exception Lattice.Unsupported("partial map top")

We lose 32 points in SV-COMP here, all these tasks are related to setjmp/longjmp somehow.

[sim642]

Could it just be that ValueContexts is used somewhere where it shouldn't be? That does call D.top after all.

[michael-schwarz]

It is (by necessity) used by all analyses.

[sim642]

But it doesn't have to be D.top for all of them. I guess some analysis simply doesn't have a top and a different element would work instead. Those analyses might have context (startstate ()) something different from D.top (), so startcontext probably should be too for them.