Merge pull request #8133 from tautschnig/cleanup/ts-config

Make ansi_c_internal_additions independent of the parser object

Author: tautschnig

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

src/ansi-c/ansi_c_internal_additions.h

@@ -12,7 +12,9 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <string>
 
-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[];

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();

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

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 &);
 

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);

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
       }

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)

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