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.

Author: kroening

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

@@ -3,7 +3,7 @@ Basic1
 --location-sensitive --constants --show
 ^EXIT=0$
 ^SIGNAL=0$
-Hello_20 = \{ \.@class_identifier="java::java\.lang\.String" \};
+Hello_20 := \{ "java::java\.lang\.String" \}
 java::java\.lang\.String\.Literal\.Hello_20=\{ \.@class_identifier="java::java\.lang\.String" \}
 --
 ^warning: ignoring

jbmc/regression/jbmc/JumpSimplification/test.desc

@@ -4,7 +4,7 @@ Test
 activate-multi-line-match
 ^EXIT=0$
 ^SIGNAL=0$
-IF \w* <= 0 THEN GOTO 1\n\s*//.*\n\s*//.*\n\s*\w*::
+IF .* ≤ 0 THEN GOTO 1\n\s*//.*\n\s*//.*\n\s*ASSIGN
 --
-IF !\(\w* <= 0\) THEN GOTO 1\n\s*//.*\n.*GOTO 2\n\s*//.*\n\s*//.*\n\s*1: \w*::
+IF ¬\(.* ≤ 0\) THEN GOTO 1\n\s*//.*\n.*GOTO 2\n\s*//.*\n\s*//.*\n\s*1: \w*::
 ^warning: ignoring

jbmc/regression/jbmc/LocalVarTable5/test.desc

@@ -1,10 +1,10 @@
 CORE
 test
 --show-goto-functions --function test.main
-dead anonlocal::1i
-dead anonlocal::2i
-dead anonlocal::3a
-dead new_tmp[0-9]+
+DEAD .*::anonlocal::1i
+DEAD .*::anonlocal::2i
+DEAD .*::anonlocal::3a
+DEAD .*::new_tmp[0-9]+
 ^EXIT=0$
 ^SIGNAL=0$
 --

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

@@ -4,7 +4,7 @@ Test
 activate-multi-line-match
 ^EXIT=0$
 ^SIGNAL=0$
-\s*// 0 no location\n\s*Other\.<clinit_wrapper>\(\);\s*// 1 no location\s*int total;
+\s*// 0 no location\n\s*CALL java::Other\.<clinit_wrapper>\(\)\s*// 1 no location\s*DECL .*::total
 --
 --
 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

@@ -4,7 +4,7 @@ Test
 activate-multi-line-match
 ^EXIT=0$
 ^SIGNAL=0$
-\s*// 0 no location\n\s*Other\.<clinit_wrapper>\(\);\s*// 1 no location\s*Third\.<clinit_wrapper>\(\);\s*// 2 no location\s*int total;
+\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
 --
 --
 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

@@ -3,6 +3,6 @@ Break
 --show-goto-functions --function Break.main
 ^EXIT=0$
 ^SIGNAL=0$
-dead i;
+DEAD .*::i
 --
 GOTO 11

jbmc/regression/jbmc/destructors/block.desc

@@ -2,19 +2,19 @@ CORE
 DestructorStackTests
 --show-goto-functions --function DestructorStackTests.mainTest --unwind 10
 activate-multi-line-match
