diff --git a/regression/ansi-c/linking1/main.c b/regression/ansi-c/linking1/main.c new file mode 100644 index 00000000000..7019f2068da --- /dev/null +++ b/regression/ansi-c/linking1/main.c @@ -0,0 +1,7 @@ +void f(int); + +int main(int argc, char *argv[]) +{ + f(argc); + return 0; +} diff --git a/regression/ansi-c/linking1/module.c b/regression/ansi-c/linking1/module.c new file mode 100644 index 00000000000..e5f70ba1388 --- /dev/null +++ b/regression/ansi-c/linking1/module.c @@ -0,0 +1,3 @@ +void f(float param) +{ +} diff --git a/regression/ansi-c/linking1/test.desc b/regression/ansi-c/linking1/test.desc new file mode 100644 index 00000000000..69f7f7c4a2d --- /dev/null +++ b/regression/ansi-c/linking1/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +module.c +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +^CONVERSION ERROR$ diff --git a/regression/cbmc/Linking7/main.c b/regression/cbmc/Linking7/main.c new file mode 100644 index 00000000000..303b752813b --- /dev/null +++ b/regression/cbmc/Linking7/main.c @@ -0,0 +1,19 @@ +struct S +{ + void *a; + void *b; +}; + +typedef void (*fptr)(struct S); + +extern void foo(struct S s); + +fptr A[] = { foo }; + +extern void bar(); + +int main() +{ + bar(); + return 0; +} diff --git a/regression/cbmc/Linking7/member-name-mismatch.desc b/regression/cbmc/Linking7/member-name-mismatch.desc new file mode 100644 index 00000000000..ff30eee14c6 --- /dev/null +++ b/regression/cbmc/Linking7/member-name-mismatch.desc @@ -0,0 +1,11 @@ +KNOWNBUG +main.c +module2.c +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +^\*\* 1 of 2 failed +-- +^warning: ignoring +-- +This is either a bug in goto-symex or value_sett (where the invariant fails). diff --git a/regression/cbmc/Linking7/module.c b/regression/cbmc/Linking7/module.c new file mode 100644 index 00000000000..7ffca0fc005 --- /dev/null +++ b/regression/cbmc/Linking7/module.c @@ -0,0 +1,32 @@ +#include + +struct S +{ + void *a; + void *b; +}; + +typedef void (*fptr)(struct S); + +extern fptr A[1]; + +struct real_S +{ + int *a; + int *b; +}; + +void foo(struct real_S g) +{ + assert(*g.a == 42); + assert(*g.b == 41); +} + +void bar() +{ + int x = 42; + struct real_S s; + s.a = &x; + s.b = &x; + A[0]((struct S){ s.a, s.b }); +} diff --git a/regression/cbmc/Linking7/module2.c b/regression/cbmc/Linking7/module2.c new file mode 100644 index 00000000000..2cc503b5c11 --- /dev/null +++ b/regression/cbmc/Linking7/module2.c @@ -0,0 +1,32 @@ +#include + +struct S +{ + void *a; + void *b; +}; + +typedef void (*fptr)(struct S); + +extern fptr A[1]; + +struct real_S +{ + int *a; + int *c; +}; + +void foo(struct real_S g) +{ + assert(*g.a == 42); + assert(*g.c == 41); +} + +void bar() +{ + int x = 42; + struct real_S s; + s.a = &x; + s.c = &x; + A[0]((struct S){ s.a, s.c }); +} diff --git a/regression/cbmc/Linking7/test.desc b/regression/cbmc/Linking7/test.desc new file mode 100644 index 00000000000..4eaef880405 --- /dev/null +++ b/regression/cbmc/Linking7/test.desc @@ -0,0 +1,9 @@ +CORE +main.c +module.c +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +^\*\* 1 of 2 failed +-- +^warning: ignoring diff --git a/src/goto-programs/remove_function_pointers.cpp b/src/goto-programs/remove_function_pointers.cpp index 7f1ef61dce2..2c611df8592 100644 --- a/src/goto-programs/remove_function_pointers.cpp +++ b/src/goto-programs/remove_function_pointers.cpp @@ -13,18 +13,18 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include +#include #include +#include +#include +#include #include #include #include #include -#include -#include #include -#include - -#include #include "remove_skip.h" #include "compute_called_functions.h" @@ -135,8 +135,8 @@ bool remove_function_pointerst::arg_is_type_compatible( return false; } - // structs/unions need to match, - // which could be made more generous + return pointer_offset_bits(call_type, ns) == + pointer_offset_bits(function_type, ns); return false; } diff --git a/src/linking/linking.cpp b/src/linking/linking.cpp index a93e0919e64..4e480e7570f 100644 --- a/src/linking/linking.cpp +++ b/src/linking/linking.cpp @@ -701,6 +701,17 @@ void linkingt::duplicate_code_symbol( if(!found) break; } + // different non-pointer arguments with implementation - the + // implementation is always right, even though such code may + // be severely broken + else if(pointer_offset_bits(t1, ns)==pointer_offset_bits(t2, ns) && + old_symbol.value.is_nil()!=new_symbol.value.is_nil()) + { + if(warn_msg.empty()) + warn_msg="non-pointer parameter types differ between " + "declaration and definition"; + replace=new_symbol.value.is_not_nil(); + } else break;