From 75a16c7f53fa7c18d9199c5ce56c295491cefa1a Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sat, 24 Jul 2021 14:04:02 +0100 Subject: [PATCH] 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. --- .../janalyzer/string-initializer/test.desc | 2 +- .../jbmc/JumpSimplification/test.desc | 4 +- jbmc/regression/jbmc/LocalVarTable5/test.desc | 8 +-- .../clinit-lifting2/test-goto-functions.desc | 2 +- .../clinit-lifting3/test-goto-functions.desc | 2 +- jbmc/regression/jbmc/destructor1/test.desc | 2 +- jbmc/regression/jbmc/destructors/block.desc | 8 +-- jbmc/regression/jbmc/destructors/break.desc | 8 +-- .../regression/jbmc/destructors/continue.desc | 8 +-- jbmc/regression/jbmc/destructors/decl.desc | 8 +-- jbmc/regression/jbmc/destructors/return.desc | 18 +++--- .../jbmc/generic_base_type/check_casts.desc | 4 +- .../callee2_with_cast.desc | 2 +- .../callee_without_cast.desc | 2 +- .../jbmc/generic_static_field/test.desc | 2 +- .../generic_virtual_function/check_casts.desc | 8 +-- .../jbmc/lazyloading_no_candidates/test.desc | 2 +- .../jbmc/reachability-slice/test.desc | 10 ++-- .../jbmc/reachability-slice/test2.desc | 10 ++-- .../jbmc/reachability-slice/test3.desc | 10 ++-- .../test.desc | 8 +-- .../jbmc/removed_virtual_functions/test.desc | 4 +- .../test_one_candidate.desc | 2 +- .../test_two_candidates_no_derefs.desc | 4 +- .../test_two_candidates_with_derefs.desc | 8 +-- .../test-c-with-string-abstraction.desc | 2 +- .../test-c-without-string-abstraction.desc | 2 +- .../cbmc/destructors/compound_literal.desc | 8 +-- .../cbmc/destructors/enter_lexical_block.desc | 28 ++++----- .../reachability-slice-interproc3/test.desc | 2 +- .../assigns_validity_pointer_01/test.desc | 22 +++---- .../assigns_validity_pointer_02/test.desc | 4 +- .../assigns_validity_pointer_03/test.desc | 2 +- .../assigns_validity_pointer_04/test.desc | 14 ++--- .../history-pointer-both-01/test.desc | 8 +-- .../history-pointer-enforce-01/test.desc | 2 +- .../history-pointer-enforce-02/test.desc | 2 +- .../history-pointer-enforce-03/test.desc | 2 +- .../history-pointer-enforce-04/test.desc | 2 +- .../history-pointer-enforce-05/test.desc | 2 +- .../history-pointer-enforce-08/test.desc | 2 +- .../history-pointer-replace-01/test.desc | 4 +- .../history-pointer-replace-02/test.desc | 4 +- .../simplify-complex-expression/test.desc | 2 +- .../simplify-lhs-array-index/test.desc | 6 +- .../test.desc | 8 +-- .../simplify-lhs-dereference/test.desc | 4 +- .../simplify-lhs-member/test.desc | 8 +-- .../test.desc | 6 +- .../simplify-multiply-by-zero/test.desc | 2 +- .../approx-array-variable-const-fp/test.desc | 18 +++--- .../test.desc | 18 +++--- .../test.desc | 18 +++--- .../test.desc | 18 +++--- .../test.desc | 18 +++--- .../test.desc | 18 +++--- .../test.desc | 18 +++--- .../test.desc | 20 +++---- .../dependence-graph10/test.desc | 4 +- .../dependence-graph11/test.desc | 2 +- .../dependence-graph12/test.desc | 4 +- .../dependence-graph14/test.desc | 4 +- .../goto-analyzer/dependence-graph4/test.desc | 2 +- .../goto-analyzer/dependence-graph7/test.desc | 2 +- .../goto-analyzer/dependence-graph8/test.desc | 2 +- .../goto-analyzer/dependence-graph9/test.desc | 4 +- .../test.desc | 2 +- .../test.desc | 18 +++--- .../test.desc | 18 +++--- .../test.desc | 18 +++--- .../test.desc | 18 +++--- .../test.desc | 18 +++--- .../test.desc | 18 +++--- .../test.desc | 18 +++--- .../test.desc | 18 +++--- .../no-match-const-fp-const-cast/test.desc | 18 +++--- .../no-match-const-fp-const-fp-null/test.desc | 2 +- .../no-match-const-fp-const-lost/test.desc | 18 +++--- .../test.desc | 2 +- .../test.desc | 18 +++--- .../test.desc | 2 +- .../test.desc | 18 +++--- .../test.desc | 18 +++--- .../test.desc | 18 +++--- .../test.desc | 18 +++--- .../test.desc | 18 +++--- .../test.desc | 18 +++--- .../no-match-const-fp-null/test.desc | 2 +- .../test.desc | 18 +++--- .../test.desc | 18 +++--- .../test.desc | 18 +++--- .../test.desc | 2 +- .../test.desc | 18 +++--- .../test.desc | 18 +++--- .../test.desc | 18 +++--- .../test.desc | 18 +++--- .../no-match-non-const-fp/test.desc | 18 +++--- .../no-match-parameter-const-fp/test.desc | 18 +++--- .../no-match-parameter-fp/test.desc | 18 +++--- .../test.desc | 18 +++--- .../test.desc | 2 +- .../precise-array-literal-const-fp/test.desc | 2 +- .../test.desc | 2 +- .../test.desc | 2 +- .../test.desc | 2 +- .../test.desc | 2 +- .../test.desc | 2 +- .../precise-const-fp-const-fp/test.desc | 2 +- .../test.desc | 2 +- .../test.desc | 2 +- .../test.desc | 2 +- .../test.desc | 2 +- .../test.desc | 18 +++--- .../goto-analyzer/precise-const-fp/test.desc | 2 +- .../test.desc | 2 +- .../test.desc | 2 +- .../test.desc | 2 +- .../goto-analyzer/precise-derefence/test.desc | 2 +- .../test.desc | 2 +- .../test.desc | 2 +- .../test.desc | 2 +- .../test.desc | 2 +- .../regenerate-entry-function/test.desc | 2 +- .../test.desc | 4 +- .../test.desc | 4 +- .../test.desc | 6 +- .../test.desc | 4 +- .../test.desc | 4 +- .../test.desc | 6 +- .../test.desc | 2 +- .../regenerate-entry-function/test.desc | 2 +- regression/goto-harness/array-types/test.desc | 2 +- .../test.desc | 18 +++--- .../test.desc | 18 +++--- .../fp-reachability-slice1/test.desc | 8 +-- .../fp-reachability-slice2/test.desc | 6 +- .../gcc_attribute_used1/test.desc | 2 +- .../goto-instrument/inline_02/test.desc | 6 +- .../goto-instrument/inline_03/test.desc | 6 +- .../goto-instrument/inline_04/test.desc | 8 +-- .../goto-instrument/inline_08/test.desc | 6 +- .../goto-instrument/inline_09/test.desc | 6 +- .../goto-instrument/is-threaded1/test.desc | 2 +- .../test.desc | 2 +- .../test.desc | 18 +++--- .../test.desc | 2 +- .../precise-const-fp-remove-all-fp/test.desc | 2 +- .../region-analysis-1/test.desc | 4 +- .../region-analysis-10/test.desc | 4 +- .../region-analysis-11/test.desc | 4 +- .../region-analysis-12/test.desc | 6 +- .../region-analysis-13/test.desc | 4 +- .../region-analysis-14/test.desc | 4 +- .../region-analysis-15/test.desc | 4 +- .../region-analysis-16/test.desc | 6 +- .../region-analysis-17/test.desc | 4 +- .../region-analysis-2/test.desc | 4 +- .../region-analysis-3/test.desc | 4 +- .../region-analysis-4/test.desc | 4 +- .../region-analysis-5/test.desc | 4 +- .../region-analysis-6/test.desc | 6 +- .../region-analysis-7/test.desc | 2 +- .../region-analysis-8/test.desc | 6 +- .../region-analysis-9/test.desc | 4 +- .../remove-calls-no-body2/test.desc | 6 +- .../replace-calls-01/test.desc | 4 +- .../replace-calls-02/test.desc | 8 +-- .../show-goto-functions1/test.desc | 2 +- .../slice-global-inits1/test.desc | 12 ++-- .../slice-global-inits2/test.desc | 4 +- .../slice-global-inits3/test.desc | 4 +- .../goto-instrument/splice_call_01/test.desc | 2 +- .../unwind-zero-unwind3/test.desc | 2 +- src/goto-programs/goto_program.cpp | 57 ++++++++++++++----- 174 files changed, 696 insertions(+), 665 deletions(-) diff --git a/jbmc/regression/janalyzer/string-initializer/test.desc b/jbmc/regression/janalyzer/string-initializer/test.desc index affa856055e..67e49735084 100644 --- a/jbmc/regression/janalyzer/string-initializer/test.desc +++ b/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 diff --git a/jbmc/regression/jbmc/JumpSimplification/test.desc b/jbmc/regression/jbmc/JumpSimplification/test.desc index b98eb8839f6..72de52a240b 100644 --- a/jbmc/regression/jbmc/JumpSimplification/test.desc +++ b/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 diff --git a/jbmc/regression/jbmc/LocalVarTable5/test.desc b/jbmc/regression/jbmc/LocalVarTable5/test.desc index 46562fc0cf6..83038f5b177 100644 --- a/jbmc/regression/jbmc/LocalVarTable5/test.desc +++ b/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$ -- diff --git a/jbmc/regression/jbmc/clinit-lifting2/test-goto-functions.desc b/jbmc/regression/jbmc/clinit-lifting2/test-goto-functions.desc index 93216e04753..f9d8e26f17a 100644 --- a/jbmc/regression/jbmc/clinit-lifting2/test-goto-functions.desc +++ b/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\.\(\);\s*// 1 no location\s*int total; +\s*// 0 no location\n\s*CALL java::Other\.\(\)\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 diff --git a/jbmc/regression/jbmc/clinit-lifting3/test-goto-functions.desc b/jbmc/regression/jbmc/clinit-lifting3/test-goto-functions.desc index 3397098c5f3..f3c4410882b 100644 --- a/jbmc/regression/jbmc/clinit-lifting3/test-goto-functions.desc +++ b/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\.\(\);\s*// 1 no location\s*Third\.\(\);\s*// 2 no location\s*int total; +\s*// 0 no location\n\s*CALL java::Other\.\(\)\s*// 1 no location\s*CALL java::Third\.\(\)\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 diff --git a/jbmc/regression/jbmc/destructor1/test.desc b/jbmc/regression/jbmc/destructor1/test.desc index 350d4266507..f201cfae114 100644 --- a/jbmc/regression/jbmc/destructor1/test.desc +++ b/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 diff --git a/jbmc/regression/jbmc/destructors/block.desc b/jbmc/regression/jbmc/destructors/block.desc index 0e919c84a98..dbf5a2bb539 100644 --- a/jbmc/regression/jbmc/destructors/block.desc +++ b/jbmc/regression/jbmc/destructors/block.desc @@ -2,7 +2,7 @@ CORE DestructorStackTests --show-goto-functions --function DestructorStackTests.mainTest --unwind 10 activate-multi-line-match -[0-9]+: dead strings;[\s]*(?P(\/\/ [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(\/\/ [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$ -- @@ -10,11 +10,11 @@ activate-multi-line-match 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 diff --git a/jbmc/regression/jbmc/destructors/break.desc b/jbmc/regression/jbmc/destructors/break.desc index 165fc5fe184..6cf469b6b8c 100644 --- a/jbmc/regression/jbmc/destructors/break.desc +++ b/jbmc/regression/jbmc/destructors/break.desc @@ -2,7 +2,7 @@ CORE DestructorStackTests --show-goto-functions --function DestructorStackTests.mainTest --unwind 10 activate-multi-line-match -(?P\/\/ [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\/\/ [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$ -- @@ -10,11 +10,11 @@ activate-multi-line-match 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 diff --git a/jbmc/regression/jbmc/destructors/continue.desc b/jbmc/regression/jbmc/destructors/continue.desc index 5f9815db194..1aaef528f31 100644 --- a/jbmc/regression/jbmc/destructors/continue.desc +++ b/jbmc/regression/jbmc/destructors/continue.desc @@ -2,7 +2,7 @@ CORE DestructorStackTests --show-goto-functions --function DestructorStackTests.mainTest --unwind 10 activate-multi-line-match -(?P\/\/ [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\/\/ [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$ -- @@ -10,11 +10,11 @@ activate-multi-line-match 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 diff --git a/jbmc/regression/jbmc/destructors/decl.desc b/jbmc/regression/jbmc/destructors/decl.desc index 496f40a795f..a4ce1207ffa 100644 --- a/jbmc/regression/jbmc/destructors/decl.desc +++ b/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\/\/ [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\/\/ [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. diff --git a/jbmc/regression/jbmc/destructors/return.desc b/jbmc/regression/jbmc/destructors/return.desc index d4bbef0abc3..2ba66288ab3 100644 --- a/jbmc/regression/jbmc/destructors/return.desc +++ b/jbmc/regression/jbmc/destructors/return.desc @@ -2,7 +2,7 @@ CORE DestructorStackTests --show-goto-functions --function DestructorStackTests.mainTest --unwind 10 activate-multi-line-match -(?\/\/ [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]+ +(?\/\/ [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$ -- @@ -10,21 +10,21 @@ activate-multi-line-match 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 diff --git a/jbmc/regression/jbmc/generic_base_type/check_casts.desc b/jbmc/regression/jbmc/generic_base_type/check_casts.desc index d9b63d75214..667675d620c 100644 --- a/jbmc/regression/jbmc/generic_base_type/check_casts.desc +++ b/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 naturally inherits, so no cast is required. diff --git a/jbmc/regression/jbmc/generic_function_parameter/callee2_with_cast.desc b/jbmc/regression/jbmc/generic_function_parameter/callee2_with_cast.desc index 6c609c1aa92..5247a3e9a50 100644 --- a/jbmc/regression/jbmc/generic_function_parameter/callee2_with_cast.desc +++ b/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. diff --git a/jbmc/regression/jbmc/generic_function_parameter/callee_without_cast.desc b/jbmc/regression/jbmc/generic_function_parameter/callee_without_cast.desc index 949a81314d2..037e1d38637 100644 --- a/jbmc/regression/jbmc/generic_function_parameter/callee_without_cast.desc +++ b/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. diff --git a/jbmc/regression/jbmc/generic_static_field/test.desc b/jbmc/regression/jbmc/generic_static_field/test.desc index 6b360e47b60..613b5072557 100644 --- a/jbmc/regression/jbmc/generic_static_field/test.desc +++ b/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 -- diff --git a/jbmc/regression/jbmc/generic_virtual_function/check_casts.desc b/jbmc/regression/jbmc/generic_virtual_function/check_casts.desc index 0a0a0902e16..c384eeeca75 100644 --- a/jbmc/regression/jbmc/generic_virtual_function/check_casts.desc +++ b/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 diff --git a/jbmc/regression/jbmc/lazyloading_no_candidates/test.desc b/jbmc/regression/jbmc/lazyloading_no_candidates/test.desc index 190e7a7eac7..20591ac6f00 100644 --- a/jbmc/regression/jbmc/lazyloading_no_candidates/test.desc +++ b/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) diff --git a/jbmc/regression/jbmc/reachability-slice/test.desc b/jbmc/regression/jbmc/reachability-slice/test.desc index 077aa8cd564..c4a9e13e408 100644 --- a/jbmc/regression/jbmc/reachability-slice/test.desc +++ b/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. diff --git a/jbmc/regression/jbmc/reachability-slice/test2.desc b/jbmc/regression/jbmc/reachability-slice/test2.desc index 083e83fb1ad..f9fffea8fd2 100644 --- a/jbmc/regression/jbmc/reachability-slice/test2.desc +++ b/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. diff --git a/jbmc/regression/jbmc/reachability-slice/test3.desc b/jbmc/regression/jbmc/reachability-slice/test3.desc index 62f38772408..e87f7f452da 100644 --- a/jbmc/regression/jbmc/reachability-slice/test3.desc +++ b/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. diff --git a/jbmc/regression/jbmc/remove_virtual_function_typecast/test.desc b/jbmc/regression/jbmc/remove_virtual_function_typecast/test.desc index 3396c94d2d5..0c84906c421 100644 --- a/jbmc/regression/jbmc/remove_virtual_function_typecast/test.desc +++ b/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$ -- diff --git a/jbmc/regression/jbmc/removed_virtual_functions/test.desc b/jbmc/regression/jbmc/removed_virtual_functions/test.desc index 8207191b63f..a08fc572eb5 100644 --- a/jbmc/regression/jbmc/removed_virtual_functions/test.desc +++ b/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) diff --git a/jbmc/regression/jbmc/virtual_temp_var_for_this_argument/test_one_candidate.desc b/jbmc/regression/jbmc/virtual_temp_var_for_this_argument/test_one_candidate.desc index b9e6cf0c0a2..f68db9b732a 100644 --- a/jbmc/regression/jbmc/virtual_temp_var_for_this_argument/test_one_candidate.desc +++ b/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 -- diff --git a/jbmc/regression/jbmc/virtual_temp_var_for_this_argument/test_two_candidates_no_derefs.desc b/jbmc/regression/jbmc/virtual_temp_var_for_this_argument/test_two_candidates_no_derefs.desc index aa1943198ef..6a590e44111 100644 --- a/jbmc/regression/jbmc/virtual_temp_var_for_this_argument/test_two_candidates_no_derefs.desc +++ b/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 -- diff --git a/jbmc/regression/jbmc/virtual_temp_var_for_this_argument/test_two_candidates_with_derefs.desc b/jbmc/regression/jbmc/virtual_temp_var_for_this_argument/test_two_candidates_with_derefs.desc index d0257dfcde6..a353ec862e8 100644 --- a/jbmc/regression/jbmc/virtual_temp_var_for_this_argument/test_two_candidates_with_derefs.desc +++ b/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 diff --git a/regression/cbmc-library/string-abstraction/test-c-with-string-abstraction.desc b/regression/cbmc-library/string-abstraction/test-c-with-string-abstraction.desc index 73e2f0b2ffc..a9c36d41d2c 100644 --- a/regression/cbmc-library/string-abstraction/test-c-with-string-abstraction.desc +++ b/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$ -- diff --git a/regression/cbmc-library/string-abstraction/test-c-without-string-abstraction.desc b/regression/cbmc-library/string-abstraction/test-c-without-string-abstraction.desc index 28c456a4bf7..d2b76c017fd 100644 --- a/regression/cbmc-library/string-abstraction/test-c-without-string-abstraction.desc +++ b/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$ -- diff --git a/regression/cbmc/destructors/compound_literal.desc b/regression/cbmc/destructors/compound_literal.desc index 46640b2c02c..47c217fed18 100644 --- a/regression/cbmc/destructors/compound_literal.desc +++ b/regression/cbmc/destructors/compound_literal.desc @@ -2,7 +2,7 @@ CORE main.c --unwind 10 --show-goto-functions activate-multi-line-match -(?P\/\/ [0-9]+ file main\.c line [0-9]+ function main)[\s]*dead newAlloc0;[\s]*(?P>comment_block)[\s]*dead pc;[\s]*(?P>comment_block)[\s]*dead literal;[\s]*(?P>comment_block)[\s]*9: END_FUNCTION +(?P\/\/ [0-9]+ file main\.c line [0-9]+ function main)[\s]*DEAD .*newAlloc0[\s]*(?P>comment_block)[\s]*DEAD .*pc[\s]*(?P>comment_block)[\s]*DEAD .*literal[\s]*(?P>comment_block)[\s]*9: END_FUNCTION ^EXIT=0$ ^SIGNAL=0$ -- @@ -10,11 +10,11 @@ activate-multi-line-match Checks for: // 49 file main.c line 44 function main - dead newAlloc0; + DEAD main::1::newAlloc0 // 50 file main.c line 44 function main - dead pc; + DEAD main::1::pc // 51 file main.c line 44 function main - dead literal; + DEAD main::$tmp::literal // 52 file main.c line 45 function main 9: END_FUNCTION diff --git a/regression/cbmc/destructors/enter_lexical_block.desc b/regression/cbmc/destructors/enter_lexical_block.desc index 3f02325816d..751e929d85d 100644 --- a/regression/cbmc/destructors/enter_lexical_block.desc +++ b/regression/cbmc/destructors/enter_lexical_block.desc @@ -2,26 +2,26 @@ CORE main.c --unwind 10 --show-goto-functions activate-multi-line-match -(?P\/\/ [0-9]+ file main\.c line [0-9]+ function main)[\s]*6: test newAlloc4;[\s]*(?P>comment_block)[\s]*newAlloc4 = \{ \.id=4 \};[\s]*(?P>comment_block)[\s]*test newAlloc6;[\s]*(?P>comment_block)[\s]*newAlloc6 = \{ \.id=6 \};[\s]*(?P>comment_block)[\s]*test newAlloc7;[\s]*(?P>comment_block)[\s]*newAlloc7 = \{ \.id=7 \};[\s]*(?P>comment_block)[\s]*GOTO 3 +(?P\/\/ [0-9]+ file main\.c line [0-9]+ function main)[\s]*6: .*newAlloc4 : struct tag-test[\s]*(?P>comment_block)[\s]*.*newAlloc4 := \{ 4 \}[\s]*(?P>comment_block)[\s]*.*newAlloc6 : struct tag-test[\s]*(?P>comment_block)[\s]*.*newAlloc6 := \{ 6 \}[\s]*(?P>comment_block)[\s]*.*newAlloc7 : struct tag-test[\s]*(?P>comment_block)[\s]*.*newAlloc7 := \{ 7 \}[\s]*(?P>comment_block)[\s]*GOTO 3 ^EXIT=0$ ^SIGNAL=0$ -- -- Checks for: - // 31 file main.c line 34 function main - 6: test newAlloc4; - // 32 file main.c line 34 function main - newAlloc4 = { .id=4 }; - // 33 file main.c line 35 function main - test newAlloc6; - // 34 file main.c line 35 function main - newAlloc6 = { .id=6 }; - // 35 file main.c line 36 function main - test newAlloc7; - // 36 file main.c line 36 function main - newAlloc7 = { .id=7 }; - // 37 file main.c line 37 function main + // 37 file main.c line 36 function main + 6: DECL main::1::2::2::newAlloc4 : struct tag-test + // 38 file main.c line 36 function main + ASSIGN main::1::2::2::newAlloc4 := { 4 } + // 39 file main.c line 37 function main + DECL main::1::2::2::newAlloc6 : struct tag-test + // 40 file main.c line 37 function main + ASSIGN main::1::2::2::newAlloc6 := { 6 } + // 41 file main.c line 38 function main + DECL main::1::2::2::newAlloc7 : struct tag-test + // 42 file main.c line 38 function main + ASSIGN main::1::2::2::newAlloc7 := { 7 } + // 43 file main.c line 39 function main GOTO 3 This asserts that when the GOTO is going into a lexical block that destructors diff --git a/regression/cbmc/reachability-slice-interproc3/test.desc b/regression/cbmc/reachability-slice-interproc3/test.desc index f2af4dc0176..66f6ca60700 100644 --- a/regression/cbmc/reachability-slice-interproc3/test.desc +++ b/regression/cbmc/reachability-slice-interproc3/test.desc @@ -3,6 +3,6 @@ main.c --reachability-slice-fb --show-goto-functions ^EXIT=0$ ^SIGNAL=0$ -main#return_value = 1; +ASSIGN main#return_value := 1 -- ^warning: ignoring diff --git a/regression/contracts/assigns_validity_pointer_01/test.desc b/regression/contracts/assigns_validity_pointer_01/test.desc index 345bde8483c..9ef4d9894d7 100644 --- a/regression/contracts/assigns_validity_pointer_01/test.desc +++ b/regression/contracts/assigns_validity_pointer_01/test.desc @@ -6,19 +6,19 @@ main.c ^VERIFICATION SUCCESSFUL$ SUCCESS // bar -ASSERT \*x > 0 -IF !\(\*x == 3\) THEN GOTO \d -IF !\(\(signed int \*\)\(void \*\)0 == \(\(signed int \*\)NULL\)\) THEN GOTO \d -tmp_if_expr = \*\(\(signed int \*\)\(void \*\)0\) == 5 \? TRUE \: FALSE; -tmp_if_expr\$\d = tmp_if_expr \? TRUE : FALSE; -ASSUME tmp_if_expr\$\d +ASSERT \*foo::x > 0 +IF ¬\(\*foo::x = 3\) THEN GOTO \d +IF ¬\(.*0.* = NULL\) THEN GOTO \d +ASSIGN .*::tmp_if_expr := \(\*\(.*0.*\) = 5 \? true : false\) +ASSIGN .*::tmp_if_expr\$\d := .*::tmp_if_expr \? true : false +ASSUME .*::tmp_if_expr\$\d // baz -IF !\(z == \(\(signed int \*\)NULL\)\) THEN GOTO \d -tmp_if_expr\$\d = \*z == 7 \? TRUE : FALSE; -ASSUME tmp_if_expr\$\d +IF ¬\(z ≠ NULL\) THEN GOTO \d +ASSIGN .*::tmp_if_expr\$\d := \(\*z = 7 \? true : false\) +ASSUME .*::tmp_if_expr\$\d // foo -ASSUME \*tmp_cc\$\d > 0 -ASSERT \*tmp_cc\$\d == 3 +ASSUME \*.*::tmp_cc\$\d > 0 +ASSERT \*.*::tmp_cc\$\d = 3 -- \[3\] file main\.c line 6 assertion: FAILURE -- diff --git a/regression/contracts/assigns_validity_pointer_02/test.desc b/regression/contracts/assigns_validity_pointer_02/test.desc index 038910fa7bf..ebfee6dc26a 100644 --- a/regression/contracts/assigns_validity_pointer_02/test.desc +++ b/regression/contracts/assigns_validity_pointer_02/test.desc @@ -6,8 +6,8 @@ main.c ^VERIFICATION SUCCESSFUL$ //^([foo\.1] line 15 assertion: FAILURE) // foo -ASSUME \*tmp_cc\$\d > 0 -ASSERT \*tmp_cc\$\d == 3 +ASSUME \*.*::tmp_cc\$\d > 0 +ASSERT \*.*::tmp_cc\$\d = 3 -- \[foo\.1\] line 24 assertion: FAILURE \[foo\.3\] line 27 assertion: FAILURE diff --git a/regression/contracts/assigns_validity_pointer_03/test.desc b/regression/contracts/assigns_validity_pointer_03/test.desc index 988ad466d7c..7c04f9cff70 100644 --- a/regression/contracts/assigns_validity_pointer_03/test.desc +++ b/regression/contracts/assigns_validity_pointer_03/test.desc @@ -7,7 +7,7 @@ main.c // bar ASSERT \*x > 0 IF !\(\*x == 3\) THEN GOTO \d -tmp_if_expr = \*y == 5 \? TRUE \: FALSE; +tmp_if_expr = \*y == 5 \? true \: false; ASSUME tmp_if_expr // baz ASSUME \*z == 7 diff --git a/regression/contracts/assigns_validity_pointer_04/test.desc b/regression/contracts/assigns_validity_pointer_04/test.desc index f6cee72a7b6..11aec0dea4b 100644 --- a/regression/contracts/assigns_validity_pointer_04/test.desc +++ b/regression/contracts/assigns_validity_pointer_04/test.desc @@ -5,15 +5,15 @@ main.c ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ // bar -ASSERT \*x > 0 -IF !\(\*x == 3\) THEN GOTO \d -tmp_if_expr = \*y == 5 \? TRUE \: FALSE; -ASSUME tmp_if_expr +ASSERT \*foo::x > 0 +IF ¬\(\*foo::x = 3\) THEN GOTO \d +ASSIGN goto_convertt::tmp_if_expr := \(\*foo::1::y = 5 \? true : false\) +ASSUME .*::tmp_if_expr // baz -ASSUME \*z == 7 +ASSUME \*z = 7 // foo -ASSUME \*tmp_cc\$\d > 0 -ASSERT \*tmp_cc\$\d == 3 +ASSUME \*.*::tmp_cc\$\d > 0 +ASSERT \*.*::tmp_cc\$\d = 3 -- -- Verification: diff --git a/regression/contracts/history-pointer-both-01/test.desc b/regression/contracts/history-pointer-both-01/test.desc index 76377d45f8a..edc7af0ddcd 100644 --- a/regression/contracts/history-pointer-both-01/test.desc +++ b/regression/contracts/history-pointer-both-01/test.desc @@ -4,10 +4,10 @@ main.c ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ -ASSUME tmp_cc\$\d != \(\(signed int \*\)NULL\) -ASSERT n != \(\(signed int \*\)NULL\) -ASSUME tmp_cc == \*n -ASSERT tmp_cc\$\d == \*tmp_cc\$\d +ASSUME .*::tmp_cc\$\d ≠ NULL +ASSERT foo::n ≠ NULL +ASSUME .*::tmp_cc = \*foo::n +ASSERT .*::tmp_cc\$\d = \*.*::tmp_cc\$\d -- -- Verification: diff --git a/regression/contracts/history-pointer-enforce-01/test.desc b/regression/contracts/history-pointer-enforce-01/test.desc index d3300daed5c..594cb8af05d 100644 --- a/regression/contracts/history-pointer-enforce-01/test.desc +++ b/regression/contracts/history-pointer-enforce-01/test.desc @@ -4,7 +4,7 @@ main.c ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ -ASSERT \*tmp_cc\$\d == tmp_cc\$\d \+ 5 +ASSERT \*.*::tmp_cc\$\d = .*::tmp_cc\$\d \+ 5 -- -- Verification: diff --git a/regression/contracts/history-pointer-enforce-02/test.desc b/regression/contracts/history-pointer-enforce-02/test.desc index 960b0eb4aaf..bd08337d8ee 100644 --- a/regression/contracts/history-pointer-enforce-02/test.desc +++ b/regression/contracts/history-pointer-enforce-02/test.desc @@ -4,7 +4,7 @@ main.c ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ -ASSERT \*tmp_cc\$\d < tmp_cc\$\d \+ 5 +ASSERT \*.*::tmp_cc\$\d < .*::tmp_cc\$\d \+ 5 -- -- Verification: diff --git a/regression/contracts/history-pointer-enforce-03/test.desc b/regression/contracts/history-pointer-enforce-03/test.desc index 9938b262b58..dc32ca22c00 100644 --- a/regression/contracts/history-pointer-enforce-03/test.desc +++ b/regression/contracts/history-pointer-enforce-03/test.desc @@ -4,7 +4,7 @@ main.c ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ -ASSERT tmp_if_expr\$\d +ASSERT .*::tmp_if_expr\$\d -- -- Verification: diff --git a/regression/contracts/history-pointer-enforce-04/test.desc b/regression/contracts/history-pointer-enforce-04/test.desc index 21bab515511..4ff79ee01ca 100644 --- a/regression/contracts/history-pointer-enforce-04/test.desc +++ b/regression/contracts/history-pointer-enforce-04/test.desc @@ -4,7 +4,7 @@ main.c ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ -ASSERT tmp_if_expr +ASSERT .*::tmp_if_expr -- -- Verification: diff --git a/regression/contracts/history-pointer-enforce-05/test.desc b/regression/contracts/history-pointer-enforce-05/test.desc index 493944290e8..5606d2d5856 100644 --- a/regression/contracts/history-pointer-enforce-05/test.desc +++ b/regression/contracts/history-pointer-enforce-05/test.desc @@ -4,7 +4,7 @@ main.c ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ -ASSERT tmp_if_expr +ASSERT .*::tmp_if_expr -- -- Verification: diff --git a/regression/contracts/history-pointer-enforce-08/test.desc b/regression/contracts/history-pointer-enforce-08/test.desc index 951fff65c6f..9049c0bc86c 100644 --- a/regression/contracts/history-pointer-enforce-08/test.desc +++ b/regression/contracts/history-pointer-enforce-08/test.desc @@ -4,7 +4,7 @@ main.c ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ -ASSERT \*tmp_cc\$\d\.y == tmp_cc\$\d \+ 5 +ASSERT \*\(.*::tmp_cc\$\d\.y\) = .*::tmp_cc\$\d \+ 5 -- -- Verification: diff --git a/regression/contracts/history-pointer-replace-01/test.desc b/regression/contracts/history-pointer-replace-01/test.desc index 3c047fc5975..611dfd7552a 100644 --- a/regression/contracts/history-pointer-replace-01/test.desc +++ b/regression/contracts/history-pointer-replace-01/test.desc @@ -4,8 +4,8 @@ main.c ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ -ASSERT \*\(&n\) > 0 -ASSUME \*\(&n\) == tmp_cc[\$\d]? \+ 2 +ASSERT \*\(address_of.*n.*\) > 0 +ASSUME \*\(address_of.*n.*\) = .*::tmp_cc[\$\d]? \+ 2 -- -- Verification: diff --git a/regression/contracts/history-pointer-replace-02/test.desc b/regression/contracts/history-pointer-replace-02/test.desc index 3903c0aa6ff..68dea109f7f 100644 --- a/regression/contracts/history-pointer-replace-02/test.desc +++ b/regression/contracts/history-pointer-replace-02/test.desc @@ -4,8 +4,8 @@ main.c ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ -ASSERT \*\(&n\) == 0 -ASSUME \*\(&n\) >= tmp_cc[\$\d]? \+ 2 +ASSERT \*\(address_of.*n.*\) = 0 +ASSUME \*\(address_of.*n.*\) ≥ .*::tmp_cc[\$\d]? \+ 2 -- -- Verification: diff --git a/regression/goto-analyzer-simplify/simplify-complex-expression/test.desc b/regression/goto-analyzer-simplify/simplify-complex-expression/test.desc index 40eb8d1a1b4..823418a6ed3 100644 --- a/regression/goto-analyzer-simplify/simplify-complex-expression/test.desc +++ b/regression/goto-analyzer-simplify/simplify-complex-expression/test.desc @@ -1,7 +1,7 @@ CORE main.c --vsd -r == 2 +r = 2 ^SIGNAL=0$ ^EXIT=0$ -- diff --git a/regression/goto-analyzer-simplify/simplify-lhs-array-index/test.desc b/regression/goto-analyzer-simplify/simplify-lhs-array-index/test.desc index d1161d20eff..5f1ac78c109 100644 --- a/regression/goto-analyzer-simplify/simplify-lhs-array-index/test.desc +++ b/regression/goto-analyzer-simplify/simplify-lhs-array-index/test.desc @@ -1,9 +1,9 @@ CORE main.c --vsd --vsd-arrays every-element -arr\[0l?l?\] = -arr\[1l?l?\] = -arr\[\(signed (long (long )?)?int\)nondet\] = +arr\[0\] := +arr\[1\] := +arr\[.*nondet.*\] := ^SIGNAL=0$ ^EXIT=0$ -- diff --git a/regression/goto-analyzer-simplify/simplify-lhs-array-pointers-index/test.desc b/regression/goto-analyzer-simplify/simplify-lhs-array-pointers-index/test.desc index 715e8782c58..9e70e14c974 100644 --- a/regression/goto-analyzer-simplify/simplify-lhs-array-pointers-index/test.desc +++ b/regression/goto-analyzer-simplify/simplify-lhs-array-pointers-index/test.desc @@ -1,10 +1,10 @@ CORE main.c --vsd --vsd-arrays every-element --vsd-pointers value-set -symbol_a = 1 -symbol_b = 2 -\*arr\[2l?l?\] = 3; -\*arr\[\(signed (long (long )?)?int\)nondet_index\] = 4; +symbol_a := 1 +symbol_b := 2 +\*\(.*::arr\[2\]\) := 3 +\*\(.*::arr\[.*nondet_index.*\]\) := 4 ^SIGNAL=0$ ^EXIT=0$ -- diff --git a/regression/goto-analyzer-simplify/simplify-lhs-dereference/test.desc b/regression/goto-analyzer-simplify/simplify-lhs-dereference/test.desc index e7dc545e387..bfe42612579 100644 --- a/regression/goto-analyzer-simplify/simplify-lhs-dereference/test.desc +++ b/regression/goto-analyzer-simplify/simplify-lhs-dereference/test.desc @@ -1,8 +1,8 @@ CORE main.c --vsd --vsd-pointers value-set -symbol = 5 -\*pointer = 6 +symbol := 5 +\*.*::pointer := 6 ^SIGNAL=0$ ^EXIT=0$ -- diff --git a/regression/goto-analyzer-simplify/simplify-lhs-member/test.desc b/regression/goto-analyzer-simplify/simplify-lhs-member/test.desc index e9181e3e47a..e3b1a22b2da 100644 --- a/regression/goto-analyzer-simplify/simplify-lhs-member/test.desc +++ b/regression/goto-analyzer-simplify/simplify-lhs-member/test.desc @@ -1,10 +1,10 @@ CORE main.c --vsd --vsd-arrays every-element --vsd-pointers value-set --vsd-structs every-field -symbol = 5 -\*value\.pointer_component = 6 -value\.array\[1l?l?\] = 2 -value\.array\[\(signed (long (long )?)?int\)nondet\] = 3 +symbol := 5 +\*\(.*::value\.pointer_component\) := 6 +value\.array\[1\] := 2 +value\.array\[.*nondet.*\] := 3 ^SIGNAL=0$ ^EXIT=0$ -- diff --git a/regression/goto-analyzer-simplify/simplify-lhs-pointer-array-dereference/test.desc b/regression/goto-analyzer-simplify/simplify-lhs-pointer-array-dereference/test.desc index f5bb0f7c897..ce92a68e65e 100644 --- a/regression/goto-analyzer-simplify/simplify-lhs-pointer-array-dereference/test.desc +++ b/regression/goto-analyzer-simplify/simplify-lhs-pointer-array-dereference/test.desc @@ -1,9 +1,9 @@ CORE main.c --vsd --vsd-arrays every-element --vsd-pointers value-set -array\[0l?l?\] = 5 -array\[\(signed (long (long )?)?int\)nondet\] = 6 -new_array\[1l?l?\] = 7 +array\[0\] := 5 +array\[.*nondet.*\] := 6 +new_array\[1\] := 7 ^SIGNAL=0$ ^EXIT=0$ -- diff --git a/regression/goto-analyzer-simplify/simplify-multiply-by-zero/test.desc b/regression/goto-analyzer-simplify/simplify-multiply-by-zero/test.desc index 59ae86c6ccf..2263eb791f3 100644 --- a/regression/goto-analyzer-simplify/simplify-multiply-by-zero/test.desc +++ b/regression/goto-analyzer-simplify/simplify-multiply-by-zero/test.desc @@ -3,7 +3,7 @@ main.c --vsd ^SIGNAL=0$ ^EXIT=0$ -main#return_value = 0; +main#return_value := 0 -- -- Tests that a multiplication diff --git a/regression/goto-analyzer/approx-array-variable-const-fp/test.desc b/regression/goto-analyzer/approx-array-variable-const-fp/test.desc index 82860e90e86..ff396910001 100644 --- a/regression/goto-analyzer/approx-array-variable-const-fp/test.desc +++ b/regression/goto-analyzer/approx-array-variable-const-fp/test.desc @@ -2,17 +2,17 @@ CORE main.c --show-goto-functions --pointer-check ^Removal of function pointers and virtual functions$ -^\s*IF fp_tbl\[.*i\] == f2 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[.*i\] == f3 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[.*i\] == f4 THEN GOTO [0-9]$ +^\s*IF fp_tbl\[.*i.*\] = address_of\(f2\) THEN GOTO [0-9]$ +^\s*IF fp_tbl\[.*i.*\] = address_of\(f3\) THEN GOTO [0-9]$ +^\s*IF fp_tbl\[.*i.*\] = address_of\(f4\) THEN GOTO [0-9]$ ^EXIT=0$ ^SIGNAL=0$ -- -^\s*IF fp_tbl\[.*i\] == f1 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[.*i\] == f5 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[.*i\] == f6 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[.*i\] == f7 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[.*i\] == f8 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[.*i\] == f9 THEN GOTO [0-9]$ +^\s*IF fp_tbl\[.*i.*\] = address_of\(f1\) THEN GOTO [0-9]$ +^\s*IF fp_tbl\[.*i.*\] = address_of\(f5\) THEN GOTO [0-9]$ +^\s*IF fp_tbl\[.*i.*\] = address_of\(f6\) THEN GOTO [0-9]$ +^\s*IF fp_tbl\[.*i.*\] = address_of\(f7\) THEN GOTO [0-9]$ +^\s*IF fp_tbl\[.*i.*\] = address_of\(f8\) THEN GOTO [0-9]$ +^\s*IF fp_tbl\[.*i.*\] = address_of\(f9\) THEN GOTO [0-9]$ ^warning: ignoring function \w+: replacing function pointer by 9 possible targets diff --git a/regression/goto-analyzer/approx-const-fp-array-variable-cast-const-fp/test.desc b/regression/goto-analyzer/approx-const-fp-array-variable-cast-const-fp/test.desc index 5b970303b37..e6adfd16987 100644 --- a/regression/goto-analyzer/approx-const-fp-array-variable-cast-const-fp/test.desc +++ b/regression/goto-analyzer/approx-const-fp-array-variable-cast-const-fp/test.desc @@ -2,17 +2,17 @@ CORE main.c --show-goto-functions --pointer-check ^Removal of function pointers and virtual functions$ -^\s*IF fp == f2 THEN GOTO [0-9]$ -^\s*IF fp == f3 THEN GOTO [0-9]$ -^\s*IF fp == f4 THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f2\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f3\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f4\) THEN GOTO [0-9]$ ^EXIT=0$ ^SIGNAL=0$ -- ^warning: ignoring -^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f1 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f5 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f6 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f7 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f8 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f9 THEN GOTO [0-9]$ +^\s*IF fp_tbl\[\.*i.*\] = address_of\(f1\) THEN GOTO [0-9]$ +^\s*IF fp_tbl\[\.*i.*\] = address_of\(f5\) THEN GOTO [0-9]$ +^\s*IF fp_tbl\[\.*i.*\] = address_of\(f6\) THEN GOTO [0-9]$ +^\s*IF fp_tbl\[\.*i.*\] = address_of\(f7\) THEN GOTO [0-9]$ +^\s*IF fp_tbl\[\.*i.*\] = address_of\(f8\) THEN GOTO [0-9]$ +^\s*IF fp_tbl\[\.*i.*\] = address_of\(f9\) THEN GOTO [0-9]$ function \w+: replacing function pointer by 9 possible targets diff --git a/regression/goto-analyzer/approx-const-fp-array-variable-const-fp-with-null/test.desc b/regression/goto-analyzer/approx-const-fp-array-variable-const-fp-with-null/test.desc index bd1f5b41a5d..20b56e58877 100644 --- a/regression/goto-analyzer/approx-const-fp-array-variable-const-fp-with-null/test.desc +++ b/regression/goto-analyzer/approx-const-fp-array-variable-const-fp-with-null/test.desc @@ -2,18 +2,18 @@ CORE main.c --show-goto-functions --pointer-check ^Removal of function pointers and virtual functions$ -^\s*IF fp == f2 THEN GOTO [0-9]$ -^\s*IF fp == f3 THEN GOTO [0-9]$ -^\s*IF fp == f4 THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f2\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f3\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f4\) THEN GOTO [0-9]$ replacing function pointer by 3 possible targets ^EXIT=0$ ^SIGNAL=0$ -- ^warning: ignoring -^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f1 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f5 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f6 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f7 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f8 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f9 THEN GOTO [0-9]$ +^\s*IF fp_tbl\[.*i.*\] = address_of\(f1\) THEN GOTO [0-9]$ +^\s*IF fp_tbl\[.*i.*\] = address_of\(f5\) THEN GOTO [0-9]$ +^\s*IF fp_tbl\[.*i.*\] = address_of\(f6\) THEN GOTO [0-9]$ +^\s*IF fp_tbl\[.*i.*\] = address_of\(f7\) THEN GOTO [0-9]$ +^\s*IF fp_tbl\[.*i.*\] = address_of\(f8\) THEN GOTO [0-9]$ +^\s*IF fp_tbl\[.*i.*\] = address_of\(f9\) THEN GOTO [0-9]$ function \w+: replacing function pointer by 9 possible targets diff --git a/regression/goto-analyzer/approx-const-fp-array-variable-const-fp/test.desc b/regression/goto-analyzer/approx-const-fp-array-variable-const-fp/test.desc index 5b970303b37..c2e7c0b8632 100644 --- a/regression/goto-analyzer/approx-const-fp-array-variable-const-fp/test.desc +++ b/regression/goto-analyzer/approx-const-fp-array-variable-const-fp/test.desc @@ -2,17 +2,17 @@ CORE main.c --show-goto-functions --pointer-check ^Removal of function pointers and virtual functions$ -^\s*IF fp == f2 THEN GOTO [0-9]$ -^\s*IF fp == f3 THEN GOTO [0-9]$ -^\s*IF fp == f4 THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f2\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f3\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f4\) THEN GOTO [0-9]$ ^EXIT=0$ ^SIGNAL=0$ -- ^warning: ignoring -^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f1 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f5 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f6 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f7 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f8 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f9 THEN GOTO [0-9]$ +^\s*IF fp_tbl\[.*i.*\] = address_of\(f1\) THEN GOTO [0-9]$ +^\s*IF fp_tbl\[.*i.*\] = address_of\(f5\) THEN GOTO [0-9]$ +^\s*IF fp_tbl\[.*i.*\] = address_of\(f6\) THEN GOTO [0-9]$ +^\s*IF fp_tbl\[.*i.*\] = address_of\(f7\) THEN GOTO [0-9]$ +^\s*IF fp_tbl\[.*i.*\] = address_of\(f8\) THEN GOTO [0-9]$ +^\s*IF fp_tbl\[.*i.*\] = address_of\(f9\) THEN GOTO [0-9]$ function \w+: replacing function pointer by 9 possible targets diff --git a/regression/goto-analyzer/approx-const-fp-array-variable-const-pointer-const-struct-non-const-fp/test.desc b/regression/goto-analyzer/approx-const-fp-array-variable-const-pointer-const-struct-non-const-fp/test.desc index 5b970303b37..c9b7b3375f1 100644 --- a/regression/goto-analyzer/approx-const-fp-array-variable-const-pointer-const-struct-non-const-fp/test.desc +++ b/regression/goto-analyzer/approx-const-fp-array-variable-const-pointer-const-struct-non-const-fp/test.desc @@ -2,17 +2,17 @@ CORE main.c --show-goto-functions --pointer-check ^Removal of function pointers and virtual functions$ -^\s*IF fp == f2 THEN GOTO [0-9]$ -^\s*IF fp == f3 THEN GOTO [0-9]$ -^\s*IF fp == f4 THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f2\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f3\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f4\) THEN GOTO [0-9]$ ^EXIT=0$ ^SIGNAL=0$ -- ^warning: ignoring -^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f1 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f5 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f6 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f7 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f8 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f9 THEN GOTO [0-9]$ +^\s*IF fp_tbl\[.*i.*\] = address_of\(f1\) THEN GOTO [0-9]$ +^\s*IF fp_tbl\[.*i.*\] == address_of\(f5\) THEN GOTO [0-9]$ +^\s*IF fp_tbl\[.*i.*\] == address_of\(f6\) THEN GOTO [0-9]$ +^\s*IF fp_tbl\[.*i.*\] == address_of\(f7\) THEN GOTO [0-9]$ +^\s*IF fp_tbl\[.*i.*\] == address_of\(f8\) THEN GOTO [0-9]$ +^\s*IF fp_tbl\[.*i.*\] == address_of\(f9\) THEN GOTO [0-9]$ function \w+: replacing function pointer by 9 possible targets diff --git a/regression/goto-analyzer/approx-const-fp-array-variable-const-struct-non-const-fp/test.desc b/regression/goto-analyzer/approx-const-fp-array-variable-const-struct-non-const-fp/test.desc index 5b970303b37..c2e7c0b8632 100644 --- a/regression/goto-analyzer/approx-const-fp-array-variable-const-struct-non-const-fp/test.desc +++ b/regression/goto-analyzer/approx-const-fp-array-variable-const-struct-non-const-fp/test.desc @@ -2,17 +2,17 @@ CORE main.c --show-goto-functions --pointer-check ^Removal of function pointers and virtual functions$ -^\s*IF fp == f2 THEN GOTO [0-9]$ -^\s*IF fp == f3 THEN GOTO [0-9]$ -^\s*IF fp == f4 THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f2\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f3\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f4\) THEN GOTO [0-9]$ ^EXIT=0$ ^SIGNAL=0$ -- ^warning: ignoring -^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f1 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f5 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f6 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f7 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f8 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f9 THEN GOTO [0-9]$ +^\s*IF fp_tbl\[.*i.*\] = address_of\(f1\) THEN GOTO [0-9]$ +^\s*IF fp_tbl\[.*i.*\] = address_of\(f5\) THEN GOTO [0-9]$ +^\s*IF fp_tbl\[.*i.*\] = address_of\(f6\) THEN GOTO [0-9]$ +^\s*IF fp_tbl\[.*i.*\] = address_of\(f7\) THEN GOTO [0-9]$ +^\s*IF fp_tbl\[.*i.*\] = address_of\(f8\) THEN GOTO [0-9]$ +^\s*IF fp_tbl\[.*i.*\] = address_of\(f9\) THEN GOTO [0-9]$ function \w+: replacing function pointer by 9 possible targets diff --git a/regression/goto-analyzer/approx-const-fp-array-variable-invalid-cast-const-fp/test.desc b/regression/goto-analyzer/approx-const-fp-array-variable-invalid-cast-const-fp/test.desc index 57386e3d576..8952e72ccd3 100644 --- a/regression/goto-analyzer/approx-const-fp-array-variable-invalid-cast-const-fp/test.desc +++ b/regression/goto-analyzer/approx-const-fp-array-variable-invalid-cast-const-fp/test.desc @@ -2,17 +2,17 @@ CORE main.c --show-goto-functions --pointer-check ^Removal of function pointers and virtual functions$ -^\s*IF fp == \(.*\)f2 THEN GOTO [0-9]$ -^\s*IF fp == \(.*\)f3 THEN GOTO [0-9]$ -^\s*IF fp == \(.*\)f4 THEN GOTO [0-9]$ +^\s*IF .*::fp = .*f2.* THEN GOTO [0-9]$ +^\s*IF .*::fp = .*f3.* THEN GOTO [0-9]$ +^\s*IF .*::fp = .*f4.* THEN GOTO [0-9]$ ^EXIT=0$ ^SIGNAL=0$ -- ^warning: ignoring -^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f1 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f5 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f6 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f7 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f8 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f9 THEN GOTO [0-9]$ +^\s*IF fp_tbl\[.*i.*\] = address_of\(f1\) THEN GOTO [0-9]$ +^\s*IF fp_tbl\[.*i.*\] == f5 THEN GOTO [0-9]$ +^\s*IF fp_tbl\[.*i.*\] == f6 THEN GOTO [0-9]$ +^\s*IF fp_tbl\[.*i.*\] == f7 THEN GOTO [0-9]$ +^\s*IF fp_tbl\[.*i.*\] == f8 THEN GOTO [0-9]$ +^\s*IF fp_tbl\[.*i.*\] == f9 THEN GOTO [0-9]$ function \w+: replacing function pointer by 9 possible targets diff --git a/regression/goto-analyzer/approx-const-fp-array-variable-struct-const-fp-with-zero/test.desc b/regression/goto-analyzer/approx-const-fp-array-variable-struct-const-fp-with-zero/test.desc index b687a13cf86..5d052a3dd17 100644 --- a/regression/goto-analyzer/approx-const-fp-array-variable-struct-const-fp-with-zero/test.desc +++ b/regression/goto-analyzer/approx-const-fp-array-variable-struct-const-fp-with-zero/test.desc @@ -2,18 +2,18 @@ CORE main.c --show-goto-functions --pointer-check ^Removal of function pointers and virtual functions$ -^\s*IF fp == f2 THEN GOTO [0-9]$ -^\s*IF fp == f3 THEN GOTO [0-9]$ -^\s*IF fp == f4 THEN GOTO [0-9]$ -^\s*ASSERT FALSE // invalid function pointer$ +^\s*IF .*::fp = address_of\(f2\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f3\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f4\) THEN GOTO [0-9]$ +^\s*ASSERT false // invalid function pointer$ ^EXIT=0$ ^SIGNAL=0$ -- ^warning: ignoring -^\s*IF fp == f1 THEN GOTO [0-9]$ -^\s*IF fp == f5 THEN GOTO [0-9]$ -^\s*IF fp == f6 THEN GOTO [0-9]$ -^\s*IF fp == f7 THEN GOTO [0-9]$ -^\s*IF fp == f8 THEN GOTO [0-9]$ -^\s*IF fp == f9 THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f1\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f5\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f6\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f7\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f8\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f9\) THEN GOTO [0-9]$ function \w+: replacing function pointer by 9 possible targets diff --git a/regression/goto-analyzer/dependence-graph10/test.desc b/regression/goto-analyzer/dependence-graph10/test.desc index 26943fc2e68..d079970cac5 100644 --- a/regression/goto-analyzer/dependence-graph10/test.desc +++ b/regression/goto-analyzer/dependence-graph10/test.desc @@ -5,9 +5,9 @@ activate-multi-line-match ^EXIT=0$ ^SIGNAL=0$ // First assignment has a control dependency on the if -\/\/ ([0-9]+).*\n.*IF.*i < 10.*THEN(.*\n)*Control dependencies: \1\n(.*\n){2,3}.*a = 1 +\/\/ ([0-9]+).*\n.*IF.*i < 10.*THEN(.*\n)*Control dependencies: \1\n(.*\n){2,3}.*a := 1 // Second assignment has a control dependency on the if -\/\/ ([0-9]+).*\n.*IF.*i < 10.*THEN(.*\n)*Control dependencies: \1\n(.*\n){2,3}.*a = 2 +\/\/ ([0-9]+).*\n.*IF.*i < 10.*THEN(.*\n)*Control dependencies: \1\n(.*\n){2,3}.*a := 2 -- ^warning: ignoring -- diff --git a/regression/goto-analyzer/dependence-graph11/test.desc b/regression/goto-analyzer/dependence-graph11/test.desc index 32969498ac0..efb84f1b68b 100644 --- a/regression/goto-analyzer/dependence-graph11/test.desc +++ b/regression/goto-analyzer/dependence-graph11/test.desc @@ -5,7 +5,7 @@ activate-multi-line-match ^EXIT=0$ ^SIGNAL=0$ // Assignment has a control dependency on the if -\/\/ ([0-9]+).*\n.*IF.*a < 10.*THEN(.*\n)*Control dependencies: \1\n(.*\n){2,3}.*a = 1 +\/\/ ([0-9]+).*\n.*IF.*a < 10.*THEN(.*\n)*Control dependencies: \1\n(.*\n){2,3}.*a := 1 -- ^warning: ignoring -- diff --git a/regression/goto-analyzer/dependence-graph12/test.desc b/regression/goto-analyzer/dependence-graph12/test.desc index 419f4efc4e1..886247aa9c6 100644 --- a/regression/goto-analyzer/dependence-graph12/test.desc +++ b/regression/goto-analyzer/dependence-graph12/test.desc @@ -5,9 +5,9 @@ activate-multi-line-match ^EXIT=0$ ^SIGNAL=0$ // Assignment has a control dependency on the first if -\/\/ ([0-9]+).*\n.*IF.*a < 7.*THEN(.*\n)*Control dependencies: (([0-9]+,\1)|(\1,[0-9]+))\n(.*\n){2,3}.*a = 2 +\/\/ ([0-9]+).*\n.*IF.*a < 7.*THEN(.*\n)*Control dependencies: (([0-9]+,\1)|(\1,[0-9]+))\n(.*\n){2,3}.*a := 2 // Assignment has a control dependency on the second if -\/\/ ([0-9]+).*\n.*IF.*a < 10.*THEN(.*\n)*Control dependencies: (([0-9]+,\1)|(\1,[0-9]+))\n(.*\n){2,3}.*a = 2 +\/\/ ([0-9]+).*\n.*IF.*a < 10.*THEN(.*\n)*Control dependencies: (([0-9]+,\1)|(\1,[0-9]+))\n(.*\n){2,3}.*a := 2 -- ^warning: ignoring -- diff --git a/regression/goto-analyzer/dependence-graph14/test.desc b/regression/goto-analyzer/dependence-graph14/test.desc index c00f0acd68a..e2d43d71192 100644 --- a/regression/goto-analyzer/dependence-graph14/test.desc +++ b/regression/goto-analyzer/dependence-graph14/test.desc @@ -4,9 +4,9 @@ main.c activate-multi-line-match ^EXIT=0$ ^SIGNAL=0$ -\/\/ ([0-9]+).*\n.*a\[(\(signed long( long)? int\))?2\] = 2;(.*\n)*Data dependencies: (\1)\n(.*\n){2,3}.*out = * +\/\/ ([0-9]+).*\n.*::a\[.*2.*\] := 2(.*\n)*Data dependencies: (\1)\n(.*\n){2,3}.*out := .* -- -\/\/ ([0-9]+).*\n.*a\[(\(signed long( long)? int\))?1\] = 1;(.*\n)*Data dependencies: (\1)\n(.*\n){2,3}.*out = * +\/\/ ([0-9]+).*\n.*::a\[.*1.*\] := 1(.*\n)*Data dependencies: (\1)\n(.*\n){2,3}.*out := .* ^warning: ignoring -- diff --git a/regression/goto-analyzer/dependence-graph4/test.desc b/regression/goto-analyzer/dependence-graph4/test.desc index 670220ddf98..37849b77ce7 100644 --- a/regression/goto-analyzer/dependence-graph4/test.desc +++ b/regression/goto-analyzer/dependence-graph4/test.desc @@ -4,7 +4,7 @@ main.c activate-multi-line-match ^EXIT=0$ ^SIGNAL=0$ -\/\/ ([0-9]+) file.*\n.*IF.*g_in1.*THEN GOTO(.*\n)*Control dependencies: \1\n\n.*\n.*g_out = 1 +\/\/ ([0-9]+) file.*\n.*IF.*g_in1.*THEN GOTO(.*\n)*Control dependencies: \1\n\n.*\n.*g_out := 1 -- ^warning: ignoring -- diff --git a/regression/goto-analyzer/dependence-graph7/test.desc b/regression/goto-analyzer/dependence-graph7/test.desc index 80a11db5a17..fbc0a0b72c4 100644 --- a/regression/goto-analyzer/dependence-graph7/test.desc +++ b/regression/goto-analyzer/dependence-graph7/test.desc @@ -5,7 +5,7 @@ activate-multi-line-match ^EXIT=0$ ^SIGNAL=0$ // Assignment has a control dependency on the loop head -\/\/ ([0-9]+).*\n.*IF.*i < 10.*THEN(.*\n)*Control dependencies: \1\n(.*\n){2,3}.*a = 1 +\/\/ ([0-9]+).*\n.*IF.*i < 10.*THEN(.*\n)*Control dependencies: \1\n(.*\n){2,3}.*a := 1 // Backedge has a control dependency on the loop head \/\/ ([0-9]+).*\n.*IF.*i < 10.*THEN(.*\n)*Control dependencies: \1\n(.*\n){2,3}\s*GOTO [0-9]+ // Loop head has a control dependency on itself diff --git a/regression/goto-analyzer/dependence-graph8/test.desc b/regression/goto-analyzer/dependence-graph8/test.desc index 50a092d6d9e..c6536ffd3ac 100644 --- a/regression/goto-analyzer/dependence-graph8/test.desc +++ b/regression/goto-analyzer/dependence-graph8/test.desc @@ -5,7 +5,7 @@ activate-multi-line-match ^EXIT=0$ ^SIGNAL=0$ // Assignment has a control dependency on the if -\/\/ ([0-9]+).*\n.*IF.*i < 7.*THEN(.*\n)*Control dependencies: \1\n(.*\n){2,3}.*a = 1 +\/\/ ([0-9]+).*\n.*IF.*i < 7.*THEN(.*\n)*Control dependencies: \1\n(.*\n){2,3}.*a := 1 // If has a control dependency on the loop head \/\/ ([0-9]+).*\n.*IF.*i < 10.*THEN(.*\n)*Control dependencies: \1\n(.*\n){2,3}.*i < 7 -- diff --git a/regression/goto-analyzer/dependence-graph9/test.desc b/regression/goto-analyzer/dependence-graph9/test.desc index c6dd50d71cb..cc445547750 100644 --- a/regression/goto-analyzer/dependence-graph9/test.desc +++ b/regression/goto-analyzer/dependence-graph9/test.desc @@ -5,11 +5,11 @@ activate-multi-line-match ^EXIT=0$ ^SIGNAL=0$ // Second assignment has a control dependency on the outer if -\/\/ ([0-9]+).*\n.*IF.*i < 10.*THEN(.*\n)*Control dependencies: \1\n(.*\n){2,3}.*a = 2 +\/\/ ([0-9]+).*\n.*IF.*i < 10.*THEN(.*\n)*Control dependencies: \1\n(.*\n){2,3}.*a := 2 -- ^warning: ignoring // Second assignment does not have a control dependency on the inner if -\/\/ ([0-9]+).*\n.*IF.*i < 7.*THEN(.*\n)*Control dependencies: \1\n(.*\n){2,3}.*a = 2 +\/\/ ([0-9]+).*\n.*IF.*i < 7.*THEN(.*\n)*Control dependencies: \1\n(.*\n){2,3}.*a := 2 -- The first regex above matches output portions like shown below (with being a location number). The intention is to check whether the assignment has a control diff --git a/regression/goto-analyzer/no-match-array-literal-const-fp-null/test.desc b/regression/goto-analyzer/no-match-array-literal-const-fp-null/test.desc index 25c0e72dadf..d42046c6e62 100644 --- a/regression/goto-analyzer/no-match-array-literal-const-fp-null/test.desc +++ b/regression/goto-analyzer/no-match-array-literal-const-fp-null/test.desc @@ -2,7 +2,7 @@ CORE main.c --show-goto-functions --pointer-check ^Removal of function pointers and virtual functions$ -^\s*ASSERT FALSE // invalid function pointer$ +^\s*ASSERT false // invalid function pointer$ ^EXIT=0$ ^SIGNAL=0$ function func: replacing function pointer by 0 possible targets diff --git a/regression/goto-analyzer/no-match-const-array-const-pointer-const-fp-const-lost/test.desc b/regression/goto-analyzer/no-match-const-array-const-pointer-const-fp-const-lost/test.desc index a439885fc9c..249a6403ecd 100644 --- a/regression/goto-analyzer/no-match-const-array-const-pointer-const-fp-const-lost/test.desc +++ b/regression/goto-analyzer/no-match-const-array-const-pointer-const-fp-const-lost/test.desc @@ -2,15 +2,15 @@ CORE main.c --show-goto-functions --pointer-check ^Removal of function pointers and virtual functions$ -^\s*IF \*fp == f1 THEN GOTO [0-9]$ -^\s*IF \*fp == f2 THEN GOTO [0-9]$ -^\s*IF \*fp == f3 THEN GOTO [0-9]$ -^\s*IF \*fp == f4 THEN GOTO [0-9]$ -^\s*IF \*fp == f5 THEN GOTO [0-9]$ -^\s*IF \*fp == f6 THEN GOTO [0-9]$ -^\s*IF \*fp == f7 THEN GOTO [0-9]$ -^\s*IF \*fp == f8 THEN GOTO [0-9]$ -^\s*IF \*fp == f9 THEN GOTO [0-9]$ +^\s*IF \*.*::fp = address_of\(f1\) THEN GOTO [0-9]$ +^\s*IF \*.*::fp = address_of\(f2\) THEN GOTO [0-9]$ +^\s*IF \*.*::fp = address_of\(f3\) THEN GOTO [0-9]$ +^\s*IF \*.*::fp = address_of\(f4\) THEN GOTO [0-9]$ +^\s*IF \*.*::fp = address_of\(f5\) THEN GOTO [0-9]$ +^\s*IF \*.*::fp = address_of\(f6\) THEN GOTO [0-9]$ +^\s*IF \*.*::fp = address_of\(f7\) THEN GOTO [0-9]$ +^\s*IF \*.*::fp = address_of\(f8\) THEN GOTO [0-9]$ +^\s*IF \*.*::fp = address_of\(f9\) THEN GOTO [0-9]$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/goto-analyzer/no-match-const-fp-array-literal-const-fp-run-time/test.desc b/regression/goto-analyzer/no-match-const-fp-array-literal-const-fp-run-time/test.desc index 9fc199c2365..2335ab71d77 100644 --- a/regression/goto-analyzer/no-match-const-fp-array-literal-const-fp-run-time/test.desc +++ b/regression/goto-analyzer/no-match-const-fp-array-literal-const-fp-run-time/test.desc @@ -2,15 +2,15 @@ CORE main.c --show-goto-functions --pointer-check ^Removal of function pointers and virtual functions$ -^\s*IF fp == f1 THEN GOTO [0-9]$ -^\s*IF fp == f2 THEN GOTO [0-9]$ -^\s*IF fp == f3 THEN GOTO [0-9]$ -^\s*IF fp == f4 THEN GOTO [0-9]$ -^\s*IF fp == f5 THEN GOTO [0-9]$ -^\s*IF fp == f6 THEN GOTO [0-9]$ -^\s*IF fp == f7 THEN GOTO [0-9]$ -^\s*IF fp == f8 THEN GOTO [0-9]$ -^\s*IF fp == f9 THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f1\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f2\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f3\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f4\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f5\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f6\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f7\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f8\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f9\) THEN GOTO [0-9]$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/goto-analyzer/no-match-const-fp-array-literal-non-const-fp-run-time/test.desc b/regression/goto-analyzer/no-match-const-fp-array-literal-non-const-fp-run-time/test.desc index 9fc199c2365..2335ab71d77 100644 --- a/regression/goto-analyzer/no-match-const-fp-array-literal-non-const-fp-run-time/test.desc +++ b/regression/goto-analyzer/no-match-const-fp-array-literal-non-const-fp-run-time/test.desc @@ -2,15 +2,15 @@ CORE main.c --show-goto-functions --pointer-check ^Removal of function pointers and virtual functions$ -^\s*IF fp == f1 THEN GOTO [0-9]$ -^\s*IF fp == f2 THEN GOTO [0-9]$ -^\s*IF fp == f3 THEN GOTO [0-9]$ -^\s*IF fp == f4 THEN GOTO [0-9]$ -^\s*IF fp == f5 THEN GOTO [0-9]$ -^\s*IF fp == f6 THEN GOTO [0-9]$ -^\s*IF fp == f7 THEN GOTO [0-9]$ -^\s*IF fp == f8 THEN GOTO [0-9]$ -^\s*IF fp == f9 THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f1\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f2\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f3\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f4\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f5\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f6\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f7\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f8\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f9\) THEN GOTO [0-9]$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/goto-analyzer/no-match-const-fp-array-literal-non-const-fp/test.desc b/regression/goto-analyzer/no-match-const-fp-array-literal-non-const-fp/test.desc index 1fb62392ced..3a415cc88c6 100644 --- a/regression/goto-analyzer/no-match-const-fp-array-literal-non-const-fp/test.desc +++ b/regression/goto-analyzer/no-match-const-fp-array-literal-non-const-fp/test.desc @@ -2,15 +2,15 @@ CORE main.c --show-goto-functions --pointer-check ^Removal of function pointers and virtual functions$ -^\s*IF fp2 == f1 THEN GOTO [0-9]$ -^\s*IF fp2 == f2 THEN GOTO [0-9]$ -^\s*IF fp2 == f3 THEN GOTO [0-9]$ -^\s*IF fp2 == f4 THEN GOTO [0-9]$ -^\s*IF fp2 == f5 THEN GOTO [0-9]$ -^\s*IF fp2 == f6 THEN GOTO [0-9]$ -^\s*IF fp2 == f7 THEN GOTO [0-9]$ -^\s*IF fp2 == f8 THEN GOTO [0-9]$ -^\s*IF fp2 == f9 THEN GOTO [0-9]$ +^\s*IF .*::fp2 = address_of\(f1\) THEN GOTO [0-9]$ +^\s*IF .*::fp2 = address_of\(f2\) THEN GOTO [0-9]$ +^\s*IF .*::fp2 = address_of\(f3\) THEN GOTO [0-9]$ +^\s*IF .*::fp2 = address_of\(f4\) THEN GOTO [0-9]$ +^\s*IF .*::fp2 = address_of\(f5\) THEN GOTO [0-9]$ +^\s*IF .*::fp2 = address_of\(f6\) THEN GOTO [0-9]$ +^\s*IF .*::fp2 = address_of\(f7\) THEN GOTO [0-9]$ +^\s*IF .*::fp2 = address_of\(f8\) THEN GOTO [0-9]$ +^\s*IF .*::fp2 = address_of\(f9\) THEN GOTO [0-9]$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/goto-analyzer/no-match-const-fp-array-non-const-fp/test.desc b/regression/goto-analyzer/no-match-const-fp-array-non-const-fp/test.desc index 1fb62392ced..3a415cc88c6 100644 --- a/regression/goto-analyzer/no-match-const-fp-array-non-const-fp/test.desc +++ b/regression/goto-analyzer/no-match-const-fp-array-non-const-fp/test.desc @@ -2,15 +2,15 @@ CORE main.c --show-goto-functions --pointer-check ^Removal of function pointers and virtual functions$ -^\s*IF fp2 == f1 THEN GOTO [0-9]$ -^\s*IF fp2 == f2 THEN GOTO [0-9]$ -^\s*IF fp2 == f3 THEN GOTO [0-9]$ -^\s*IF fp2 == f4 THEN GOTO [0-9]$ -^\s*IF fp2 == f5 THEN GOTO [0-9]$ -^\s*IF fp2 == f6 THEN GOTO [0-9]$ -^\s*IF fp2 == f7 THEN GOTO [0-9]$ -^\s*IF fp2 == f8 THEN GOTO [0-9]$ -^\s*IF fp2 == f9 THEN GOTO [0-9]$ +^\s*IF .*::fp2 = address_of\(f1\) THEN GOTO [0-9]$ +^\s*IF .*::fp2 = address_of\(f2\) THEN GOTO [0-9]$ +^\s*IF .*::fp2 = address_of\(f3\) THEN GOTO [0-9]$ +^\s*IF .*::fp2 = address_of\(f4\) THEN GOTO [0-9]$ +^\s*IF .*::fp2 = address_of\(f5\) THEN GOTO [0-9]$ +^\s*IF .*::fp2 = address_of\(f6\) THEN GOTO [0-9]$ +^\s*IF .*::fp2 = address_of\(f7\) THEN GOTO [0-9]$ +^\s*IF .*::fp2 = address_of\(f8\) THEN GOTO [0-9]$ +^\s*IF .*::fp2 = address_of\(f9\) THEN GOTO [0-9]$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/goto-analyzer/no-match-const-fp-binary-op-const-lost/test.desc b/regression/goto-analyzer/no-match-const-fp-binary-op-const-lost/test.desc index 9fc199c2365..2335ab71d77 100644 --- a/regression/goto-analyzer/no-match-const-fp-binary-op-const-lost/test.desc +++ b/regression/goto-analyzer/no-match-const-fp-binary-op-const-lost/test.desc @@ -2,15 +2,15 @@ CORE main.c --show-goto-functions --pointer-check ^Removal of function pointers and virtual functions$ -^\s*IF fp == f1 THEN GOTO [0-9]$ -^\s*IF fp == f2 THEN GOTO [0-9]$ -^\s*IF fp == f3 THEN GOTO [0-9]$ -^\s*IF fp == f4 THEN GOTO [0-9]$ -^\s*IF fp == f5 THEN GOTO [0-9]$ -^\s*IF fp == f6 THEN GOTO [0-9]$ -^\s*IF fp == f7 THEN GOTO [0-9]$ -^\s*IF fp == f8 THEN GOTO [0-9]$ -^\s*IF fp == f9 THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f1\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f2\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f3\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f4\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f5\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f6\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f7\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f8\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f9\) THEN GOTO [0-9]$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/goto-analyzer/no-match-const-fp-const-array-index-lost/test.desc b/regression/goto-analyzer/no-match-const-fp-const-array-index-lost/test.desc index a439885fc9c..249a6403ecd 100644 --- a/regression/goto-analyzer/no-match-const-fp-const-array-index-lost/test.desc +++ b/regression/goto-analyzer/no-match-const-fp-const-array-index-lost/test.desc @@ -2,15 +2,15 @@ CORE main.c --show-goto-functions --pointer-check ^Removal of function pointers and virtual functions$ -^\s*IF \*fp == f1 THEN GOTO [0-9]$ -^\s*IF \*fp == f2 THEN GOTO [0-9]$ -^\s*IF \*fp == f3 THEN GOTO [0-9]$ -^\s*IF \*fp == f4 THEN GOTO [0-9]$ -^\s*IF \*fp == f5 THEN GOTO [0-9]$ -^\s*IF \*fp == f6 THEN GOTO [0-9]$ -^\s*IF \*fp == f7 THEN GOTO [0-9]$ -^\s*IF \*fp == f8 THEN GOTO [0-9]$ -^\s*IF \*fp == f9 THEN GOTO [0-9]$ +^\s*IF \*.*::fp = address_of\(f1\) THEN GOTO [0-9]$ +^\s*IF \*.*::fp = address_of\(f2\) THEN GOTO [0-9]$ +^\s*IF \*.*::fp = address_of\(f3\) THEN GOTO [0-9]$ +^\s*IF \*.*::fp = address_of\(f4\) THEN GOTO [0-9]$ +^\s*IF \*.*::fp = address_of\(f5\) THEN GOTO [0-9]$ +^\s*IF \*.*::fp = address_of\(f6\) THEN GOTO [0-9]$ +^\s*IF \*.*::fp = address_of\(f7\) THEN GOTO [0-9]$ +^\s*IF \*.*::fp = address_of\(f8\) THEN GOTO [0-9]$ +^\s*IF \*.*::fp = address_of\(f9\) THEN GOTO [0-9]$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/goto-analyzer/no-match-const-fp-const-array-lost/test.desc b/regression/goto-analyzer/no-match-const-fp-const-array-lost/test.desc index a439885fc9c..249a6403ecd 100644 --- a/regression/goto-analyzer/no-match-const-fp-const-array-lost/test.desc +++ b/regression/goto-analyzer/no-match-const-fp-const-array-lost/test.desc @@ -2,15 +2,15 @@ CORE main.c --show-goto-functions --pointer-check ^Removal of function pointers and virtual functions$ -^\s*IF \*fp == f1 THEN GOTO [0-9]$ -^\s*IF \*fp == f2 THEN GOTO [0-9]$ -^\s*IF \*fp == f3 THEN GOTO [0-9]$ -^\s*IF \*fp == f4 THEN GOTO [0-9]$ -^\s*IF \*fp == f5 THEN GOTO [0-9]$ -^\s*IF \*fp == f6 THEN GOTO [0-9]$ -^\s*IF \*fp == f7 THEN GOTO [0-9]$ -^\s*IF \*fp == f8 THEN GOTO [0-9]$ -^\s*IF \*fp == f9 THEN GOTO [0-9]$ +^\s*IF \*.*::fp = address_of\(f1\) THEN GOTO [0-9]$ +^\s*IF \*.*::fp = address_of\(f2\) THEN GOTO [0-9]$ +^\s*IF \*.*::fp = address_of\(f3\) THEN GOTO [0-9]$ +^\s*IF \*.*::fp = address_of\(f4\) THEN GOTO [0-9]$ +^\s*IF \*.*::fp = address_of\(f5\) THEN GOTO [0-9]$ +^\s*IF \*.*::fp = address_of\(f6\) THEN GOTO [0-9]$ +^\s*IF \*.*::fp = address_of\(f7\) THEN GOTO [0-9]$ +^\s*IF \*.*::fp = address_of\(f8\) THEN GOTO [0-9]$ +^\s*IF \*.*::fp = address_of\(f9\) THEN GOTO [0-9]$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/goto-analyzer/no-match-const-fp-const-cast/test.desc b/regression/goto-analyzer/no-match-const-fp-const-cast/test.desc index 9fc199c2365..2335ab71d77 100644 --- a/regression/goto-analyzer/no-match-const-fp-const-cast/test.desc +++ b/regression/goto-analyzer/no-match-const-fp-const-cast/test.desc @@ -2,15 +2,15 @@ CORE main.c --show-goto-functions --pointer-check ^Removal of function pointers and virtual functions$ -^\s*IF fp == f1 THEN GOTO [0-9]$ -^\s*IF fp == f2 THEN GOTO [0-9]$ -^\s*IF fp == f3 THEN GOTO [0-9]$ -^\s*IF fp == f4 THEN GOTO [0-9]$ -^\s*IF fp == f5 THEN GOTO [0-9]$ -^\s*IF fp == f6 THEN GOTO [0-9]$ -^\s*IF fp == f7 THEN GOTO [0-9]$ -^\s*IF fp == f8 THEN GOTO [0-9]$ -^\s*IF fp == f9 THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f1\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f2\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f3\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f4\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f5\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f6\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f7\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f8\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f9\) THEN GOTO [0-9]$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/goto-analyzer/no-match-const-fp-const-fp-null/test.desc b/regression/goto-analyzer/no-match-const-fp-const-fp-null/test.desc index da6211eba82..6072f5b10f4 100644 --- a/regression/goto-analyzer/no-match-const-fp-const-fp-null/test.desc +++ b/regression/goto-analyzer/no-match-const-fp-const-fp-null/test.desc @@ -2,7 +2,7 @@ CORE main.c --show-goto-functions --pointer-check ^Removal of function pointers and virtual functions$ -^\s*ASSERT FALSE // invalid function pointer$ +^\s*ASSERT false // invalid function pointer$ ^EXIT=0$ ^SIGNAL=0$ replacing function pointer by 0 possible targets diff --git a/regression/goto-analyzer/no-match-const-fp-const-lost/test.desc b/regression/goto-analyzer/no-match-const-fp-const-lost/test.desc index 9fc199c2365..2335ab71d77 100644 --- a/regression/goto-analyzer/no-match-const-fp-const-lost/test.desc +++ b/regression/goto-analyzer/no-match-const-fp-const-lost/test.desc @@ -2,15 +2,15 @@ CORE main.c --show-goto-functions --pointer-check ^Removal of function pointers and virtual functions$ -^\s*IF fp == f1 THEN GOTO [0-9]$ -^\s*IF fp == f2 THEN GOTO [0-9]$ -^\s*IF fp == f3 THEN GOTO [0-9]$ -^\s*IF fp == f4 THEN GOTO [0-9]$ -^\s*IF fp == f5 THEN GOTO [0-9]$ -^\s*IF fp == f6 THEN GOTO [0-9]$ -^\s*IF fp == f7 THEN GOTO [0-9]$ -^\s*IF fp == f8 THEN GOTO [0-9]$ -^\s*IF fp == f9 THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f1\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f2\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f3\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f4\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f5\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f6\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f7\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f8\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f9\) THEN GOTO [0-9]$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/goto-analyzer/no-match-const-fp-const-pointer-const-struct-const-fp-null/test.desc b/regression/goto-analyzer/no-match-const-fp-const-pointer-const-struct-const-fp-null/test.desc index 24ca16f13c1..35d7e0bfdc0 100644 --- a/regression/goto-analyzer/no-match-const-fp-const-pointer-const-struct-const-fp-null/test.desc +++ b/regression/goto-analyzer/no-match-const-fp-const-pointer-const-struct-const-fp-null/test.desc @@ -2,7 +2,7 @@ CORE main.c --show-goto-functions --pointer-check ^Removal of function pointers and virtual functions$ -^\s*ASSERT FALSE // invalid function pointer$ +^\s*ASSERT false // invalid function pointer$ replacing function pointer by 9 possible targets ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-analyzer/no-match-const-fp-const-pointer-non-const-struct-const-fp/test.desc b/regression/goto-analyzer/no-match-const-fp-const-pointer-non-const-struct-const-fp/test.desc index 9fc199c2365..2335ab71d77 100644 --- a/regression/goto-analyzer/no-match-const-fp-const-pointer-non-const-struct-const-fp/test.desc +++ b/regression/goto-analyzer/no-match-const-fp-const-pointer-non-const-struct-const-fp/test.desc @@ -2,15 +2,15 @@ CORE main.c --show-goto-functions --pointer-check ^Removal of function pointers and virtual functions$ -^\s*IF fp == f1 THEN GOTO [0-9]$ -^\s*IF fp == f2 THEN GOTO [0-9]$ -^\s*IF fp == f3 THEN GOTO [0-9]$ -^\s*IF fp == f4 THEN GOTO [0-9]$ -^\s*IF fp == f5 THEN GOTO [0-9]$ -^\s*IF fp == f6 THEN GOTO [0-9]$ -^\s*IF fp == f7 THEN GOTO [0-9]$ -^\s*IF fp == f8 THEN GOTO [0-9]$ -^\s*IF fp == f9 THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f1\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f2\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f3\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f4\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f5\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f6\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f7\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f8\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f9\) THEN GOTO [0-9]$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/goto-analyzer/no-match-const-fp-dereference-const-pointer-null/test.desc b/regression/goto-analyzer/no-match-const-fp-dereference-const-pointer-null/test.desc index 24ca16f13c1..35d7e0bfdc0 100644 --- a/regression/goto-analyzer/no-match-const-fp-dereference-const-pointer-null/test.desc +++ b/regression/goto-analyzer/no-match-const-fp-dereference-const-pointer-null/test.desc @@ -2,7 +2,7 @@ CORE main.c --show-goto-functions --pointer-check ^Removal of function pointers and virtual functions$ -^\s*ASSERT FALSE // invalid function pointer$ +^\s*ASSERT false // invalid function pointer$ replacing function pointer by 9 possible targets ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-analyzer/no-match-const-fp-dereference-non-const-pointer-const-fp/test.desc b/regression/goto-analyzer/no-match-const-fp-dereference-non-const-pointer-const-fp/test.desc index 4b204902e0b..30fd992061e 100644 --- a/regression/goto-analyzer/no-match-const-fp-dereference-non-const-pointer-const-fp/test.desc +++ b/regression/goto-analyzer/no-match-const-fp-dereference-non-const-pointer-const-fp/test.desc @@ -2,15 +2,15 @@ CORE main.c --show-goto-functions --pointer-check ^Removal of function pointers and virtual functions$ -^\s*IF final_fp == f1 THEN GOTO [0-9]$ -^\s*IF final_fp == f2 THEN GOTO [0-9]$ -^\s*IF final_fp == f3 THEN GOTO [0-9]$ -^\s*IF final_fp == f4 THEN GOTO [0-9]$ -^\s*IF final_fp == f5 THEN GOTO [0-9]$ -^\s*IF final_fp == f6 THEN GOTO [0-9]$ -^\s*IF final_fp == f7 THEN GOTO [0-9]$ -^\s*IF final_fp == f8 THEN GOTO [0-9]$ -^\s*IF final_fp == f9 THEN GOTO [0-9]$ +^\s*IF .*::final_fp = address_of\(f1\) THEN GOTO [0-9]$ +^\s*IF .*::final_fp = address_of\(f2\) THEN GOTO [0-9]$ +^\s*IF .*::final_fp = address_of\(f3\) THEN GOTO [0-9]$ +^\s*IF .*::final_fp = address_of\(f4\) THEN GOTO [0-9]$ +^\s*IF .*::final_fp = address_of\(f5\) THEN GOTO [0-9]$ +^\s*IF .*::final_fp = address_of\(f6\) THEN GOTO [0-9]$ +^\s*IF .*::final_fp = address_of\(f7\) THEN GOTO [0-9]$ +^\s*IF .*::final_fp = address_of\(f8\) THEN GOTO [0-9]$ +^\s*IF .*::final_fp = address_of\(f9\) THEN GOTO [0-9]$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/goto-analyzer/no-match-const-fp-dynamic-array-non-const-fp/test.desc b/regression/goto-analyzer/no-match-const-fp-dynamic-array-non-const-fp/test.desc index c1c2246e027..4548ea5c4c8 100644 --- a/regression/goto-analyzer/no-match-const-fp-dynamic-array-non-const-fp/test.desc +++ b/regression/goto-analyzer/no-match-const-fp-dynamic-array-non-const-fp/test.desc @@ -2,15 +2,15 @@ CORE main.c --show-goto-functions --pointer-check ^Removal of function pointers and virtual functions$ -^\s*IF fp == f1 THEN GOTO [0-9]+$ -^\s*IF fp == f2 THEN GOTO [0-9]+$ -^\s*IF fp == f3 THEN GOTO [0-9]+$ -^\s*IF fp == f4 THEN GOTO [0-9]+$ -^\s*IF fp == f5 THEN GOTO [0-9]+$ -^\s*IF fp == f6 THEN GOTO [0-9]+$ -^\s*IF fp == f7 THEN GOTO [0-9]+$ -^\s*IF fp == f8 THEN GOTO [0-9]+$ -^\s*IF fp == f9 THEN GOTO [0-9]+$ +^\s*IF .*::fp = address_of\(f1\) THEN GOTO [0-9]+$ +^\s*IF .*::fp = address_of\(f2\) THEN GOTO [0-9]+$ +^\s*IF .*::fp = address_of\(f3\) THEN GOTO [0-9]+$ +^\s*IF .*::fp = address_of\(f4\) THEN GOTO [0-9]+$ +^\s*IF .*::fp = address_of\(f5\) THEN GOTO [0-9]+$ +^\s*IF .*::fp = address_of\(f6\) THEN GOTO [0-9]+$ +^\s*IF .*::fp = address_of\(f7\) THEN GOTO [0-9]+$ +^\s*IF .*::fp = address_of\(f8\) THEN GOTO [0-9]+$ +^\s*IF .*::fp = address_of\(f9\) THEN GOTO [0-9]+$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/goto-analyzer/no-match-const-fp-non-const-fp-direct-assignment/test.desc b/regression/goto-analyzer/no-match-const-fp-non-const-fp-direct-assignment/test.desc index 1fb62392ced..3a415cc88c6 100644 --- a/regression/goto-analyzer/no-match-const-fp-non-const-fp-direct-assignment/test.desc +++ b/regression/goto-analyzer/no-match-const-fp-non-const-fp-direct-assignment/test.desc @@ -2,15 +2,15 @@ CORE main.c --show-goto-functions --pointer-check ^Removal of function pointers and virtual functions$ -^\s*IF fp2 == f1 THEN GOTO [0-9]$ -^\s*IF fp2 == f2 THEN GOTO [0-9]$ -^\s*IF fp2 == f3 THEN GOTO [0-9]$ -^\s*IF fp2 == f4 THEN GOTO [0-9]$ -^\s*IF fp2 == f5 THEN GOTO [0-9]$ -^\s*IF fp2 == f6 THEN GOTO [0-9]$ -^\s*IF fp2 == f7 THEN GOTO [0-9]$ -^\s*IF fp2 == f8 THEN GOTO [0-9]$ -^\s*IF fp2 == f9 THEN GOTO [0-9]$ +^\s*IF .*::fp2 = address_of\(f1\) THEN GOTO [0-9]$ +^\s*IF .*::fp2 = address_of\(f2\) THEN GOTO [0-9]$ +^\s*IF .*::fp2 = address_of\(f3\) THEN GOTO [0-9]$ +^\s*IF .*::fp2 = address_of\(f4\) THEN GOTO [0-9]$ +^\s*IF .*::fp2 = address_of\(f5\) THEN GOTO [0-9]$ +^\s*IF .*::fp2 = address_of\(f6\) THEN GOTO [0-9]$ +^\s*IF .*::fp2 = address_of\(f7\) THEN GOTO [0-9]$ +^\s*IF .*::fp2 = address_of\(f8\) THEN GOTO [0-9]$ +^\s*IF .*::fp2 = address_of\(f9\) THEN GOTO [0-9]$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/goto-analyzer/no-match-const-fp-non-const-pointer-non-const-struct-const-fp/test.desc b/regression/goto-analyzer/no-match-const-fp-non-const-pointer-non-const-struct-const-fp/test.desc index 9fc199c2365..2335ab71d77 100644 --- a/regression/goto-analyzer/no-match-const-fp-non-const-pointer-non-const-struct-const-fp/test.desc +++ b/regression/goto-analyzer/no-match-const-fp-non-const-pointer-non-const-struct-const-fp/test.desc @@ -2,15 +2,15 @@ CORE main.c --show-goto-functions --pointer-check ^Removal of function pointers and virtual functions$ -^\s*IF fp == f1 THEN GOTO [0-9]$ -^\s*IF fp == f2 THEN GOTO [0-9]$ -^\s*IF fp == f3 THEN GOTO [0-9]$ -^\s*IF fp == f4 THEN GOTO [0-9]$ -^\s*IF fp == f5 THEN GOTO [0-9]$ -^\s*IF fp == f6 THEN GOTO [0-9]$ -^\s*IF fp == f7 THEN GOTO [0-9]$ -^\s*IF fp == f8 THEN GOTO [0-9]$ -^\s*IF fp == f9 THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f1\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f2\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f3\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f4\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f5\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f6\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f7\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f8\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f9\) THEN GOTO [0-9]$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/goto-analyzer/no-match-const-fp-non-const-struct-const-fp/test.desc b/regression/goto-analyzer/no-match-const-fp-non-const-struct-const-fp/test.desc index 9fc199c2365..2335ab71d77 100644 --- a/regression/goto-analyzer/no-match-const-fp-non-const-struct-const-fp/test.desc +++ b/regression/goto-analyzer/no-match-const-fp-non-const-struct-const-fp/test.desc @@ -2,15 +2,15 @@ CORE main.c --show-goto-functions --pointer-check ^Removal of function pointers and virtual functions$ -^\s*IF fp == f1 THEN GOTO [0-9]$ -^\s*IF fp == f2 THEN GOTO [0-9]$ -^\s*IF fp == f3 THEN GOTO [0-9]$ -^\s*IF fp == f4 THEN GOTO [0-9]$ -^\s*IF fp == f5 THEN GOTO [0-9]$ -^\s*IF fp == f6 THEN GOTO [0-9]$ -^\s*IF fp == f7 THEN GOTO [0-9]$ -^\s*IF fp == f8 THEN GOTO [0-9]$ -^\s*IF fp == f9 THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f1\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f2\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f3\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f4\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f5\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f6\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f7\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f8\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f9\) THEN GOTO [0-9]$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/goto-analyzer/no-match-const-fp-non-const-struct-non-const-fp/test.desc b/regression/goto-analyzer/no-match-const-fp-non-const-struct-non-const-fp/test.desc index 9fc199c2365..2335ab71d77 100644 --- a/regression/goto-analyzer/no-match-const-fp-non-const-struct-non-const-fp/test.desc +++ b/regression/goto-analyzer/no-match-const-fp-non-const-struct-non-const-fp/test.desc @@ -2,15 +2,15 @@ CORE main.c --show-goto-functions --pointer-check ^Removal of function pointers and virtual functions$ -^\s*IF fp == f1 THEN GOTO [0-9]$ -^\s*IF fp == f2 THEN GOTO [0-9]$ -^\s*IF fp == f3 THEN GOTO [0-9]$ -^\s*IF fp == f4 THEN GOTO [0-9]$ -^\s*IF fp == f5 THEN GOTO [0-9]$ -^\s*IF fp == f6 THEN GOTO [0-9]$ -^\s*IF fp == f7 THEN GOTO [0-9]$ -^\s*IF fp == f8 THEN GOTO [0-9]$ -^\s*IF fp == f9 THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f1\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f2\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f3\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f4\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f5\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f6\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f7\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f8\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f9\) THEN GOTO [0-9]$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/goto-analyzer/no-match-const-fp-null/test.desc b/regression/goto-analyzer/no-match-const-fp-null/test.desc index 0abb9994d73..9fdf5e55158 100644 --- a/regression/goto-analyzer/no-match-const-fp-null/test.desc +++ b/regression/goto-analyzer/no-match-const-fp-null/test.desc @@ -2,7 +2,7 @@ CORE main.c --show-goto-functions --pointer-check ^Removal of function pointers and virtual functions$ -^\s*ASSERT FALSE // invalid function pointer$ +^\s*ASSERT false // invalid function pointer$ function func: replacing function pointer by 0 possible targets ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-analyzer/no-match-const-fp-ternerary-op-const-lost/test.desc b/regression/goto-analyzer/no-match-const-fp-ternerary-op-const-lost/test.desc index 9fc199c2365..2335ab71d77 100644 --- a/regression/goto-analyzer/no-match-const-fp-ternerary-op-const-lost/test.desc +++ b/regression/goto-analyzer/no-match-const-fp-ternerary-op-const-lost/test.desc @@ -2,15 +2,15 @@ CORE main.c --show-goto-functions --pointer-check ^Removal of function pointers and virtual functions$ -^\s*IF fp == f1 THEN GOTO [0-9]$ -^\s*IF fp == f2 THEN GOTO [0-9]$ -^\s*IF fp == f3 THEN GOTO [0-9]$ -^\s*IF fp == f4 THEN GOTO [0-9]$ -^\s*IF fp == f5 THEN GOTO [0-9]$ -^\s*IF fp == f6 THEN GOTO [0-9]$ -^\s*IF fp == f7 THEN GOTO [0-9]$ -^\s*IF fp == f8 THEN GOTO [0-9]$ -^\s*IF fp == f9 THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f1\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f2\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f3\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f4\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f5\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f6\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f7\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f8\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f9\) THEN GOTO [0-9]$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/goto-analyzer/no-match-const-pointer-const-struct-const-fp-const-cast/test.desc b/regression/goto-analyzer/no-match-const-pointer-const-struct-const-fp-const-cast/test.desc index 39b4bf06fa6..83bb08b57d9 100644 --- a/regression/goto-analyzer/no-match-const-pointer-const-struct-const-fp-const-cast/test.desc +++ b/regression/goto-analyzer/no-match-const-pointer-const-struct-const-fp-const-cast/test.desc @@ -2,15 +2,15 @@ CORE main.c --show-goto-functions --pointer-check ^Removal of function pointers and virtual functions$ -^\s*IF container_pointer->fp == f1 THEN GOTO [0-9]$ -^\s*IF container_pointer->fp == f2 THEN GOTO [0-9]$ -^\s*IF container_pointer->fp == f3 THEN GOTO [0-9]$ -^\s*IF container_pointer->fp == f4 THEN GOTO [0-9]$ -^\s*IF container_pointer->fp == f5 THEN GOTO [0-9]$ -^\s*IF container_pointer->fp == f6 THEN GOTO [0-9]$ -^\s*IF container_pointer->fp == f7 THEN GOTO [0-9]$ -^\s*IF container_pointer->fp == f8 THEN GOTO [0-9]$ -^\s*IF container_pointer->fp == f9 THEN GOTO [0-9]$ +^\s*IF .*container_pointer\.fp = address_of\(f1\) THEN GOTO [0-9]$ +^\s*IF .*container_pointer\.fp = address_of\(f2\) THEN GOTO [0-9]$ +^\s*IF .*container_pointer\.fp = address_of\(f3\) THEN GOTO [0-9]$ +^\s*IF .*container_pointer\.fp = address_of\(f4\) THEN GOTO [0-9]$ +^\s*IF .*container_pointer\.fp = address_of\(f5\) THEN GOTO [0-9]$ +^\s*IF .*container_pointer\.fp = address_of\(f6\) THEN GOTO [0-9]$ +^\s*IF .*container_pointer\.fp = address_of\(f7\) THEN GOTO [0-9]$ +^\s*IF .*container_pointer\.fp = address_of\(f8\) THEN GOTO [0-9]$ +^\s*IF .*container_pointer\.fp = address_of\(f9\) THEN GOTO [0-9]$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/goto-analyzer/no-match-const-pointer-non-const-struct-const-fp/test.desc b/regression/goto-analyzer/no-match-const-pointer-non-const-struct-const-fp/test.desc index c2854d7bb90..32128bfe112 100644 --- a/regression/goto-analyzer/no-match-const-pointer-non-const-struct-const-fp/test.desc +++ b/regression/goto-analyzer/no-match-const-pointer-non-const-struct-const-fp/test.desc @@ -2,15 +2,15 @@ CORE main.c --show-goto-functions --pointer-check ^Removal of function pointers and virtual functions$ -^\s*IF pts->go == f1 THEN GOTO [0-9]$ -^\s*IF pts->go == f2 THEN GOTO [0-9]$ -^\s*IF pts->go == f3 THEN GOTO [0-9]$ -^\s*IF pts->go == f4 THEN GOTO [0-9]$ -^\s*IF pts->go == f5 THEN GOTO [0-9]$ -^\s*IF pts->go == f6 THEN GOTO [0-9]$ -^\s*IF pts->go == f7 THEN GOTO [0-9]$ -^\s*IF pts->go == f8 THEN GOTO [0-9]$ -^\s*IF pts->go == f9 THEN GOTO [0-9]$ +^\s*IF .*pts\.go = address_of\(f1\) THEN GOTO [0-9]$ +^\s*IF .*pts\.go = address_of\(f2\) THEN GOTO [0-9]$ +^\s*IF .*pts\.go = address_of\(f3\) THEN GOTO [0-9]$ +^\s*IF .*pts\.go = address_of\(f4\) THEN GOTO [0-9]$ +^\s*IF .*pts\.go = address_of\(f5\) THEN GOTO [0-9]$ +^\s*IF .*pts\.go = address_of\(f6\) THEN GOTO [0-9]$ +^\s*IF .*pts\.go = address_of\(f7\) THEN GOTO [0-9]$ +^\s*IF .*pts\.go = address_of\(f8\) THEN GOTO [0-9]$ +^\s*IF .*pts\.go = address_of\(f9\) THEN GOTO [0-9]$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/goto-analyzer/no-match-const-struct-non-const-fp-null/test.desc b/regression/goto-analyzer/no-match-const-struct-non-const-fp-null/test.desc index da6211eba82..6072f5b10f4 100644 --- a/regression/goto-analyzer/no-match-const-struct-non-const-fp-null/test.desc +++ b/regression/goto-analyzer/no-match-const-struct-non-const-fp-null/test.desc @@ -2,7 +2,7 @@ CORE main.c --show-goto-functions --pointer-check ^Removal of function pointers and virtual functions$ -^\s*ASSERT FALSE // invalid function pointer$ +^\s*ASSERT false // invalid function pointer$ ^EXIT=0$ ^SIGNAL=0$ replacing function pointer by 0 possible targets diff --git a/regression/goto-analyzer/no-match-dereference-const-pointer-const-array-literal-pointer-const-fp/test.desc b/regression/goto-analyzer/no-match-dereference-const-pointer-const-array-literal-pointer-const-fp/test.desc index 63c375d058a..90e20e43fc4 100644 --- a/regression/goto-analyzer/no-match-dereference-const-pointer-const-array-literal-pointer-const-fp/test.desc +++ b/regression/goto-analyzer/no-match-dereference-const-pointer-const-array-literal-pointer-const-fp/test.desc @@ -2,15 +2,15 @@ CORE main.c --show-goto-functions --pointer-check ^Removal of function pointers and virtual functions$ -^\s*IF \*container_ptr->fp_tbl\[.*1\] == f1 THEN GOTO [0-9]$ -^\s*IF \*container_ptr->fp_tbl\[.*1\] == f2 THEN GOTO [0-9]$ -^\s*IF \*container_ptr->fp_tbl\[.*1\] == f3 THEN GOTO [0-9]$ -^\s*IF \*container_ptr->fp_tbl\[.*1\] == f4 THEN GOTO [0-9]$ -^\s*IF \*container_ptr->fp_tbl\[.*1\] == f5 THEN GOTO [0-9]$ -^\s*IF \*container_ptr->fp_tbl\[.*1\] == f6 THEN GOTO [0-9]$ -^\s*IF \*container_ptr->fp_tbl\[.*1\] == f7 THEN GOTO [0-9]$ -^\s*IF \*container_ptr->fp_tbl\[.*1\] == f8 THEN GOTO [0-9]$ -^\s*IF \*container_ptr->fp_tbl\[.*1\] == f9 THEN GOTO [0-9]$ +^\s*IF \*\(.*::container_ptr.fp_tbl\[.*1.*\]\) = address_of\(f1\) THEN GOTO [0-9]$ +^\s*IF \*\(.*::container_ptr.fp_tbl\[.*1.*\]\) = address_of\(f2\) THEN GOTO [0-9]$ +^\s*IF \*\(.*::container_ptr.fp_tbl\[.*1.*\]\) = address_of\(f3\) THEN GOTO [0-9]$ +^\s*IF \*\(.*::container_ptr.fp_tbl\[.*1.*\]\) = address_of\(f4\) THEN GOTO [0-9]$ +^\s*IF \*\(.*::container_ptr.fp_tbl\[.*1.*\]\) = address_of\(f5\) THEN GOTO [0-9]$ +^\s*IF \*\(.*::container_ptr.fp_tbl\[.*1.*\]\) = address_of\(f6\) THEN GOTO [0-9]$ +^\s*IF \*\(.*::container_ptr.fp_tbl\[.*1.*\]\) = address_of\(f7\) THEN GOTO [0-9]$ +^\s*IF \*\(.*::container_ptr.fp_tbl\[.*1.*\]\) = address_of\(f8\) THEN GOTO [0-9]$ +^\s*IF \*\(.*::container_ptr.fp_tbl\[.*1.*\]\) = address_of\(f9\) THEN GOTO [0-9]$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/goto-analyzer/no-match-dereference-non-const-struct-const-pointer-const-fp/test.desc b/regression/goto-analyzer/no-match-dereference-non-const-struct-const-pointer-const-fp/test.desc index 7c7f7c5d265..7bb43ba7876 100644 --- a/regression/goto-analyzer/no-match-dereference-non-const-struct-const-pointer-const-fp/test.desc +++ b/regression/goto-analyzer/no-match-dereference-non-const-struct-const-pointer-const-fp/test.desc @@ -2,15 +2,15 @@ CORE main.c --show-goto-functions --pointer-check ^Removal of function pointers and virtual functions$ -^\s*IF \*container_container\.container == f1 THEN GOTO [0-9]$ -^\s*IF \*container_container\.container == f2 THEN GOTO [0-9]$ -^\s*IF \*container_container\.container == f3 THEN GOTO [0-9]$ -^\s*IF \*container_container\.container == f4 THEN GOTO [0-9]$ -^\s*IF \*container_container\.container == f5 THEN GOTO [0-9]$ -^\s*IF \*container_container\.container == f6 THEN GOTO [0-9]$ -^\s*IF \*container_container\.container == f7 THEN GOTO [0-9]$ -^\s*IF \*container_container\.container == f8 THEN GOTO [0-9]$ -^\s*IF \*container_container\.container == f9 THEN GOTO [0-9]$ +^\s*IF \*\(.*::container_container\.container\) = address_of\(f1\) THEN GOTO [0-9]$ +^\s*IF \*\(.*::container_container\.container\) = address_of\(f2\) THEN GOTO [0-9]$ +^\s*IF \*\(.*::container_container\.container\) = address_of\(f3\) THEN GOTO [0-9]$ +^\s*IF \*\(.*::container_container\.container\) = address_of\(f4\) THEN GOTO [0-9]$ +^\s*IF \*\(.*::container_container\.container\) = address_of\(f5\) THEN GOTO [0-9]$ +^\s*IF \*\(.*::container_container\.container\) = address_of\(f6\) THEN GOTO [0-9]$ +^\s*IF \*\(.*::container_container\.container\) = address_of\(f7\) THEN GOTO [0-9]$ +^\s*IF \*\(.*::container_container\.container\) = address_of\(f8\) THEN GOTO [0-9]$ +^\s*IF \*\(.*::container_container\.container\) = address_of\(f9\) THEN GOTO [0-9]$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/goto-analyzer/no-match-dereference-non-const-struct-non-const-pointer-const-fp/test.desc b/regression/goto-analyzer/no-match-dereference-non-const-struct-non-const-pointer-const-fp/test.desc index 7c7f7c5d265..7bb43ba7876 100644 --- a/regression/goto-analyzer/no-match-dereference-non-const-struct-non-const-pointer-const-fp/test.desc +++ b/regression/goto-analyzer/no-match-dereference-non-const-struct-non-const-pointer-const-fp/test.desc @@ -2,15 +2,15 @@ CORE main.c --show-goto-functions --pointer-check ^Removal of function pointers and virtual functions$ -^\s*IF \*container_container\.container == f1 THEN GOTO [0-9]$ -^\s*IF \*container_container\.container == f2 THEN GOTO [0-9]$ -^\s*IF \*container_container\.container == f3 THEN GOTO [0-9]$ -^\s*IF \*container_container\.container == f4 THEN GOTO [0-9]$ -^\s*IF \*container_container\.container == f5 THEN GOTO [0-9]$ -^\s*IF \*container_container\.container == f6 THEN GOTO [0-9]$ -^\s*IF \*container_container\.container == f7 THEN GOTO [0-9]$ -^\s*IF \*container_container\.container == f8 THEN GOTO [0-9]$ -^\s*IF \*container_container\.container == f9 THEN GOTO [0-9]$ +^\s*IF \*\(.*::container_container\.container\) = address_of\(f1\) THEN GOTO [0-9]$ +^\s*IF \*\(.*::container_container\.container\) = address_of\(f2\) THEN GOTO [0-9]$ +^\s*IF \*\(.*::container_container\.container\) = address_of\(f3\) THEN GOTO [0-9]$ +^\s*IF \*\(.*::container_container\.container\) = address_of\(f4\) THEN GOTO [0-9]$ +^\s*IF \*\(.*::container_container\.container\) = address_of\(f5\) THEN GOTO [0-9]$ +^\s*IF \*\(.*::container_container\.container\) = address_of\(f6\) THEN GOTO [0-9]$ +^\s*IF \*\(.*::container_container\.container\) = address_of\(f7\) THEN GOTO [0-9]$ +^\s*IF \*\(.*::container_container\.container\) = address_of\(f8\) THEN GOTO [0-9]$ +^\s*IF \*\(.*::container_container\.container\) = address_of\(f9\) THEN GOTO [0-9]$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/goto-analyzer/no-match-non-const-fp-const-fp-direct-assignment/test.desc b/regression/goto-analyzer/no-match-non-const-fp-const-fp-direct-assignment/test.desc index 1fb62392ced..3a415cc88c6 100644 --- a/regression/goto-analyzer/no-match-non-const-fp-const-fp-direct-assignment/test.desc +++ b/regression/goto-analyzer/no-match-non-const-fp-const-fp-direct-assignment/test.desc @@ -2,15 +2,15 @@ CORE main.c --show-goto-functions --pointer-check ^Removal of function pointers and virtual functions$ -^\s*IF fp2 == f1 THEN GOTO [0-9]$ -^\s*IF fp2 == f2 THEN GOTO [0-9]$ -^\s*IF fp2 == f3 THEN GOTO [0-9]$ -^\s*IF fp2 == f4 THEN GOTO [0-9]$ -^\s*IF fp2 == f5 THEN GOTO [0-9]$ -^\s*IF fp2 == f6 THEN GOTO [0-9]$ -^\s*IF fp2 == f7 THEN GOTO [0-9]$ -^\s*IF fp2 == f8 THEN GOTO [0-9]$ -^\s*IF fp2 == f9 THEN GOTO [0-9]$ +^\s*IF .*::fp2 = address_of\(f1\) THEN GOTO [0-9]$ +^\s*IF .*::fp2 = address_of\(f2\) THEN GOTO [0-9]$ +^\s*IF .*::fp2 = address_of\(f3\) THEN GOTO [0-9]$ +^\s*IF .*::fp2 = address_of\(f4\) THEN GOTO [0-9]$ +^\s*IF .*::fp2 = address_of\(f5\) THEN GOTO [0-9]$ +^\s*IF .*::fp2 = address_of\(f6\) THEN GOTO [0-9]$ +^\s*IF .*::fp2 = address_of\(f7\) THEN GOTO [0-9]$ +^\s*IF .*::fp2 = address_of\(f8\) THEN GOTO [0-9]$ +^\s*IF .*::fp2 = address_of\(f9\) THEN GOTO [0-9]$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/goto-analyzer/no-match-non-const-fp/test.desc b/regression/goto-analyzer/no-match-non-const-fp/test.desc index 9fc199c2365..2335ab71d77 100644 --- a/regression/goto-analyzer/no-match-non-const-fp/test.desc +++ b/regression/goto-analyzer/no-match-non-const-fp/test.desc @@ -2,15 +2,15 @@ CORE main.c --show-goto-functions --pointer-check ^Removal of function pointers and virtual functions$ -^\s*IF fp == f1 THEN GOTO [0-9]$ -^\s*IF fp == f2 THEN GOTO [0-9]$ -^\s*IF fp == f3 THEN GOTO [0-9]$ -^\s*IF fp == f4 THEN GOTO [0-9]$ -^\s*IF fp == f5 THEN GOTO [0-9]$ -^\s*IF fp == f6 THEN GOTO [0-9]$ -^\s*IF fp == f7 THEN GOTO [0-9]$ -^\s*IF fp == f8 THEN GOTO [0-9]$ -^\s*IF fp == f9 THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f1\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f2\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f3\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f4\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f5\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f6\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f7\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f8\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f9\) THEN GOTO [0-9]$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/goto-analyzer/no-match-parameter-const-fp/test.desc b/regression/goto-analyzer/no-match-parameter-const-fp/test.desc index 9fc199c2365..2335ab71d77 100644 --- a/regression/goto-analyzer/no-match-parameter-const-fp/test.desc +++ b/regression/goto-analyzer/no-match-parameter-const-fp/test.desc @@ -2,15 +2,15 @@ CORE main.c --show-goto-functions --pointer-check ^Removal of function pointers and virtual functions$ -^\s*IF fp == f1 THEN GOTO [0-9]$ -^\s*IF fp == f2 THEN GOTO [0-9]$ -^\s*IF fp == f3 THEN GOTO [0-9]$ -^\s*IF fp == f4 THEN GOTO [0-9]$ -^\s*IF fp == f5 THEN GOTO [0-9]$ -^\s*IF fp == f6 THEN GOTO [0-9]$ -^\s*IF fp == f7 THEN GOTO [0-9]$ -^\s*IF fp == f8 THEN GOTO [0-9]$ -^\s*IF fp == f9 THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f1\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f2\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f3\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f4\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f5\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f6\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f7\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f8\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f9\) THEN GOTO [0-9]$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/goto-analyzer/no-match-parameter-fp/test.desc b/regression/goto-analyzer/no-match-parameter-fp/test.desc index 9fc199c2365..2335ab71d77 100644 --- a/regression/goto-analyzer/no-match-parameter-fp/test.desc +++ b/regression/goto-analyzer/no-match-parameter-fp/test.desc @@ -2,15 +2,15 @@ CORE main.c --show-goto-functions --pointer-check ^Removal of function pointers and virtual functions$ -^\s*IF fp == f1 THEN GOTO [0-9]$ -^\s*IF fp == f2 THEN GOTO [0-9]$ -^\s*IF fp == f3 THEN GOTO [0-9]$ -^\s*IF fp == f4 THEN GOTO [0-9]$ -^\s*IF fp == f5 THEN GOTO [0-9]$ -^\s*IF fp == f6 THEN GOTO [0-9]$ -^\s*IF fp == f7 THEN GOTO [0-9]$ -^\s*IF fp == f8 THEN GOTO [0-9]$ -^\s*IF fp == f9 THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f1\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f2\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f3\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f4\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f5\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f6\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f7\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f8\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f9\) THEN GOTO [0-9]$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/goto-analyzer/no-match-pointer-const-struct-array-literal-non-const-fp/test.desc b/regression/goto-analyzer/no-match-pointer-const-struct-array-literal-non-const-fp/test.desc index ca24699d5a0..5dd35ba8d55 100644 --- a/regression/goto-analyzer/no-match-pointer-const-struct-array-literal-non-const-fp/test.desc +++ b/regression/goto-analyzer/no-match-pointer-const-struct-array-literal-non-const-fp/test.desc @@ -2,15 +2,15 @@ CORE main.c --show-goto-functions --pointer-check ^Removal of function pointers and virtual functions$ -^\s*IF container_ptr->fp_tbl\[.*1\] == f1 THEN GOTO [0-9]$ -^\s*IF container_ptr->fp_tbl\[.*1\] == f2 THEN GOTO [0-9]$ -^\s*IF container_ptr->fp_tbl\[.*1\] == f3 THEN GOTO [0-9]$ -^\s*IF container_ptr->fp_tbl\[.*1\] == f4 THEN GOTO [0-9]$ -^\s*IF container_ptr->fp_tbl\[.*1\] == f5 THEN GOTO [0-9]$ -^\s*IF container_ptr->fp_tbl\[.*1\] == f6 THEN GOTO [0-9]$ -^\s*IF container_ptr->fp_tbl\[.*1\] == f7 THEN GOTO [0-9]$ -^\s*IF container_ptr->fp_tbl\[.*1\] == f8 THEN GOTO [0-9]$ -^\s*IF container_ptr->fp_tbl\[.*1\] == f9 THEN GOTO [0-9]$ +^\s*IF .*container_ptr\.fp_tbl\[.*1.*\] = address_of\(f1\) THEN GOTO [0-9]$ +^\s*IF .*container_ptr\.fp_tbl\[.*1.*\] = address_of\(f2\) THEN GOTO [0-9]$ +^\s*IF .*container_ptr\.fp_tbl\[.*1.*\] = address_of\(f3\) THEN GOTO [0-9]$ +^\s*IF .*container_ptr\.fp_tbl\[.*1.*\] = address_of\(f4\) THEN GOTO [0-9]$ +^\s*IF .*container_ptr\.fp_tbl\[.*1.*\] = address_of\(f5\) THEN GOTO [0-9]$ +^\s*IF .*container_ptr\.fp_tbl\[.*1.*\] = address_of\(f6\) THEN GOTO [0-9]$ +^\s*IF .*container_ptr\.fp_tbl\[.*1.*\] = address_of\(f7\) THEN GOTO [0-9]$ +^\s*IF .*container_ptr\.fp_tbl\[.*1.*\] = address_of\(f8\) THEN GOTO [0-9]$ +^\s*IF .*container_ptr\.fp_tbl\[.*1.*\] = address_of\(f9\) THEN GOTO [0-9]$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/goto-analyzer/precise-array-calculation-const-fp/test.desc b/regression/goto-analyzer/precise-array-calculation-const-fp/test.desc index 02bf70c4391..59a16b0d748 100644 --- a/regression/goto-analyzer/precise-array-calculation-const-fp/test.desc +++ b/regression/goto-analyzer/precise-array-calculation-const-fp/test.desc @@ -2,7 +2,7 @@ CORE main.c --show-goto-functions --pointer-check ^Removal of function pointers and virtual functions$ -^\s*f3\(\);$ +^\s*CALL f3\(\)$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/goto-analyzer/precise-array-literal-const-fp/test.desc b/regression/goto-analyzer/precise-array-literal-const-fp/test.desc index 02bf70c4391..59a16b0d748 100644 --- a/regression/goto-analyzer/precise-array-literal-const-fp/test.desc +++ b/regression/goto-analyzer/precise-array-literal-const-fp/test.desc @@ -2,7 +2,7 @@ CORE main.c --show-goto-functions --pointer-check ^Removal of function pointers and virtual functions$ -^\s*f3\(\);$ +^\s*CALL f3\(\)$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/goto-analyzer/precise-const-fp-array-const-variable-const-fp/test.desc b/regression/goto-analyzer/precise-const-fp-array-const-variable-const-fp/test.desc index 02bf70c4391..59a16b0d748 100644 --- a/regression/goto-analyzer/precise-const-fp-array-const-variable-const-fp/test.desc +++ b/regression/goto-analyzer/precise-const-fp-array-const-variable-const-fp/test.desc @@ -2,7 +2,7 @@ CORE main.c --show-goto-functions --pointer-check ^Removal of function pointers and virtual functions$ -^\s*f3\(\);$ +^\s*CALL f3\(\)$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/goto-analyzer/precise-const-fp-array-literal-const-fp-run-time/test.desc b/regression/goto-analyzer/precise-const-fp-array-literal-const-fp-run-time/test.desc index 02bf70c4391..59a16b0d748 100644 --- a/regression/goto-analyzer/precise-const-fp-array-literal-const-fp-run-time/test.desc +++ b/regression/goto-analyzer/precise-const-fp-array-literal-const-fp-run-time/test.desc @@ -2,7 +2,7 @@ CORE main.c --show-goto-functions --pointer-check ^Removal of function pointers and virtual functions$ -^\s*f3\(\);$ +^\s*CALL f3\(\)$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/goto-analyzer/precise-const-fp-array-literal-const-fp/test.desc b/regression/goto-analyzer/precise-const-fp-array-literal-const-fp/test.desc index 02bf70c4391..59a16b0d748 100644 --- a/regression/goto-analyzer/precise-const-fp-array-literal-const-fp/test.desc +++ b/regression/goto-analyzer/precise-const-fp-array-literal-const-fp/test.desc @@ -2,7 +2,7 @@ CORE main.c --show-goto-functions --pointer-check ^Removal of function pointers and virtual functions$ -^\s*f3\(\);$ +^\s*CALL f3\(\)$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/goto-analyzer/precise-const-fp-array-literal-const-struct-non-const-fp/test.desc b/regression/goto-analyzer/precise-const-fp-array-literal-const-struct-non-const-fp/test.desc index 02bf70c4391..59a16b0d748 100644 --- a/regression/goto-analyzer/precise-const-fp-array-literal-const-struct-non-const-fp/test.desc +++ b/regression/goto-analyzer/precise-const-fp-array-literal-const-struct-non-const-fp/test.desc @@ -2,7 +2,7 @@ CORE main.c --show-goto-functions --pointer-check ^Removal of function pointers and virtual functions$ -^\s*f3\(\);$ +^\s*CALL f3\(\)$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/goto-analyzer/precise-const-fp-array-variable-const-pointer-const-struct-non-const-fp/test.desc b/regression/goto-analyzer/precise-const-fp-array-variable-const-pointer-const-struct-non-const-fp/test.desc index 791dbe0703c..f6359140fef 100644 --- a/regression/goto-analyzer/precise-const-fp-array-variable-const-pointer-const-struct-non-const-fp/test.desc +++ b/regression/goto-analyzer/precise-const-fp-array-variable-const-pointer-const-struct-non-const-fp/test.desc @@ -2,7 +2,7 @@ CORE main.c --show-goto-functions --pointer-check ^Removal of function pointers and virtual functions$ -^\s*f2\(\); +^\s*CALL f2\(\) ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/goto-analyzer/precise-const-fp-const-fp/test.desc b/regression/goto-analyzer/precise-const-fp-const-fp/test.desc index 479c26e4afe..a5e81889688 100644 --- a/regression/goto-analyzer/precise-const-fp-const-fp/test.desc +++ b/regression/goto-analyzer/precise-const-fp-const-fp/test.desc @@ -2,7 +2,7 @@ CORE main.c --show-goto-functions --pointer-check ^Removal of function pointers and virtual functions$ -^\s*f2\(\);$ +^\s*CALL f2\(\)$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/goto-analyzer/precise-const-fp-const-struct-const-array-literal-fp/test.desc b/regression/goto-analyzer/precise-const-fp-const-struct-const-array-literal-fp/test.desc index 02bf70c4391..59a16b0d748 100644 --- a/regression/goto-analyzer/precise-const-fp-const-struct-const-array-literal-fp/test.desc +++ b/regression/goto-analyzer/precise-const-fp-const-struct-const-array-literal-fp/test.desc @@ -2,7 +2,7 @@ CORE main.c --show-goto-functions --pointer-check ^Removal of function pointers and virtual functions$ -^\s*f3\(\);$ +^\s*CALL f3\(\)$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/goto-analyzer/precise-const-fp-const-struct-non-const-array-literal-fp/test.desc b/regression/goto-analyzer/precise-const-fp-const-struct-non-const-array-literal-fp/test.desc index 02bf70c4391..59a16b0d748 100644 --- a/regression/goto-analyzer/precise-const-fp-const-struct-non-const-array-literal-fp/test.desc +++ b/regression/goto-analyzer/precise-const-fp-const-struct-non-const-array-literal-fp/test.desc @@ -2,7 +2,7 @@ CORE main.c --show-goto-functions --pointer-check ^Removal of function pointers and virtual functions$ -^\s*f3\(\);$ +^\s*CALL f3\(\)$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/goto-analyzer/precise-const-fp-const-struct-non-const-fp/test.desc b/regression/goto-analyzer/precise-const-fp-const-struct-non-const-fp/test.desc index 791dbe0703c..f6359140fef 100644 --- a/regression/goto-analyzer/precise-const-fp-const-struct-non-const-fp/test.desc +++ b/regression/goto-analyzer/precise-const-fp-const-struct-non-const-fp/test.desc @@ -2,7 +2,7 @@ CORE main.c --show-goto-functions --pointer-check ^Removal of function pointers and virtual functions$ -^\s*f2\(\); +^\s*CALL f2\(\) ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/goto-analyzer/precise-const-fp-dereference-const-pointer-const-fp/test.desc b/regression/goto-analyzer/precise-const-fp-dereference-const-pointer-const-fp/test.desc index 02bf70c4391..59a16b0d748 100644 --- a/regression/goto-analyzer/precise-const-fp-dereference-const-pointer-const-fp/test.desc +++ b/regression/goto-analyzer/precise-const-fp-dereference-const-pointer-const-fp/test.desc @@ -2,7 +2,7 @@ CORE main.c --show-goto-functions --pointer-check ^Removal of function pointers and virtual functions$ -^\s*f3\(\);$ +^\s*CALL f3\(\)$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/goto-analyzer/precise-const-fp-supurious-const-loss/test.desc b/regression/goto-analyzer/precise-const-fp-supurious-const-loss/test.desc index 15fc1e17ef7..a36c3f3a4fc 100644 --- a/regression/goto-analyzer/precise-const-fp-supurious-const-loss/test.desc +++ b/regression/goto-analyzer/precise-const-fp-supurious-const-loss/test.desc @@ -2,19 +2,19 @@ CORE main.c --show-goto-functions --pointer-check ^Removal of function pointers and virtual functions$ -^\s*f2\(\); +^\s*CALL f2\(\) ^EXIT=0$ ^SIGNAL=0$ -- ^warning: ignoring -^\s*\d+:\s*f1\(\); -^\s*\d+:\s*f3\(\); -^\s*\d+:\s*f4\(\); -^\s*\d+:\s*f5\(\); -^\s*\d+:\s*f6\(\); -^\s*\d+:\s*f7\(\); -^\s*\d+:\s*f8\(\); -^\s*\d+:\s*f9\(\); +^\s*\d+:\s*CALL f1\(\) +^\s*\d+:\s*CALL f3\(\) +^\s*\d+:\s*CALL f4\(\) +^\s*\d+:\s*CALL f5\(\) +^\s*\d+:\s*CALL f6\(\) +^\s*\d+:\s*CALL f7\(\) +^\s*\d+:\s*CALL f8\(\) +^\s*\d+:\s*CALL f9\(\) -- Though this example program appears to lose const-ness, since it is a primitive it is a copy so it is irrelevant. diff --git a/regression/goto-analyzer/precise-const-fp/test.desc b/regression/goto-analyzer/precise-const-fp/test.desc index 791dbe0703c..f6359140fef 100644 --- a/regression/goto-analyzer/precise-const-fp/test.desc +++ b/regression/goto-analyzer/precise-const-fp/test.desc @@ -2,7 +2,7 @@ CORE main.c --show-goto-functions --pointer-check ^Removal of function pointers and virtual functions$ -^\s*f2\(\); +^\s*CALL f2\(\) ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/goto-analyzer/precise-const-pointer-const-struct-fp/test.desc b/regression/goto-analyzer/precise-const-pointer-const-struct-fp/test.desc index 479c26e4afe..a5e81889688 100644 --- a/regression/goto-analyzer/precise-const-pointer-const-struct-fp/test.desc +++ b/regression/goto-analyzer/precise-const-pointer-const-struct-fp/test.desc @@ -2,7 +2,7 @@ CORE main.c --show-goto-functions --pointer-check ^Removal of function pointers and virtual functions$ -^\s*f2\(\);$ +^\s*CALL f2\(\)$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/goto-analyzer/precise-const-struct-non-const-fp/test.desc b/regression/goto-analyzer/precise-const-struct-non-const-fp/test.desc index 791dbe0703c..f6359140fef 100644 --- a/regression/goto-analyzer/precise-const-struct-non-const-fp/test.desc +++ b/regression/goto-analyzer/precise-const-struct-non-const-fp/test.desc @@ -2,7 +2,7 @@ CORE main.c --show-goto-functions --pointer-check ^Removal of function pointers and virtual functions$ -^\s*f2\(\); +^\s*CALL f2\(\) ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/goto-analyzer/precise-derefence-const-pointer-const-fp/test.desc b/regression/goto-analyzer/precise-derefence-const-pointer-const-fp/test.desc index 02bf70c4391..59a16b0d748 100644 --- a/regression/goto-analyzer/precise-derefence-const-pointer-const-fp/test.desc +++ b/regression/goto-analyzer/precise-derefence-const-pointer-const-fp/test.desc @@ -2,7 +2,7 @@ CORE main.c --show-goto-functions --pointer-check ^Removal of function pointers and virtual functions$ -^\s*f3\(\);$ +^\s*CALL f3\(\)$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/goto-analyzer/precise-derefence/test.desc b/regression/goto-analyzer/precise-derefence/test.desc index 791dbe0703c..f6359140fef 100644 --- a/regression/goto-analyzer/precise-derefence/test.desc +++ b/regression/goto-analyzer/precise-derefence/test.desc @@ -2,7 +2,7 @@ CORE main.c --show-goto-functions --pointer-check ^Removal of function pointers and virtual functions$ -^\s*f2\(\); +^\s*CALL f2\(\) ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/goto-analyzer/precise-dereference-address-pointer-const-fp/test.desc b/regression/goto-analyzer/precise-dereference-address-pointer-const-fp/test.desc index 02bf70c4391..59a16b0d748 100644 --- a/regression/goto-analyzer/precise-dereference-address-pointer-const-fp/test.desc +++ b/regression/goto-analyzer/precise-dereference-address-pointer-const-fp/test.desc @@ -2,7 +2,7 @@ CORE main.c --show-goto-functions --pointer-check ^Removal of function pointers and virtual functions$ -^\s*f3\(\);$ +^\s*CALL f3\(\)$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/goto-analyzer/precise-dereference-const-struct-const-pointer-const-fp/test.desc b/regression/goto-analyzer/precise-dereference-const-struct-const-pointer-const-fp/test.desc index 02bf70c4391..59a16b0d748 100644 --- a/regression/goto-analyzer/precise-dereference-const-struct-const-pointer-const-fp/test.desc +++ b/regression/goto-analyzer/precise-dereference-const-struct-const-pointer-const-fp/test.desc @@ -2,7 +2,7 @@ CORE main.c --show-goto-functions --pointer-check ^Removal of function pointers and virtual functions$ -^\s*f3\(\);$ +^\s*CALL f3\(\)$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/goto-analyzer/precise-dereference-const-struct-const-pointer-const-struct-const-fp/test.desc b/regression/goto-analyzer/precise-dereference-const-struct-const-pointer-const-struct-const-fp/test.desc index 02bf70c4391..59a16b0d748 100644 --- a/regression/goto-analyzer/precise-dereference-const-struct-const-pointer-const-struct-const-fp/test.desc +++ b/regression/goto-analyzer/precise-dereference-const-struct-const-pointer-const-struct-const-fp/test.desc @@ -2,7 +2,7 @@ CORE main.c --show-goto-functions --pointer-check ^Removal of function pointers and virtual functions$ -^\s*f3\(\);$ +^\s*CALL f3\(\)$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/goto-analyzer/precise-dereference-const-struct-pointer-const-fp/test.desc b/regression/goto-analyzer/precise-dereference-const-struct-pointer-const-fp/test.desc index 02bf70c4391..59a16b0d748 100644 --- a/regression/goto-analyzer/precise-dereference-const-struct-pointer-const-fp/test.desc +++ b/regression/goto-analyzer/precise-dereference-const-struct-pointer-const-fp/test.desc @@ -2,7 +2,7 @@ CORE main.c --show-goto-functions --pointer-check ^Removal of function pointers and virtual functions$ -^\s*f3\(\);$ +^\s*CALL f3\(\)$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/goto-analyzer/regenerate-entry-function/test.desc b/regression/goto-analyzer/regenerate-entry-function/test.desc index ecc9f85a199..6d810517674 100644 --- a/regression/goto-analyzer/regenerate-entry-function/test.desc +++ b/regression/goto-analyzer/regenerate-entry-function/test.desc @@ -1,7 +1,7 @@ CORE main.c --function fun --show-goto-functions -^\s*fun\(x\);$ +^\s*CALL fun\(.*::x\)$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/goto-analyzer/unreachable-instructions-basic-json/test.desc b/regression/goto-analyzer/unreachable-instructions-basic-json/test.desc index 830458c1c3f..b87d694580e 100644 --- a/regression/goto-analyzer/unreachable-instructions-basic-json/test.desc +++ b/regression/goto-analyzer/unreachable-instructions-basic-json/test.desc @@ -6,7 +6,7 @@ CORE "sourceLocation": "function": "not_called", "line": "5", -"statement": "not_called#return_value = x \+ x;" +"statement": "ASSIGN not_called#return_value := .*x \+ .*x" "sourceLocation": "function": "not_called", "line": "5", @@ -16,7 +16,7 @@ CORE "sourceLocation": "function": "dead_inside", "line": "12", -"statement": "y = y \+ 1;" +"statement": "ASSIGN .*::y := .*::y \+ 1" ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/goto-analyzer/unreachable-instructions-basic-text/test.desc b/regression/goto-analyzer/unreachable-instructions-basic-text/test.desc index c71ba15f5c9..00a9b7d50e8 100644 --- a/regression/goto-analyzer/unreachable-instructions-basic-text/test.desc +++ b/regression/goto-analyzer/unreachable-instructions-basic-text/test.desc @@ -5,11 +5,11 @@ unreachable.c ^SIGNAL=0$ not_called // 28 file unreachable.c line 5 function not_called$ -not_called#return_value = x \+ x;$ +not_called#return_value := .*::x \+ .*::x$ // 29 file unreachable.c line 5 function not_called$ GOTO 1$ dead_inside // 34 file unreachable.c line 12 function dead_inside$ -y = y \+ 1;$ +y := .*::y \+ 1$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/unreachable-instructions-domain-text/test.desc b/regression/goto-analyzer/unreachable-instructions-domain-text/test.desc index fd3ce8b0c91..e7c3e0888ce 100644 --- a/regression/goto-analyzer/unreachable-instructions-domain-text/test.desc +++ b/regression/goto-analyzer/unreachable-instructions-domain-text/test.desc @@ -5,14 +5,14 @@ CORE ^SIGNAL=0$ not_called // 28 file unreachable.c line 5 function not_called$ -not_called#return_value = x \+ x;$ +not_called#return_value := .*::x \+ .*::x$ // 29 file unreachable.c line 5 function not_called$ GOTO 1$ dead_inside // 34 file unreachable.c line 12 function dead_inside$ -y = y \+ 1;$ +y := .*::y \+ 1$ obviously_dead // 40 file unreachable-instructions-basic-text/unreachable.c line 20 function obviously_dead -x = x \+ 1; +x := .*::x \+ 1 -- ^warning: ignoring diff --git a/regression/goto-analyzer/variable-sensitivity-annihiliator-test/test.desc b/regression/goto-analyzer/variable-sensitivity-annihiliator-test/test.desc index 5584947a6dc..8c7c3d455bd 100644 --- a/regression/goto-analyzer/variable-sensitivity-annihiliator-test/test.desc +++ b/regression/goto-analyzer/variable-sensitivity-annihiliator-test/test.desc @@ -4,7 +4,7 @@ main.c ^EXIT=0$ ^SIGNAL=0$ line 18 function func -g_out = 1; +g_out := 1 line 24 function func -g_out = 3; +g_out := 3 -- diff --git a/regression/goto-analyzer/variable-sensitivity-dependence-graph-02/test.desc b/regression/goto-analyzer/variable-sensitivity-dependence-graph-02/test.desc index 1f0332d5afc..61b790678ee 100644 --- a/regression/goto-analyzer/variable-sensitivity-dependence-graph-02/test.desc +++ b/regression/goto-analyzer/variable-sensitivity-dependence-graph-02/test.desc @@ -4,7 +4,7 @@ main.c activate-multi-line-match ^EXIT=0$ ^SIGNAL=0$ -Control dependencies: [0-9]+ \[TRUE\]\n.*\n.*\n\s+a = 1; -Control dependencies: [0-9]+ \[UNCONDITIONAL\]\n.*\n.*\n\s+a = 2; +Control dependencies: [0-9]+ \[TRUE\]\n.*\n.*\n\s+ASSIGN .*a := 1 +Control dependencies: [0-9]+ \[UNCONDITIONAL\]\n.*\n.*\n\s+ASSIGN .*a := 2 -- ^warning: ignoring diff --git a/regression/goto-analyzer/variable-sensitivity-dependence-graph15/test.desc b/regression/goto-analyzer/variable-sensitivity-dependence-graph15/test.desc index 6217396b36b..9c4f3a823d8 100644 --- a/regression/goto-analyzer/variable-sensitivity-dependence-graph15/test.desc +++ b/regression/goto-analyzer/variable-sensitivity-dependence-graph15/test.desc @@ -4,8 +4,8 @@ main.c activate-multi-line-match ^EXIT=0$ ^SIGNAL=0$ -Control dependencies: [0-9]+ \[UNCONDITIONAL\]\n(.*\n){2,3}.*g_out2 = t1; -Control dependencies: [0-9]+ \[TRUE\]\n(.*\n){2,3}.*g_out1 = t2; -Control dependencies: [0-9]+ \[FALSE\]\n(.*\n){2,3}.*g_out1 = 0; +Control dependencies: [0-9]+ \[UNCONDITIONAL\]\n(.*\n){2,3}.*g_out2 := .*t1 +Control dependencies: [0-9]+ \[TRUE\]\n(.*\n){2,3}.*g_out1 := .*t2 +Control dependencies: [0-9]+ \[FALSE\]\n(.*\n){2,3}.*g_out1 := 0 -- ^warning: ignoring diff --git a/regression/goto-analyzer/variable-sensitivity-dependence-graph16/test.desc b/regression/goto-analyzer/variable-sensitivity-dependence-graph16/test.desc index d9c98288288..1132fa4e2c1 100644 --- a/regression/goto-analyzer/variable-sensitivity-dependence-graph16/test.desc +++ b/regression/goto-analyzer/variable-sensitivity-dependence-graph16/test.desc @@ -6,5 +6,5 @@ activate-multi-line-match ^SIGNAL=0$ // Assignment from the result of a function call to a function with no body // should have a data dependency on the function -^Data dependencies: 3 \[f2\]\n(.*\n).*\/\/ 4 file .*main.c line 15 function main\n.*t2 = NONDET\([^)]*\); +^Data dependencies: 3 \[f2\]\n(.*\n).*\/\/ 4 file .*main.c line 15 function main\n.*t2 := .*nondet.* -- diff --git a/regression/goto-cc-goto-analyzer/regenerate-entry-function/test.desc b/regression/goto-cc-goto-analyzer/regenerate-entry-function/test.desc index 40cb3664871..68b40c1af3a 100644 --- a/regression/goto-cc-goto-analyzer/regenerate-entry-function/test.desc +++ b/regression/goto-cc-goto-analyzer/regenerate-entry-function/test.desc @@ -1,7 +1,7 @@ CORE main.c '--function fun --show-goto-functions' -^\s*fun\(x\);$ +^\s*CALL fun\(.*::x\)$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/goto-harness/array-types/test.desc b/regression/goto-harness/array-types/test.desc index e27b1735f72..1585a54f583 100644 --- a/regression/goto-harness/array-types/test.desc +++ b/regression/goto-harness/array-types/test.desc @@ -4,7 +4,7 @@ example.c VERIFICATION SUCCESSFUL ^EXIT=0$ ^SIGNAL=0$ -type_constructor_ptr_int\(0, &arr, \(signed int \*\)\(void \*\)0\); +CALL type_constructor_ptr_int\(0, address_of.*::arr\), .*0.*\) -- incompatible pointer types -- diff --git a/regression/goto-instrument/approx-array-variable-const-fp-only-remove-const/test.desc b/regression/goto-instrument/approx-array-variable-const-fp-only-remove-const/test.desc index 1cbd689c4b8..1ca7d58db7b 100644 --- a/regression/goto-instrument/approx-array-variable-const-fp-only-remove-const/test.desc +++ b/regression/goto-instrument/approx-array-variable-const-fp-only-remove-const/test.desc @@ -1,16 +1,16 @@ CORE main.c --pointer-check --remove-const-function-pointers -^\s*IF fp_tbl\[.*i\] == f2 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[.*i\] == f3 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[.*i\] == f4 THEN GOTO [0-9]$ +^\s*IF fp_tbl\[.*i.*\] = address_of\(f2\) THEN GOTO [0-9]$ +^\s*IF fp_tbl\[.*i.*\] = address_of\(f3\) THEN GOTO [0-9]$ +^\s*IF fp_tbl\[.*i.*\] = address_of\(f4\) THEN GOTO [0-9]$ ^EXIT=0$ ^SIGNAL=0$ -- -^\s*IF fp_tbl\[.*i\] == f1 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[.*i\] == f5 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[.*i\] == f6 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[.*i\] == f7 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[.*i\] == f8 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[.*i\] == f9 THEN GOTO [0-9]$ +^\s*IF fp_tbl\[.*i.*\] = address_of\(f1\) THEN GOTO [0-9]$ +^\s*IF fp_tbl\[.*i.*\] = address_of\(f5\) THEN GOTO [0-9]$ +^\s*IF fp_tbl\[.*i.*\] = address_of\(f6\) THEN GOTO [0-9]$ +^\s*IF fp_tbl\[.*i.*\] = address_of\(f7\) THEN GOTO [0-9]$ +^\s*IF fp_tbl\[.*i.*\] = address_of\(f8\) THEN GOTO [0-9]$ +^\s*IF fp_tbl\[.*i.*\] = address_of\(f9\) THEN GOTO [0-9]$ ^warning: ignoring diff --git a/regression/goto-instrument/approx-array-variable-const-fp-remove-all-fp/test.desc b/regression/goto-instrument/approx-array-variable-const-fp-remove-all-fp/test.desc index 3669d114ae0..196c7328eeb 100644 --- a/regression/goto-instrument/approx-array-variable-const-fp-remove-all-fp/test.desc +++ b/regression/goto-instrument/approx-array-variable-const-fp-remove-all-fp/test.desc @@ -1,16 +1,16 @@ CORE main.c --pointer-check --remove-function-pointers -^\s*IF fp_tbl\[.*i\] == f2 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[.*i\] == f3 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[.*i\] == f4 THEN GOTO [0-9]$ +^\s*IF fp_tbl\[.*i.*\] = address_of\(f2\) THEN GOTO [0-9]$ +^\s*IF fp_tbl\[.*i.*\] = address_of\(f3\) THEN GOTO [0-9]$ +^\s*IF fp_tbl\[.*i.*\] = address_of\(f4\) THEN GOTO [0-9]$ ^EXIT=0$ ^SIGNAL=0$ -- -^\s*IF fp_tbl\[.*i\] == f1 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[.*i\] == f5 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[.*i\] == f6 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[.*i\] == f7 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[.*i\] == f8 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[.*i\] == f9 THEN GOTO [0-9]$ +^\s*IF fp_tbl\[.*i.*\] = address_of\(f1\) THEN GOTO [0-9]$ +^\s*IF fp_tbl\[.*i.*\] = address_of\(f5\) THEN GOTO [0-9]$ +^\s*IF fp_tbl\[.*i.*\] = address_of\(f6\) THEN GOTO [0-9]$ +^\s*IF fp_tbl\[.*i.*\] = address_of\(f7\) THEN GOTO [0-9]$ +^\s*IF fp_tbl\[.*i.*\] = address_of\(f8\) THEN GOTO [0-9]$ +^\s*IF fp_tbl\[.*i.*\] = address_of\(f9\) THEN GOTO [0-9]$ ^warning: ignoring diff --git a/regression/goto-instrument/fp-reachability-slice1/test.desc b/regression/goto-instrument/fp-reachability-slice1/test.desc index 803f790ee84..5c7b08aa83f 100644 --- a/regression/goto-instrument/fp-reachability-slice1/test.desc +++ b/regression/goto-instrument/fp-reachability-slice1/test.desc @@ -3,9 +3,9 @@ main.c --fp-reachability-slice c ^EXIT=0$ ^SIGNAL=0$ -1: ASSUME FALSE -dead e; -dead d; +1: ASSUME false +DEAD .*::e +DEAD .*::d -- ^warning: ignoring -dead f; +DEAD .*::f diff --git a/regression/goto-instrument/fp-reachability-slice2/test.desc b/regression/goto-instrument/fp-reachability-slice2/test.desc index 36f6ee8dafc..f593c6822d5 100644 --- a/regression/goto-instrument/fp-reachability-slice2/test.desc +++ b/regression/goto-instrument/fp-reachability-slice2/test.desc @@ -3,8 +3,8 @@ main.c --fp-reachability-slice a,c ^EXIT=0$ ^SIGNAL=0$ -dead d; -dead e; +DEAD .*::d +DEAD .*::e -- ^warning: ignoring -dead f; +DEAD .*::f diff --git a/regression/goto-instrument/gcc_attribute_used1/test.desc b/regression/goto-instrument/gcc_attribute_used1/test.desc index 99890290f0e..ef8311e5230 100644 --- a/regression/goto-instrument/gcc_attribute_used1/test.desc +++ b/regression/goto-instrument/gcc_attribute_used1/test.desc @@ -3,7 +3,7 @@ main.c ^EXIT=0$ ^SIGNAL=0$ -^[[:space:]]*foo = 42;$ +^[[:space:]]*ASSIGN foo := 42$ -- ^warning: ignoring ^CONVERSION ERROR$ diff --git a/regression/goto-instrument/inline_02/test.desc b/regression/goto-instrument/inline_02/test.desc index 20e93e09f77..5dd60ae89a6 100644 --- a/regression/goto-instrument/inline_02/test.desc +++ b/regression/goto-instrument/inline_02/test.desc @@ -4,8 +4,8 @@ main.c ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ -f[\(].*[\)];$ -g[\(].*[\)];$ -h[\(].*[\)];$ +f[\(].*[\)]$ +g[\(].*[\)]$ +h[\(].*[\)]$ -- ^warning: ignoring diff --git a/regression/goto-instrument/inline_03/test.desc b/regression/goto-instrument/inline_03/test.desc index 3b6645c8a4c..2277e6cee3c 100644 --- a/regression/goto-instrument/inline_03/test.desc +++ b/regression/goto-instrument/inline_03/test.desc @@ -4,8 +4,8 @@ main.c ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ -f[\(].*[\)];$ -g[\(].*[\)];$ +f[\(].*[\)]$ +g[\(].*[\)]$ -- -h[\(].*[\)];$ +h[\(].*[\)]$ ^warning: ignoring diff --git a/regression/goto-instrument/inline_04/test.desc b/regression/goto-instrument/inline_04/test.desc index 8f2f03cf5f3..49195dfa496 100644 --- a/regression/goto-instrument/inline_04/test.desc +++ b/regression/goto-instrument/inline_04/test.desc @@ -4,9 +4,9 @@ main.c ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ -g[\(].*[\)];$ -h[\(].*[\)];$ +g[\(].*[\)]$ +h[\(].*[\)]$ -- -f[\(].*[\)];$ -other_func[\(].*[\)];$ +f[\(].*[\)]$ +other_func[\(].*[\)]$ ^warning: ignoring diff --git a/regression/goto-instrument/inline_08/test.desc b/regression/goto-instrument/inline_08/test.desc index 63e8a494a30..b866f33be66 100644 --- a/regression/goto-instrument/inline_08/test.desc +++ b/regression/goto-instrument/inline_08/test.desc @@ -4,8 +4,8 @@ main.c ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ -y = 1; -y = 2; -y = 3; +y := 1 +y := 2 +y := 3 -- ^warning: ignoring diff --git a/regression/goto-instrument/inline_09/test.desc b/regression/goto-instrument/inline_09/test.desc index 5bb9b6b5e91..2bdaae22126 100644 --- a/regression/goto-instrument/inline_09/test.desc +++ b/regression/goto-instrument/inline_09/test.desc @@ -4,9 +4,9 @@ main.c ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ -^\s*x;$ -^\s*c;$ -^\s*a;$ +^\s*.*::x$ +^\s*.*::c$ +^\s*.*::a$ no body.*'f -- f\(\) diff --git a/regression/goto-instrument/is-threaded1/test.desc b/regression/goto-instrument/is-threaded1/test.desc index 100f5087714..58a6e7b2348 100644 --- a/regression/goto-instrument/is-threaded1/test.desc +++ b/regression/goto-instrument/is-threaded1/test.desc @@ -2,7 +2,7 @@ CORE main.c --show-threaded activate-multi-line-match -x = 2;\nIs threaded: True +ASSIGN x := 2\nIs threaded: True ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/goto-instrument/no-match-non-const-fp-only-remove-const/test.desc b/regression/goto-instrument/no-match-non-const-fp-only-remove-const/test.desc index 12541b9b590..c1a5c2a90c8 100644 --- a/regression/goto-instrument/no-match-non-const-fp-only-remove-const/test.desc +++ b/regression/goto-instrument/no-match-non-const-fp-only-remove-const/test.desc @@ -1,7 +1,7 @@ CORE main.c --pointer-check --remove-const-function-pointers -^\s*fp\(\);$ +^\s*CALL \*.*::fp\(\)$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/goto-instrument/no-match-non-const-fp-remove-all-fp/test.desc b/regression/goto-instrument/no-match-non-const-fp-remove-all-fp/test.desc index e01224edbd5..f9a3edad66b 100644 --- a/regression/goto-instrument/no-match-non-const-fp-remove-all-fp/test.desc +++ b/regression/goto-instrument/no-match-non-const-fp-remove-all-fp/test.desc @@ -1,15 +1,15 @@ CORE main.c --pointer-check --remove-function-pointers -^\s*IF fp == f1 THEN GOTO [0-9]$ -^\s*IF fp == f2 THEN GOTO [0-9]$ -^\s*IF fp == f3 THEN GOTO [0-9]$ -^\s*IF fp == f4 THEN GOTO [0-9]$ -^\s*IF fp == f5 THEN GOTO [0-9]$ -^\s*IF fp == f6 THEN GOTO [0-9]$ -^\s*IF fp == f7 THEN GOTO [0-9]$ -^\s*IF fp == f8 THEN GOTO [0-9]$ -^\s*IF fp == f9 THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f1\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f2\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f3\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f4\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f5\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f6\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f7\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f8\) THEN GOTO [0-9]$ +^\s*IF .*::fp = address_of\(f9\) THEN GOTO [0-9]$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/goto-instrument/precise-const-fp-only-remove-const/test.desc b/regression/goto-instrument/precise-const-fp-only-remove-const/test.desc index a04500200da..4693e9cc936 100644 --- a/regression/goto-instrument/precise-const-fp-only-remove-const/test.desc +++ b/regression/goto-instrument/precise-const-fp-only-remove-const/test.desc @@ -1,7 +1,7 @@ CORE main.c --pointer-check --remove-const-function-pointers -^\s*f2\(\); +^\s*CALL f2\(\) ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/goto-instrument/precise-const-fp-remove-all-fp/test.desc b/regression/goto-instrument/precise-const-fp-remove-all-fp/test.desc index 381d1c41c72..c9076a57e63 100644 --- a/regression/goto-instrument/precise-const-fp-remove-all-fp/test.desc +++ b/regression/goto-instrument/precise-const-fp-remove-all-fp/test.desc @@ -1,7 +1,7 @@ CORE main.c --pointer-check --remove-function-pointers -^\s*f2\(\); +^\s*CALL f2\(\) ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/goto-instrument/region-analysis-1/test.desc b/regression/goto-instrument/region-analysis-1/test.desc index ad0a13b16e9..1e2124e2727 100644 --- a/regression/goto-instrument/region-analysis-1/test.desc +++ b/regression/goto-instrument/region-analysis-1/test.desc @@ -1,8 +1,8 @@ CORE test.c --show-sese-regions -^Region starting at \(1, [0-9]+\) IF !\(argc % 2 != 0\) THEN GOTO 1 ends at \(5, [0-9]+\) 2: SKIP$ -^Region starting at \(0, [0-9]+\) IF !\(argc % 5 != 0\) THEN GOTO 3 ends at \(8, [0-9]+\) 4: SKIP$ +^Region starting at \(1, [0-9]+\) IF .*2.* THEN GOTO 1 ends at \(5, [0-9]+\) 2: SKIP$ +^Region starting at \(0, [0-9]+\) IF .*5.* THEN GOTO 3 ends at \(8, [0-9]+\) 4: SKIP$ ^Function contains 2 single-entry, single-exit regions:$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-instrument/region-analysis-10/test.desc b/regression/goto-instrument/region-analysis-10/test.desc index cd0ecbbe0a5..1d2d865f932 100644 --- a/regression/goto-instrument/region-analysis-10/test.desc +++ b/regression/goto-instrument/region-analysis-10/test.desc @@ -2,7 +2,7 @@ CORE test.c --show-sese-regions ^Function contains 2 single-entry, single-exit regions:$ -^Region starting at \(2, [0-9]+\) x = 0; ends at \(6, [0-9]+\) 2: SKIP$ -^Region starting at \(0, [0-9]+\) IF !\(argc % 5 != 0\) THEN GOTO 3 ends at \(10, [0-9]+\) 4: SKIP$ +^Region starting at \(2, [0-9]+\) .*::x := 0 ends at \(6, [0-9]+\) 2: SKIP$ +^Region starting at \(0, [0-9]+\) IF .*5.* THEN GOTO 3 ends at \(10, [0-9]+\) 4: SKIP$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-instrument/region-analysis-11/test.desc b/regression/goto-instrument/region-analysis-11/test.desc index 72705c3e7e7..214c3e45004 100644 --- a/regression/goto-instrument/region-analysis-11/test.desc +++ b/regression/goto-instrument/region-analysis-11/test.desc @@ -2,7 +2,7 @@ CORE test.c --show-sese-regions ^Function contains 2 single-entry, single-exit regions:$ -^Region starting at \(2, [0-9]+\) x = 0; ends at \(9, [0-9]+\) 2: SKIP$ -^Region starting at \(0, [0-9]+\) IF !\(argc % 5 != 0\) THEN GOTO 3 ends at \(13, [0-9]+\) 4: SKIP$ +^Region starting at \(2, [0-9]+\) .*::x := 0 ends at \(9, [0-9]+\) 2: SKIP$ +^Region starting at \(0, [0-9]+\) IF .*5.* THEN GOTO 3 ends at \(13, [0-9]+\) 4: SKIP$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-instrument/region-analysis-12/test.desc b/regression/goto-instrument/region-analysis-12/test.desc index d84ef86a0e4..90279660ac2 100644 --- a/regression/goto-instrument/region-analysis-12/test.desc +++ b/regression/goto-instrument/region-analysis-12/test.desc @@ -2,8 +2,8 @@ CORE test.c --show-sese-regions ^Function contains 3 single-entry, single-exit regions:$ -^Region starting at \(4, [0-9]+\) IF !\(x % 7 != 0\) THEN GOTO 2 ends at \(9, [0-9]+\) 3: GOTO 1$ -^Region starting at \(0, [0-9]+\) IF !\(argc % 5 != 0\) THEN GOTO 5 ends at \(14, [0-9]+\) 6: SKIP$ -^Region starting at \(2, [0-9]+\) x = 0; ends at \(10, [0-9]+\) 4: SKIP$ +^Region starting at \(4, [0-9]+\) IF .*7.* THEN GOTO 2 ends at \(9, [0-9]+\) 3: GOTO 1$ +^Region starting at \(0, [0-9]+\) IF .*5.* THEN GOTO 5 ends at \(14, [0-9]+\) 6: SKIP$ +^Region starting at \(2, [0-9]+\) .*::x := 0 ends at \(10, [0-9]+\) 4: SKIP$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-instrument/region-analysis-13/test.desc b/regression/goto-instrument/region-analysis-13/test.desc index e9adb5859c1..c74a00a1fbd 100644 --- a/regression/goto-instrument/region-analysis-13/test.desc +++ b/regression/goto-instrument/region-analysis-13/test.desc @@ -2,8 +2,8 @@ FUTURE test.c --show-sese-regions ^Function contains 2 single-entry, single-exit regions:$ -^Region starting at \(2, [0-9]+\) x = 0; ends at \(10, [0-9]+\) 3: SKIP$ -^Region starting at \(0, [0-9]+\) IF !\(argc % 5 != 0\) THEN GOTO 4 ends at \(14, [0-9]+\) 5: SKIP$ +^Region starting at \(2, [0-9]+\) .* x := 0 ends at \(10, [0-9]+\) 3: SKIP$ +^Region starting at \(0, [0-9]+\) IF .*5.* THEN GOTO 4 ends at \(14, [0-9]+\) 5: SKIP$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/goto-instrument/region-analysis-14/test.desc b/regression/goto-instrument/region-analysis-14/test.desc index d8b0cc462ce..ff87ce2a2e6 100644 --- a/regression/goto-instrument/region-analysis-14/test.desc +++ b/regression/goto-instrument/region-analysis-14/test.desc @@ -2,7 +2,7 @@ CORE test.c --show-sese-regions ^Function contains 2 single-entry, single-exit regions:$ -^Region starting at \(2, [0-9]+\) x = 0; ends at \(5, [0-9]+\) SKIP$ -^Region starting at \(0, [0-9]+\) IF !\(argc % 5 != 0\) THEN GOTO 2 ends at \(9, [0-9]+\) 3: SKIP$ +^Region starting at \(2, [0-9]+\) .*::x := 0 ends at \(5, [0-9]+\) SKIP$ +^Region starting at \(0, [0-9]+\) IF .*5.* THEN GOTO 2 ends at \(9, [0-9]+\) 3: SKIP$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-instrument/region-analysis-15/test.desc b/regression/goto-instrument/region-analysis-15/test.desc index 6c7e6d6aab1..910291e08be 100644 --- a/regression/goto-instrument/region-analysis-15/test.desc +++ b/regression/goto-instrument/region-analysis-15/test.desc @@ -2,7 +2,7 @@ CORE test.c --show-sese-regions ^Function contains 2 single-entry, single-exit regions:$ -^Region starting at \(2, [0-9]+\) x = 0; ends at \(8, [0-9]+\) 2: SKIP$ -^Region starting at \(0, [0-9]+\) IF !\(argc % 5 != 0\) THEN GOTO 3 ends at \(12, [0-9]+\) 4: SKIP$ +^Region starting at \(2, [0-9]+\) .*::x := 0 ends at \(8, [0-9]+\) 2: SKIP$ +^Region starting at \(0, [0-9]+\) IF .*5.* THEN GOTO 3 ends at \(12, [0-9]+\) 4: SKIP$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-instrument/region-analysis-16/test.desc b/regression/goto-instrument/region-analysis-16/test.desc index b68f743c7f3..92d06f8055b 100644 --- a/regression/goto-instrument/region-analysis-16/test.desc +++ b/regression/goto-instrument/region-analysis-16/test.desc @@ -2,8 +2,8 @@ CORE test.c --show-sese-regions ^Function contains 3 single-entry, single-exit regions:$ -^Region starting at \(3, [0-9]+\) 1: IF !\(x % 7 != 0\) THEN GOTO 2 ends at \(8, [0-9]+\) 3: IF x < 10 THEN GOTO 1$ -^Region starting at \(0, [0-9]+\) IF !\(argc % 5 != 0\) THEN GOTO 4 ends at \(13, [0-9]+\) 5: SKIP$ -^Region starting at \(2, [0-9]+\) x = 0; ends at \(9, [0-9]+\) SKIP$ +^Region starting at \(3, [0-9]+\) 1: IF .*7.* THEN GOTO 2 ends at \(8, [0-9]+\) 3: IF .*::x < 10 THEN GOTO 1$ +^Region starting at \(0, [0-9]+\) IF .*5.* THEN GOTO 4 ends at \(13, [0-9]+\) 5: SKIP$ +^Region starting at \(2, [0-9]+\) .*::x := 0 ends at \(9, [0-9]+\) SKIP$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-instrument/region-analysis-17/test.desc b/regression/goto-instrument/region-analysis-17/test.desc index b101ffcd32b..2d6391f463f 100644 --- a/regression/goto-instrument/region-analysis-17/test.desc +++ b/regression/goto-instrument/region-analysis-17/test.desc @@ -2,8 +2,8 @@ FUTURE test.c --show-sese-regions ^Function contains 2 single-entry, single-exit regions:$ -^Region starting at \(2, [0-9]+\) x = 0; ends at \(10, [0-9]+\) 3: SKIP$ -^Region starting at \(0, [0-9]+\) IF !\(argc % 5 != 0\) THEN GOTO 4 ends at \(14, [0-9]+\) 5: SKIP$ +^Region starting at \(2, [0-9]+\) .* x := 0 ends at \(10, [0-9]+\) 3: SKIP$ +^Region starting at \(0, [0-9]+\) IF .*5.* THEN GOTO 4 ends at \(14, [0-9]+\) 5: SKIP$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/goto-instrument/region-analysis-2/test.desc b/regression/goto-instrument/region-analysis-2/test.desc index e6da6617df1..742fb8a1f0f 100644 --- a/regression/goto-instrument/region-analysis-2/test.desc +++ b/regression/goto-instrument/region-analysis-2/test.desc @@ -2,7 +2,7 @@ CORE test.c --show-sese-regions ^Function contains 2 single-entry, single-exit regions:$ -^Region starting at \(4, [0-9]+\) IF !\(argc % 2 != 0\) THEN GOTO 1 ends at \(8, [0-9]+\) 2: SKIP$ -^Region starting at \(0, [0-9]+\) IF argc % 7 != 0 THEN GOTO 3 ends at \(11, [0-9]+\) 4: SKIP$ +^Region starting at \(4, [0-9]+\) IF .*2.* THEN GOTO 1 ends at \(8, [0-9]+\) 2: SKIP$ +^Region starting at \(0, [0-9]+\) IF .*7.* THEN GOTO 3 ends at \(11, [0-9]+\) 4: SKIP$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-instrument/region-analysis-3/test.desc b/regression/goto-instrument/region-analysis-3/test.desc index 6258f57ae2b..9e47190c660 100644 --- a/regression/goto-instrument/region-analysis-3/test.desc +++ b/regression/goto-instrument/region-analysis-3/test.desc @@ -2,7 +2,7 @@ CORE test.c --show-sese-regions ^Function contains 2 single-entry, single-exit regions:$ -^Region starting at \(1, [0-9]+\) IF !\(argc % 2 != 0\) THEN GOTO 1 ends at \(5, [0-9]+\) 2: SKIP$ -^Region starting at \(0, [0-9]+\) IF !\(argc % 5 != 0\) THEN GOTO 3 ends at \(12, [0-9]+\) 5: END_FUNCTION$ +^Region starting at \(1, [0-9]+\) IF .*2.* THEN GOTO 1 ends at \(5, [0-9]+\) 2: SKIP$ +^Region starting at \(0, [0-9]+\) IF .*5.* THEN GOTO 3 ends at \(12, [0-9]+\) 5: END_FUNCTION$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-instrument/region-analysis-4/test.desc b/regression/goto-instrument/region-analysis-4/test.desc index e52001ec89a..5563acac130 100644 --- a/regression/goto-instrument/region-analysis-4/test.desc +++ b/regression/goto-instrument/region-analysis-4/test.desc @@ -2,7 +2,7 @@ CORE test.c --show-sese-regions ^Function contains 2 single-entry, single-exit regions:$ -^Region starting at \(2, [0-9]+\) x = 0; ends at \(7, [0-9]+\) 2: SKIP$ -^Region starting at \(0, [0-9]+\) IF !\(argc % 5 != 0\) THEN GOTO 3 ends at \(11, [0-9]+\) 4: SKIP$ +^Region starting at \(2, [0-9]+\) .*::x := 0 ends at \(7, [0-9]+\) 2: SKIP$ +^Region starting at \(0, [0-9]+\) IF .*5.* THEN GOTO 3 ends at \(11, [0-9]+\) 4: SKIP$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-instrument/region-analysis-5/test.desc b/regression/goto-instrument/region-analysis-5/test.desc index 30440d57f54..8816462f8b8 100644 --- a/regression/goto-instrument/region-analysis-5/test.desc +++ b/regression/goto-instrument/region-analysis-5/test.desc @@ -2,7 +2,7 @@ CORE test.c --show-sese-regions ^Function contains 2 single-entry, single-exit regions:$ -^Region starting at \(2, [0-9]+\) x = 0; ends at \(10, [0-9]+\) 2: SKIP$ -^Region starting at \(0, [0-9]+\) IF !\(argc % 5 != 0\) THEN GOTO 3 ends at \(14, [0-9]+\) 4: SKIP$ +^Region starting at \(2, [0-9]+\) .*::x := 0 ends at \(10, [0-9]+\) 2: SKIP$ +^Region starting at \(0, [0-9]+\) IF .*5.* THEN GOTO 3 ends at \(14, [0-9]+\) 4: SKIP$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-instrument/region-analysis-6/test.desc b/regression/goto-instrument/region-analysis-6/test.desc index 642f487b5da..4eef6ebd2b2 100644 --- a/regression/goto-instrument/region-analysis-6/test.desc +++ b/regression/goto-instrument/region-analysis-6/test.desc @@ -2,8 +2,8 @@ CORE test.c --show-sese-regions ^Function contains 3 single-entry, single-exit regions:$ -^Region starting at \(4, [0-9]+\) IF x % 7 != 0 THEN GOTO 2 ends at \(8, [0-9]+\) 2: x = x \+ 1;$ -^Region starting at \(0, [0-9]+\) IF !\(argc % 5 != 0\) THEN GOTO 4 ends at \(14, [0-9]+\) 5: SKIP$ -^Region starting at \(2, [0-9]+\) x = 0; ends at \(10, [0-9]+\) 3: SKIP$ +^Region starting at \(4, [0-9]+\) IF .*7.* THEN GOTO 2 ends at \(8, [0-9]+\) 2: .*x := .*x \+ 1$ +^Region starting at \(0, [0-9]+\) IF .*5.* THEN GOTO 4 ends at \(14, [0-9]+\) 5: SKIP$ +^Region starting at \(2, [0-9]+\) .*::x := 0 ends at \(10, [0-9]+\) 3: SKIP$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-instrument/region-analysis-7/test.desc b/regression/goto-instrument/region-analysis-7/test.desc index a4576526ea6..73a071d2a2c 100644 --- a/regression/goto-instrument/region-analysis-7/test.desc +++ b/regression/goto-instrument/region-analysis-7/test.desc @@ -2,6 +2,6 @@ CORE test.c --show-sese-regions ^Function contains 1 single-entry, single-exit regions:$ -^Region starting at \(0, [0-9]+\) IF !\(argc % 5 != 0\) THEN GOTO 4 ends at \(19, [0-9]+\) 6: END_FUNCTION$ +^Region starting at \(0, [0-9]+\) IF .*5.* THEN GOTO 4 ends at \(19, [0-9]+\) 6: END_FUNCTION$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-instrument/region-analysis-8/test.desc b/regression/goto-instrument/region-analysis-8/test.desc index 59534b3fc2a..29f3bceae7d 100644 --- a/regression/goto-instrument/region-analysis-8/test.desc +++ b/regression/goto-instrument/region-analysis-8/test.desc @@ -2,8 +2,8 @@ CORE test.c --show-sese-regions ^Function contains 3 single-entry, single-exit regions:$ -^Region starting at \(5, [0-9]+\) y = 0; ends at \(10, [0-9]+\) 3: SKIP$ -^Region starting at \(0, [0-9]+\) IF !\(argc % 5 != 0\) THEN GOTO 5 ends at \(18, [0-9]+\) 6: SKIP$ -^Region starting at \(2, [0-9]+\) x = 0; ends at \(14, [0-9]+\) 4: SKIP$ +^Region starting at \(5, [0-9]+\) .*::y := 0 ends at \(10, [0-9]+\) 3: SKIP$ +^Region starting at \(0, [0-9]+\) IF .*5.* THEN GOTO 5 ends at \(18, [0-9]+\) 6: SKIP$ +^Region starting at \(2, [0-9]+\) .*::x := 0 ends at \(14, [0-9]+\) 4: SKIP$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-instrument/region-analysis-9/test.desc b/regression/goto-instrument/region-analysis-9/test.desc index 6ff8f290bc3..b9245004445 100644 --- a/regression/goto-instrument/region-analysis-9/test.desc +++ b/regression/goto-instrument/region-analysis-9/test.desc @@ -2,7 +2,7 @@ CORE test.c --show-sese-regions ^Function contains 2 single-entry, single-exit regions:$ -^Region starting at \(2, [0-9]+\) x = 0; ends at \(21, [0-9]+\) 6: argc = argc \+ 1;$ -^Region starting at \(0, [0-9]+\) IF !\(argc % 5 != 0\) THEN GOTO 7 ends at \(24, [0-9]+\) 8: SKIP$ +^Region starting at \(2, [0-9]+\) .*::x := 0 ends at \(21, [0-9]+\) 6: ASSIGN main::argc := main::argc \+ 1$ +^Region starting at \(0, [0-9]+\) IF .*5.* THEN GOTO 7 ends at \(24, [0-9]+\) 8: SKIP$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-instrument/remove-calls-no-body2/test.desc b/regression/goto-instrument/remove-calls-no-body2/test.desc index 29c4bb40375..3af61ff6e61 100644 --- a/regression/goto-instrument/remove-calls-no-body2/test.desc +++ b/regression/goto-instrument/remove-calls-no-body2/test.desc @@ -6,9 +6,9 @@ main.c ^VERIFICATION SUCCESSFUL$ func3\(\) func4\(\) -567; -285; -ret1.*=.*NONDET +567\) +285\) +ret1 :=.*nondet.* -- func1\(.*\) func2\(.*\) diff --git a/regression/goto-instrument/replace-calls-01/test.desc b/regression/goto-instrument/replace-calls-01/test.desc index 7c5582321b5..65b936d4d70 100644 --- a/regression/goto-instrument/replace-calls-01/test.desc +++ b/regression/goto-instrument/replace-calls-01/test.desc @@ -1,10 +1,10 @@ CORE main.c --replace-calls f:g -g\(0\); +g\(0\) ^VERIFICATION SUCCESSFUL$ ^EXIT=0$ ^SIGNAL=0$ -- -f\(0\); +f\(0\) ^warning: ignoring diff --git a/regression/goto-instrument/replace-calls-02/test.desc b/regression/goto-instrument/replace-calls-02/test.desc index a63737f5209..4023c000f62 100644 --- a/regression/goto-instrument/replace-calls-02/test.desc +++ b/regression/goto-instrument/replace-calls-02/test.desc @@ -1,12 +1,12 @@ CORE main.c --replace-calls f:g --replace-calls h:i -g\(\); -i\(\); +g\(\) +i\(\) ^VERIFICATION SUCCESSFUL$ ^EXIT=0$ ^SIGNAL=0$ -- -f\(\); -h\(\); +f\(\) +h\(\) ^warning: ignoring diff --git a/regression/goto-instrument/show-goto-functions1/test.desc b/regression/goto-instrument/show-goto-functions1/test.desc index 250c679543a..0aef764297b 100644 --- a/regression/goto-instrument/show-goto-functions1/test.desc +++ b/regression/goto-instrument/show-goto-functions1/test.desc @@ -1,7 +1,7 @@ CORE main.c --show-goto-functions -HAVOC_OBJECT \(void \*\)a +HAVOC_OBJECT .*a.* ^SIGNAL=0$ ^EXIT=0$ -- diff --git a/regression/goto-instrument/slice-global-inits1/test.desc b/regression/goto-instrument/slice-global-inits1/test.desc index e6cfe4981f8..9096221dd35 100644 --- a/regression/goto-instrument/slice-global-inits1/test.desc +++ b/regression/goto-instrument/slice-global-inits1/test.desc @@ -1,13 +1,13 @@ CORE main.c --slice-global-inits -z = 0;$ -a = -s2 = +z := 0$ +a := +s2 := ^EXIT=0$ ^SIGNAL=0$ -- -x = 0;$ -y = 0;$ -s1 = +x := 0$ +y := 0$ +s1 := ^warning: ignoring diff --git a/regression/goto-instrument/slice-global-inits2/test.desc b/regression/goto-instrument/slice-global-inits2/test.desc index 8d2e0699012..709dbe16ba3 100644 --- a/regression/goto-instrument/slice-global-inits2/test.desc +++ b/regression/goto-instrument/slice-global-inits2/test.desc @@ -1,8 +1,8 @@ CORE main.c --slice-global-inits -x = 0;$ -y = 0;$ +x := 0$ +y := 0$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/goto-instrument/slice-global-inits3/test.desc b/regression/goto-instrument/slice-global-inits3/test.desc index 8d2e0699012..709dbe16ba3 100644 --- a/regression/goto-instrument/slice-global-inits3/test.desc +++ b/regression/goto-instrument/slice-global-inits3/test.desc @@ -1,8 +1,8 @@ CORE main.c --slice-global-inits -x = 0;$ -y = 0;$ +x := 0$ +y := 0$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/goto-instrument/splice_call_01/test.desc b/regression/goto-instrument/splice_call_01/test.desc index 3e3233e216d..235b628f5a8 100644 --- a/regression/goto-instrument/splice_call_01/test.desc +++ b/regression/goto-instrument/splice_call_01/test.desc @@ -2,6 +2,6 @@ CORE main.c --splice-call main,moo activate-multi-line-match -moo\(\);\n.*function main.* +moo\(\)\n.*function main.* ^EXIT=0$ ^SIGNAL=0$ \ No newline at end of file diff --git a/regression/goto-instrument/unwind-zero-unwind3/test.desc b/regression/goto-instrument/unwind-zero-unwind3/test.desc index 94ddc4f8e82..5091bc953ae 100644 --- a/regression/goto-instrument/unwind-zero-unwind3/test.desc +++ b/regression/goto-instrument/unwind-zero-unwind3/test.desc @@ -5,5 +5,5 @@ main.c ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ -- -ASSUME FALSE +ASSUME false ^warning: ignoring diff --git a/src/goto-programs/goto_program.cpp b/src/goto-programs/goto_program.cpp index 5aac7fc0b60..de9aec6ffb1 100644 --- a/src/goto-programs/goto_program.cpp +++ b/src/goto-programs/goto_program.cpp @@ -16,6 +16,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include +#include #include #include #include @@ -75,8 +77,7 @@ std::ostream &goto_programt::output_instruction( case INCOMPLETE_GOTO: if(!instruction.get_condition().is_true()) { - out << "IF " << from_expr(ns, identifier, instruction.get_condition()) - << " THEN "; + out << "IF " << format(instruction.get_condition()) << " THEN "; } out << "GOTO "; @@ -103,22 +104,55 @@ std::ostream &goto_programt::output_instruction( case OTHER: if(instruction.get_other().id() == ID_code) { - const auto &code = to_code(instruction.get_other()); + const auto &code = instruction.get_other(); if(code.get_statement() == ID_havoc_object) { - out << "HAVOC_OBJECT " << from_expr(ns, identifier, code.op0()) << '\n'; + out << "HAVOC_OBJECT " << format(code.op0()) << '\n'; break; } // fallthrough } - // fallthrough + out << "OTHER " << format(instruction.get_other()); + break; case RETURN: + out << "RETURN " << format(instruction.return_value()) << '\n'; + break; + case DECL: + out << "DECL " << format(instruction.decl_symbol()) << " : " + << format(instruction.decl_symbol().type()) << '\n'; + break; + case DEAD: + out << "DEAD " << format(instruction.dead_symbol()) << '\n'; + break; + case FUNCTION_CALL: + out << "CALL "; + { + auto &call = instruction.get_function_call(); + if(call.lhs().is_not_nil()) + out << format(call.lhs()) << " := "; + out << format(call.function()); + out << '('; + bool first = true; + for(const auto &argument : call.arguments()) + { + if(first) + first = false; + else + out << ", "; + out << format(argument); + } + out << ')'; + out << '\n'; + } + break; + case ASSIGN: - out << from_expr(ns, identifier, instruction.get_code()) << '\n'; + out << "ASSIGN " << format(instruction.assign_lhs()) + << " := " << format(instruction.assign_rhs()) << '\n'; break; case ASSUME: @@ -129,7 +163,7 @@ std::ostream &goto_programt::output_instruction( out << "ASSERT "; { - out << from_expr(ns, identifier, instruction.get_condition()); + out << format(instruction.get_condition()); const irep_idt &comment=instruction.source_location.get_comment(); if(!comment.empty()) @@ -163,7 +197,7 @@ std::ostream &goto_programt::output_instruction( } if(instruction.get_code().operands().size() == 1) - out << ": " << from_expr(ns, identifier, instruction.get_code().op0()); + out << ": " << format(instruction.get_code().op0()); out << '\n'; break; @@ -173,11 +207,8 @@ std::ostream &goto_programt::output_instruction( if(instruction.get_code().get_statement() == ID_exception_landingpad) { const auto &landingpad = to_code_landingpad(instruction.get_code()); - out << "EXCEPTION LANDING PAD (" - << from_type(ns, identifier, landingpad.catch_expr().type()) - << ' ' - << from_expr(ns, identifier, landingpad.catch_expr()) - << ")"; + out << "EXCEPTION LANDING PAD (" << format(landingpad.catch_expr().type()) + << ' ' << format(landingpad.catch_expr()) << ")"; } else if(instruction.get_code().get_statement() == ID_push_catch) {