Skip to content

Commit 026738b

Browse files
kroeningkroening
authored
Merge pull request #6251 from diffblue/goto_program_use_format
goto_programt::output_instruction now uses format(...)
2 parents b0b71d0 + 75a16c7 commit 026738b

File tree

174 files changed

+696
-665
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

174 files changed

+696
-665
lines changed

‎jbmc/regression/janalyzer/string-initializer/test.desc‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ Basic1
33
--location-sensitive --constants --show
44
^EXIT=0$
55
^SIGNAL=0$
6-
Hello_20 = \{ \.@class_identifier="java::java\.lang\.String" \};
6+
Hello_20 := \{ "java::java\.lang\.String" \}
77
java::java\.lang\.String\.Literal\.Hello_20=\{ \.@class_identifier="java::java\.lang\.String" \}
88
--
99
^warning: ignoring

‎jbmc/regression/jbmc/JumpSimplification/test.desc‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ Test
44
activate-multi-line-match
55
^EXIT=0$
66
^SIGNAL=0$
7-
IF \w* <= 0 THEN GOTO 1\n\s*//.*\n\s*//.*\n\s*\w*::
7+
IF .* ≤ 0 THEN GOTO 1\n\s*//.*\n\s*//.*\n\s*ASSIGN
88
--
9-
IF !\(\w* <= 0\) THEN GOTO 1\n\s*//.*\n.*GOTO 2\n\s*//.*\n\s*//.*\n\s*1: \w*::
9+
IF ¬\(.* ≤ 0\) THEN GOTO 1\n\s*//.*\n.*GOTO 2\n\s*//.*\n\s*//.*\n\s*1: \w*::
1010
^warning: ignoring

‎jbmc/regression/jbmc/LocalVarTable5/test.desc‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,10 @@
11
CORE
22
test
33
--show-goto-functions --function test.main
4-
dead anonlocal::1i
5-
dead anonlocal::2i
6-
dead anonlocal::3a
7-
dead new_tmp[0-9]+
4+
DEAD .*::anonlocal::1i
5+
DEAD .*::anonlocal::2i
6+
DEAD .*::anonlocal::3a
7+
DEAD .*::new_tmp[0-9]+
88
^EXIT=0$
99
^SIGNAL=0$
1010
--

‎jbmc/regression/jbmc/clinit-lifting2/test-goto-functions.desc‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ Test
44
activate-multi-line-match
55
^EXIT=0$
66
^SIGNAL=0$
7-
\s*// 0 no location\n\s*Other\.<clinit_wrapper>\(\);\s*// 1 no location\s*int total;
7+
\s*// 0 no location\n\s*CALL java::Other\.<clinit_wrapper>\(\)\s*// 1 no location\s*DECL .*::total
88
--
99
--
1010
This checks that the clinit-wrapper function is called once, even though there are two calls in the source

‎jbmc/regression/jbmc/clinit-lifting3/test-goto-functions.desc‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ Test
44
activate-multi-line-match
55
^EXIT=0$
66
^SIGNAL=0$
7-
\s*// 0 no location\n\s*Other\.<clinit_wrapper>\(\);\s*// 1 no location\s*Third\.<clinit_wrapper>\(\);\s*// 2 no location\s*int total;
7+
\s*// 0 no location\n\s*CALL java::Other\.<clinit_wrapper>\(\)\s*// 1 no location\s*CALL java::Third\.<clinit_wrapper>\(\)\s*// 2 no location\s*DECL .*::total
88
--
99
--
1010
This checks that the clinit-wrapper function is called once, even though there are two calls in the source

‎jbmc/regression/jbmc/destructor1/test.desc‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,6 @@ Break
33
--show-goto-functions --function Break.main
44
^EXIT=0$
55
^SIGNAL=0$
6-
dead i;
6+
DEAD .*::i
77
--
88
GOTO 11

