From 8cc300c67cc26df9561bb6eaf419883deeb080d6 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 1 Apr 2024 18:02:51 +0300 Subject: [PATCH] Change YAML witness columns to 1-indexed --- src/analyses/unassumeAnalysis.ml | 2 +- src/witness/yamlWitness.ml | 4 +- .../56-witness/01-base-lor-enums.yml | 10 +- .../56-witness/02-base-lor-addr.yml | 10 +- .../56-witness/03-int-log-short.yml | 4 +- .../56-witness/04-base-priv-sync-prune.yml | 2 +- tests/regression/56-witness/05-prec-problem.t | 6 +- .../56-witness/07-base-lor-interval.yml | 4 +- .../56-witness/08-witness-all-locals.t | 10 +- .../56-witness/10-apron-unassume-interval.yml | 4 +- .../56-witness/11-base-unassume-interval.yml | 4 +- .../56-witness/12-apron-unassume-branch.yml | 4 +- .../56-witness/13-base-unassume-branch.yml | 4 +- .../14-base-unassume-precondition.yml | 6 +- .../56-witness/15-base-unassume-query.yml | 4 +- .../56-witness/16-base-unassume-dependent.yml | 6 +- .../56-witness/17-base-unassume-tauto.yml | 2 +- .../56-witness/18-base-unassume-contra.yml | 2 +- .../56-witness/19-base-unassume-mem.yml | 4 +- .../56-witness/20-apron-unassume-global.yml | 4 +- .../56-witness/21-apron-unassume-priv.yml | 2 +- .../56-witness/22-base-unassume-priv.yml | 2 +- .../56-witness/23-base-unassume-priv2.yml | 2 +- .../56-witness/24-apron-unassume-priv2.yml | 2 +- .../25-apron-unassume-strengthening.yml | 2 +- .../56-witness/26-mine-tutorial-ex4.6.yml | 2 +- .../56-witness/27-mine-tutorial-ex4.7.yml | 2 +- .../56-witness/28-mine-tutorial-ex4.8.yml | 2 +- .../56-witness/29-mine-tutorial-ex4.10.yml | 2 +- .../56-witness/30-base-unassume-inc-dec.yml | 4 +- .../56-witness/31-base-unassume-mem-ex.yml | 6 +- .../56-witness/32-base-unassume-lor-addr.yml | 2 +- .../56-witness/33-base-unassume-lor-enums.yml | 2 +- .../34-base-unassume-inc-dec-traces.yml | 4 +- tests/regression/56-witness/35-hh-ex1b.yml | 2 +- tests/regression/56-witness/36-hh-ex2b.yml | 2 +- tests/regression/56-witness/37-hh-ex3.yml | 2 +- tests/regression/56-witness/38-bh-ex3.yml | 2 +- tests/regression/56-witness/39-bh-ex-add.yml | 2 +- .../regression/56-witness/40-bh-ex1-poly.yml | 2 +- tests/regression/56-witness/41-as-hybrid.yml | 2 +- .../56-witness/42-base-unassume-precheck.yml | 2 +- .../56-witness/43-apron-unassume-precheck.yml | 4 +- .../56-witness/44-base-unassume-array.yml | 4 +- .../62-tm-inv-transfer-protection-witness.yml | 76 ++++++------- .../regression/56-witness/63-hh-ex3-term.yml | 2 +- tests/regression/cfg/foo.t/run.t | 26 ++--- tests/regression/cfg/loops.t/run.t | 106 +++++++++--------- tests/regression/cfg/pr-758.t/run.t | 24 ++-- 49 files changed, 195 insertions(+), 195 deletions(-) diff --git a/src/analyses/unassumeAnalysis.ml b/src/analyses/unassumeAnalysis.ml index 58ac1d06ea..e662bd115a 100644 --- a/src/analyses/unassumeAnalysis.ml +++ b/src/analyses/unassumeAnalysis.ml @@ -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; diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml index c7694f67be..252f8e17e6 100644 --- 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 index 836255d5d4..a99f906477 100644 --- a/tests/regression/56-witness/01-base-lor-enums.yml +++ b/tests/regression/56-witness/01-base-lor-enums.yml @@ -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 @@ -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 @@ -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 @@ -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 @@ -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 diff --git a/tests/regression/56-witness/02-base-lor-addr.yml b/tests/regression/56-witness/02-base-lor-addr.yml index b2980416a5..3b31161392 100644 --- a/tests/regression/56-witness/02-base-lor-addr.yml +++ b/tests/regression/56-witness/02-base-lor-addr.yml @@ -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 @@ -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 @@ -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 @@ -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 @@ -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 diff --git a/tests/regression/56-witness/03-int-log-short.yml b/tests/regression/56-witness/03-int-log-short.yml index dfcde23f59..42a579d23d 100644 --- a/tests/regression/56-witness/03-int-log-short.yml +++ b/tests/regression/56-witness/03-int-log-short.yml @@ -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 @@ -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)' diff --git a/tests/regression/56-witness/04-base-priv-sync-prune.yml b/tests/regression/56-witness/04-base-priv-sync-prune.yml index d85f152415..6a175cde48 100644 --- a/tests/regression/56-witness/04-base-priv-sync-prune.yml +++ b/tests/regression/56-witness/04-base-priv-sync-prune.yml @@ -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 diff --git a/tests/regression/56-witness/05-prec-problem.t b/tests/regression/56-witness/05-prec-problem.t index 4c7dd02fa9..733f16269e 100644 --- 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 index 07b1eef0fb..ef7c9f88e8 100644 --- a/tests/regression/56-witness/07-base-lor-interval.yml +++ b/tests/regression/56-witness/07-base-lor-interval.yml @@ -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 @@ -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 diff --git a/tests/regression/56-witness/08-witness-all-locals.t b/tests/regression/56-witness/08-witness-all-locals.t index bd7012ec25..fc4462201d 100644 --- 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 index f7958922ae..1ed888aeb0 100644 --- 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 index df939b7ca4..cf678ebcc7 100644 --- 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 index 0ea4445131..72b18dbe21 100644 --- 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 index f9186f626d..79cd544742 100644 --- 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 index 2d84e4ea9f..68986ee251 100644 --- 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 index cf037d2d62..0096e69854 100644 --- a/tests/regression/56-witness/15-base-unassume-query.yml +++ b/tests/regression/56-witness/15-base-unassume-query.yml @@ -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 @@ -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 diff --git a/tests/regression/56-witness/16-base-unassume-dependent.yml b/tests/regression/56-witness/16-base-unassume-dependent.yml index fe8dcd303b..65cbe41114 100644 --- a/tests/regression/56-witness/16-base-unassume-dependent.yml +++ b/tests/regression/56-witness/16-base-unassume-dependent.yml @@ -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 @@ -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 @@ -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 diff --git a/tests/regression/56-witness/17-base-unassume-tauto.yml b/tests/regression/56-witness/17-base-unassume-tauto.yml index 358434238c..a50debae59 100644 --- a/tests/regression/56-witness/17-base-unassume-tauto.yml +++ b/tests/regression/56-witness/17-base-unassume-tauto.yml @@ -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 diff --git a/tests/regression/56-witness/18-base-unassume-contra.yml b/tests/regression/56-witness/18-base-unassume-contra.yml index c3306e1ffa..02da202e03 100644 --- a/tests/regression/56-witness/18-base-unassume-contra.yml +++ b/tests/regression/56-witness/18-base-unassume-contra.yml @@ -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 diff --git a/tests/regression/56-witness/19-base-unassume-mem.yml b/tests/regression/56-witness/19-base-unassume-mem.yml index 9d68446eba..30774edca5 100644 --- a/tests/regression/56-witness/19-base-unassume-mem.yml +++ b/tests/regression/56-witness/19-base-unassume-mem.yml @@ -19,7 +19,7 @@ file_name: 19-base-unassume-mem.c file_hash: d71d7065e36b8e0a2c42c96e5f6ea057d28065adae2d85b516989b8d43e77c91 line: 14 - column: 2 + column: 3 function: main location_invariant: string: '*p >= 0' @@ -46,7 +46,7 @@ file_name: 19-base-unassume-mem.c file_hash: d71d7065e36b8e0a2c42c96e5f6ea057d28065adae2d85b516989b8d43e77c91 line: 14 - column: 2 + column: 3 function: main location_invariant: string: '*p <= 10' diff --git a/tests/regression/56-witness/20-apron-unassume-global.yml b/tests/regression/56-witness/20-apron-unassume-global.yml index 6f824d4f9f..b1c8b63756 100644 --- a/tests/regression/56-witness/20-apron-unassume-global.yml +++ b/tests/regression/56-witness/20-apron-unassume-global.yml @@ -20,7 +20,7 @@ file_name: 20-apron-unassume-global.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: 20-apron-unassume-global.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/21-apron-unassume-priv.yml b/tests/regression/56-witness/21-apron-unassume-priv.yml index ab3eb0c6c1..860c51d27c 100644 --- a/tests/regression/56-witness/21-apron-unassume-priv.yml +++ b/tests/regression/56-witness/21-apron-unassume-priv.yml @@ -21,7 +21,7 @@ file_name: 21-apron-unassume-priv.c file_hash: bc48bad1f602a9b79db764c73e42950810b763f19ebda683b33603c8941f2e80 line: 12 - column: 2 + column: 3 function: t_fun location_invariant: string: '0 <= g && g <= 10' diff --git a/tests/regression/56-witness/22-base-unassume-priv.yml b/tests/regression/56-witness/22-base-unassume-priv.yml index f063ed7e6b..3303552eec 100644 --- a/tests/regression/56-witness/22-base-unassume-priv.yml +++ b/tests/regression/56-witness/22-base-unassume-priv.yml @@ -21,7 +21,7 @@ file_name: 22-base-unassume-priv.c file_hash: bc48bad1f602a9b79db764c73e42950810b763f19ebda683b33603c8941f2e80 line: 12 - column: 2 + column: 3 function: t_fun location_invariant: string: '0 <= g && g <= 10' diff --git a/tests/regression/56-witness/23-base-unassume-priv2.yml b/tests/regression/56-witness/23-base-unassume-priv2.yml index 4ca5142b0a..12fd1df44c 100644 --- a/tests/regression/56-witness/23-base-unassume-priv2.yml +++ b/tests/regression/56-witness/23-base-unassume-priv2.yml @@ -21,7 +21,7 @@ file_name: 23-base-unassume-priv2.c file_hash: bc48bad1f602a9b79db764c73e42950810b763f19ebda683b33603c8941f2e80 line: 11 - column: 2 + column: 3 function: t_fun location_invariant: string: '0 <= g && g <= 10' diff --git a/tests/regression/56-witness/24-apron-unassume-priv2.yml b/tests/regression/56-witness/24-apron-unassume-priv2.yml index d775d14929..3fde132519 100644 --- a/tests/regression/56-witness/24-apron-unassume-priv2.yml +++ b/tests/regression/56-witness/24-apron-unassume-priv2.yml @@ -21,7 +21,7 @@ file_name: 24-apron-unassume-priv2.c file_hash: bc48bad1f602a9b79db764c73e42950810b763f19ebda683b33603c8941f2e80 line: 11 - column: 2 + column: 3 function: t_fun location_invariant: string: '0 <= g && g <= 10' diff --git a/tests/regression/56-witness/25-apron-unassume-strengthening.yml b/tests/regression/56-witness/25-apron-unassume-strengthening.yml index 75d4df8026..a9771faf52 100644 --- a/tests/regression/56-witness/25-apron-unassume-strengthening.yml +++ b/tests/regression/56-witness/25-apron-unassume-strengthening.yml @@ -21,7 +21,7 @@ file_name: 25-apron-unassume-strengthening.c file_hash: b2a50e3b423ade600ec2de58fa8ace6ec9a08b85fdc016cbdb7fbe9a3ba80d83 line: 8 - column: 4 + column: 5 function: main location_invariant: string: x >= 0 diff --git a/tests/regression/56-witness/26-mine-tutorial-ex4.6.yml b/tests/regression/56-witness/26-mine-tutorial-ex4.6.yml index 659537ba77..f0299f1d44 100644 --- a/tests/regression/56-witness/26-mine-tutorial-ex4.6.yml +++ b/tests/regression/56-witness/26-mine-tutorial-ex4.6.yml @@ -19,7 +19,7 @@ file_name: 26-mine-tutorial-ex4.6.c file_hash: e119cc77f5ce2a60d7c2b65c5dfbe8037f877b5621deab62b9580c5bbdebd97b line: 5 - column: 2 + column: 3 function: main loop_invariant: string: 0 <= x && x <= 40 diff --git a/tests/regression/56-witness/27-mine-tutorial-ex4.7.yml b/tests/regression/56-witness/27-mine-tutorial-ex4.7.yml index c87b070d40..a3361635fd 100644 --- a/tests/regression/56-witness/27-mine-tutorial-ex4.7.yml +++ b/tests/regression/56-witness/27-mine-tutorial-ex4.7.yml @@ -21,7 +21,7 @@ file_name: 27-mine-tutorial-ex4.7.c file_hash: 4d06e38718d405171bd503e630f6c7a247bb3b0d3c1c6c951466e4989883b43c line: 6 - column: 2 + column: 3 function: main loop_invariant: string: 0 <= x && x <= 40 diff --git a/tests/regression/56-witness/28-mine-tutorial-ex4.8.yml b/tests/regression/56-witness/28-mine-tutorial-ex4.8.yml index c92f0223e4..5d7b57c4ba 100644 --- a/tests/regression/56-witness/28-mine-tutorial-ex4.8.yml +++ b/tests/regression/56-witness/28-mine-tutorial-ex4.8.yml @@ -21,7 +21,7 @@ file_name: 28-mine-tutorial-ex4.8.c file_hash: bd5b719b0d268dd7669edc1dd21b55a2bacab3187f26f112839093b910c91347 line: 6 - column: 2 + column: 3 function: main loop_invariant: string: 0 <= v && v <= 1 diff --git a/tests/regression/56-witness/29-mine-tutorial-ex4.10.yml b/tests/regression/56-witness/29-mine-tutorial-ex4.10.yml index c719c76c0a..35d9f54546 100644 --- a/tests/regression/56-witness/29-mine-tutorial-ex4.10.yml +++ b/tests/regression/56-witness/29-mine-tutorial-ex4.10.yml @@ -22,7 +22,7 @@ file_name: 29-mine-tutorial-ex4.10.c file_hash: e0399cba2a1ab555c14e500606561777d5f029de891ea5bf3cfd8bda880a7ac8 line: 6 - column: 2 + column: 3 function: main loop_invariant: string: 1 <= v && v <= 52 diff --git a/tests/regression/56-witness/30-base-unassume-inc-dec.yml b/tests/regression/56-witness/30-base-unassume-inc-dec.yml index d328abe556..2f254319fd 100644 --- a/tests/regression/56-witness/30-base-unassume-inc-dec.yml +++ b/tests/regression/56-witness/30-base-unassume-inc-dec.yml @@ -21,7 +21,7 @@ file_name: 30-base-unassume-inc-dec.c file_hash: 3df8890403a9efa4ab1c824bac7eba729e187ba93605beda5034793b99ab7bf0 line: 10 - column: 4 + column: 5 function: t_fun location_invariant: string: -10 <= g && g <= 10 @@ -50,7 +50,7 @@ file_name: 30-base-unassume-inc-dec.c file_hash: 3df8890403a9efa4ab1c824bac7eba729e187ba93605beda5034793b99ab7bf0 line: 20 - column: 4 + column: 5 function: t_fun2 location_invariant: string: -10 <= g && g <= 10 diff --git a/tests/regression/56-witness/31-base-unassume-mem-ex.yml b/tests/regression/56-witness/31-base-unassume-mem-ex.yml index 75b1dba18d..4a94de3445 100644 --- a/tests/regression/56-witness/31-base-unassume-mem-ex.yml +++ b/tests/regression/56-witness/31-base-unassume-mem-ex.yml @@ -21,7 +21,7 @@ file_name: 31-base-unassume-mem-ex.c file_hash: 33f8f073cefa79d294ce1e534a3d6db19a6d27ba83efc6b80e0407921997d659 line: 16 - column: 6 + column: 7 function: main location_invariant: string: i >= 0 && j >= 0 @@ -50,7 +50,7 @@ file_name: 31-base-unassume-mem-ex.c file_hash: 33f8f073cefa79d294ce1e534a3d6db19a6d27ba83efc6b80e0407921997d659 line: 23 - column: 6 + column: 7 function: main location_invariant: string: (p == &i || p == &j) && *p >= 0 @@ -79,7 +79,7 @@ file_name: 31-base-unassume-mem-ex.c file_hash: 33f8f073cefa79d294ce1e534a3d6db19a6d27ba83efc6b80e0407921997d659 line: 30 - column: 6 + column: 7 function: main location_invariant: string: '*p >= 0' diff --git a/tests/regression/56-witness/32-base-unassume-lor-addr.yml b/tests/regression/56-witness/32-base-unassume-lor-addr.yml index a0c6476fe1..cecf2ad395 100644 --- a/tests/regression/56-witness/32-base-unassume-lor-addr.yml +++ b/tests/regression/56-witness/32-base-unassume-lor-addr.yml @@ -20,7 +20,7 @@ file_name: 32-base-unassume-lor-addr.c file_hash: 36ab59c15763945f1d20bc6bc4240e220286b6c8e4cef83742733bf75bc397b0 line: 8 - column: 2 + column: 3 function: main location_invariant: string: p == &i || p == &j diff --git a/tests/regression/56-witness/33-base-unassume-lor-enums.yml b/tests/regression/56-witness/33-base-unassume-lor-enums.yml index c3220fca14..fb4da71448 100644 --- a/tests/regression/56-witness/33-base-unassume-lor-enums.yml +++ b/tests/regression/56-witness/33-base-unassume-lor-enums.yml @@ -21,7 +21,7 @@ file_name: 33-base-unassume-lor-enums.c file_hash: 5014d96b45984600f1ce8a4f6f208ab856539c33e7124a71e41836a1a2cbdd40 line: 7 - column: 2 + column: 3 function: main location_invariant: string: i == 0 || i == 1 || i == 2 diff --git a/tests/regression/56-witness/34-base-unassume-inc-dec-traces.yml b/tests/regression/56-witness/34-base-unassume-inc-dec-traces.yml index 55fa88bd52..6e61b8d8dd 100644 --- a/tests/regression/56-witness/34-base-unassume-inc-dec-traces.yml +++ b/tests/regression/56-witness/34-base-unassume-inc-dec-traces.yml @@ -21,7 +21,7 @@ file_name: 34-base-unassume-inc-dec-traces.c file_hash: 3df8890403a9efa4ab1c824bac7eba729e187ba93605beda5034793b99ab7bf0 line: 10 - column: 4 + column: 5 function: t_fun location_invariant: string: -10 <= g && g <= 10 @@ -50,7 +50,7 @@ file_name: 34-base-unassume-inc-dec-traces.c file_hash: 3df8890403a9efa4ab1c824bac7eba729e187ba93605beda5034793b99ab7bf0 line: 20 - column: 4 + column: 5 function: t_fun2 location_invariant: string: -10 <= g && g <= 10 diff --git a/tests/regression/56-witness/35-hh-ex1b.yml b/tests/regression/56-witness/35-hh-ex1b.yml index 084c71cc97..627f06c28e 100644 --- a/tests/regression/56-witness/35-hh-ex1b.yml +++ b/tests/regression/56-witness/35-hh-ex1b.yml @@ -21,7 +21,7 @@ file_name: 35-hh-ex1b.c file_hash: 9fe07d5f950140350848bae4342d9d1b7c6c9f625f6985746089a36a37243600 line: 7 - column: 4 + column: 5 function: main loop_invariant: string: 0 <= i && i <= 99 diff --git a/tests/regression/56-witness/36-hh-ex2b.yml b/tests/regression/56-witness/36-hh-ex2b.yml index d2a7218a28..0049bee97c 100644 --- a/tests/regression/56-witness/36-hh-ex2b.yml +++ b/tests/regression/56-witness/36-hh-ex2b.yml @@ -21,7 +21,7 @@ file_name: 36-hh-ex2b.c file_hash: e4a0ecee56af00cc83ce75411061e74f80edce8c562310a7ea11499eb606d133 line: 6 - column: 2 + column: 3 function: main loop_invariant: string: 0 <= n && n <= 60 diff --git a/tests/regression/56-witness/37-hh-ex3.yml b/tests/regression/56-witness/37-hh-ex3.yml index d6cd5150a4..b60124d73a 100644 --- a/tests/regression/56-witness/37-hh-ex3.yml +++ b/tests/regression/56-witness/37-hh-ex3.yml @@ -21,7 +21,7 @@ file_name: 37-hh-ex3.c file_hash: 9c984e89a790b595d2b37ca8a05e5967a15130592cb2567fac2fae4aff668a4f line: 6 - column: 4 + column: 5 function: main location_invariant: string: 0 <= i && i <= 3 diff --git a/tests/regression/56-witness/38-bh-ex3.yml b/tests/regression/56-witness/38-bh-ex3.yml index 2e489e1f17..a115770b99 100644 --- a/tests/regression/56-witness/38-bh-ex3.yml +++ b/tests/regression/56-witness/38-bh-ex3.yml @@ -21,7 +21,7 @@ file_name: 38-bh-ex3.c file_hash: 9d2cb05c2decf8564defade7194c336478ec5ae4be1ee79202269ff09830dada line: 7 - column: 2 + column: 3 function: main loop_invariant: string: 0 <= m && m <= 60 && 0 <= n && n <= 60 diff --git a/tests/regression/56-witness/39-bh-ex-add.yml b/tests/regression/56-witness/39-bh-ex-add.yml index 29d3006276..1ea46c9b56 100644 --- a/tests/regression/56-witness/39-bh-ex-add.yml +++ b/tests/regression/56-witness/39-bh-ex-add.yml @@ -21,7 +21,7 @@ file_name: 39-bh-ex-add.c file_hash: 9d2cb05c2decf8564defade7194c336478ec5ae4be1ee79202269ff09830dada line: 7 - column: 2 + column: 3 function: main loop_invariant: string: 0 <= m && m <= 60 && 0 <= n && n <= 60 diff --git a/tests/regression/56-witness/40-bh-ex1-poly.yml b/tests/regression/56-witness/40-bh-ex1-poly.yml index cdbd8d666b..5166700933 100644 --- a/tests/regression/56-witness/40-bh-ex1-poly.yml +++ b/tests/regression/56-witness/40-bh-ex1-poly.yml @@ -21,7 +21,7 @@ file_name: 40-bh-ex1-poly.c file_hash: 34f781dcae089ecb6b7b2811027395fcb501b8477b7e5016f7b38081724bea28 line: 7 - column: 4 + column: 5 function: main location_invariant: string: 0 <= i && i <= 3 diff --git a/tests/regression/56-witness/41-as-hybrid.yml b/tests/regression/56-witness/41-as-hybrid.yml index 8eac9f75f7..70e3dc3ed6 100644 --- a/tests/regression/56-witness/41-as-hybrid.yml +++ b/tests/regression/56-witness/41-as-hybrid.yml @@ -21,7 +21,7 @@ file_name: 41-as-hybrid.c file_hash: 74adb6d33dd35bafe5415bc407a94fa277812ad9921726a7c1f5ee00d3a39af6 line: 5 - column: 2 + column: 3 function: main loop_invariant: string: 0 <= i && i <= 9 diff --git a/tests/regression/56-witness/42-base-unassume-precheck.yml b/tests/regression/56-witness/42-base-unassume-precheck.yml index 30f8901c3a..6b495fbfa7 100644 --- a/tests/regression/56-witness/42-base-unassume-precheck.yml +++ b/tests/regression/56-witness/42-base-unassume-precheck.yml @@ -20,7 +20,7 @@ file_name: 42-base-unassume-precheck.c file_hash: e173c414639b0c08d00854dc6974f87ccf2ae29829c2e5542f984eb8a52929ce line: 7 - column: 2 + column: 3 function: main location_invariant: string: 100 <= i && i < 999 diff --git a/tests/regression/56-witness/43-apron-unassume-precheck.yml b/tests/regression/56-witness/43-apron-unassume-precheck.yml index 355283228c..9cf285f3ab 100644 --- a/tests/regression/56-witness/43-apron-unassume-precheck.yml +++ b/tests/regression/56-witness/43-apron-unassume-precheck.yml @@ -20,7 +20,7 @@ file_name: 43-apron-unassume-precheck.c file_hash: e173c414639b0c08d00854dc6974f87ccf2ae29829c2e5542f984eb8a52929ce line: 7 - column: 2 + column: 3 function: main location_invariant: string: 0 <= i && i < 9 @@ -48,7 +48,7 @@ file_name: 43-apron-unassume-precheck.c file_hash: e173c414639b0c08d00854dc6974f87ccf2ae29829c2e5542f984eb8a52929ce line: 8 - column: 2 + column: 3 function: main location_invariant: string: 100 <= i && i < 999 diff --git a/tests/regression/56-witness/44-base-unassume-array.yml b/tests/regression/56-witness/44-base-unassume-array.yml index ad2e3a3ad2..b43131824b 100644 --- a/tests/regression/56-witness/44-base-unassume-array.yml +++ b/tests/regression/56-witness/44-base-unassume-array.yml @@ -21,7 +21,7 @@ file_name: 44-base-unassume-array.c file_hash: 9d9dc013c8d8aee483852aa73d0b4ac48ee7ea0f5433dc86ee28c3fe54c49726 line: 7 - column: 2 + column: 3 function: main loop_invariant: string: 0 <= a[(long )"all_index"] @@ -50,7 +50,7 @@ file_name: 44-base-unassume-array.c file_hash: 9d9dc013c8d8aee483852aa73d0b4ac48ee7ea0f5433dc86ee28c3fe54c49726 line: 7 - column: 2 + column: 3 function: main loop_invariant: string: a[(long )"all_index"] < 3 diff --git a/tests/regression/56-witness/62-tm-inv-transfer-protection-witness.yml b/tests/regression/56-witness/62-tm-inv-transfer-protection-witness.yml index 5f98df568b..374c353ed9 100644 --- a/tests/regression/56-witness/62-tm-inv-transfer-protection-witness.yml +++ b/tests/regression/56-witness/62-tm-inv-transfer-protection-witness.yml @@ -21,7 +21,7 @@ file_name: 62-tm-inv-transfer-protection-witness.c file_hash: f3fd475486e1259fbd3c64c1b66b2ded22ee682bc9120914578ac370a630548b line: 11 - column: 2 + column: 3 function: t_fun location_invariant: string: 0 <= g @@ -50,7 +50,7 @@ file_name: 62-tm-inv-transfer-protection-witness.c file_hash: f3fd475486e1259fbd3c64c1b66b2ded22ee682bc9120914578ac370a630548b line: 11 - column: 2 + column: 3 function: t_fun location_invariant: string: 40 <= g @@ -79,7 +79,7 @@ file_name: 62-tm-inv-transfer-protection-witness.c file_hash: f3fd475486e1259fbd3c64c1b66b2ded22ee682bc9120914578ac370a630548b line: 11 - column: 2 + column: 3 function: t_fun location_invariant: string: g <= 41 @@ -108,7 +108,7 @@ file_name: 62-tm-inv-transfer-protection-witness.c file_hash: f3fd475486e1259fbd3c64c1b66b2ded22ee682bc9120914578ac370a630548b line: 11 - column: 2 + column: 3 function: t_fun location_invariant: string: g <= 127 @@ -137,7 +137,7 @@ file_name: 62-tm-inv-transfer-protection-witness.c file_hash: f3fd475486e1259fbd3c64c1b66b2ded22ee682bc9120914578ac370a630548b line: 11 - column: 2 + column: 3 function: t_fun location_invariant: string: (unsigned long )arg == 0UL @@ -166,7 +166,7 @@ file_name: 62-tm-inv-transfer-protection-witness.c file_hash: f3fd475486e1259fbd3c64c1b66b2ded22ee682bc9120914578ac370a630548b line: 11 - column: 2 + column: 3 function: t_fun location_invariant: string: g != 0 @@ -195,7 +195,7 @@ file_name: 62-tm-inv-transfer-protection-witness.c file_hash: f3fd475486e1259fbd3c64c1b66b2ded22ee682bc9120914578ac370a630548b line: 12 - column: 2 + column: 3 function: t_fun location_invariant: string: 0 <= g @@ -224,7 +224,7 @@ file_name: 62-tm-inv-transfer-protection-witness.c file_hash: f3fd475486e1259fbd3c64c1b66b2ded22ee682bc9120914578ac370a630548b line: 12 - column: 2 + column: 3 function: t_fun location_invariant: string: 40 <= g @@ -253,7 +253,7 @@ file_name: 62-tm-inv-transfer-protection-witness.c file_hash: f3fd475486e1259fbd3c64c1b66b2ded22ee682bc9120914578ac370a630548b line: 12 - column: 2 + column: 3 function: t_fun location_invariant: string: g <= 41 @@ -282,7 +282,7 @@ file_name: 62-tm-inv-transfer-protection-witness.c file_hash: f3fd475486e1259fbd3c64c1b66b2ded22ee682bc9120914578ac370a630548b line: 12 - column: 2 + column: 3 function: t_fun location_invariant: string: g <= 127 @@ -311,7 +311,7 @@ file_name: 62-tm-inv-transfer-protection-witness.c file_hash: f3fd475486e1259fbd3c64c1b66b2ded22ee682bc9120914578ac370a630548b line: 12 - column: 2 + column: 3 function: t_fun location_invariant: string: (unsigned long )arg == 0UL @@ -340,7 +340,7 @@ file_name: 62-tm-inv-transfer-protection-witness.c file_hash: f3fd475486e1259fbd3c64c1b66b2ded22ee682bc9120914578ac370a630548b line: 12 - column: 2 + column: 3 function: t_fun location_invariant: string: g != 0 @@ -369,7 +369,7 @@ file_name: 62-tm-inv-transfer-protection-witness.c file_hash: f3fd475486e1259fbd3c64c1b66b2ded22ee682bc9120914578ac370a630548b line: 15 - column: 2 + column: 3 function: t_fun location_invariant: string: 0 <= g @@ -398,7 +398,7 @@ file_name: 62-tm-inv-transfer-protection-witness.c file_hash: f3fd475486e1259fbd3c64c1b66b2ded22ee682bc9120914578ac370a630548b line: 15 - column: 2 + column: 3 function: t_fun location_invariant: string: 41 <= g @@ -427,7 +427,7 @@ file_name: 62-tm-inv-transfer-protection-witness.c file_hash: f3fd475486e1259fbd3c64c1b66b2ded22ee682bc9120914578ac370a630548b line: 15 - column: 2 + column: 3 function: t_fun location_invariant: string: g <= 42 @@ -456,7 +456,7 @@ file_name: 62-tm-inv-transfer-protection-witness.c file_hash: f3fd475486e1259fbd3c64c1b66b2ded22ee682bc9120914578ac370a630548b line: 15 - column: 2 + column: 3 function: t_fun location_invariant: string: g <= 127 @@ -485,7 +485,7 @@ file_name: 62-tm-inv-transfer-protection-witness.c file_hash: f3fd475486e1259fbd3c64c1b66b2ded22ee682bc9120914578ac370a630548b line: 15 - column: 2 + column: 3 function: t_fun location_invariant: string: (unsigned long )arg == 0UL @@ -514,7 +514,7 @@ file_name: 62-tm-inv-transfer-protection-witness.c file_hash: f3fd475486e1259fbd3c64c1b66b2ded22ee682bc9120914578ac370a630548b line: 15 - column: 2 + column: 3 function: t_fun location_invariant: string: g != 0 @@ -543,7 +543,7 @@ file_name: 62-tm-inv-transfer-protection-witness.c file_hash: f3fd475486e1259fbd3c64c1b66b2ded22ee682bc9120914578ac370a630548b line: 23 - column: 2 + column: 3 function: t_fun2 location_invariant: string: 0 <= g @@ -572,7 +572,7 @@ file_name: 62-tm-inv-transfer-protection-witness.c file_hash: f3fd475486e1259fbd3c64c1b66b2ded22ee682bc9120914578ac370a630548b line: 23 - column: 2 + column: 3 function: t_fun2 location_invariant: string: g <= 42 @@ -601,7 +601,7 @@ file_name: 62-tm-inv-transfer-protection-witness.c file_hash: f3fd475486e1259fbd3c64c1b66b2ded22ee682bc9120914578ac370a630548b line: 23 - column: 2 + column: 3 function: t_fun2 location_invariant: string: g <= 127 @@ -630,7 +630,7 @@ file_name: 62-tm-inv-transfer-protection-witness.c file_hash: f3fd475486e1259fbd3c64c1b66b2ded22ee682bc9120914578ac370a630548b line: 23 - column: 2 + column: 3 function: t_fun2 location_invariant: string: (unsigned long )arg == 0UL @@ -659,7 +659,7 @@ file_name: 62-tm-inv-transfer-protection-witness.c file_hash: f3fd475486e1259fbd3c64c1b66b2ded22ee682bc9120914578ac370a630548b line: 23 - column: 2 + column: 3 function: t_fun2 location_invariant: string: g != 0 @@ -688,7 +688,7 @@ file_name: 62-tm-inv-transfer-protection-witness.c file_hash: f3fd475486e1259fbd3c64c1b66b2ded22ee682bc9120914578ac370a630548b line: 34 - column: 2 + column: 3 function: main location_invariant: string: 0 <= g @@ -717,7 +717,7 @@ file_name: 62-tm-inv-transfer-protection-witness.c file_hash: f3fd475486e1259fbd3c64c1b66b2ded22ee682bc9120914578ac370a630548b line: 34 - column: 2 + column: 3 function: main location_invariant: string: 40 <= g @@ -746,7 +746,7 @@ file_name: 62-tm-inv-transfer-protection-witness.c file_hash: f3fd475486e1259fbd3c64c1b66b2ded22ee682bc9120914578ac370a630548b line: 34 - column: 2 + column: 3 function: main location_invariant: string: g <= 41 @@ -775,7 +775,7 @@ file_name: 62-tm-inv-transfer-protection-witness.c file_hash: f3fd475486e1259fbd3c64c1b66b2ded22ee682bc9120914578ac370a630548b line: 34 - column: 2 + column: 3 function: main location_invariant: string: g <= 127 @@ -804,7 +804,7 @@ file_name: 62-tm-inv-transfer-protection-witness.c file_hash: f3fd475486e1259fbd3c64c1b66b2ded22ee682bc9120914578ac370a630548b line: 34 - column: 2 + column: 3 function: main location_invariant: string: g != 0 @@ -833,7 +833,7 @@ file_name: 62-tm-inv-transfer-protection-witness.c file_hash: f3fd475486e1259fbd3c64c1b66b2ded22ee682bc9120914578ac370a630548b line: 35 - column: 2 + column: 3 function: main location_invariant: string: 0 <= g @@ -862,7 +862,7 @@ file_name: 62-tm-inv-transfer-protection-witness.c file_hash: f3fd475486e1259fbd3c64c1b66b2ded22ee682bc9120914578ac370a630548b line: 35 - column: 2 + column: 3 function: main location_invariant: string: 40 <= g @@ -891,7 +891,7 @@ file_name: 62-tm-inv-transfer-protection-witness.c file_hash: f3fd475486e1259fbd3c64c1b66b2ded22ee682bc9120914578ac370a630548b line: 35 - column: 2 + column: 3 function: main location_invariant: string: g <= 41 @@ -920,7 +920,7 @@ file_name: 62-tm-inv-transfer-protection-witness.c file_hash: f3fd475486e1259fbd3c64c1b66b2ded22ee682bc9120914578ac370a630548b line: 35 - column: 2 + column: 3 function: main location_invariant: string: g <= 127 @@ -949,7 +949,7 @@ file_name: 62-tm-inv-transfer-protection-witness.c file_hash: f3fd475486e1259fbd3c64c1b66b2ded22ee682bc9120914578ac370a630548b line: 35 - column: 2 + column: 3 function: main location_invariant: string: g != 0 @@ -978,7 +978,7 @@ file_name: 62-tm-inv-transfer-protection-witness.c file_hash: f3fd475486e1259fbd3c64c1b66b2ded22ee682bc9120914578ac370a630548b line: 41 - column: 2 + column: 3 function: main location_invariant: string: 0 <= g @@ -1007,7 +1007,7 @@ file_name: 62-tm-inv-transfer-protection-witness.c file_hash: f3fd475486e1259fbd3c64c1b66b2ded22ee682bc9120914578ac370a630548b line: 41 - column: 2 + column: 3 function: main location_invariant: string: 40 <= g @@ -1036,7 +1036,7 @@ file_name: 62-tm-inv-transfer-protection-witness.c file_hash: f3fd475486e1259fbd3c64c1b66b2ded22ee682bc9120914578ac370a630548b line: 41 - column: 2 + column: 3 function: main location_invariant: string: g <= 41 @@ -1065,7 +1065,7 @@ file_name: 62-tm-inv-transfer-protection-witness.c file_hash: f3fd475486e1259fbd3c64c1b66b2ded22ee682bc9120914578ac370a630548b line: 41 - column: 2 + column: 3 function: main location_invariant: string: g <= 127 @@ -1094,7 +1094,7 @@ file_name: 62-tm-inv-transfer-protection-witness.c file_hash: f3fd475486e1259fbd3c64c1b66b2ded22ee682bc9120914578ac370a630548b line: 41 - column: 2 + column: 3 function: main location_invariant: string: g != 0 diff --git a/tests/regression/56-witness/63-hh-ex3-term.yml b/tests/regression/56-witness/63-hh-ex3-term.yml index e635e24014..7813464ea4 100644 --- a/tests/regression/56-witness/63-hh-ex3-term.yml +++ b/tests/regression/56-witness/63-hh-ex3-term.yml @@ -17,7 +17,7 @@ file_name: 63-hh-ex3-term.c file_hash: 9c984e89a790b595d2b37ca8a05e5967a15130592cb2567fac2fae4aff668a4f line: 17 - column: 4 + column: 5 function: main location_invariant: string: 0 <= i && i <= 3 diff --git a/tests/regression/cfg/foo.t/run.t b/tests/regression/cfg/foo.t/run.t index 6dcb21863e..705fb8d497 100644 --- a/tests/regression/cfg/foo.t/run.t +++ b/tests/regression/cfg/foo.t/run.t @@ -75,7 +75,7 @@ file_name: foo.c file_hash: $FILE_HASH line: 3 - column: 2 + column: 3 function: main loop_invariant: string: b <= 1 @@ -86,7 +86,7 @@ file_name: foo.c file_hash: $FILE_HASH line: 3 - column: 2 + column: 3 function: main loop_invariant: string: 1 <= a @@ -97,7 +97,7 @@ file_name: foo.c file_hash: $FILE_HASH line: 7 - column: 2 + column: 3 function: main location_invariant: string: b == 0 @@ -108,7 +108,7 @@ file_name: foo.c file_hash: $FILE_HASH line: 7 - column: 2 + column: 3 function: main location_invariant: string: a != 0 @@ -119,7 +119,7 @@ file_name: foo.c file_hash: $FILE_HASH line: 7 - column: 2 + column: 3 function: main location_invariant: string: 1 <= a @@ -130,7 +130,7 @@ file_name: foo.c file_hash: $FILE_HASH line: 5 - column: 4 + column: 5 function: main location_invariant: string: b <= 1 @@ -141,7 +141,7 @@ file_name: foo.c file_hash: $FILE_HASH line: 5 - column: 4 + column: 5 function: main location_invariant: string: b != 0 @@ -152,7 +152,7 @@ file_name: foo.c file_hash: $FILE_HASH line: 5 - column: 4 + column: 5 function: main location_invariant: string: a != 1 @@ -163,7 +163,7 @@ file_name: foo.c file_hash: $FILE_HASH line: 5 - column: 4 + column: 5 function: main location_invariant: string: 2 <= a @@ -174,7 +174,7 @@ file_name: foo.c file_hash: $FILE_HASH line: 4 - column: 4 + column: 5 function: main location_invariant: string: b <= 1 @@ -185,7 +185,7 @@ file_name: foo.c file_hash: $FILE_HASH line: 4 - column: 4 + column: 5 function: main location_invariant: string: b != 0 @@ -196,7 +196,7 @@ file_name: foo.c file_hash: $FILE_HASH line: 4 - column: 4 + column: 5 function: main location_invariant: string: a != 0 @@ -207,7 +207,7 @@ file_name: foo.c file_hash: $FILE_HASH line: 4 - column: 4 + column: 5 function: main location_invariant: string: 1 <= a diff --git a/tests/regression/cfg/loops.t/run.t b/tests/regression/cfg/loops.t/run.t index 01216a624e..6596e7b4a4 100644 --- a/tests/regression/cfg/loops.t/run.t +++ b/tests/regression/cfg/loops.t/run.t @@ -227,7 +227,7 @@ file_name: loops.c file_hash: $FILE_HASH line: 45 - column: 2 + column: 3 function: main loop_invariant: string: k == 0 @@ -238,7 +238,7 @@ file_name: loops.c file_hash: $FILE_HASH line: 45 - column: 2 + column: 3 function: main loop_invariant: string: j == 10 @@ -249,7 +249,7 @@ file_name: loops.c file_hash: $FILE_HASH line: 45 - column: 2 + column: 3 function: main loop_invariant: string: i <= 9 @@ -260,7 +260,7 @@ file_name: loops.c file_hash: $FILE_HASH line: 45 - column: 2 + column: 3 function: main loop_invariant: string: 0 <= i @@ -271,7 +271,7 @@ file_name: loops.c file_hash: $FILE_HASH line: 39 - column: 2 + column: 3 function: main loop_invariant: string: k == 0 @@ -282,7 +282,7 @@ file_name: loops.c file_hash: $FILE_HASH line: 39 - column: 2 + column: 3 function: main loop_invariant: string: j == 10 @@ -293,7 +293,7 @@ file_name: loops.c file_hash: $FILE_HASH line: 39 - column: 2 + column: 3 function: main loop_invariant: string: i <= 10 @@ -304,7 +304,7 @@ file_name: loops.c file_hash: $FILE_HASH line: 39 - column: 2 + column: 3 function: main loop_invariant: string: 0 <= i @@ -315,7 +315,7 @@ file_name: loops.c file_hash: $FILE_HASH line: 34 - column: 2 + column: 3 function: main loop_invariant: string: j <= 10 @@ -326,7 +326,7 @@ file_name: loops.c file_hash: $FILE_HASH line: 34 - column: 2 + column: 3 function: main loop_invariant: string: i == 10 @@ -337,7 +337,7 @@ file_name: loops.c file_hash: $FILE_HASH line: 34 - column: 2 + column: 3 function: main loop_invariant: string: 0 <= j @@ -348,7 +348,7 @@ file_name: loops.c file_hash: $FILE_HASH line: 29 - column: 2 + column: 3 function: main loop_invariant: string: i <= 10 @@ -359,7 +359,7 @@ file_name: loops.c file_hash: $FILE_HASH line: 29 - column: 2 + column: 3 function: main loop_invariant: string: 0 <= i @@ -370,7 +370,7 @@ file_name: loops.c file_hash: $FILE_HASH line: 23 - column: 2 + column: 3 function: main loop_invariant: string: i <= 10 @@ -381,7 +381,7 @@ file_name: loops.c file_hash: $FILE_HASH line: 23 - column: 2 + column: 3 function: main loop_invariant: string: 0 <= i @@ -392,7 +392,7 @@ file_name: loops.c file_hash: $FILE_HASH line: 18 - column: 2 + column: 3 function: main loop_invariant: string: i <= 10 @@ -403,7 +403,7 @@ file_name: loops.c file_hash: $FILE_HASH line: 18 - column: 2 + column: 3 function: main loop_invariant: string: 0 <= i @@ -414,7 +414,7 @@ file_name: loops.c file_hash: $FILE_HASH line: 13 - column: 2 + column: 3 function: main loop_invariant: string: i <= 10 @@ -425,7 +425,7 @@ file_name: loops.c file_hash: $FILE_HASH line: 13 - column: 2 + column: 3 function: main loop_invariant: string: 0 <= i @@ -436,7 +436,7 @@ file_name: loops.c file_hash: $FILE_HASH line: 8 - column: 2 + column: 3 function: main loop_invariant: string: i <= 10 @@ -447,7 +447,7 @@ file_name: loops.c file_hash: $FILE_HASH line: 8 - column: 2 + column: 3 function: main loop_invariant: string: 0 <= i @@ -458,7 +458,7 @@ file_name: loops.c file_hash: $FILE_HASH line: 49 - column: 2 + column: 3 function: main location_invariant: string: k == 0 @@ -469,7 +469,7 @@ file_name: loops.c file_hash: $FILE_HASH line: 49 - column: 2 + column: 3 function: main location_invariant: string: j == 10 @@ -480,7 +480,7 @@ file_name: loops.c file_hash: $FILE_HASH line: 49 - column: 2 + column: 3 function: main location_invariant: string: i == 10 @@ -491,7 +491,7 @@ file_name: loops.c file_hash: $FILE_HASH line: 46 - column: 4 + column: 5 function: main location_invariant: string: k == 0 @@ -502,7 +502,7 @@ file_name: loops.c file_hash: $FILE_HASH line: 46 - column: 4 + column: 5 function: main location_invariant: string: j == 10 @@ -513,7 +513,7 @@ file_name: loops.c file_hash: $FILE_HASH line: 46 - column: 4 + column: 5 function: main location_invariant: string: i <= 9 @@ -524,7 +524,7 @@ file_name: loops.c file_hash: $FILE_HASH line: 46 - column: 4 + column: 5 function: main location_invariant: string: 0 <= i @@ -535,7 +535,7 @@ file_name: loops.c file_hash: $FILE_HASH line: 44 - column: 2 + column: 3 function: main location_invariant: string: k == 0 @@ -546,7 +546,7 @@ file_name: loops.c file_hash: $FILE_HASH line: 44 - column: 2 + column: 3 function: main location_invariant: string: j == 10 @@ -557,7 +557,7 @@ file_name: loops.c file_hash: $FILE_HASH line: 44 - column: 2 + column: 3 function: main location_invariant: string: i == 10 @@ -568,7 +568,7 @@ file_name: loops.c file_hash: $FILE_HASH line: 40 - column: 4 + column: 5 function: main location_invariant: string: k == 0 @@ -579,7 +579,7 @@ file_name: loops.c file_hash: $FILE_HASH line: 40 - column: 4 + column: 5 function: main location_invariant: string: j == 10 @@ -590,7 +590,7 @@ file_name: loops.c file_hash: $FILE_HASH line: 40 - column: 4 + column: 5 function: main location_invariant: string: i <= 9 @@ -601,7 +601,7 @@ file_name: loops.c file_hash: $FILE_HASH line: 40 - column: 4 + column: 5 function: main location_invariant: string: 0 <= i @@ -612,7 +612,7 @@ file_name: loops.c file_hash: $FILE_HASH line: 39 - column: 2 + column: 3 function: main location_invariant: string: j == 10 @@ -623,7 +623,7 @@ file_name: loops.c file_hash: $FILE_HASH line: 39 - column: 2 + column: 3 function: main location_invariant: string: i == 10 @@ -634,7 +634,7 @@ file_name: loops.c file_hash: $FILE_HASH line: 35 - column: 4 + column: 5 function: main location_invariant: string: j <= 9 @@ -645,7 +645,7 @@ file_name: loops.c file_hash: $FILE_HASH line: 35 - column: 4 + column: 5 function: main location_invariant: string: i == 10 @@ -656,7 +656,7 @@ file_name: loops.c file_hash: $FILE_HASH line: 35 - column: 4 + column: 5 function: main location_invariant: string: 0 <= j @@ -667,7 +667,7 @@ file_name: loops.c file_hash: $FILE_HASH line: 34 - column: 2 + column: 3 function: main location_invariant: string: i == 10 @@ -678,7 +678,7 @@ file_name: loops.c file_hash: $FILE_HASH line: 30 - column: 4 + column: 5 function: main location_invariant: string: i <= 9 @@ -689,7 +689,7 @@ file_name: loops.c file_hash: $FILE_HASH line: 30 - column: 4 + column: 5 function: main location_invariant: string: 0 <= i @@ -700,7 +700,7 @@ file_name: loops.c file_hash: $FILE_HASH line: 28 - column: 2 + column: 3 function: main location_invariant: string: i == 10 @@ -711,7 +711,7 @@ file_name: loops.c file_hash: $FILE_HASH line: 24 - column: 4 + column: 5 function: main location_invariant: string: i <= 9 @@ -722,7 +722,7 @@ file_name: loops.c file_hash: $FILE_HASH line: 24 - column: 4 + column: 5 function: main location_invariant: string: 0 <= i @@ -733,7 +733,7 @@ file_name: loops.c file_hash: $FILE_HASH line: 23 - column: 2 + column: 3 function: main location_invariant: string: i == 10 @@ -744,7 +744,7 @@ file_name: loops.c file_hash: $FILE_HASH line: 18 - column: 2 + column: 3 function: main location_invariant: string: i == 10 @@ -755,7 +755,7 @@ file_name: loops.c file_hash: $FILE_HASH line: 14 - column: 4 + column: 5 function: main location_invariant: string: i <= 9 @@ -766,7 +766,7 @@ file_name: loops.c file_hash: $FILE_HASH line: 14 - column: 4 + column: 5 function: main location_invariant: string: 0 <= i @@ -777,7 +777,7 @@ file_name: loops.c file_hash: $FILE_HASH line: 13 - column: 2 + column: 3 function: main location_invariant: string: i == 10 @@ -788,7 +788,7 @@ file_name: loops.c file_hash: $FILE_HASH line: 9 - column: 4 + column: 5 function: main location_invariant: string: i <= 9 @@ -799,7 +799,7 @@ file_name: loops.c file_hash: $FILE_HASH line: 9 - column: 4 + column: 5 function: main location_invariant: string: 0 <= i diff --git a/tests/regression/cfg/pr-758.t/run.t b/tests/regression/cfg/pr-758.t/run.t index 04a68be3b6..58bbb88ce4 100644 --- a/tests/regression/cfg/pr-758.t/run.t +++ b/tests/regression/cfg/pr-758.t/run.t @@ -101,7 +101,7 @@ file_name: pr-758.c file_hash: $FILE_HASH line: 6 - column: 2 + column: 3 function: main loop_invariant: string: x <= 10 @@ -112,7 +112,7 @@ file_name: pr-758.c file_hash: $FILE_HASH line: 6 - column: 2 + column: 3 function: main loop_invariant: string: 0 <= x @@ -123,7 +123,7 @@ file_name: pr-758.c file_hash: $FILE_HASH line: 21 - column: 2 + column: 3 function: main location_invariant: string: x == 10 @@ -134,7 +134,7 @@ file_name: pr-758.c file_hash: $FILE_HASH line: 21 - column: 2 + column: 3 function: main location_invariant: string: k == 0 @@ -145,7 +145,7 @@ file_name: pr-758.c file_hash: $FILE_HASH line: 21 - column: 2 + column: 3 function: main location_invariant: string: i == 0 @@ -156,7 +156,7 @@ file_name: pr-758.c file_hash: $FILE_HASH line: 21 - column: 2 + column: 3 function: main location_invariant: string: a.kaal == 2 @@ -167,7 +167,7 @@ file_name: pr-758.c file_hash: $FILE_HASH line: 21 - column: 2 + column: 3 function: main location_invariant: string: a.hind == 3 @@ -178,7 +178,7 @@ file_name: pr-758.c file_hash: $FILE_HASH line: 20 - column: 2 + column: 3 function: main location_invariant: string: x == 10 @@ -189,7 +189,7 @@ file_name: pr-758.c file_hash: $FILE_HASH line: 20 - column: 2 + column: 3 function: main location_invariant: string: k == 0 @@ -200,7 +200,7 @@ file_name: pr-758.c file_hash: $FILE_HASH line: 20 - column: 2 + column: 3 function: main location_invariant: string: i == 0 @@ -211,7 +211,7 @@ file_name: pr-758.c file_hash: $FILE_HASH line: 12 - column: 2 + column: 3 function: main location_invariant: string: x == 10 @@ -222,7 +222,7 @@ file_name: pr-758.c file_hash: $FILE_HASH line: 6 - column: 2 + column: 3 function: main location_invariant: string: x == 42