Skip to content

Commit 3c69aa1

Browse files
authored
Merge pull request #7011 from tautschnig/bugfixes/6983-take-2
Enable the function-pointer fall-back assertion by default
2 parents a96dea4 + 86c8181 commit 3c69aa1

File tree

14 files changed

+32
-101
lines changed

14 files changed

+32
-101
lines changed

jbmc/src/jdiff/jdiff_parse_options.cpp

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -172,8 +172,7 @@ bool jdiff_parse_optionst::process_goto_program(
172172
// remove function pointers
173173
log.status() << "Removing function pointers and virtual functions"
174174
<< messaget::eom;
175-
remove_function_pointers(
176-
ui_message_handler, goto_model, cmdline.isset("pointer-check"));
175+
remove_function_pointers(ui_message_handler, goto_model, false);
177176

178177
// Java virtual functions -> explicit dispatch tables:
179178
remove_virtual_functions(goto_model);

regression/cbmc-concurrency/pthread_join1/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,6 @@ main.c
55
^SIGNAL=0$
66
^\[main\.assertion\.1\] line 21 assertion i==1: FAILURE$
77
^\[main\.assertion\.2\] line 22 assertion i==2: SUCCESS$
8-
^\*\* 1 of 2 failed
8+
^\*\* 1 of 3 failed
99
--
1010
^warning: ignoring

regression/cbmc-library/pthread_cond_wait-01/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ main.c
33
--bounds-check
44
^EXIT=10$
55
^SIGNAL=0$
6-
^\*\* 1 of 2 failed
6+
^\*\* 1 of 3 failed
77
^VERIFICATION FAILED$
88
--
99
^warning: ignoring
Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,12 @@
11
CORE
22
main.c
33

4-
^EXIT=0$
4+
^EXIT=10$
55
^SIGNAL=0$
66
\[f2.assertion.1\] line [0-9]+ assertion 0: SUCCESS
7+
\[main.pointer_dereference.1\] line 28 dereferenced function pointer must be f2: FAILURE$
78
\[main.assertion.1\] line [0-9]+ assertion x == 1: SUCCESS
89
\[main.assertion.2\] line [0-9]+ assertion x == 2: SUCCESS
9-
^VERIFICATION SUCCESSFUL$
10+
^VERIFICATION FAILED$
1011
--
1112
^warning: ignoring

regression/cbmc/Linking7/member-name-mismatch.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,6 @@ module2.c
66
^VERIFICATION FAILED$
77
line 21 assertion \*g\.a == 42: SUCCESS
88
line 22 assertion \*g\.c == 41: FAILURE
9-
^\*\* 1 of 2 failed
9+
^\*\* 1 of 3 failed
1010
--
1111
^warning: ignoring

regression/cbmc/Linking7/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ module.c
44
^EXIT=10$
55
^SIGNAL=0$
66
^VERIFICATION FAILED$
7-
^\*\* 1 of 2 failed
7+
^\*\* 1 of 3 failed
88
line 21 assertion \*g\.a == 42: SUCCESS
99
line 22 assertion \*g\.b == 41: FAILURE
1010
--

regression/goto-instrument/value-set-fi-fp-removal4/test.desc

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,11 @@
11
CORE
22
test.c
33
--value-set-fi-fp-removal
4-
^EXIT=0$
4+
^EXIT=10$
55
^SIGNAL=0$
66
^file test.c line 20 function main: replacing function pointer by 2 possible targets$
7+
\[main.pointer_dereference.1\] line 20 dereferenced function pointer must be one of \[(g, f|f, g)\]: FAILURE$
8+
--
79
--
810
This test checks that the value-set-fi-based function pointer removal
911
precisely identifies the function to call for a particular function pointer

regression/goto-instrument/value-set-fi-fp-removal5/test.desc

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,11 @@
11
CORE
22
test.c
33
--value-set-fi-fp-removal
4-
^EXIT=0$
4+
^EXIT=10$
55
^SIGNAL=0$
66
^file test.c line 19 function main: replacing function pointer by 0 possible targets$
7+
\[main.pointer_dereference.1\] line 19 no candidates for dereferenced function pointer: FAILURE$
8+
--
79
--
810
This test checks that the value-set-fi-based function pointer removal
911
precisely identifies the function to call for a particular function pointer

src/goto-instrument/goto_instrument_parse_options.cpp

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -945,8 +945,7 @@ void goto_instrument_parse_optionst::do_indirect_call_and_rtti_removal(
945945
function_pointer_removal_done=true;
946946

947947
log.status() << "Function Pointer Removal" << messaget::eom;
948-
remove_function_pointers(
949-
ui_message_handler, goto_model, cmdline.isset("pointer-check"));
948+
remove_function_pointers(ui_message_handler, goto_model, false);
950949
log.status() << "Virtual function removal" << messaget::eom;
951950
remove_virtual_functions(goto_model);
952951
log.status() << "Cleaning inline assembler statements" << messaget::eom;
@@ -969,7 +968,6 @@ void goto_instrument_parse_optionst::do_remove_const_function_pointers_only()
969968
remove_function_pointers(
970969
ui_message_handler,
971970
goto_model,
972-
cmdline.isset("pointer-check"),
973971
true); // abort if we can't resolve via const pointers
974972
}
975973

src/goto-instrument/value_set_fi_fp_removal.cpp

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -75,8 +75,7 @@ void value_set_fi_fp_removal(
7575
f.second.body,
7676
f.first,
7777
target,
78-
functions,
79-
true);
78+
functions);
8079
}
8180
}
8281
}

0 commit comments

Comments
 (0)