From d8be117080e1f6d0bdc9e8331e888f2d3ac2cf7c Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 15 Apr 2024 11:45:01 +0300 Subject: [PATCH] Update new witness cram tests to PR #1400 --- .../11-unrolled-loop-invariant.t | 32 +++++------ tests/regression/witness/typedef.t/run.t | 54 +++++++++---------- 2 files changed, 43 insertions(+), 43 deletions(-) diff --git a/tests/regression/55-loop-unrolling/11-unrolled-loop-invariant.t b/tests/regression/55-loop-unrolling/11-unrolled-loop-invariant.t index b3cdedcf49..32ec663717 100644 --- a/tests/regression/55-loop-unrolling/11-unrolled-loop-invariant.t +++ b/tests/regression/55-loop-unrolling/11-unrolled-loop-invariant.t @@ -219,7 +219,7 @@ file_name: 11-unrolled-loop-invariant.c file_hash: $FILE_HASH line: 8 - column: 4 + column: 5 function: main loop_invariant: string: i == 10 @@ -230,7 +230,7 @@ file_name: 11-unrolled-loop-invariant.c file_hash: $FILE_HASH line: 8 - column: 4 + column: 5 function: main loop_invariant: string: (((((((k == 100 && (((j == 2 || (5 <= j && j <= 9)) || j == 1) || j == @@ -244,7 +244,7 @@ file_name: 11-unrolled-loop-invariant.c file_hash: $FILE_HASH line: 7 - column: 2 + column: 3 function: main loop_invariant: string: i == 10 @@ -255,7 +255,7 @@ file_name: 11-unrolled-loop-invariant.c file_hash: $FILE_HASH line: 7 - column: 2 + column: 3 function: main loop_invariant: string: ((k == 100 && (((j == 2 || (5 <= j && j <= 10)) || j == 1) || j == 4)) @@ -267,7 +267,7 @@ file_name: 11-unrolled-loop-invariant.c file_hash: $FILE_HASH line: 3 - column: 2 + column: 3 function: main loop_invariant: string: (((((5 <= i && i <= 10) || i == 4) || i == 3) || i == 2) || i == 1) || @@ -279,7 +279,7 @@ file_name: 11-unrolled-loop-invariant.c file_hash: $FILE_HASH line: 12 - column: 2 + column: 3 function: main location_invariant: string: k == 100 @@ -290,7 +290,7 @@ file_name: 11-unrolled-loop-invariant.c file_hash: $FILE_HASH line: 12 - column: 2 + column: 3 function: main location_invariant: string: j == 10 @@ -301,7 +301,7 @@ file_name: 11-unrolled-loop-invariant.c file_hash: $FILE_HASH line: 12 - column: 2 + column: 3 function: main location_invariant: string: i == 10 @@ -312,7 +312,7 @@ file_name: 11-unrolled-loop-invariant.c file_hash: $FILE_HASH line: 10 - column: 4 + column: 5 function: main location_invariant: string: k == 100 @@ -323,7 +323,7 @@ file_name: 11-unrolled-loop-invariant.c file_hash: $FILE_HASH line: 10 - column: 4 + column: 5 function: main location_invariant: string: i == 10 @@ -334,7 +334,7 @@ file_name: 11-unrolled-loop-invariant.c file_hash: $FILE_HASH line: 10 - column: 4 + column: 5 function: main location_invariant: string: ((((j == 1 || j == 4) || j == 0) || j == 3) || j == 2) || (5 <= j && j @@ -346,7 +346,7 @@ file_name: 11-unrolled-loop-invariant.c file_hash: $FILE_HASH line: 9 - column: 6 + column: 7 function: main location_invariant: string: j == 0 @@ -357,7 +357,7 @@ file_name: 11-unrolled-loop-invariant.c file_hash: $FILE_HASH line: 9 - column: 6 + column: 7 function: main location_invariant: string: i == 10 @@ -368,7 +368,7 @@ file_name: 11-unrolled-loop-invariant.c file_hash: $FILE_HASH line: 9 - column: 6 + column: 7 function: main location_invariant: string: (((((5 <= k && k <= 99) || k == 4) || k == 3) || k == 2) || k == 1) || @@ -380,7 +380,7 @@ file_name: 11-unrolled-loop-invariant.c file_hash: $FILE_HASH line: 6 - column: 2 + column: 3 function: main location_invariant: string: i == 10 @@ -391,7 +391,7 @@ file_name: 11-unrolled-loop-invariant.c file_hash: $FILE_HASH line: 4 - column: 4 + column: 5 function: main location_invariant: string: (((((5 <= i && i <= 9) || i == 4) || i == 3) || i == 2) || i == 1) || diff --git a/tests/regression/witness/typedef.t/run.t b/tests/regression/witness/typedef.t/run.t index b06164743b..55dcc1f911 100644 --- a/tests/regression/witness/typedef.t/run.t +++ b/tests/regression/witness/typedef.t/run.t @@ -12,7 +12,7 @@ file_name: typedef.c file_hash: $FILE_HASH line: 14 - column: 2 + column: 3 function: main location_invariant: string: x == 42 @@ -23,7 +23,7 @@ file_name: typedef.c file_hash: $FILE_HASH line: 14 - column: 2 + column: 3 function: main location_invariant: string: q == (void *)(& a) @@ -34,7 +34,7 @@ file_name: typedef.c file_hash: $FILE_HASH line: 14 - column: 2 + column: 3 function: main location_invariant: string: p == (void *)(& x) @@ -45,7 +45,7 @@ file_name: typedef.c file_hash: $FILE_HASH line: 14 - column: 2 + column: 3 function: main location_invariant: string: a.f == 43 @@ -56,7 +56,7 @@ file_name: typedef.c file_hash: $FILE_HASH line: 14 - column: 2 + column: 3 function: main location_invariant: string: '*((int *)p) == 42' @@ -67,7 +67,7 @@ file_name: typedef.c file_hash: $FILE_HASH line: 13 - column: 2 + column: 3 function: main location_invariant: string: x == 42 @@ -78,7 +78,7 @@ file_name: typedef.c file_hash: $FILE_HASH line: 13 - column: 2 + column: 3 function: main location_invariant: string: p == (void *)(& x) @@ -89,7 +89,7 @@ file_name: typedef.c file_hash: $FILE_HASH line: 13 - column: 2 + column: 3 function: main location_invariant: string: a.f == 43 @@ -100,7 +100,7 @@ file_name: typedef.c file_hash: $FILE_HASH line: 13 - column: 2 + column: 3 function: main location_invariant: string: '*((int *)p) == 42' @@ -111,7 +111,7 @@ file_name: typedef.c file_hash: $FILE_HASH line: 12 - column: 2 + column: 3 function: main location_invariant: string: x == 42 @@ -122,7 +122,7 @@ file_name: typedef.c file_hash: $FILE_HASH line: 12 - column: 2 + column: 3 function: main location_invariant: string: p == (void *)(& x) @@ -133,7 +133,7 @@ file_name: typedef.c file_hash: $FILE_HASH line: 12 - column: 2 + column: 3 function: main location_invariant: string: '*((int *)p) == 42' @@ -144,7 +144,7 @@ file_name: typedef.c file_hash: $FILE_HASH line: 9 - column: 2 + column: 3 function: main location_invariant: string: x == 42 @@ -165,7 +165,7 @@ file_name: typedef.c file_hash: $FILE_HASH line: 14 - column: 2 + column: 3 function: main location_invariant: string: x == 42 @@ -176,7 +176,7 @@ file_name: typedef.c file_hash: $FILE_HASH line: 14 - column: 2 + column: 3 function: main location_invariant: string: q == (void *)(& a) @@ -187,7 +187,7 @@ file_name: typedef.c file_hash: $FILE_HASH line: 14 - column: 2 + column: 3 function: main location_invariant: string: p == (void *)(& x) @@ -198,7 +198,7 @@ file_name: typedef.c file_hash: $FILE_HASH line: 14 - column: 2 + column: 3 function: main location_invariant: string: a.f == 43 @@ -209,7 +209,7 @@ file_name: typedef.c file_hash: $FILE_HASH line: 14 - column: 2 + column: 3 function: main location_invariant: string: '*((myint *)p) == 42' @@ -220,7 +220,7 @@ file_name: typedef.c file_hash: $FILE_HASH line: 14 - column: 2 + column: 3 function: main location_invariant: string: ((s *)q)->f == 43 @@ -231,7 +231,7 @@ file_name: typedef.c file_hash: $FILE_HASH line: 13 - column: 2 + column: 3 function: main location_invariant: string: x == 42 @@ -242,7 +242,7 @@ file_name: typedef.c file_hash: $FILE_HASH line: 13 - column: 2 + column: 3 function: main location_invariant: string: p == (void *)(& x) @@ -253,7 +253,7 @@ file_name: typedef.c file_hash: $FILE_HASH line: 13 - column: 2 + column: 3 function: main location_invariant: string: a.f == 43 @@ -264,7 +264,7 @@ file_name: typedef.c file_hash: $FILE_HASH line: 13 - column: 2 + column: 3 function: main location_invariant: string: '*((myint *)p) == 42' @@ -275,7 +275,7 @@ file_name: typedef.c file_hash: $FILE_HASH line: 12 - column: 2 + column: 3 function: main location_invariant: string: x == 42 @@ -286,7 +286,7 @@ file_name: typedef.c file_hash: $FILE_HASH line: 12 - column: 2 + column: 3 function: main location_invariant: string: p == (void *)(& x) @@ -297,7 +297,7 @@ file_name: typedef.c file_hash: $FILE_HASH line: 12 - column: 2 + column: 3 function: main location_invariant: string: '*((myint *)p) == 42' @@ -308,7 +308,7 @@ file_name: typedef.c file_hash: $FILE_HASH line: 9 - column: 2 + column: 3 function: main location_invariant: string: x == 42