diff --git a/src/ansi-c/ansi_c_internal_additions.cpp b/src/ansi-c/ansi_c_internal_additions.cpp index 749353af3ce..e3eaa05834e 100644 --- a/src/ansi-c/ansi_c_internal_additions.cpp +++ b/src/ansi-c/ansi_c_internal_additions.cpp @@ -158,7 +158,9 @@ max_malloc_size(std::size_t pointer_width, std::size_t object_bits) return ((mp_integer)1) << (mp_integer)bits_for_positive_offset; } -void ansi_c_internal_additions(std::string &code) +void ansi_c_internal_additions( + std::string &code, + bool support_ts_18661_3_Floatn_types) { // clang-format off // do the built-in types and variables @@ -247,9 +249,7 @@ void ansi_c_internal_additions(std::string &code) config.ansi_c.mode == configt::ansi_ct::flavourt::ARM) { code+=gcc_builtin_headers_types; - // check the parser and not config.ansi_c.ts_18661_3_Floatn_types to adjust - // behaviour depending on C or C++ context - if(ansi_c_parser.ts_18661_3_Floatn_types) + if(support_ts_18661_3_Floatn_types) code += gcc_builtin_headers_types_gcc7plus; // there are many more, e.g., look at diff --git a/src/ansi-c/ansi_c_internal_additions.h b/src/ansi-c/ansi_c_internal_additions.h index 735022d6703..c2531b65337 100644 --- a/src/ansi-c/ansi_c_internal_additions.h +++ b/src/ansi-c/ansi_c_internal_additions.h @@ -12,7 +12,9 @@ Author: Daniel Kroening, kroening@kroening.com #include -void ansi_c_internal_additions(std::string &code); +void ansi_c_internal_additions( + std::string &code, + bool support_ts_18661_3_Floatn_types); void ansi_c_architecture_strings(std::string &code); extern const char clang_builtin_headers[]; diff --git a/src/ansi-c/ansi_c_language.cpp b/src/ansi-c/ansi_c_language.cpp index af29ed2599e..c4eb9cadc14 100644 --- a/src/ansi-c/ansi_c_language.cpp +++ b/src/ansi-c/ansi_c_language.cpp @@ -68,7 +68,7 @@ bool ansi_c_languaget::parse( // parsing std::string code; - ansi_c_internal_additions(code); + ansi_c_internal_additions(code, config.ansi_c.ts_18661_3_Floatn_types); std::istringstream codestr(code); ansi_c_parser.clear(); diff --git a/src/ansi-c/builtin_factory.cpp b/src/ansi-c/builtin_factory.cpp index 0d9de3c48cd..bfed926cb03 100644 --- a/src/ansi-c/builtin_factory.cpp +++ b/src/ansi-c/builtin_factory.cpp @@ -97,6 +97,7 @@ static bool convert( //! \return 'true' on error bool builtin_factory( const irep_idt &identifier, + bool support_ts_18661_3_Floatn_types, symbol_table_baset &symbol_table, message_handlert &mh) { @@ -106,7 +107,7 @@ bool builtin_factory( std::ostringstream s; std::string code; - ansi_c_internal_additions(code); + ansi_c_internal_additions(code, support_ts_18661_3_Floatn_types); s << code; // our own extensions diff --git a/src/ansi-c/builtin_factory.h b/src/ansi-c/builtin_factory.h index 8a012894c3f..e270d4917f1 100644 --- a/src/ansi-c/builtin_factory.h +++ b/src/ansi-c/builtin_factory.h @@ -17,6 +17,7 @@ class symbol_table_baset; //! \return 'true' in case of error bool builtin_factory( const irep_idt &identifier, + bool support_ts_18661_3_Floatn_types, symbol_table_baset &, message_handlert &); diff --git a/src/ansi-c/c_typecheck_base.h b/src/ansi-c/c_typecheck_base.h index bbe4948376e..dc0b11a209a 100644 --- a/src/ansi-c/c_typecheck_base.h +++ b/src/ansi-c/c_typecheck_base.h @@ -250,6 +250,8 @@ class c_typecheck_baset: virtual bool gcc_types_compatible_p(const typet &, const typet &); + virtual bool builtin_factory(const irep_idt &); + // types virtual void typecheck_type(typet &type); virtual void typecheck_compound_type(struct_union_typet &type); diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index df210afc6cf..1879b6a8dc2 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -2072,6 +2072,15 @@ void c_typecheck_baset::typecheck_obeys_contract_call( expr.type() = bool_typet(); } +bool c_typecheck_baset::builtin_factory(const irep_idt &identifier) +{ + return ::builtin_factory( + identifier, + config.ansi_c.ts_18661_3_Floatn_types, + symbol_table, + get_message_handler()); +} + void c_typecheck_baset::typecheck_side_effect_function_call( side_effect_expr_function_callt &expr) { @@ -2106,7 +2115,7 @@ void c_typecheck_baset::typecheck_side_effect_function_call( typecheck_typed_target_call(expr); } // Is this a builtin? - else if(!builtin_factory(identifier, symbol_table, get_message_handler())) + else if(!builtin_factory(identifier)) { // yes, it's a builtin } diff --git a/src/cpp/cpp_typecheck.cpp b/src/cpp/cpp_typecheck.cpp index 06f6f69009b..6f888c1cb79 100644 --- a/src/cpp/cpp_typecheck.cpp +++ b/src/cpp/cpp_typecheck.cpp @@ -325,7 +325,8 @@ void cpp_typecheckt::clean_up() bool cpp_typecheckt::builtin_factory(const irep_idt &identifier) { - return ::builtin_factory(identifier, symbol_table, get_message_handler()); + return ::builtin_factory( + identifier, false, symbol_table, get_message_handler()); } bool cpp_typecheckt::contains_cpp_name(const exprt &expr) diff --git a/src/cpp/cpp_typecheck.h b/src/cpp/cpp_typecheck.h index 814b3d8c13e..0e64a2f38cb 100644 --- a/src/cpp/cpp_typecheck.h +++ b/src/cpp/cpp_typecheck.h @@ -343,7 +343,7 @@ class cpp_typecheckt:public c_typecheck_baset void add_method_body(symbolt *_method_symbol); - bool builtin_factory(const irep_idt &); + bool builtin_factory(const irep_idt &) override; // types