diff --git a/tests/regression/13-privatized/63-access-threadspawn-lval.t b/tests/regression/13-privatized/63-access-threadspawn-lval.t index 313459637c..2b7acced59 100644 --- a/tests/regression/13-privatized/63-access-threadspawn-lval.t +++ b/tests/regression/13-privatized/63-access-threadspawn-lval.t @@ -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 diff --git a/tests/regression/36-apron/12-traces-min-rpb1.t b/tests/regression/36-apron/12-traces-min-rpb1.t index 2a760c0dcb..1bdfd3633b 100644 --- a/tests/regression/36-apron/12-traces-min-rpb1.t +++ b/tests/regression/36-apron/12-traces-min-rpb1.t @@ -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