Skip to content

Commit 75a16c7

Browse files
kroeningkroening
committed
goto_programt::output_instruction now uses format(...)
Goto programs are intended as an internal representation that is independent of the specific input programming langauge. This commit switches the debug output for the instructions of goto programs to format(...), which is also designed to be language independent.
1 parent d5c9ef8 commit 75a16c7

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)