Default fall-through for function pointer removal
When the pointer points to neither of the candidates we shouldn't just call the first one (which does happen if the user does not request pointer-check). This PR inserts an ASSUME (false) which makes all subsequent assertions unreachable (and thus reported as not being violated). A small regression test is included.
This commit is contained in:
parent
73be2edd16
commit
eaa73cbb1e
|
@ -0,0 +1,34 @@
|
|||
// f is set to 0 -> does not point to either f1 or f2
|
||||
#include <assert.h>
|
||||
|
||||
typedef int (*f_ptr)(int);
|
||||
|
||||
extern f_ptr f;
|
||||
|
||||
int f1(int j);
|
||||
int f2(int i);
|
||||
|
||||
int f1(int j)
|
||||
{
|
||||
f = &f2;
|
||||
return 1;
|
||||
}
|
||||
int f2(int i)
|
||||
{
|
||||
assert(0);
|
||||
return 2;
|
||||
}
|
||||
|
||||
f_ptr f = 0;
|
||||
|
||||
int main()
|
||||
{
|
||||
int x = 0;
|
||||
|
||||
x = f(x);
|
||||
assert(x == 1);
|
||||
x = f(x);
|
||||
assert(x == 2);
|
||||
|
||||
return 0;
|
||||
}
|
|
@ -0,0 +1,11 @@
|
|||
CORE
|
||||
main.c
|
||||
|
||||
^EXIT=0$
|
||||
^SIGNAL=0$
|
||||
\[f2.assertion.1\] line [0-9]+ assertion 0: SUCCESS
|
||||
\[main.assertion.1\] line [0-9]+ assertion x == 1: SUCCESS
|
||||
\[main.assertion.2\] line [0-9]+ assertion x == 2: SUCCESS
|
||||
^VERIFICATION SUCCESSFUL$
|
||||
--
|
||||
^warning: ignoring
|
|
@ -416,6 +416,7 @@ void remove_function_pointerst::remove_function_pointer(
|
|||
t->source_location.set_property_class("pointer dereference");
|
||||
t->source_location.set_comment("invalid function pointer");
|
||||
}
|
||||
new_code_gotos.add(goto_programt::make_assumption(false_exprt()));
|
||||
|
||||
goto_programt new_code;
|
||||
|
||||
|
|
Loading…
Reference in New Issue