SMV: IVAR declarations

This adds IVAR declarations to the SMV frontend.

Author: kroening

regression/smv/ivar/ivar1.smv

@@ -1,3 +1,9 @@
 MODULE main
 
 IVAR some_input : boolean;
+
+-- these should all fail
+LTLSPEC some_input
+LTLSPEC !some_input
+LTLSPEC X some_input
+LTLSPEC X !some_input

src/smvlang/parser.y

@@ -419,7 +419,15 @@ frozenvar_declaration:
 
 simple_var_list:
              identifier ':' simple_type_specifier ';'
+           {
+             init($$);
+             stack_expr($$).add_to_operands(unary_exprt{ID_decl, stack_expr($1), stack_type($3)});
+           }
            | simple_var_list identifier ':' simple_type_specifier ';'
+           {
+             $$ = $1;
+             stack_expr($$).add_to_operands(unary_exprt{ID_decl, stack_expr($2), stack_type($4)});
+           }
            ;
 
 define_declaration:

src/smvlang/smv_parse_tree.cpp

@@ -76,6 +76,8 @@ std::string to_string(smv_parse_treet::modulet::itemt::item_typet i)
     return "DEFINE";
   case smv_parse_treet::modulet::itemt::ENUM:
     return "ENUM";
+  case smv_parse_treet::modulet::itemt::IVAR:
+    return "IVAR";
   case smv_parse_treet::modulet::itemt::VAR:
     return "VAR";
 

src/smvlang/smv_parse_tree.h

@@ -52,6 +52,7 @@ class smv_parse_treet
         FAIRNESS,
         INIT,
         INVAR,
+        IVAR,
         LTLSPEC,
         TRANS,
         VAR
@@ -260,6 +261,13 @@ class smv_parse_treet
       items.emplace_back(itemt::TRANS, std::move(expr), std::move(location));
     }
 
+    void add_ivar(exprt expr, typet type)
+    {
+      expr.type() = std::move(type);
+      auto location = expr.source_location();
+      items.emplace_back(itemt::IVAR, std::move(expr), std::move(location));
+    }
+
     void add_var(exprt expr, typet type)
     {
       expr.type() = std::move(type);

src/smvlang/smv_typecheck.cpp

@@ -2033,6 +2033,7 @@ void smv_typecheckt::typecheck(
     return;
 
   case smv_parse_treet::modulet::itemt::ENUM:
+  case smv_parse_treet::modulet::itemt::IVAR:
   case smv_parse_treet::modulet::itemt::VAR:
     return;
   }