-[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
+[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
 ^EXIT=0$
 ^SIGNAL=0$
 --
 --
 Checks for:
 
            // Labels: pc187
-       12: dead strings;
+       12: DEAD strings
            // 250 file DestructorStackTests.java line 42 function java::DestructorStackTests.mainTest:(Z)V bytecode-index 90
-           dead minor1;
+           DEAD minor1
            // 251 file DestructorStackTests.java line 42 function java::DestructorStackTests.mainTest:(Z)V bytecode-index 90
-           dead anonlocal::4a;
+           DEAD anonlocal::4a
            // 252 no location
        13: END_FUNCTION
 

jbmc/regression/jbmc/destructors/break.desc

@@ -2,19 +2,19 @@ CORE
 DestructorStackTests
 --show-goto-functions --function DestructorStackTests.mainTest --unwind 10
 activate-multi-line-match
-(?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]+
+(?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]+
 ^EXIT=0$
 ^SIGNAL=0$
 --
 --
 Checks for:
 
         // 228 file DestructorStackTests.java line 34 function java::DestructorStackTests.mainTest:(Z)V bytecode-index 84
-        dead throwaway;
+        DEAD throwaway
         // 229 file DestructorStackTests.java line 34 function java::DestructorStackTests.mainTest:(Z)V bytecode-index 84
-        dead new_tmp16;
+        DEAD new_tmp16
         // 230 file DestructorStackTests.java line 34 function java::DestructorStackTests.mainTest:(Z)V bytecode-index 84
-        dead val;
+        DEAD val
         // 231 file DestructorStackTests.java line 34 function java::DestructorStackTests.mainTest:(Z)V bytecode-index 84
         GOTO 12
 

jbmc/regression/jbmc/destructors/continue.desc

@@ -2,19 +2,19 @@ CORE
 DestructorStackTests
 --show-goto-functions --function DestructorStackTests.mainTest --unwind 10
 activate-multi-line-match
-(?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]+
+(?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]+
 ^EXIT=0$
 ^SIGNAL=0$
 --
 --
 Checks for:
 
         // 242 file DestructorStackTests.java line 39 function java::DestructorStackTests.mainTest:(Z)V bytecode-index 89
-        dead throwaway;
+        DEAD throwaway
         // 243 file DestructorStackTests.java line 39 function java::DestructorStackTests.mainTest:(Z)V bytecode-index 89
-        dead new_tmp17;
+        DEAD new_tmp17
         // 244 file DestructorStackTests.java line 39 function java::DestructorStackTests.mainTest:(Z)V bytecode-index 89
-        dead val;
+        DEAD val
         // 245 file DestructorStackTests.java line 39 function java::DestructorStackTests.mainTest:(Z)V bytecode-index 89
         GOTO 3
 

jbmc/regression/jbmc/destructors/decl.desc

@@ -2,20 +2,20 @@ CORE
 DestructorStackTests
 --show-goto-functions --function DestructorStackTests.mainTest --unwind 10
 activate-multi-line-match
-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]*
+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]*
 ^EXIT=0$
 ^SIGNAL=0$
 --
 --
 Checks for:
 
-        IF !((int)unknown == 0) THEN GOTO 1
+        IF ¬(cast(java::DestructorStackTests.mainTest:(Z)V::unknown, signedbv[32]) = 0) THEN GOTO 1
         // 44 file DestructorStackTests.java line 24 function java::DestructorStackTests.mainTest:(Z)V bytecode-index 50
-        dead new_tmp0;
+        DEAD java::DestructorStackTests.mainTest:(Z)V::new_tmp0
         // 45 file DestructorStackTests.java line 24 function java::DestructorStackTests.mainTest:(Z)V bytecode-index 50
         GOTO 2
         // 46 no location
-     1: dead new_tmp0;
+     1: DEAD java::DestructorStackTests.mainTest:(Z)V::new_tmp0
 
 Tests to make sure a declaration kills its temp variable before continuing.
 Numbers vary between symex load / normal load.

jbmc/regression/jbmc/destructors/return.desc

@@ -2,29 +2,29 @@ CORE
 DestructorStackTests
 --show-goto-functions --function DestructorStackTests.mainTest --unwind 10
 activate-multi-line-match
-(?<comment_block>\/\/ [0-9]+ file DestructorStackTests\.java line 18 function java::DestructorStackTests.mainTest:\(Z\)V bytecode-index 40)[\s]*dead minor[0-9]+;[\s]*(?P>comment_block)[\s]*dead new_tmp[0-9]+;[\s]*(?P>comment_block)[\s]*dead anonlocal::[0-9a-zA-Z]+;[\s]*(?P>comment_block)[\s]*dead new_tmp[0-9]+;[\s]*(?P>comment_block)[\s]*dead ex;[\s]*(?P>comment_block)[\s]*dead minor2;[\s]*(?P>comment_block)[\s]*dead minor1;[\s]*(?P>comment_block)[\s]*dead anonlocal::[0-9a-zA-Z]+;[\s]*(?P>comment_block)[\s]*GOTO [0-9]+
+(?<comment_block>\/\/ [0-9]+ file DestructorStackTests\.java line 18 function java::DestructorStackTests.mainTest:\(Z\)V bytecode-index 40)[\s]*DEAD .*::minor[0-9]+[\s]*(?P>comment_block)[\s]*DEAD .*::new_tmp[0-9]+[\s]*(?P>comment_block)[\s]*DEAD .*anonlocal::[0-9a-zA-Z]+[\s]*(?P>comment_block)[\s]*DEAD .*::new_tmp[0-9]+[\s]*(?P>comment_block)[\s]*DEAD .*::ex[\s]*(?P>comment_block)[\s]*DEAD .*::minor2[\s]*(?P>comment_block)[\s]*DEAD .*::minor1[\s]*(?P>comment_block)[\s]*DEAD .*::anonlocal::[0-9a-zA-Z]+[\s]*(?P>comment_block)[\s]*GOTO [0-9]+
 ^EXIT=0$
 ^SIGNAL=0$
 --
 --
 Checks for:
 
         // 98 file DestructorStackTests.java line 18 function java::DestructorStackTests.mainTest:(Z)V bytecode-index 40
