SMV: grammar for self expression

This adds the grammar for parsing self expressions.  They are rejected by
the type checker as unsupported.

Author: kroening

regression/smv/modules/self1.desc

@@ -1,9 +1,9 @@
-KNOWNBUG
+CORE
 self1.smv
 
-^EXIT=0$
+^file .* line 4: no support for self$
+^EXIT=2$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-This does not parse.

src/hw_cbmc_irep_ids.h

@@ -36,6 +36,7 @@ IREP_ID_TWO(C_smv_iff, "#smv_iff")
 IREP_ID_ONE(smv_range)
 IREP_ID_ONE(smv_resize)
 IREP_ID_ONE(smv_toint)
+IREP_ID_ONE(smv_self)
 IREP_ID_ONE(smv_set)
 IREP_ID_ONE(smv_setin)
 IREP_ID_ONE(smv_setnotin)

src/smvlang/parser.y

@@ -738,6 +738,11 @@ basic_expr : constant
              unary($$, ID_member, $1);
              stack_expr($$).set(ID_component_name, stack_expr($3).id());
            }
+           | self_Token
+           {
+             // This rule is part of "complex_identifier" in the NuSMV manual.
+             init($$, ID_smv_self);
+           }
            | basic_expr '(' basic_expr ')'
            {
              // Not in the NuSMV grammar.

src/smvlang/smv_typecheck.cpp

@@ -1928,6 +1928,11 @@ void smv_typecheckt::convert(exprt &expr)
     tmp.set_identifier(id2string(tmp.get_identifier()) + '.' + index_string);
     expr = tmp;
   }
+  else if(expr.id() == ID_smv_self)
+  {
+    throw errort().with_location(expr.source_location())
+      << "no support for self";
+  }
   else if(expr.id()=="smv_nondet_choice" ||
           expr.id()=="smv_union")
   {