SMV: remove legacy grammar rules

This removes the parser rules and type checking related to the following
legacy constructs:

* EXTERN
* INC, DEC, ADD, SUB
* complex identifiers that contain round ( ... ) parentheses
* switch
* notin

None of these are recognised by NuSMV.

Author: kroening

CHANGELOG

@@ -1,3 +1,7 @@
+# EBMC 6.0
+
+* SMV: removed legacy keywords EXTERN and switch
+
 # EBMC 5.9
 
 * Verilog: fix for four-valued | and &

regression/smv/smv/smv1.desc

@@ -782,9 +782,6 @@ expr2smvt::resultt expr2smvt::convert_rec(const exprt &src)
   else if(src.id() == ID_smv_setin)
     return convert_binary(to_binary_expr(src), "in", precedencet::IN);
 
-  else if(src.id() == ID_smv_setnotin)
-    return convert_binary(to_binary_expr(src), "notin", precedencet::IN);
-
   else if(src.id() == ID_smv_union)
     return convert_binary(to_binary_expr(src), "union", precedencet::UNION);
 

regression/smv/smv/smv1.smv

@@ -257,9 +257,6 @@ static smv_parse_treet::modulet &new_module(YYSTYPE &location, YYSTYPE &module_n
 %token min_Token	"min"
 
 /* Not in the NuSMV manual */
-%token EXTERN_Token	"EXTERN"
-%token switch_Token	"switch"
-%token notin_Token	"notin"
 %token R_Token		"R"
 
 %token DOTDOT_Token   ".."
@@ -280,12 +277,7 @@ static smv_parse_treet::modulet &new_module(YYSTYPE &location, YYSTYPE &module_n
 %token NOTEQUAL_Token "!="
 %token LTLT_Token     "<<"
 %token GTGT_Token     ">>"
-
-%token INC_Token
-%token DEC_Token
 %token BECOMES_Token  ":="
-%token ADD_Token
-%token SUB_Token
 
 %token IDENTIFIER_Token   "identifier"
 %token QIDENTIFIER_Token  "quoted identifier"
@@ -360,9 +352,6 @@ module_element:
            | ltl_specification
            | compute_specification
            | isa_declaration
-           /* not in the NuSMV manual */
-           | EXTERN_Token extern_var semi_opt
-           | EXTERN_Token
            ;
 
 var_declaration:
@@ -523,9 +512,6 @@ ltl_specification:
            }
            ;
 
-extern_var : variable_identifier EQUAL_Token STRING_Token
-           ;
-
 var_list   : var_decl
            | var_list var_decl
            ;
@@ -742,11 +728,6 @@ basic_expr : constant
              // This rule is part of "complex_identifier" in the NuSMV manual.
              init($$, ID_smv_self);
            }
-           | basic_expr '(' simple_expr ')'
-           {
-             // Not in the NuSMV grammar.
-             binary($$, $1, ID_index, $3);
-           }
            | '(' formula ')'                      { $$=$2; }
            | NOT_Token basic_expr                 { init($$, ID_not); mto($$, $2); }
            | "abs" '(' basic_expr ')'             { unary($$, ID_smv_abs, $3); }
@@ -793,12 +774,6 @@ basic_expr : constant
                                                   { init($$, ID_if); mto($$, $1); mto($$, $3); mto($$, $5); }
            | case_Token cases esac_Token          { $$=$2; }
            | next_Token '(' basic_expr ')'        { init($$, ID_smv_next); mto($$, $3); }
-           /* Not in NuSMV manual */
-           | INC_Token '(' basic_expr ')'         { init($$, "inc"); mto($$, $3); }
-           | DEC_Token '(' basic_expr ')'         { init($$, "dec"); mto($$, $3); }
-           | ADD_Token '(' basic_expr ',' basic_expr ')' { j_binary($$, $3, ID_plus, $5); }
-           | SUB_Token '(' basic_expr ',' basic_expr ')' { init($$, ID_minus); mto($$, $3); mto($$, $5); }
-           | switch_Token '(' variable_identifier ')' '{' switches '}' { init($$, ID_switch); mto($$, $3); mto($$, $6); }
            /* CTL */
            | AX_Token  basic_expr                 { init($$, ID_AX);  mto($$, $2); }
            | AF_Token  basic_expr                 { init($$, ID_AF);  mto($$, $2); }
@@ -910,11 +885,6 @@ complex_identifier:
            {
              binary($$, $1, ID_index, $3);
            }
-           | complex_identifier '(' basic_expr ')'
-           {
-             // Not in the NuSMV grammar.
-             binary($$, $1, ID_index, $3);
-           }
            ;
 
 cases      :
@@ -927,16 +897,6 @@ case       : formula ':' formula ';'
            { binary($$, $1, ID_case, $3); }
            ;
 
-switches   :
-           { init($$, "switches"); }
-           | switches switch
-           { $$=$1; mto($$, $2); }
-           ;
-
-switch     : NUMBER_Token ':' basic_expr ';'
-           { init($$, ID_switch); mto($$, $1); mto($$, $3); }
-           ;
-
 %%
 
 int yysmverror(const std::string &error)

src/smvlang/expr2smv.cpp

@@ -168,9 +168,6 @@ void newlocation(YYSTYPE &x)
 "min"		token(min_Token);
 
  /* Not in the NuSMV manual */
-"EXTERN"	token(EXTERN_Token);
-"switch"	token(switch_Token);
-"notin"		token(notin_Token);
 "R"		token(R_Token);
 
 [\$A-Za-z_][A-Za-z0-9_\$#-]*	{

src/smvlang/parser.y

@@ -1115,10 +1115,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode, bool next)
 
     expr.type() = bool_typet();
   }
-  else if(expr.id() == ID_smv_setnotin)
-  {
-    expr.type()=bool_typet();
-  }
   else if(expr.id() == ID_unary_minus)
   {
     auto &uminus_expr = to_unary_minus_expr(expr);