SMV: clean up parser code

This removes an unused functionality to read a CTL formula.

Author: kroening

regression/smv/syntax-errors/syntax2.desc

@@ -1,7 +1,7 @@
 CORE
 syntax2.smv
 
-^file .* line 3: syntax error, unexpected VAR before 'VAR'$
+^file .* line 3: syntax error, unexpected VAR, expecting MODULE before 'VAR'$
 ^EXIT=1$
 ^SIGNAL=0$
 --

src/smvlang/parser.y

@@ -140,7 +140,6 @@ static void new_module(YYSTYPE &module)
   PARSER.module=&PARSER.parse_tree.modules[name];
   PARSER.module->name=name;
   PARSER.module->base_name=stack_expr(module).id_string();
-  PARSER.module->used=true;
 }
 
 /*------------------------------------------------------------------------*/
@@ -236,8 +235,6 @@ static void new_module(YYSTYPE &module)
 %%
 
 start      : modules
-           | formula { PARSER.module->add_ctlspec(stack_expr($1));
-                       PARSER.module->used=true; }
            ;
 
 modules    : module

src/smvlang/smv_language.cpp

@@ -34,21 +34,11 @@ bool smv_languaget::parse(
 {
   smv_parsert smv_parser(message_handler);
 
-  const std::string main_name=smv_module_symbol("main");
-  smv_parser.module=&smv_parser.parse_tree.modules[main_name];
-  smv_parser.module->name=main_name;
-  smv_parser.module->base_name="main";
-
   smv_parser.set_file(path);
   smv_parser.in=&instream;
 
   bool result=smv_parser.parse();
 
-  // see if we used main
-
-  if(!smv_parser.parse_tree.modules[main_name].used)
-    smv_parser.parse_tree.modules.erase(main_name);
-
   smv_parse_tree.swap(smv_parser.parse_tree);
 
   return result;

src/smvlang/smv_parse_tree.h

@@ -175,11 +175,8 @@ class smv_parse_treet
 
     mc_varst vars;
     enum_sett enum_set;
-    bool used;
-    
+
     std::list<irep_idt> ports;
-    
-    modulet():used(false) { }
   };
 
   typedef std::unordered_map<irep_idt, modulet, irep_id_hash> modulest;

src/smvlang/smv_parser.h

@@ -34,7 +34,7 @@ class smv_parsert:public parsert
 
   smv_parse_treet parse_tree;
   smv_parse_treet::modulet *module;
-  
+
   virtual bool parse()
   {
     return yysmvparse();