File tree 7 files changed +14
-14
lines changed
jbmc/regression/jbmc/phi-merge_uninitialized_values
regression/cbmc/phi-merge_uninitialized_values
7 files changed +14
-14
lines changed Original file line number Diff line number Diff line change @@ -5,8 +5,8 @@ activate-multi-line-match
5
5
^EXIT=0$
6
6
^SIGNAL=0$
7
7
--
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\)
10
10
--
11
11
These regexes are making sure that a variable of generation 0 dosen't appear in a phi merge, so the below
12
12
statement:
Original file line number Diff line number Diff line change @@ -5,8 +5,8 @@ activate-multi-line-match
5
5
^EXIT=0$
6
6
^SIGNAL=0$
7
7
--
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\)
10
10
--
11
11
These regexes are making sure that a variable of generation 0 dosen't appear in a phi merge, so the below
12
12
statement:
Original file line number Diff line number Diff line change @@ -5,8 +5,8 @@ activate-multi-line-match
5
5
^EXIT=0$
6
6
^SIGNAL=0$
7
7
--
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\)
10
10
--
11
11
These regexes are making sure that a variable of generation 0 dosen't appear in a phi merge, so the below
12
12
statement:
Original file line number Diff line number Diff line change @@ -5,8 +5,8 @@ activate-multi-line-match
5
5
^EXIT=0$
6
6
^SIGNAL=0$
7
7
--
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]+#0 : [^\s]+\)
10
10
--
11
11
These regexes are making sure that a variable of generation 0 dosen't appear in a phi merge, so the below
12
12
statement:
Original file line number Diff line number Diff line change @@ -5,8 +5,8 @@ activate-multi-line-match
5
5
^EXIT=0$
6
6
^SIGNAL=0$
7
7
--
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]+#0 : [^\s]+\)
10
10
--
11
11
These regexes are making sure that a variable of generation 0 dosen't appear in a phi merge, so the below
12
12
statement:
Original file line number Diff line number Diff line change @@ -5,8 +5,8 @@ activate-multi-line-match
5
5
^EXIT=0$
6
6
^SIGNAL=0$
7
7
--
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]+#0 : [^\s]+\)
10
10
--
11
11
These regexes are making sure that a variable of generation 0 dosen't appear in a phi merge, so the below
12
12
statement:
Original file line number Diff line number Diff line change @@ -5,8 +5,8 @@ activate-multi-line-match
5
5
^EXIT=0$
6
6
^SIGNAL=0$
7
7
--
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]+#0 : [^\s]+\)
10
10
--
11
11
These regexes are making sure that a variable of generation 0 dosen't appear in a phi merge, so the below
12
12
statement:
You can’t perform that action at this time.
0 commit comments