Unsoundness with context-insensitive analyses: sv-comp test "funloop_hard1"

[SchiJoha]

If all analyses are context insensitive, the sv-comp testcase goblint-regression/06-symbeq_04-funloop_hard1.i fails with the svcomp24.json configuration. It seems that some analyses produce unsound results if they are analyzed context-insensitively.

To set all analyses context insensitive I changed the mCP.ml file in line 83 from cont_inse := map' find_id @@ get_string_list "ana.ctx_insens"; to cont_inse := xs;. After compiling and executing the sv-comp testcase, Goblint incorrectly declares the testcase free of data races. The SV-COMP result is true, but false is expected. I used this command to run the testcase:

./goblint --conf conf/svcomp24.json --sets ana.specification "CHECK( init(main()), LTL(G ! data-race) )" ../../sv-benchmarks/c/goblint-regression/06-symbeq_04-funloop_hard1.i 

If only one of the analyses threadid, base, thread, threadflag, region, var_eq is analyzed context sensitive (and the remaining context insensitive), the test produces the correct result (so the SV-COMP result is unknown). An overview can be found in the following picture.