Skip to content
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

Change YAML witness columns to 1-indexed #1400

Merged
merged 1 commit into from
Apr 15, 2024
Merged

Change YAML witness columns to 1-indexed #1400

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
2 changes: 1 addition & 1 deletion src/analyses/unassumeAnalysis.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -77,7 +77,7 @@ struct
let loc_of_location (location: YamlWitnessType.Location.t): Cil.location = {
file = location.file_name;
line = location.line;
column = location.column + 1;
column = location.column;
byte = -1;
endLine = -1;
endColumn = -1;
Expand Down
4 changes: 2 additions & 2 deletions src/witness/yamlWitness.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -47,7 +47,7 @@ struct
file_name = loc.file;
file_hash = sha256_file loc.file;
line = loc.line;
column = loc.column - 1;
column = loc.column;
function_ = location_function;
}

Expand Down Expand Up @@ -556,7 +556,7 @@ struct
let loc_of_location (location: YamlWitnessType.Location.t): Cil.location = {
file = location.file_name;
line = location.line;
column = location.column + 1;
column = location.column;
byte = -1;
endLine = -1;
endColumn = -1;
Expand Down
10 changes: 5 additions & 5 deletions tests/regression/56-witness/01-base-lor-enums.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@
file_name: 01-base-lor-enums.c
file_hash: 5f686f726d140fbb7f3052f778e99aa09e3807cc6972a4d4905df2f6ed0c3e01
line: 17
column: 2
column: 3
function: main
location_invariant:
string: (x == 1 || x == 3) || x == 6
Expand Down Expand Up @@ -48,7 +48,7 @@
file_name: 01-base-lor-enums.c
file_hash: 5f686f726d140fbb7f3052f778e99aa09e3807cc6972a4d4905df2f6ed0c3e01
line: 18
column: 2
column: 3
function: main
location_invariant:
string: (x == 1 || x == 3) || x == 7
Expand Down Expand Up @@ -76,7 +76,7 @@
file_name: 01-base-lor-enums.c
file_hash: 5f686f726d140fbb7f3052f778e99aa09e3807cc6972a4d4905df2f6ed0c3e01
line: 29
column: 2
column: 3
function: main
location_invariant:
string: y == 11 || y == x
Expand Down Expand Up @@ -104,7 +104,7 @@
file_name: 01-base-lor-enums.c
file_hash: 5f686f726d140fbb7f3052f778e99aa09e3807cc6972a4d4905df2f6ed0c3e01
line: 30
column: 2
column: 3
function: main
location_invariant:
string: (y == 1 || y == 3) || y == 6 || y == 11
Expand Down Expand Up @@ -132,7 +132,7 @@
file_name: 01-base-lor-enums.c
file_hash: 5f686f726d140fbb7f3052f778e99aa09e3807cc6972a4d4905df2f6ed0c3e01
line: 31
column: 2
column: 3
function: main
location_invariant:
string: y == 42 || y == x
Expand Down
10 changes: 5 additions & 5 deletions tests/regression/56-witness/02-base-lor-addr.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@
file_name: 02-base-lor-addr.c
file_hash: 5f686f726d140fbb7f3052f778e99aa09e3807cc6972a4d4905df2f6ed0c3e01
line: 17
column: 2
column: 3
function: main
location_invariant:
string: (x == &a || x == &b) || x == &c
Expand Down Expand Up @@ -48,7 +48,7 @@
file_name: 02-base-lor-addr.c
file_hash: 5f686f726d140fbb7f3052f778e99aa09e3807cc6972a4d4905df2f6ed0c3e01
line: 18
column: 2
column: 3
function: main
location_invariant:
string: (x == &a || x == &b) || x == &d
Expand Down Expand Up @@ -76,7 +76,7 @@
file_name: 02-base-lor-addr.c
file_hash: 5f686f726d140fbb7f3052f778e99aa09e3807cc6972a4d4905df2f6ed0c3e01
line: 29
column: 2
column: 3
function: main
location_invariant:
string: y == &e || y == x
Expand Down Expand Up @@ -104,7 +104,7 @@
file_name: 02-base-lor-addr.c
file_hash: 5f686f726d140fbb7f3052f778e99aa09e3807cc6972a4d4905df2f6ed0c3e01
line: 30
column: 2
column: 3
function: main
location_invariant:
string: (y == &a || y == &b) || y == &c || y == &e
Expand Down Expand Up @@ -132,7 +132,7 @@
file_name: 02-base-lor-addr.c
file_hash: 5f686f726d140fbb7f3052f778e99aa09e3807cc6972a4d4905df2f6ed0c3e01
line: 31
column: 2
column: 3
function: main
location_invariant:
string: y == &d || y == x
Expand Down
4 changes: 2 additions & 2 deletions tests/regression/56-witness/03-int-log-short.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,7 @@
file_name: 03-int-log-short.c
file_hash: 055e8b0b611a6bbe2b072f5c92f094e63fa339ac53190660ac3e54f2fd40d379
line: 8
column: 2
column: 3
function: main
location_invariant:
string: r || x
Expand Down Expand Up @@ -50,7 +50,7 @@
file_name: 03-int-log-short.c
file_hash: 055e8b0b611a6bbe2b072f5c92f094e63fa339ac53190660ac3e54f2fd40d379
line: 9
column: 2
column: 3
function: main
location_invariant:
string: '!(r && y)'
Expand Down
2 changes: 1 addition & 1 deletion tests/regression/56-witness/04-base-priv-sync-prune.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,7 @@
file_name: 04-base-priv-sync-prune.c
file_hash: 20f9b103c97d1a16c6c4e39478f949ffbf1bb4c7ed7b17af7d7399aa57c8f158
line: 8
column: 2
column: 3
function: main
location_invariant:
string: g == 2
Expand Down
6 changes: 3 additions & 3 deletions tests/regression/56-witness/05-prec-problem.t
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ The sound invariant is `result == 1 || result == 0`.
file_name: 05-prec-problem.c
file_hash: $FILE_HASH
line: 13
column: 4
column: 5
function: foo
loop_invariant:
string: result == 1 || result == 0
Expand All @@ -35,7 +35,7 @@ The sound invariant is `result == 1 || result == 0`.
file_name: 05-prec-problem.c
file_hash: $FILE_HASH
line: 13
column: 4
column: 5
function: foo
loop_invariant:
string: '*ptr2 == 5'
Expand All @@ -50,7 +50,7 @@ The sound invariant is `result == 1 || result == 0`.
file_name: 05-prec-problem.c
file_hash: $FILE_HASH
line: 13
column: 4
column: 5
function: foo
loop_invariant:
string: '*ptr1 == 5'
Expand Down
4 changes: 2 additions & 2 deletions tests/regression/56-witness/07-base-lor-interval.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,7 @@
file_name: 07-base-lor-interval.c
file_hash: 6aaf25a17ef6c1a6b16300f34c4ef196baeb5a505a0e863ca0340e6060ef84e4
line: 8
column: 2
column: 3
function: main
location_invariant:
string: r || 2 <= x
Expand Down Expand Up @@ -52,7 +52,7 @@
file_name: 07-base-lor-interval.c
file_hash: 6aaf25a17ef6c1a6b16300f34c4ef196baeb5a505a0e863ca0340e6060ef84e4
line: 9
column: 2
column: 3
function: main
location_invariant:
string: 2 <= x || r
Expand Down
10 changes: 5 additions & 5 deletions tests/regression/56-witness/08-witness-all-locals.t
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@
file_name: 08-witness-all-locals.c
file_hash: $FILE_HASH
line: 9
column: 2
column: 3
function: main
location_invariant:
string: y == 10
Expand All @@ -23,7 +23,7 @@
file_name: 08-witness-all-locals.c
file_hash: $FILE_HASH
line: 9
column: 2
column: 3
function: main
location_invariant:
string: x == 5
Expand All @@ -34,7 +34,7 @@
file_name: 08-witness-all-locals.c
file_hash: $FILE_HASH
line: 7
column: 4
column: 5
function: main
location_invariant:
string: x == 5
Expand All @@ -58,7 +58,7 @@ Fewer entries are emitted if locals from nested block scopes are excluded:
file_name: 08-witness-all-locals.c
file_hash: $FILE_HASH
line: 9
column: 2
column: 3
function: main
location_invariant:
string: x == 5
Expand All @@ -69,7 +69,7 @@ Fewer entries are emitted if locals from nested block scopes are excluded:
file_name: 08-witness-all-locals.c
file_hash: $FILE_HASH
line: 7
column: 4
column: 5
function: main
location_invariant:
string: x == 5
Expand Down
4 changes: 2 additions & 2 deletions tests/regression/56-witness/10-apron-unassume-interval.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@
file_name: 10-apron-unassume-interval.c
file_hash: 71e40ed99b5217343d0831e293e7207e5bd30ce53f6ab73f0c1ef6ced1afcc60
line: 6
column: 2
column: 3
function: main
loop_invariant:
string: 100LL - (long long )i >= 0LL
Expand Down Expand Up @@ -48,7 +48,7 @@
file_name: 10-apron-unassume-interval.c
file_hash: 71e40ed99b5217343d0831e293e7207e5bd30ce53f6ab73f0c1ef6ced1afcc60
line: 6
column: 2
column: 3
function: main
loop_invariant:
string: (long long )i >= 0LL
Expand Down
4 changes: 2 additions & 2 deletions tests/regression/56-witness/11-base-unassume-interval.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@
file_name: 11-base-unassume-interval.c
file_hash: 71e40ed99b5217343d0831e293e7207e5bd30ce53f6ab73f0c1ef6ced1afcc60
line: 6
column: 2
column: 3
function: main
loop_invariant:
string: 100LL - (long long )i >= 0LL
Expand Down Expand Up @@ -48,7 +48,7 @@
file_name: 11-base-unassume-interval.c
file_hash: 71e40ed99b5217343d0831e293e7207e5bd30ce53f6ab73f0c1ef6ced1afcc60
line: 6
column: 2
column: 3
function: main
loop_invariant:
string: (long long )i >= 0LL
Expand Down
4 changes: 2 additions & 2 deletions tests/regression/56-witness/12-apron-unassume-branch.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@
file_name: 12-apron-unassume-branch.c
file_hash: 71e40ed99b5217343d0831e293e7207e5bd30ce53f6ab73f0c1ef6ced1afcc60
line: 7
column: 4
column: 3
function: main
location_invariant:
string: 99LL - (long long )i >= 0LL
Expand Down Expand Up @@ -48,7 +48,7 @@
file_name: 12-apron-unassume-branch.c
file_hash: 71e40ed99b5217343d0831e293e7207e5bd30ce53f6ab73f0c1ef6ced1afcc60
line: 7
column: 4
column: 3
function: main
location_invariant:
string: (long long )i >= 0LL
Expand Down
4 changes: 2 additions & 2 deletions tests/regression/56-witness/13-base-unassume-branch.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@
file_name: 13-base-unassume-branch.c
file_hash: 71e40ed99b5217343d0831e293e7207e5bd30ce53f6ab73f0c1ef6ced1afcc60
line: 7
column: 4
column: 5
function: main
location_invariant:
string: 99LL - (long long )i >= 0LL
Expand Down Expand Up @@ -48,7 +48,7 @@
file_name: 13-base-unassume-branch.c
file_hash: 71e40ed99b5217343d0831e293e7207e5bd30ce53f6ab73f0c1ef6ced1afcc60
line: 7
column: 4
column: 5
function: main
location_invariant:
string: (long long )i >= 0LL
Expand Down
6 changes: 3 additions & 3 deletions tests/regression/56-witness/14-base-unassume-precondition.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,7 @@
file_name: 14-base-unassume-precondition.c
file_hash: 67e6b56700825db19b04a972291f7b05465b5ec2f797799026fae5c0d83e536f
line: 6
column: 2
column: 3
function: foo
loop_invariant:
string: 0 <= i
Expand All @@ -46,7 +46,7 @@
file_name: 14-base-unassume-precondition.c
file_hash: 67e6b56700825db19b04a972291f7b05465b5ec2f797799026fae5c0d83e536f
line: 6
column: 2
column: 3
function: foo
loop_invariant:
string: i <= 100
Expand Down Expand Up @@ -77,7 +77,7 @@
file_name: 14-base-unassume-precondition.c
file_hash: 67e6b56700825db19b04a972291f7b05465b5ec2f797799026fae5c0d83e536f
line: 6
column: 2
column: 3
function: foo
loop_invariant:
string: i <= 50
Expand Down
4 changes: 2 additions & 2 deletions tests/regression/56-witness/15-base-unassume-query.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,7 @@
file_name: 15-base-unassume-query.c
file_hash: 8bad487944a1627a53420a3ea2c079197fc5313416ed1f3e77e9d4c68f236bdd
line: 16
column: 2
column: 3
function: main
location_invariant:
string: i == 2
Expand All @@ -44,7 +44,7 @@
file_name: 15-base-unassume-query.c
file_hash: 8bad487944a1627a53420a3ea2c079197fc5313416ed1f3e77e9d4c68f236bdd
line: 16
column: 2
column: 3
function: main
location_invariant:
string: j == 3
Expand Down
6 changes: 3 additions & 3 deletions tests/regression/56-witness/16-base-unassume-dependent.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@
file_name: 16-base-unassume-dependent.c
file_hash: 82334866168bcd385cfdd9f7e9b4431c30259b8cbae87905462829efa85de98c
line: 8
column: 2
column: 3
function: main
location_invariant:
string: 0 <= i
Expand Down Expand Up @@ -48,7 +48,7 @@
file_name: 16-base-unassume-dependent.c
file_hash: 82334866168bcd385cfdd9f7e9b4431c30259b8cbae87905462829efa85de98c
line: 8
column: 2
column: 3
function: main
location_invariant:
string: i <= j
Expand Down Expand Up @@ -76,7 +76,7 @@
file_name: 16-base-unassume-dependent.c
file_hash: 82334866168bcd385cfdd9f7e9b4431c30259b8cbae87905462829efa85de98c
line: 8
column: 2
column: 3
function: main
location_invariant:
string: j <= 42
Expand Down
2 changes: 1 addition & 1 deletion tests/regression/56-witness/17-base-unassume-tauto.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@
file_name: 17-base-unassume-tauto.c
file_hash: a1dbab3d2dc60945ace118bcacd88e4d448ddb3aaa5e9aebe3d0872266256f89
line: 7
column: 2
column: 3
function: main
location_invariant:
string: i <= i + 1
Expand Down
2 changes: 1 addition & 1 deletion tests/regression/56-witness/18-base-unassume-contra.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@
file_name: 18-base-unassume-contra.c
file_hash: e173c414639b0c08d00854dc6974f87ccf2ae29829c2e5542f984eb8a52929ce
line: 7
column: 2
column: 3
function: main
location_invariant:
string: i + 1 <= i
Expand Down
Loading
Loading