Skip to content

Commit 466ac7a

Browse files
committed
Loosening regex on phi merge zero generation regression tests
The tests that should have caught this were too specific when checking for the names of the variables and at some point in the past dynamic_object got given a prefix, which meant that the check to make sure no zero generation existed always passed (even with a #0 there) because the variable name wasn't exact. Made the matching far more forgiving and it now looks for anything that vaguely looks like a guard statement with a 0 generation object.
1 parent eca9b59 commit 466ac7a

File tree

7 files changed

+14
-14
lines changed

7 files changed

+14
-14
lines changed

jbmc/regression/jbmc/phi-merge_uninitialized_values/field.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -5,8 +5,8 @@ activate-multi-line-match
55
^EXIT=0$
66
^SIGNAL=0$
77
--
8-
^.*:\s+(dynamic_object|new_tmp)[0-9]+(@[0-9]+)?#0\)
9-
^.*\?\s+(dynamic_object|new_tmp)[0-9]+(@[0-9]+)?#0\s+:
8+
\([^\s]+guard[^\s]+ \? [^\s]+#0 : [^\s]+\)
9+
\([^\s]+guard[^\s]+ \? [^\s]+ : [^\s]+#0\)
1010
--
1111
These regexes are making sure that a variable of generation 0 dosen't appear in a phi merge, so the below
1212
statement:

jbmc/regression/jbmc/phi-merge_uninitialized_values/local.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -5,8 +5,8 @@ activate-multi-line-match
55
^EXIT=0$
66
^SIGNAL=0$
77
--
8-
^.*:\s+(dynamic_object|new_tmp)[0-9]+(@[0-9]+)?#0\)
9-
^.*\?\s+(dynamic_object|new_tmp)[0-9]+(@[0-9]+)?#0\s+:
8+
\([^\s]+guard[^\s]+ \? [^\s]+#0 : [^\s]+\)
9+
\([^\s]+guard[^\s]+ \? [^\s]+ : [^\s]+#0\)
1010
--
1111
These regexes are making sure that a variable of generation 0 dosen't appear in a phi merge, so the below
1212
statement:

jbmc/regression/jbmc/phi-merge_uninitialized_values/static_field.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -5,8 +5,8 @@ activate-multi-line-match
55
^EXIT=0$
66
^SIGNAL=0$
77
--
8-
^.*:\s+(dynamic_object|new_tmp)[0-9]+(@[0-9]+)?#0\)
9-
^.*\?\s+(dynamic_object|new_tmp)[0-9]+(@[0-9]+)?#0\s+:
8+
\([^\s]+guard[^\s]+ \? [^\s]+#0 : [^\s]+\)
9+
\([^\s]+guard[^\s]+ \? [^\s]+ : [^\s]+#0\)
1010
--
1111
These regexes are making sure that a variable of generation 0 dosen't appear in a phi merge, so the below
1212
statement:

regression/cbmc/phi-merge_uninitialized_values/dynamic.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -5,8 +5,8 @@ activate-multi-line-match
55
^EXIT=0$
66
^SIGNAL=0$
77
--
8-
^.*:\s+dynamic_object[0-9]+(@[0-9]+)?#0\)
9-
^.*\?\s+dynamic_object[0-9]+(@[0-9]+)?#0\s+:
8+
\([^\s]+guard[^\s]+ \? [^\s]+#0 : [^\s]+\)
9+
\([^\s]+guard[^\s]+ \? [^\s]+ : [^\s]+#0\)
1010
--
1111
These regexes are making sure that a variable of generation 0 dosen't appear in a phi merge, so the below
1212
statement:

regression/cbmc/phi-merge_uninitialized_values/global.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -5,8 +5,8 @@ activate-multi-line-match
55
^EXIT=0$
66
^SIGNAL=0$
77
--
8-
^.*:\s+global(@[0-9]+)?#0\)
9-
^.*\?\s+global(@[0-9]+)?#0\s+:
8+
\([^\s]+guard[^\s]+ \? [^\s]+#0 : [^\s]+\)
9+
\([^\s]+guard[^\s]+ \? [^\s]+ : [^\s]+#0\)
1010
--
1111
These regexes are making sure that a variable of generation 0 dosen't appear in a phi merge, so the below
1212
statement:

regression/cbmc/phi-merge_uninitialized_values/local.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -5,8 +5,8 @@ activate-multi-line-match
55
^EXIT=0$
66
^SIGNAL=0$
77
--
8-
^.*:\s+local(@[0-9]+)?#0\)
9-
^.*\?\s+local(@[0-9]+)?#0\s+:
8+
\([^\s]+guard[^\s]+ \? [^\s]+#0 : [^\s]+\)
9+
\([^\s]+guard[^\s]+ \? [^\s]+ : [^\s]+#0\)
1010
--
1111
These regexes are making sure that a variable of generation 0 dosen't appear in a phi merge, so the below
1212
statement:

regression/cbmc/phi-merge_uninitialized_values/static_local.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -5,8 +5,8 @@ activate-multi-line-match
55
^EXIT=0$
66
^SIGNAL=0$
77
--
8-
^.*:\s+staticLocal(@[0-9]+)?#0\)
9-
^.*\?\s+staticLocal(@[0-9]+)?#0\s+:
8+
\([^\s]+guard[^\s]+ \? [^\s]+#0 : [^\s]+\)
9+
\([^\s]+guard[^\s]+ \? [^\s]+ : [^\s]+#0\)
1010
--
1111
These regexes are making sure that a variable of generation 0 dosen't appear in a phi merge, so the below
1212
statement:

0 commit comments

Comments
 (0)