Merge pull request #1400 from goblint/yaml-witness-column

Change YAML witness columns to 1-indexed
goblint · Apr 15, 2024 · c6fc9c2 · c6fc9c2
2 parents 3abe965 + 8cc300c
commit c6fc9c2
Show file tree

Hide file tree

Showing 49 changed files with 195 additions and 195 deletions.
diff --git a/src/analyses/unassumeAnalysis.ml b/src/analyses/unassumeAnalysis.ml
@@ -74,7 +74,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;

diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml
@@ -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;
   }
 
@@ -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;

diff --git a/tests/regression/56-witness/01-base-lor-enums.yml b/tests/regression/56-witness/01-base-lor-enums.yml
@@ -17,7 +17,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
@@ -42,7 +42,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
@@ -67,7 +67,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
@@ -92,7 +92,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
@@ -117,7 +117,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

diff --git a/tests/regression/56-witness/02-base-lor-addr.yml b/tests/regression/56-witness/02-base-lor-addr.yml
@@ -17,7 +17,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
@@ -42,7 +42,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
@@ -67,7 +67,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
@@ -92,7 +92,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
@@ -117,7 +117,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

diff --git a/tests/regression/56-witness/03-int-log-short.yml b/tests/regression/56-witness/03-int-log-short.yml
@@ -17,7 +17,7 @@
     file_name: 03-int-log-short.c
     file_hash: 055e8b0b611a6bbe2b072f5c92f094e63fa339ac53190660ac3e54f2fd40d379
     line: 8
-    column: 2
+    column: 3
     function: main
   location_invariant:
     string: r || x
@@ -42,7 +42,7 @@
     file_name: 03-int-log-short.c
     file_hash: 055e8b0b611a6bbe2b072f5c92f094e63fa339ac53190660ac3e54f2fd40d379
     line: 9
-    column: 2
+    column: 3
     function: main
   location_invariant:
     string: '!(r && y)'

diff --git a/tests/regression/56-witness/04-base-priv-sync-prune.yml b/tests/regression/56-witness/04-base-priv-sync-prune.yml
@@ -17,7 +17,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

diff --git a/tests/regression/56-witness/05-prec-problem.t b/tests/regression/56-witness/05-prec-problem.t
@@ -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
@@ -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'
@@ -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'

diff --git a/tests/regression/56-witness/07-base-lor-interval.yml b/tests/regression/56-witness/07-base-lor-interval.yml
@@ -17,7 +17,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
@@ -42,7 +42,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

diff --git a/tests/regression/56-witness/08-witness-all-locals.t b/tests/regression/56-witness/08-witness-all-locals.t
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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

diff --git a/tests/regression/56-witness/10-apron-unassume-interval.yml b/tests/regression/56-witness/10-apron-unassume-interval.yml
@@ -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
@@ -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

diff --git a/tests/regression/56-witness/11-base-unassume-interval.yml b/tests/regression/56-witness/11-base-unassume-interval.yml
@@ -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
@@ -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

diff --git a/tests/regression/56-witness/12-apron-unassume-branch.yml b/tests/regression/56-witness/12-apron-unassume-branch.yml
@@ -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
@@ -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

diff --git a/tests/regression/56-witness/13-base-unassume-branch.yml b/tests/regression/56-witness/13-base-unassume-branch.yml
@@ -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
@@ -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

diff --git a/tests/regression/56-witness/14-base-unassume-precondition.yml b/tests/regression/56-witness/14-base-unassume-precondition.yml
@@ -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
@@ -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
@@ -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

diff --git a/tests/regression/56-witness/15-base-unassume-query.yml b/tests/regression/56-witness/15-base-unassume-query.yml
@@ -17,7 +17,7 @@
     file_name: 15-base-unassume-query.c
     file_hash: 8bad487944a1627a53420a3ea2c079197fc5313416ed1f3e77e9d4c68f236bdd
     line: 16
-    column: 2
+    column: 3
     function: main
   location_invariant:
     string: i == 2
@@ -42,7 +42,7 @@
     file_name: 15-base-unassume-query.c
     file_hash: 8bad487944a1627a53420a3ea2c079197fc5313416ed1f3e77e9d4c68f236bdd
     line: 16
-    column: 2
+    column: 3
     function: main
   location_invariant:
     string: j == 3

diff --git a/tests/regression/56-witness/16-base-unassume-dependent.yml b/tests/regression/56-witness/16-base-unassume-dependent.yml
@@ -17,7 +17,7 @@
     file_name: 16-base-unassume-dependent.c
     file_hash: 82334866168bcd385cfdd9f7e9b4431c30259b8cbae87905462829efa85de98c
     line: 8
-    column: 2
+    column: 3
     function: main
   location_invariant:
     string: 0 <= i
@@ -42,7 +42,7 @@
     file_name: 16-base-unassume-dependent.c
     file_hash: 82334866168bcd385cfdd9f7e9b4431c30259b8cbae87905462829efa85de98c
     line: 8
-    column: 2
+    column: 3
     function: main
   location_invariant:
     string: i <= j
@@ -67,7 +67,7 @@
     file_name: 16-base-unassume-dependent.c
     file_hash: 82334866168bcd385cfdd9f7e9b4431c30259b8cbae87905462829efa85de98c
     line: 8
-    column: 2
+    column: 3
     function: main
   location_invariant:
     string: j <= 42

diff --git a/tests/regression/56-witness/17-base-unassume-tauto.yml b/tests/regression/56-witness/17-base-unassume-tauto.yml
@@ -17,7 +17,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

diff --git a/tests/regression/56-witness/18-base-unassume-contra.yml b/tests/regression/56-witness/18-base-unassume-contra.yml
@@ -17,7 +17,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