goto_programt::output_instruction now uses format(...)

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$
 --