From d074537b7a7e2d5bdd4a02a0ae58edb651ab3d0b Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sat, 9 Sep 2017 17:57:47 +0100 Subject: [PATCH 1/2] test for signature conflict with undeclared function --- regression/cbmc/return6/f_def.c | 4 ++++ regression/cbmc/return6/main.c | 11 +++++++++++ regression/cbmc/return6/test.desc | 8 ++++++++ 3 files changed, 23 insertions(+) create mode 100644 regression/cbmc/return6/f_def.c create mode 100644 regression/cbmc/return6/main.c create mode 100644 regression/cbmc/return6/test.desc diff --git a/regression/cbmc/return6/f_def.c b/regression/cbmc/return6/f_def.c new file mode 100644 index 00000000000..1a49f8dd048 --- /dev/null +++ b/regression/cbmc/return6/f_def.c @@ -0,0 +1,4 @@ +unsigned f() +{ + return 0x34; +} diff --git a/regression/cbmc/return6/main.c b/regression/cbmc/return6/main.c new file mode 100644 index 00000000000..46af9aecc3b --- /dev/null +++ b/regression/cbmc/return6/main.c @@ -0,0 +1,11 @@ +#include + +// Do not declare f(). +// This is invalid from C99 upwards, but kind of ok before. + +int main() +{ + int return_value; + return_value=f(); + assert(return_value==0x34); +} diff --git a/regression/cbmc/return6/test.desc b/regression/cbmc/return6/test.desc new file mode 100644 index 00000000000..41ed6840d59 --- /dev/null +++ b/regression/cbmc/return6/test.desc @@ -0,0 +1,8 @@ +KNOWNBUG +main.c +f_def.c +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring From 5c18ccc729a91289c351525eb5fef95035db6e04 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 2 Mar 2018 17:51:17 +0000 Subject: [PATCH 2/2] Type conflicts on the return value of implicitly declared functions are errors --- regression/cbmc/return6/test.desc | 7 ++++--- src/linking/linking.cpp | 35 +++++++++++++++++++++---------- 2 files changed, 28 insertions(+), 14 deletions(-) diff --git a/regression/cbmc/return6/test.desc b/regression/cbmc/return6/test.desc index 41ed6840d59..2fc10d239b2 100644 --- a/regression/cbmc/return6/test.desc +++ b/regression/cbmc/return6/test.desc @@ -1,8 +1,9 @@ -KNOWNBUG +CORE main.c f_def.c -^EXIT=0$ +^EXIT=6$ ^SIGNAL=0$ -^VERIFICATION SUCCESSFUL$ +CONVERSION ERROR -- ^warning: ignoring +^VERIFICATION SUCCESSFUL$ diff --git a/src/linking/linking.cpp b/src/linking/linking.cpp index 7b2289256bf..601b77c3d4c 100644 --- a/src/linking/linking.cpp +++ b/src/linking/linking.cpp @@ -452,15 +452,23 @@ void linkingt::duplicate_code_symbol( const code_typet &old_t=to_code_type(old_symbol.type); const code_typet &new_t=to_code_type(new_symbol.type); - // if one of them was an implicit declaration, just issue a warning + // if one of them was an implicit declaration then only conflicts on the + // return type are an error as we would end up with assignments with + // mismatching types; as we currently do not patch these by inserting type + // casts we need to fail hard if(!old_symbol.location.get_function().empty() && old_symbol.value.is_nil()) { - // issue a warning and overwrite - link_warning( - old_symbol, - new_symbol, - "implicit function declaration"); + if(base_type_eq(old_t.return_type(), new_t.return_type(), ns)) + link_warning( + old_symbol, + new_symbol, + "implicit function declaration"); + else + link_error( + old_symbol, + new_symbol, + "implicit function declaration"); old_symbol.type=new_symbol.type; old_symbol.location=new_symbol.location; @@ -469,11 +477,16 @@ void linkingt::duplicate_code_symbol( else if(!new_symbol.location.get_function().empty() && new_symbol.value.is_nil()) { - // issue a warning - link_warning( - old_symbol, - new_symbol, - "ignoring conflicting implicit function declaration"); + if(base_type_eq(old_t.return_type(), new_t.return_type(), ns)) + link_warning( + old_symbol, + new_symbol, + "ignoring conflicting implicit function declaration"); + else + link_error( + old_symbol, + new_symbol, + "implicit function declaration"); } // handle (incomplete) function prototypes else if(base_type_eq(old_t.return_type(), new_t.return_type(), ns) &&