Skip to content

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

@SchiJoha

Description

@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.
Auswertung

Metadata

Metadata

Assignees

No one assigned

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions