From fad80239194acc2e65c24d5a5f5e43f04e095cbd Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 30 Sep 2022 10:37:57 +0000 Subject: [PATCH] C front-end: floating-point built-ins are in the symbol table It should never be the case that no symbol for `__CPROVER_isgreaterf`, `__CPROVER_isgreaterd` and similar floating-point built-ins is present for these are declared in cprover_builtin_headers.h. This commit removes dead code and adds an additional consistency check. --- src/goto-programs/builtin_functions.cpp | 14 +++++--------- 1 file changed, 5 insertions(+), 9 deletions(-) diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp index a66085357bc..6cfe2c7e335 100644 --- a/src/goto-programs/builtin_functions.cpp +++ b/src/goto-programs/builtin_functions.cpp @@ -24,7 +24,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include +#include #include @@ -1473,6 +1473,10 @@ void goto_convertt::do_function_call_symbol( // append d or f for double/float name+=use_double?'d':'f'; + DATA_INVARIANT( + ns.lookup(name).type == f_type, + "builtin declaration should match constructed type"); + symbol_exprt new_function=function; new_function.set_identifier(name); new_function.type()=f_type; @@ -1480,14 +1484,6 @@ void goto_convertt::do_function_call_symbol( code_function_callt function_call(lhs, new_function, new_arguments); function_call.add_source_location()=function.source_location(); - if(!symbol_table.has_symbol(name)) - { - symbolt new_symbol{name, f_type, mode}; - new_symbol.base_name=name; - new_symbol.location=function.source_location(); - symbol_table.add(new_symbol); - } - copy(function_call, FUNCTION_CALL, dest); } else if(identifier == "alloca" || identifier == "__builtin_alloca")