Skip to content

Convert most old YAML witnesses to version 2.0 #1852

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 3 commits into from
Oct 27, 2025
Merged

Convert most old YAML witnesses to version 2.0 #1852

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
fc3235b
Convert most remaining output YAML witnesses in cram tests to invaria…
sim642 Oct 24, 2025
6032ec7
Convert 46-apron2/95-witness-mm-escape.yml to invariant_set
sim642 Oct 24, 2025
e31c82d
Convert 36-apron/52-queuesize.t to invariant_set
sim642 Oct 24, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
252 changes: 124 additions & 128 deletions tests/regression/13-privatized/01-priv_nr.t
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
`protection` privatization:

$ goblint --enable witness.yaml.enabled --set witness.yaml.entry-types '["location_invariant"]' --disable witness.invariant.other --set ana.base.privatization protection 01-priv_nr.c
$ goblint --enable witness.yaml.enabled --set witness.yaml.invariant-types '["location_invariant"]' --disable witness.invariant.other --set ana.base.privatization protection 01-priv_nr.c
[Success][Assert] Assertion "glob1 == 5" will succeed (01-priv_nr.c:22:3-22:30)
[Success][Assert] Assertion "t == 5" will succeed (01-priv_nr.c:12:3-12:26)
[Success][Assert] Assertion "glob1 == -10" will succeed (01-priv_nr.c:14:3-14:32)
Expand All @@ -13,48 +13,47 @@
location invariants: 3
loop invariants: 0
flow-insensitive invariants: 0
total generation entries: 3
total generation entries: 1
[Info][Race] Memory locations race summary:
safe: 1
vulnerable: 0
unsafe: 0
total memory locations: 1

$ yamlWitnessStrip < witness.yml
- entry_type: location_invariant
location:
file_name: 01-priv_nr.c
line: 25
column: 3
function: main
location_invariant:
string: glob1 == 5
type: assertion
format: C
- entry_type: location_invariant
location:
file_name: 01-priv_nr.c
line: 11
column: 3
function: t_fun
location_invariant:
string: glob1 == 5
type: assertion
format: C
- entry_type: location_invariant
location:
file_name: 01-priv_nr.c
line: 11
column: 3
function: t_fun
location_invariant:
string: (unsigned long )arg == 0UL
type: assertion
format: C
- entry_type: invariant_set
content:
- invariant:
type: location_invariant
location:
file_name: 01-priv_nr.c
line: 11
column: 3
function: t_fun
value: (unsigned long )arg == 0UL
format: c_expression
- invariant:
type: location_invariant
location:
file_name: 01-priv_nr.c
line: 11
column: 3
function: t_fun
value: glob1 == 5
format: c_expression
- invariant:
type: location_invariant
location:
file_name: 01-priv_nr.c
line: 25
column: 3
function: main
value: glob1 == 5
format: c_expression

`vojdani` privatization:

$ goblint --enable witness.yaml.enabled --set witness.yaml.entry-types '["location_invariant"]' --disable witness.invariant.other --set ana.base.privatization vojdani 01-priv_nr.c
$ goblint --enable witness.yaml.enabled --set witness.yaml.invariant-types '["location_invariant"]' --disable witness.invariant.other --set ana.base.privatization vojdani 01-priv_nr.c
[Success][Assert] Assertion "glob1 == 5" will succeed (01-priv_nr.c:22:3-22:30)
[Success][Assert] Assertion "t == 5" will succeed (01-priv_nr.c:12:3-12:26)
[Success][Assert] Assertion "glob1 == -10" will succeed (01-priv_nr.c:14:3-14:32)
Expand All @@ -67,48 +66,47 @@
location invariants: 3
loop invariants: 0
flow-insensitive invariants: 0
total generation entries: 3
total generation entries: 1
[Info][Race] Memory locations race summary:
safe: 1
vulnerable: 0
unsafe: 0
total memory locations: 1

$ yamlWitnessStrip < witness.yml
- entry_type: location_invariant
location:
file_name: 01-priv_nr.c
line: 25
column: 3
function: main
location_invariant:
string: glob1 == 5
type: assertion
format: C
- entry_type: location_invariant
location:
file_name: 01-priv_nr.c
line: 11
column: 3
function: t_fun
location_invariant:
string: glob1 == 5
type: assertion
format: C
- entry_type: location_invariant
location:
file_name: 01-priv_nr.c
line: 11
column: 3
function: t_fun
location_invariant:
string: (unsigned long )arg == 0UL
type: assertion
format: C
- entry_type: invariant_set
content:
- invariant:
type: location_invariant
location:
file_name: 01-priv_nr.c
line: 11
column: 3
function: t_fun
value: (unsigned long )arg == 0UL
format: c_expression
- invariant:
type: location_invariant
location:
file_name: 01-priv_nr.c
line: 11
column: 3
function: t_fun
value: glob1 == 5
format: c_expression
- invariant:
type: location_invariant
location:
file_name: 01-priv_nr.c
line: 25
column: 3
function: main
value: glob1 == 5
format: c_expression

`mutex-meet` privatization:

$ goblint --enable witness.yaml.enabled --set witness.yaml.entry-types '["location_invariant"]' --disable witness.invariant.other --set ana.base.privatization mutex-meet 01-priv_nr.c
$ goblint --enable witness.yaml.enabled --set witness.yaml.invariant-types '["location_invariant"]' --disable witness.invariant.other --set ana.base.privatization mutex-meet 01-priv_nr.c
[Success][Assert] Assertion "glob1 == 5" will succeed (01-priv_nr.c:22:3-22:30)
[Success][Assert] Assertion "t == 5" will succeed (01-priv_nr.c:12:3-12:26)
[Success][Assert] Assertion "glob1 == -10" will succeed (01-priv_nr.c:14:3-14:32)
Expand All @@ -121,48 +119,47 @@
location invariants: 3
loop invariants: 0
flow-insensitive invariants: 0
total generation entries: 3
total generation entries: 1
[Info][Race] Memory locations race summary:
safe: 1
vulnerable: 0
unsafe: 0
total memory locations: 1