-        dead minor5;
+        DEAD minor5
         // 99 file DestructorStackTests.java line 18 function java::DestructorStackTests.mainTest:(Z)V bytecode-index 40
-        dead new_tmp6;
+        DEAD new_tmp6
         // 100 file DestructorStackTests.java line 18 function java::DestructorStackTests.mainTest:(Z)V bytecode-index 40
-        dead anonlocal::6a;
+        DEAD anonlocal::6a
         // 101 file DestructorStackTests.java line 18 function java::DestructorStackTests.mainTest:(Z)V bytecode-index 40
-        dead new_tmp5;
+        DEAD new_tmp5
         // 102 file DestructorStackTests.java line 18 function java::DestructorStackTests.mainTest:(Z)V bytecode-index 40
-        dead ex;
+        DEAD ex
         // 103 file DestructorStackTests.java line 18 function java::DestructorStackTests.mainTest:(Z)V bytecode-index 40
-        dead minor2;
+        DEAD minor2
         // 104 file DestructorStackTests.java line 18 function java::DestructorStackTests.mainTest:(Z)V bytecode-index 40
-        dead minor1;
+        DEAD minor1
         // 105 file DestructorStackTests.java line 18 function java::DestructorStackTests.mainTest:(Z)V bytecode-index 40
-        dead anonlocal::4a;
+        DEAD anonlocal::4a
         // 106 file DestructorStackTests.java line 18 function java::DestructorStackTests.mainTest:(Z)V bytecode-index 40
         GOTO 13
 

jbmc/regression/jbmc/generic_base_type/check_casts.desc

@@ -3,8 +3,8 @@ Test
 --function Test.main --show-goto-functions
 ^EXIT=0$
 ^SIGNAL=0$
-this \. Test\.callee:\(LBase;\)V\(\(struct Base \*\)&return_tmp0->@Base\);
-this \. Test\.callee2:\(LBase;\)V\(&return_tmp1->@Base\);
+CALL java::Test\.callee:\(LBase;\)V\(.*::this, cast\(address_of\(\*java::Test\.main:\(Z\)V::return_tmp0\.@Base\), struct java::Base\*\)\)
+CALL java::Test\.callee2:\(LBase;\)V\(.*::this, address_of\(\*java::Test\.main:\(Z\)V::return_tmp1\.@Base\)\)
 --
 callee has a qualified Base type, and so requires a cast.
 callee2 has the unqualified type that Test<T> naturally inherits, so no cast is required.

jbmc/regression/jbmc/generic_function_parameter/callee2_with_cast.desc

@@ -3,7 +3,7 @@ Test
 --function Test.main2 --show-goto-functions
 ^EXIT=0$
 ^SIGNAL=0$
-this \. Test.callee2:\(LTest;\)V\(\(struct Test \*\)param\);
+java::Test.callee2:\(LTest;\)V\(.*::this, cast\(java::Test\.main2:\(LTest;\)V::param, struct java::Test\*\)\)
 --
 --
 Test and callee2 have differing parameter types, so there should be a cast at the callsite.

jbmc/regression/jbmc/generic_function_parameter/callee_without_cast.desc

@@ -3,7 +3,7 @@ Test
 --function Test.main --show-goto-functions
 ^EXIT=0$
 ^SIGNAL=0$
-this \. Test.callee:\(LTest;\)V\(param\);
+Test.callee:\(LTest;\)V\(.*::this, .*::param\)
 --
 --
 Test and callee have matching parameter types, so there should be no cast at the callsite.

jbmc/regression/jbmc/generic_static_field/test.desc

@@ -3,7 +3,7 @@ Test
 --function Test.test --validate-goto-model --show-goto-functions
 ^EXIT=0$
 ^SIGNAL=0$
-Test\.test:\(\)LTest;#return_value = static_field;
+ASSIGN java::Test\.test:\(\)LTest;#return_value := java::Test\.static_field$
 --
 ^warning: ignoring
 --

jbmc/regression/jbmc/generic_virtual_function/check_casts.desc

