Skip to content

Commit

Permalink
Use yamlWitnessStrip for 56-witness/08-witness-all-locals
Browse files Browse the repository at this point in the history
  • Loading branch information
sim642 committed Feb 29, 2024
1 parent 786affd commit 07430d2
Showing 1 changed file with 57 additions and 2 deletions.
59 changes: 57 additions & 2 deletions tests/regression/56-witness/08-witness-all-locals.t
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,40 @@
[Info][Witness] witness generation summary:
total generation entries: 3

TODO: check witness.yml content with yamlWitnessStrip
$ yamlWitnessStrip < witness.yml
- entry_type: location_invariant
location:
file_name: 08-witness-all-locals.c
file_hash: $FILE_HASH
line: 9
column: 2
function: main
location_invariant:
string: y == 10
type: assertion
format: C
- entry_type: location_invariant
location:
file_name: 08-witness-all-locals.c
file_hash: $FILE_HASH
line: 9
column: 2
function: main
location_invariant:
string: x == 5
type: assertion
format: C
- entry_type: location_invariant
location:
file_name: 08-witness-all-locals.c
file_hash: $FILE_HASH
line: 7
column: 4
function: main
location_invariant:
string: x == 5
type: assertion
format: C

Fewer entries are emitted if locals from nested block scopes are excluded:

Expand All @@ -19,4 +52,26 @@ Fewer entries are emitted if locals from nested block scopes are excluded:
[Info][Witness] witness generation summary:
total generation entries: 2

TODO: check witness.yml content with yamlWitnessStrip
$ yamlWitnessStrip < witness.yml
- entry_type: location_invariant
location:
file_name: 08-witness-all-locals.c
file_hash: $FILE_HASH
line: 9
column: 2
function: main
location_invariant:
string: x == 5
type: assertion
format: C
- entry_type: location_invariant
location:
file_name: 08-witness-all-locals.c
file_hash: $FILE_HASH
line: 7
column: 4
function: main
location_invariant:
string: x == 5
type: assertion
format: C

0 comments on commit 07430d2

Please sign in to comment.