Merge pull request #8141 from tautschnig/cleanup/ansi_c_parsert

ansi_c_parsert: construct with message handler

regression/cbmc/fault_localization-all_properties2/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+FUTURE
 main.c
 --localize-faults
 ^EXIT=10$
@@ -8,4 +8,6 @@ line 9 function main$
 --
 --
 CBMC wrongly reports line 7 as the faulty statement when instead it should be
-line 9.
+line 9. The test is marked as "FUTURE" as it will sometimes pass, depending on
+what model the solver produces. It would, therefore, break our checking of
+"KNOWNBUG" tests.

src/ansi-c/ansi_c_language.cpp

@@ -71,10 +71,9 @@ bool ansi_c_languaget::parse(
   ansi_c_internal_additions(code, config.ansi_c.float16_type);
   std::istringstream codestr(code);
 
-  ansi_c_parser.clear();
+  ansi_c_parsert ansi_c_parser{message_handler};
   ansi_c_parser.set_file(ID_built_in);
   ansi_c_parser.in=&codestr;
-  ansi_c_parser.log.set_message_handler(message_handler);
   ansi_c_parser.for_has_scope=config.ansi_c.for_has_scope;
   ansi_c_parser.ts_18661_3_Floatn_types=config.ansi_c.ts_18661_3_Floatn_types;
   ansi_c_parser.float16_type = config.ansi_c.float16_type;
@@ -83,25 +82,19 @@ bool ansi_c_languaget::parse(
   ansi_c_parser.cpp11=false; // it's not C++
   ansi_c_parser.mode=config.ansi_c.mode;
 
-  ansi_c_scanner_init();
-
   bool result=ansi_c_parser.parse();
 
   if(!result)
   {
     ansi_c_parser.set_line_no(0);
     ansi_c_parser.set_file(path);
     ansi_c_parser.in=&i_preprocessed;
-    ansi_c_scanner_init();
     result=ansi_c_parser.parse();
   }
 
   // save result
   parse_tree.swap(ansi_c_parser.parse_tree);
 
-  // save some memory
-  ansi_c_parser.clear();
-
   return result;
 }
 
@@ -199,15 +192,16 @@ bool ansi_c_languaget::to_expr(
 
   // parsing
 
-  ansi_c_parser.clear();
+  ansi_c_parsert ansi_c_parser{message_handler};
   ansi_c_parser.set_file(irep_idt());
   ansi_c_parser.in=&i_preprocessed;
-  ansi_c_parser.log.set_message_handler(message_handler);
-  ansi_c_parser.mode=config.ansi_c.mode;
+  ansi_c_parser.for_has_scope = config.ansi_c.for_has_scope;
   ansi_c_parser.ts_18661_3_Floatn_types=config.ansi_c.ts_18661_3_Floatn_types;
   ansi_c_parser.float16_type = config.ansi_c.float16_type;
   ansi_c_parser.bf16_type = config.ansi_c.bf16_type;
-  ansi_c_scanner_init();
+  ansi_c_parser.cpp98 = false; // it's not C++
+  ansi_c_parser.cpp11 = false; // it's not C++
+  ansi_c_parser.mode = config.ansi_c.mode;
 
   bool result=ansi_c_parser.parse();
 
@@ -221,9 +215,6 @@ bool ansi_c_languaget::to_expr(
     result = ansi_c_typecheck(expr, message_handler, ns);
   }
 
-  // save some memory
-  ansi_c_parser.clear();
-
   // now remove that (void) cast
   if(expr.id()==ID_typecast &&
      expr.type().id()==ID_empty &&

src/ansi-c/ansi_c_parser.cpp

@@ -10,7 +10,22 @@ Author: Daniel Kroening, [email protected]
 
 #include "c_storage_spec.h"
 
-ansi_c_parsert ansi_c_parser;
+int yyansi_clex_init_extra(ansi_c_parsert *, void **);
+int yyansi_clex_destroy(void *);
+int yyansi_cparse(ansi_c_parsert &, void *);
+void yyansi_cset_debug(int, void *);
+
+bool ansi_c_parsert::parse()
+{
+  void *scanner;
+  yyansi_clex_init_extra(this, &scanner);
+#ifdef ANSI_C_DEBUG
+  yyansi_cset_debug(1, scanner);
+#endif
+  bool parse_fail = yyansi_cparse(*this, scanner) != 0;
+  yyansi_clex_destroy(scanner);
+  return parse_fail;
+}
 
 ansi_c_id_classt ansi_c_parsert::lookup(
   const irep_idt &base_name,
@@ -73,14 +88,6 @@ void ansi_c_parsert::add_tag_with_body(irept &tag)
   }
 }
 
-extern char *yyansi_ctext;
-
-int yyansi_cerror(const std::string &error)
-{
-  ansi_c_parser.parse_error(error, yyansi_ctext);
-  return 0;
-}
-
 void ansi_c_parsert::add_declarator(
   exprt &declaration,
   irept &declarator)

src/ansi-c/ansi_c_parser.h

@@ -18,15 +18,14 @@ Author: Daniel Kroening, [email protected]
 #include "ansi_c_parse_tree.h"
 #include "ansi_c_scope.h"
 
-int yyansi_cparse();
-
 class ansi_c_parsert:public parsert
 {
 public:
   ansi_c_parse_treet parse_tree;
 
-  ansi_c_parsert()
-    : tag_following(false),
+  explicit ansi_c_parsert(message_handlert &message_handler)
+    : parsert(message_handler),
+      tag_following(false),
       asm_block_following(false),
       parenthesis_counter(0),
       mode(modet::NONE),
@@ -37,14 +36,14 @@ class ansi_c_parsert:public parsert
       float16_type(false),
       bf16_type(false)
   {
+    // set up global scope
+    scopes.clear();
+    scopes.push_back(scopet());
   }
 
-  virtual bool parse() override
-  {
-    return yyansi_cparse()!=0;
-  }
+  bool parse() override;
 
-  virtual void clear() override
+  void clear() override
   {
     parsert::clear();
     parse_tree.clear();
@@ -170,9 +169,4 @@ class ansi_c_parsert:public parsert
   std::list<std::map<const irep_idt, bool>> pragma_cprover_stack;
 };
 
-extern ansi_c_parsert ansi_c_parser;
-
-int yyansi_cerror(const std::string &error);
-void ansi_c_scanner_init();
-
 #endif // CPROVER_ANSI_C_ANSI_C_PARSER_H

src/ansi-c/builtin_factory.cpp

@@ -47,17 +47,17 @@ static bool convert(
 {
   std::istringstream in(s.str());
 
-  ansi_c_parser.clear();
+  ansi_c_parsert ansi_c_parser{message_handler};
   ansi_c_parser.set_file(ID_built_in);
   ansi_c_parser.in=∈
-  ansi_c_parser.log.set_message_handler(message_handler);
   ansi_c_parser.for_has_scope=config.ansi_c.for_has_scope;
+  ansi_c_parser.ts_18661_3_Floatn_types = config.ansi_c.ts_18661_3_Floatn_types;
+  ansi_c_parser.float16_type = config.ansi_c.float16_type;
+  ansi_c_parser.bf16_type = config.ansi_c.bf16_type;
   ansi_c_parser.cpp98=false; // it's not C++
   ansi_c_parser.cpp11=false; // it's not C++
   ansi_c_parser.mode=config.ansi_c.mode;
 
-  ansi_c_scanner_init();
-
   if(ansi_c_parser.parse())
     return true;