$ yamlWitnessStrip < witness.yml
- entry_type: location_invariant
location:
file_name: 01-priv_nr.c
line: 25
column: 3
function: main
location_invariant:
string: glob1 == 5
type: assertion
format: C
- entry_type: location_invariant
location:
file_name: 01-priv_nr.c
line: 11
column: 3
function: t_fun
location_invariant:
string: glob1 == 5
type: assertion
format: C
- entry_type: location_invariant
location:
file_name: 01-priv_nr.c
line: 11
column: 3
function: t_fun
location_invariant:
string: (unsigned long )arg == 0UL
type: assertion
format: C
- entry_type: invariant_set
content:
- invariant:
type: location_invariant
location:
file_name: 01-priv_nr.c
line: 11
column: 3
function: t_fun
value: (unsigned long )arg == 0UL
format: c_expression
- invariant:
type: location_invariant
location:
file_name: 01-priv_nr.c
line: 11
column: 3
function: t_fun
value: glob1 == 5
format: c_expression
- invariant:
type: location_invariant
location:
file_name: 01-priv_nr.c
line: 25
column: 3
function: main
value: glob1 == 5
format: c_expression

`write+lock` privatization:

$ goblint --enable witness.yaml.enabled --set witness.yaml.entry-types '["location_invariant"]' --disable witness.invariant.other --set ana.base.privatization write+lock 01-priv_nr.c
$ goblint --enable witness.yaml.enabled --set witness.yaml.invariant-types '["location_invariant"]' --disable witness.invariant.other --set ana.base.privatization write+lock 01-priv_nr.c
[Success][Assert] Assertion "glob1 == 5" will succeed (01-priv_nr.c:22:3-22:30)
[Success][Assert] Assertion "t == 5" will succeed (01-priv_nr.c:12:3-12:26)
[Success][Assert] Assertion "glob1 == -10" will succeed (01-priv_nr.c:14:3-14:32)
Expand All @@ -175,41 +172,40 @@
location invariants: 3
loop invariants: 0
flow-insensitive invariants: 0
total generation entries: 3
total generation entries: 1
[Info][Race] Memory locations race summary:
safe: 1
vulnerable: 0
unsafe: 0
total memory locations: 1

$ yamlWitnessStrip < witness.yml
- entry_type: location_invariant
location:
file_name: 01-priv_nr.c
line: 25
column: 3
function: main
location_invariant:
string: glob1 == 5
type: assertion
format: C
- entry_type: location_invariant
location:
file_name: 01-priv_nr.c
line: 11
column: 3
function: t_fun
location_invariant:
string: glob1 == 5
type: assertion
format: C
- entry_type: location_invariant
location:
file_name: 01-priv_nr.c
line: 11
column: 3
function: t_fun
location_invariant:
string: (unsigned long )arg == 0UL
type: assertion
format: C
- entry_type: invariant_set
content:
- invariant:
type: location_invariant
location:
file_name: 01-priv_nr.c
line: 11
column: 3
function: t_fun
value: (unsigned long )arg == 0UL
format: c_expression
- invariant:
type: location_invariant
location:
file_name: 01-priv_nr.c
line: 11
column: 3
function: t_fun
value: glob1 == 5
format: c_expression
- invariant:
type: location_invariant
location:
file_name: 01-priv_nr.c
line: 25
column: 3
function: main
value: glob1 == 5
format: c_expression
63 changes: 31 additions & 32 deletions tests/regression/36-apron/12-traces-min-rpb1.t
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
$ 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
$ goblint --enable witness.yaml.enabled --enable warn.deterministic --set witness.yaml.invariant-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)
Expand All @@ -21,39 +21,38 @@
location invariants: 3
loop invariants: 0
flow-insensitive invariants: 0
total generation entries: 3
total generation entries: 1

$ yamlWitnessStrip < witness.yml
- entry_type: location_invariant
location:
file_name: 12-traces-min-rpb1.c
line: 29
column: 3
function: main
location_invariant:
string: (long long )h == (long long )g
type: assertion
format: C
- entry_type: location_invariant
location:
file_name: 12-traces-min-rpb1.c
line: 19
column: 3
function: t_fun
location_invariant:
string: (long long )h == (long long )g
type: assertion
format: C
- entry_type: location_invariant
location:
file_name: 12-traces-min-rpb1.c
line: 14
column: 3
function: t_fun
location_invariant:
string: (long long )h == (long long )g
type: assertion
format: C
- entry_type: invariant_set
content:
- invariant:
type: location_invariant
location:
file_name: 12-traces-min-rpb1.c
line: 14
column: 3
function: t_fun
value: (long long )h == (long long )g
format: c_expression
- invariant:
type: location_invariant
location:
file_name: 12-traces-min-rpb1.c
line: 19
column: 3
function: t_fun
value: (long long )h == (long long )g
format: c_expression
- invariant:
type: location_invariant
location:
file_name: 12-traces-min-rpb1.c
line: 29
column: 3
function: main
value: (long long )h == (long long )g
format: c_expression


$ goblint --enable warn.deterministic --set ana.activated[+] apron --set ana.path_sens[+] threadflag --enable ana.sv-comp.functions --enable witness.yaml.enabled --set ana.activated[+] mutexGhosts --set witness.yaml.entry-types '["flow_insensitive_invariant", "ghost_instrumentation"]' 12-traces-min-rpb1.c --enable ana.apron.invariant.diff-box
Expand Down
Loading
Loading