@@ -3,10 +3,10 @@ Base
 --function Base.main --show-goto-functions
 ^EXIT=0$
 ^SIGNAL=0$
-\(struct Impl1 \*\)b \. Impl1\.f:\(Ljava/lang/Object;\)V\(\(struct java\.lang\.Object \*\)this->genericData\);
-\(struct Impl2 \*\)b \. Impl2\.f:\(Ljava/lang/Object;\)V\(\(struct java\.lang\.Object \*\)this->genericData\);
-\(struct Impl2 \*\)b \. Impl2\.g:\(Ljava/lang/String;\)V\(this->nonGenericData\);
-\(struct Impl1 \*\)b \. Impl1\.g:\(Ljava/lang/String;\)V\(this->nonGenericData\);
+CALL java::Impl1\.f:\(Ljava/lang/Object;\)V\(cast\(.*::b, struct java::Impl1\*\), cast\(\*.*\.genericData, struct java::java\.lang\.Object\*\)\)
+CALL java::Impl2\.f:\(Ljava/lang/Object;\)V\(cast\(.*::b, struct java::Impl2\*\), cast\(\*.*\.genericData, struct java::java\.lang\.Object\*\)\)
+CALL java::Impl2\.g:\(Ljava/lang/String;\)V\(cast\(.*::b, struct java::Impl2\*\), \*.*\.nonGenericData\)
+CALL java::Impl1\.g:\(Ljava/lang/String;\)V\(cast\(.*::b, struct java::Impl1\*\), \*.*\.nonGenericData\)
 --
 --
 Both the implementation classes use a different generic token (Impl1::T and Impl2::T) to refer

jbmc/regression/jbmc/lazyloading_no_candidates/test.desc

@@ -4,7 +4,7 @@ Test
 ^EXIT=0$
 ^SIGNAL=0$
 ^CI lazy methods: elaborate java::Test\$intf\.f:\(\)V$
-Test\$intf\.f:\(\)V\(\);$
+Test\$intf\.f:\(\)V\(.*\)$
 --
 --
 This doesn't work under symex-driven lazy loading because it is incompatible with lazy-methods (default)

jbmc/regression/jbmc/reachability-slice/test.desc

@@ -3,11 +3,11 @@ A
 --reachability-slice --function A.foo --show-goto-functions --property 'java::A.foo:(I)V.assertion.1'
 ^EXIT=0$
 ^SIGNAL=0$
-= \(int\)\(short\)1001
-= \(int\)\(short\)1002
-= \(int\)\(short\)1003
+:= .*1001
+:= .*1002
+:= .*1003
 --
-= \(int\)\(short\)1004
-= \(int\)\(short\)1005
+:= .*1004
+:= .*1005
 --
 Doesn't work with symex-driven lazy loading because the reachability slicer is a whole-program pass.

jbmc/regression/jbmc/reachability-slice/test2.desc

@@ -3,11 +3,11 @@ A
 --reachability-slice --function A.foo --show-goto-functions --property 'java::A.foo:(I)V.assertion.2'
 ^EXIT=0$
 ^SIGNAL=0$
-= \(int\)\(short\)1001
-= \(int\)\(short\)1004
+:= .*1001
+:= .*1004
 --
-= \(int\)\(short\)1002
-= \(int\)\(short\)1003
-= \(int\)\(short\)1005
+:= .*1002
+:= .*1003
+:= .*1005
 --
 Doesn't work with symex-driven lazy loading because the reachability slicer is a whole-program pass.

jbmc/regression/jbmc/reachability-slice/test3.desc

@@ -3,11 +3,11 @@ A
 --reachability-slice --function A.foo --show-goto-functions
 ^EXIT=0$
 ^SIGNAL=0$
-= \(int\)\(short\)1001
-= \(int\)\(short\)1002
-= \(int\)\(short\)1003
-= \(int\)\(short\)1004
-= \(int\)\(short\)1005
+:= .*1001
+:= .*1002
+:= .*1003
+:= .*1004
+:= .*1005
 --
 --
 Doesn't work with symex-driven lazy loading because the reachability slicer is a whole-program pass.

jbmc/regression/jbmc/remove_virtual_function_typecast/test.desc

@@ -1,10 +1,10 @@
 CORE symex-driven-lazy-loading-expected-failure
 VirtualFunctions
 --java-max-vla-length 48 --unwind 8 --java-unwind-enum-static --trace --function VirtualFunctions.check --show-goto-functions
