From aa01c8fb2556b4f41d37625102cb2d1ef2bffe92 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Thu, 6 Feb 2025 17:33:06 +0000
Subject: [PATCH] SMV: clean up parser code

This removes an unused functionality to read a CTL formula.
---
 regression/smv/syntax-errors/syntax2.desc |  2 +-
 src/smvlang/parser.y                      |  3 ---
 src/smvlang/smv_language.cpp              | 10 ----------
 src/smvlang/smv_parse_tree.h              |  5 +----
 src/smvlang/smv_parser.h                  |  2 +-
 5 files changed, 3 insertions(+), 19 deletions(-)

diff --git a/regression/smv/syntax-errors/syntax2.desc b/regression/smv/syntax-errors/syntax2.desc
index a70f65a7f..0337f3e08 100644
--- a/regression/smv/syntax-errors/syntax2.desc
+++ b/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$
 --
diff --git a/src/smvlang/parser.y b/src/smvlang/parser.y
index e4fb057a6..1b25fdc62 100644
--- a/src/smvlang/parser.y
+++ b/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
diff --git a/src/smvlang/smv_language.cpp b/src/smvlang/smv_language.cpp
index 326d201c9..4b04e86bd 100644
--- a/src/smvlang/smv_language.cpp
+++ b/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;
diff --git a/src/smvlang/smv_parse_tree.h b/src/smvlang/smv_parse_tree.h
index cc1076d3e..7191c99ce 100644
--- a/src/smvlang/smv_parse_tree.h
+++ b/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;
diff --git a/src/smvlang/smv_parser.h b/src/smvlang/smv_parser.h
index 7f48407cc..683d8844d 100644
--- a/src/smvlang/smv_parser.h
+++ b/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();