Skip to content

Commit

Permalink
Use warn.deterministic for more cram tests (References #1647)
Browse files Browse the repository at this point in the history
  • Loading branch information
@michael-schwarz
michael-schwarz committed Feb 17, 2025
1 parent 6e2207c commit 7356e84
Show file tree
Hide file tree
Showing 2 changed files with 29 additions and 29 deletions.
32 changes: 16 additions & 16 deletions tests/regression/13-privatized/63-access-threadspawn-lval.t
View file
Original file line number Diff line number Diff line change
@@ -1,24 +1,24 @@
Should have (safe) write accesses to id1 and id2:

$ goblint --enable allglobs 63-access-threadspawn-lval.c
[Error][Imprecise][Unsound] Function definition missing for magic2 (63-access-threadspawn-lval.c:21:3-21:12)
[Info][Imprecise] INVALIDATING ALL GLOBALS! (63-access-threadspawn-lval.c:21:3-21:12)
[Info][Imprecise] Invalidating expressions: & A, & id2, & id1, & e (63-access-threadspawn-lval.c:21:3-21:12)
[Error][Imprecise][Unsound] Function definition missing for magic1 (63-access-threadspawn-lval.c:13:3-13:11)
[Info][Imprecise] INVALIDATING ALL GLOBALS! (63-access-threadspawn-lval.c:13:3-13:11)
[Info][Imprecise] Invalidating expressions: & A, & id2, & id1 (63-access-threadspawn-lval.c:13:3-13:11)
[Info][Deadcode] Logical lines of code (LLoC) summary:
live: 13
dead: 0
total lines: 13
[Success][Race] Memory location id1 (safe): (63-access-threadspawn-lval.c:4:11-4:14)
write with [multi:false, thread:[main]] (conf. 110) (exp: & *((pthread_t * __restrict )(& id1))) (63-access-threadspawn-lval.c:27:3-27:37)
[Success][Race] Memory location id2 (safe): (63-access-threadspawn-lval.c:5:11-5:14)
write with [mhp:{created={[main, f@63-access-threadspawn-lval.c:27:3-27:37]}}, thread:[main]] (conf. 110) (exp: (pthread_t * __restrict )(& id2)) (63-access-threadspawn-lval.c:28:3-28:37)
write with [mhp:{created={[main, f@63-access-threadspawn-lval.c:27:3-27:37]}}, thread:[main]] (conf. 110) (exp: & *((pthread_t * __restrict )(& id2))) (63-access-threadspawn-lval.c:28:3-28:37)
$ goblint --enable warn.deterministic --enable allglobs 63-access-threadspawn-lval.c
[Info][Race] Memory locations race summary:
safe: 2
vulnerable: 0
unsafe: 0
total memory locations: 2
[Success][Race] Memory location id1 (safe): (63-access-threadspawn-lval.c:4:11-4:14)
write with [multi:false, thread:[main]] (conf. 110) (exp: & *((pthread_t * __restrict )(& id1))) (63-access-threadspawn-lval.c:27:3-27:37)
[Success][Race] Memory location id2 (safe): (63-access-threadspawn-lval.c:5:11-5:14)
write with [mhp:{created={[main, f@63-access-threadspawn-lval.c:27:3-27:37]}}, thread:[main]] (conf. 110) (exp: (pthread_t * __restrict )(& id2)) (63-access-threadspawn-lval.c:28:3-28:37)
write with [mhp:{created={[main, f@63-access-threadspawn-lval.c:27:3-27:37]}}, thread:[main]] (conf. 110) (exp: & *((pthread_t * __restrict )(& id2))) (63-access-threadspawn-lval.c:28:3-28:37)
[Info][Deadcode] Logical lines of code (LLoC) summary:
live: 13
dead: 0
total lines: 13
[Info][Imprecise] INVALIDATING ALL GLOBALS! (63-access-threadspawn-lval.c:13:3-13:11)
[Info][Imprecise] Invalidating expressions: & A, & id2, & id1 (63-access-threadspawn-lval.c:13:3-13:11)
[Info][Imprecise] INVALIDATING ALL GLOBALS! (63-access-threadspawn-lval.c:21:3-21:12)
[Info][Imprecise] Invalidating expressions: & A, & id2, & id1, & e (63-access-threadspawn-lval.c:21:3-21:12)
[Error][Imprecise][Unsound] Function definition missing for magic1 (63-access-threadspawn-lval.c:13:3-13:11)
[Error][Imprecise][Unsound] Function definition missing for magic2 (63-access-threadspawn-lval.c:21:3-21:12)
[Error][Imprecise][Unsound] Function definition missing
26 changes: 13 additions & 13 deletions tests/regression/36-apron/12-traces-min-rpb1.t
View file
Original file line number Diff line number Diff line change
@@ -1,27 +1,27 @@
$ goblint --enable witness.yaml.enabled --set witness.yaml.entry-types '["location_invariant"]' --disable witness.invariant.other --disable ana.base.invariant.enabled --set ana.relation.privatization mutex-meet --set ana.activated[+] apron --enable ana.sv-comp.functions --set ana.apron.domain polyhedra 12-traces-min-rpb1.c
[Success][Assert] Assertion "g == h" will succeed (12-traces-min-rpb1.c:16:3-16:26)
$ goblint --enable witness.yaml.enabled --enable warn.deterministic --set witness.yaml.entry-types '["location_invariant"]' --disable witness.invariant.other --disable ana.base.invariant.enabled --set ana.relation.privatization mutex-meet --set ana.activated[+] apron --enable ana.sv-comp.functions --set ana.apron.domain polyhedra 12-traces-min-rpb1.c
[Warning][Assert] Assertion "g == h" is unknown. (12-traces-min-rpb1.c:27:3-27:26)
[Success][Assert] Assertion "g == h" will succeed (12-traces-min-rpb1.c:16:3-16:26)
[Success][Assert] Assertion "g == h" will succeed (12-traces-min-rpb1.c:29:3-29:26)
[Warning][Race] Memory location g (race with conf. 110): (12-traces-min-rpb1.c:7:5-7:10)
write with [lock:{A}, thread:[main, t_fun@12-traces-min-rpb1.c:25:3-25:40]] (conf. 110) (exp: & g) (12-traces-min-rpb1.c:14:3-14:8)
read with [mhp:{created={[main, t_fun@12-traces-min-rpb1.c:25:3-25:40]}}, thread:[main]] (conf. 110) (exp: & g) (12-traces-min-rpb1.c:27:3-27:26)
[Warning][Race] Memory location h (race with conf. 110): (12-traces-min-rpb1.c:8:5-8:10)
write with [lock:{A}, thread:[main, t_fun@12-traces-min-rpb1.c:25:3-25:40]] (conf. 110) (exp: & h) (12-traces-min-rpb1.c:15:3-15:8)
read with [mhp:{created={[main, t_fun@12-traces-min-rpb1.c:25:3-25:40]}}, thread:[main]] (conf. 110) (exp: & h) (12-traces-min-rpb1.c:27:3-27:26)
[Info][Race] Memory locations race summary:
safe: 0
vulnerable: 0
unsafe: 2
total memory locations: 2
[Info][Deadcode] Logical lines of code (LLoC) summary:
live: 18
dead: 0
total lines: 18
[Warning][Race] Memory location h (race with conf. 110): (12-traces-min-rpb1.c:8:5-8:10)
write with [lock:{A}, thread:[main, t_fun@12-traces-min-rpb1.c:25:3-25:40]] (conf. 110) (exp: & h) (12-traces-min-rpb1.c:15:3-15:8)
read with [mhp:{created={[main, t_fun@12-traces-min-rpb1.c:25:3-25:40]}}, thread:[main]] (conf. 110) (exp: & h) (12-traces-min-rpb1.c:27:3-27:26)
[Warning][Race] Memory location g (race with conf. 110): (12-traces-min-rpb1.c:7:5-7:10)
write with [lock:{A}, thread:[main, t_fun@12-traces-min-rpb1.c:25:3-25:40]] (conf. 110) (exp: & g) (12-traces-min-rpb1.c:14:3-14:8)
read with [mhp:{created={[main, t_fun@12-traces-min-rpb1.c:25:3-25:40]}}, thread:[main]] (conf. 110) (exp: & g) (12-traces-min-rpb1.c:27:3-27:26)
[Info][Witness] witness generation summary:
location invariants: 3
loop invariants: 0
flow-insensitive invariants: 0
total generation entries: 3
[Info][Race] Memory locations race summary:
safe: 0
vulnerable: 0
unsafe: 2
total memory locations: 2

$ yamlWitnessStrip < witness.yml
- entry_type: location_invariant
Expand Down

0 comments on commit 7356e84

Please sign in to comment.