- \(struct VirtualFunctions\$B \*\)a \. VirtualFunctions\$B\.f:\(\)V\(\);$
- a \. VirtualFunctions\$A\.f:\(\)V\(\);$
- b \. VirtualFunctions\$B\.f:\(\)V\(\);$
- \(struct VirtualFunctions\$B \*\)c \. VirtualFunctions\$B\.f:\(\)V\(\);$
+CALL java::VirtualFunctions\$B\.f:\(\)V\(cast\(.*::a, struct java::VirtualFunctions\$B\*\)\)$
+CALL java::VirtualFunctions\$A\.f:\(\)V\(.*::a\)$
+CALL java::VirtualFunctions\$B\.f:\(\)V\(.*::b\)$
+CALL java::VirtualFunctions\$B\.f:\(\)V\(cast\(.*::c, struct java::VirtualFunctions\$B\*\)\)$
 ^EXIT=0$
 ^SIGNAL=0$
 --

jbmc/regression/jbmc/removed_virtual_functions/test.desc

@@ -1,10 +1,10 @@
 CORE symex-driven-lazy-loading-expected-failure
 ArrayListEquals
 --java-max-vla-length 48 --unwind 8 --java-unwind-enum-static --trace --function ArrayListEquals.check2 --show-goto-functions
-e2 . ArrayList\$Itr.hasNext:\(\)Z\(\);
+java::ArrayList\$Itr.hasNext:\(\)Z\(.*\)
 ^EXIT=0$
 ^SIGNAL=0$
 --
-e2 . ListIterator.hasNext:\(\)Z\(\);
+java::ListIterator.hasNext:\(\)Z\(.*\)
 --
 This doesn't work under symex-driven lazy loading because it is incompatible with lazy-methods (default)

jbmc/regression/jbmc/virtual_temp_var_for_this_argument/test_one_candidate.desc

@@ -3,7 +3,7 @@ Main
 --show-goto-functions --function Main.oneCandidate
 ^EXIT=0$
 ^SIGNAL=0$
-B\.f:\(\)V\(\);$
+B\.f:\(\)V\(.*::b\)$
 --
 this_argument
 --

jbmc/regression/jbmc/virtual_temp_var_for_this_argument/test_two_candidates_no_derefs.desc

@@ -3,8 +3,8 @@ Main
 --show-goto-functions --function Main.twoCandidatesNoDerefs
 ^EXIT=0$
 ^SIGNAL=0$
-a \. A\.f:\(\)V\(\);$
-a \. B\.f:\(\)V\(\);$
+CALL java::A\.f:\(\)V\(.*::a\)$
+CALL java::B\.f:\(\)V\(.*::a.*\)$
 --
 this_argument
 --

jbmc/regression/jbmc/virtual_temp_var_for_this_argument/test_two_candidates_with_derefs.desc

@@ -3,10 +3,10 @@ Main
 --show-goto-functions --function Main.twoCandidatesWithDerefs
 ^EXIT=0$
 ^SIGNAL=0$
-struct A \*this_argument;$
-this_argument = aContainer->a_field;$
-this_argument \. A\.f:\(\)V\(\);$
-this_argument \. B\.f:\(\)V\(\);$
+DECL .*::this_argument : struct java::A\*$
+ASSIGN .*::this_argument := \*.*::aContainer\.a_field$
+CALL java::A\.f:\(\)V\(.*this_argument.*\)$
+CALL java::B\.f:\(\)V\(.*this_argument.*\)$
 --
 --
 The temporary variable `this_argument` should be created, because it

regression/cbmc-library/string-abstraction/test-c-with-string-abstraction.desc

@@ -1,7 +1,7 @@
 CORE
 test.c
 --string-abstraction --show-goto-functions
-strlen#return_value = \(.*\)s#str->length - POINTER_OFFSET\(s\)\)*;
+ASSIGN strlen#return_value := cast\(cast\(\*strlen::s::s#str\.length, signedbv\[.*\]\) - pointer_offset\(strlen::s\), unsignedbv\[.*\]\)
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/cbmc-library/string-abstraction/test-c-without-string-abstraction.desc

@@ -1,7 +1,7 @@
 CORE
 test.c
 --show-goto-functions
-IF !\(\(signed int\)s\[\(.*\)len\] != 0\) THEN GOTO 2
+IF ¬\(cast\(\*\(strlen::s \+ cast\(strlen::1::len, signedbv\[.*\]\)\), signedbv\[32\]\) ≠ 0\) THEN GOTO 2
 ^EXIT=0$
 ^SIGNAL=0$
 --