‎jbmc/regression/jbmc/destructors/block.desc‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -2,19 +2,19 @@ CORE
22
DestructorStackTests
33
--show-goto-functions --function DestructorStackTests.mainTest --unwind 10
44
activate-multi-line-match
5-
[0-9]+: dead strings;[\s]*(?P<comment_block>(\/\/ [0-9]+ file DestructorStackTests\.java line 42 function java::DestructorStackTests\.mainTest:\(Z\)V bytecode-index 90)|(\/\/ [0-9]+ no location))[\s]*dead minor1;[\s]*(?P>comment_block)[\s]*dead anonlocal::[0-9a-zA-Z]+;[\s]*(?P>comment_block)[\s]*[0-9]+: END_FUNCTION
5+
[0-9]+: DEAD .*::strings[\s]*(?P<comment_block>(\/\/ [0-9]+ file DestructorStackTests\.java line 42 function java::DestructorStackTests\.mainTest:\(Z\)V bytecode-index 90)|(\/\/ [0-9]+ no location))[\s]*DEAD .*::minor1[\s]*(?P>comment_block)[\s]*DEAD .*::anonlocal::[0-9a-zA-Z]+[\s]*(?P>comment_block)[\s]*[0-9]+: END_FUNCTION
66
^EXIT=0$
77
^SIGNAL=0$
88
--
99
--
1010
Checks for:
1111

1212
// Labels: pc187
13-
12: dead strings;
13+
12: DEAD strings
1414
// 250 file DestructorStackTests.java line 42 function java::DestructorStackTests.mainTest:(Z)V bytecode-index 90
15-
dead minor1;
15+
DEAD minor1
1616
// 251 file DestructorStackTests.java line 42 function java::DestructorStackTests.mainTest:(Z)V bytecode-index 90
17-
dead anonlocal::4a;
17+
DEAD anonlocal::4a
1818
// 252 no location
1919
13: END_FUNCTION
2020

‎jbmc/regression/jbmc/destructors/break.desc‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -2,19 +2,19 @@ CORE
22
DestructorStackTests
33
--show-goto-functions --function DestructorStackTests.mainTest --unwind 10
44
activate-multi-line-match
5-
(?P<comment_block>\/\/ [0-9]+ file DestructorStackTests\.java line 34 function java::DestructorStackTests\.mainTest:\(Z\)V bytecode-index 84)[\s]*dead throwaway;[\s]*(?P>comment_block)[\s]*dead new_tmp[0-9]+;[\s]*(?P>comment_block)[\s]*dead val;[\s]*(?P>comment_block)[\s]*GOTO [0-9]+
5+
(?P<comment_block>\/\/ [0-9]+ file DestructorStackTests\.java line 34 function java::DestructorStackTests\.mainTest:\(Z\)V bytecode-index 84)[\s]*DEAD .*::throwaway[\s]*(?P>comment_block)[\s]*DEAD .*::new_tmp[0-9]+[\s]*(?P>comment_block)[\s]*DEAD .*::val[\s]*(?P>comment_block)[\s]*GOTO [0-9]+
66
^EXIT=0$
77
^SIGNAL=0$
88
--
99
--
1010
Checks for:
1111

1212
// 228 file DestructorStackTests.java line 34 function java::DestructorStackTests.mainTest:(Z)V bytecode-index 84
13-
dead throwaway;
13+
DEAD throwaway
1414
// 229 file DestructorStackTests.java line 34 function java::DestructorStackTests.mainTest:(Z)V bytecode-index 84
15-
dead new_tmp16;
15+
DEAD new_tmp16
1616
// 230 file DestructorStackTests.java line 34 function java::DestructorStackTests.mainTest:(Z)V bytecode-index 84
17-
dead val;
17+
DEAD val
1818
// 231 file DestructorStackTests.java line 34 function java::DestructorStackTests.mainTest:(Z)V bytecode-index 84
1919
GOTO 12
2020

