File tree Expand file tree Collapse file tree 1 file changed +2
-2
lines changed
tests/regression/46-apron2 Expand file tree Collapse file tree 1 file changed +2
-2
lines changed Original file line number Diff line number Diff line change 1- $ goblint -- disable ana. dead-code. lines -- disable warn . race -- disable warn . behavior -- set ana. activated[+ ] apron -- set ana. path_sens[+ ] threadflag -- set ana. relation. privatization mutex-meet-tid-cluster12 -- enable witness. yaml. enabled -- disable witness. invariant. other -- disable witness. invariant. loop-head 96 -witness-mm-escape2. c -- set witness. yaml. path 96 -witness-mm-escape2. yml
1+ $ goblint -- disable ana. dead-code. lines -- disable warn . race -- enable warn . deterministic -- disable warn . behavior -- set ana. activated[+ ] apron -- set ana. path_sens[+ ] threadflag -- set ana. relation. privatization mutex-meet-tid-cluster12 -- enable witness. yaml. enabled -- disable witness. invariant. other -- disable witness. invariant. loop-head 96 -witness-mm-escape2. c -- set witness. yaml. path 96 -witness-mm-escape2. yml
22 [Info][Witness] witness generation summary:
33 location invariants: 8
44 loop invariants: 0
55 flow-insensitive invariants: 1
66 total generation entries: 6
77
8- $ goblint -- disable ana. dead-code. lines -- disable warn . race -- disable warn . behavior -- set ana. activated[+ ] apron -- set ana. path_sens[+ ] threadflag -- set ana. relation. privatization mutex-meet-tid-cluster12 -- set witness. yaml. validate 96 -witness-mm-escape2. yml 96 -witness-mm-escape2. c
8+ $ goblint -- disable ana. dead-code. lines -- disable warn . race -- enable warn . deterministic -- disable warn . behavior -- set ana. activated[+ ] apron -- set ana. path_sens[+ ] threadflag -- set ana. relation. privatization mutex-meet-tid-cluster12 -- set witness. yaml. validate 96 -witness-mm-escape2. yml 96 -witness-mm-escape2. c
99 [Success][Witness] invariant confirmed: (unsigned long )arg == 0 UL (96 -witness-mm-escape2. c: 8 : 5 )
1010 [Success][Witness] invariant confirmed: -128 <= g (96 -witness-mm-escape2. c: 22 : 1 )
1111 [Success][Witness] invariant confirmed: g <= 127 (96 -witness-mm-escape2. c: 22 : 1 )
You can’t perform that action at this time.
0 commit comments