File tree Expand file tree Collapse file tree 1 file changed +1
-8
lines changed
tests/regression/46-apron2 Expand file tree Collapse file tree 1 file changed +1
-8
lines changed Original file line number Diff line number Diff line change 11Check that the invariant (long long )f + 2147483648 LL >= (long long )e is not confirmed, as it presumes information about f and e which are supposed to be invalidated
2- $ goblint -- set ana.activated[+] apron --enable witness.invariant.after-lock --disable witness.invariant.other --disable witness.invariant.loop-head --disable sem.unknown_function.invalidate.globals --set ana.path_sens[+] threadflag --set ana.relation.privatization mutex-meet-tid-cluster12 --set witness.yaml.entry-types[*] invariant_set --set witness.yaml.validate 94-weird.yml 94-weird.c
3- [Info][Imprecise] Invalidating expressions: & e (94 - weird.c:10 :3 - 10 :35 )
2+ $ goblint -- set dbg.level warning --disable warn.imprecise --disable warn.race --set ana.activated[+] apron --enable witness.invariant.after-lock --disable witness.invariant.other --disable witness.invariant.loop-head --disable sem.unknown_function.invalidate.globals --set ana.path_sens[+] threadflag --set ana.relation.privatization mutex-meet-tid-cluster12 --set witness.yaml.entry-types[*] invariant_set --set witness.yaml.validate 94-weird.yml 94-weird.c
43 [Error][Imprecise][Unsound] Function definition missing for b (94 - weird.c:10 :3 - 10 :35 )
5- [Info][Imprecise] Invalidating expressions: (void * __restrict )(& f) (94 - weird.c:10 :3 - 10 :35 )
64 [Error][Imprecise][Unsound] Created a thread from unknown function b (94-weird.c:10:3-10:35 )
75 [Info][Deadcode] Logical lines of code (LLoC) summary:
86 live: 7
@@ -18,9 +16,4 @@ Check that the invariant (long long )f + 2147483648LL >= (long long )e is not co
1816 unsupported: 0
1917 disabled: 0
2018 total validation entries: 1
21- [Info][Race] Memory locations race summary:
22- safe: 1
23- vulnerable: 0
24- unsafe: 0
25- total memory locations: 1
2619 [Error][Imprecise][Unsound] Function definition missing
You can’t perform that action at this time.
0 commit comments