‎jbmc/regression/jbmc/destructors/continue.desc‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -2,19 +2,19 @@ CORE
22
DestructorStackTests
33
--show-goto-functions --function DestructorStackTests.mainTest --unwind 10
44
activate-multi-line-match
5-
(?P<comment_block>\/\/ [0-9]+ file DestructorStackTests\.java line 39 function java::DestructorStackTests\.mainTest:\(Z\)V bytecode-index 89)[\s]*dead throwaway;[\s]*(?P>comment_block)[\s]*dead new_tmp[0-9]+;[\s]*(?P>comment_block)[\s]*dead val;[\s]*(?P>comment_block)[\s]*GOTO [0-9]+
5+
(?P<comment_block>\/\/ [0-9]+ file DestructorStackTests\.java line 39 function java::DestructorStackTests\.mainTest:\(Z\)V bytecode-index 89)[\s]*DEAD .*::throwaway[\s]*(?P>comment_block)[\s]*DEAD .*::new_tmp[0-9]+[\s]*(?P>comment_block)[\s]*DEAD .*::val[\s]*(?P>comment_block)[\s]*GOTO [0-9]+
66
^EXIT=0$
77
^SIGNAL=0$
88
--
99
--
1010
Checks for:
1111

1212
// 242 file DestructorStackTests.java line 39 function java::DestructorStackTests.mainTest:(Z)V bytecode-index 89
13-
dead throwaway;
13+
DEAD throwaway
1414
// 243 file DestructorStackTests.java line 39 function java::DestructorStackTests.mainTest:(Z)V bytecode-index 89
15-
dead new_tmp17;
15+
DEAD new_tmp17
1616
// 244 file DestructorStackTests.java line 39 function java::DestructorStackTests.mainTest:(Z)V bytecode-index 89
17-
dead val;
17+
DEAD val
1818
// 245 file DestructorStackTests.java line 39 function java::DestructorStackTests.mainTest:(Z)V bytecode-index 89
1919
GOTO 3
2020

‎jbmc/regression/jbmc/destructors/decl.desc‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -2,20 +2,20 @@ CORE
22
DestructorStackTests
33
--show-goto-functions --function DestructorStackTests.mainTest --unwind 10
44
activate-multi-line-match
5-
IF !\(\(int\)unknown == 0\) THEN GOTO [0-9]+[\s]*(?P<comment_block>\/\/ [0-9]+ file DestructorStackTests\.java line 24 function java::DestructorStackTests\.mainTest:\(Z\)V bytecode-index 50)[\s]*dead new_tmp[0-9]+;[\s]*(?P>comment_block)[\s]*GOTO [0-9]+[\s]*\/\/ [0-9]+ no location[\s]*[0-9]+: dead new_tmp[0-9]+;[\s]*
5+
IF ¬\(.*unknown.* = 0\) THEN GOTO [0-9]+[\s]*(?P<comment_block>\/\/ [0-9]+ file DestructorStackTests\.java line 24 function java::DestructorStackTests\.mainTest:\(Z\)V bytecode-index 50)[\s]*DEAD .*::new_tmp[0-9]+[\s]*(?P>comment_block)[\s]*GOTO [0-9]+[\s]*\/\/ [0-9]+ no location[\s]*[0-9]+: DEAD .*::new_tmp[0-9]+[\s]*
66
^EXIT=0$
77
^SIGNAL=0$
88
--
99
--
1010
Checks for:
1111

12-
IF !((int)unknown == 0) THEN GOTO 1
12+
IF ¬(cast(java::DestructorStackTests.mainTest:(Z)V::unknown, signedbv[32]) = 0) THEN GOTO 1
1313
// 44 file DestructorStackTests.java line 24 function java::DestructorStackTests.mainTest:(Z)V bytecode-index 50
14-
dead new_tmp0;
14+
DEAD java::DestructorStackTests.mainTest:(Z)V::new_tmp0
1515
// 45 file DestructorStackTests.java line 24 function java::DestructorStackTests.mainTest:(Z)V bytecode-index 50
1616
GOTO 2
1717
// 46 no location
18-
1: dead new_tmp0;
18+
1: DEAD java::DestructorStackTests.mainTest:(Z)V::new_tmp0
1919

2020
Tests to make sure a declaration kills its temp variable before continuing.
2121
Numbers vary between symex load / normal load.

0 commit comments

Comments
 (0)