Merge pull request #982 from diffblue/define2

SMV: do not allow defining identifiers that are already declared

Author: kroening

regression/smv/assign/assign1.desc

@@ -0,0 +1,8 @@
+KNOWNBUG
+assign1.smv
+
+^file .* line 6: variable `x' already assigned.*$
+^EXIT=1$
+^SIGNAL=0$
+--
+--

regression/smv/assign/assign1.smv

@@ -0,0 +1,8 @@
+MODULE main
+
+VAR x : 1..4;
+
+ASSIGN x := 1;
+
+-- not allowed, x is already assigned
+ASSIGN init(x) := 2;

regression/smv/assign/assign2.desc

@@ -0,0 +1,8 @@
+KNOWNBUG
+assign1.smv
+
+^file .* line 6: variable `x' already assigned.*$
+^EXIT=1$
+^SIGNAL=0$
+--
+--

regression/smv/assign/assign2.smv

@@ -0,0 +1,8 @@
+MODULE main
+
+VAR x : 1..4;
+
+ASSIGN x := 1;
+
+-- not allowed, x is already assigned
+ASSIGN next(x) := 2;

regression/smv/define/define2.desc

@@ -0,0 +1,8 @@
+CORE
+define2.smv
+
+^file .* line 6: variable `x' already declared.*$
+^EXIT=1$
+^SIGNAL=0$
+--
+--

regression/smv/define/define2.smv

@@ -0,0 +1,6 @@
+MODULE main
+
+VAR x : boolean;
+
+-- not allowed, x is already a variable
+DEFINE x := TRUE;

regression/smv/define/define3.desc

@@ -0,0 +1,8 @@
+CORE
+define3.smv
+
+^file .* line 6: variable `x' already defined.*$
+^EXIT=1$
+^SIGNAL=0$
+--
+--

regression/smv/define/define3.smv

@@ -0,0 +1,6 @@
+MODULE main
+
+DEFINE x := TRUE;
+
+-- not allowed, x is already defined
+VAR x : boolean;

regression/smv/define/define4.desc

@@ -0,0 +1,8 @@
+CORE
+define4.smv
+
+^file .* line 6: variable `x' already defined.*$
+^EXIT=1$
+^SIGNAL=0$
+--
+--

regression/smv/define/define4.smv

@@ -0,0 +1,6 @@
+MODULE main
+
+DEFINE x := TRUE;
+
+-- not allowed, x is already defined
+ASSIGN x := TRUE;

regression/smv/define/define5.desc

@@ -0,0 +1,8 @@
+KNOWNBUG
+define5.smv
+
+^file .* line 6: variable `x' already defined.*$
+^EXIT=1$
+^SIGNAL=0$
+--
+--

regression/smv/define/define5.smv

@@ -0,0 +1,6 @@
+MODULE main
+
+DEFINE x := TRUE;
+
+-- not allowed, x is already defined
+ASSIGN next(x) := TRUE;

regression/smv/define/define6.desc

@@ -0,0 +1,8 @@
+KNOWNBUG
+define6.smv
+
+^file .* line 6: variable `x' already defined.*$
+^EXIT=1$
+^SIGNAL=0$
+--
+--

regression/smv/define/define6.smv

@@ -0,0 +1,6 @@
+MODULE main
+
+DEFINE x := TRUE;
+
+-- not allowed, x is already defined
+ASSIGN init(x) := TRUE;

src/smvlang/parser.y

@@ -477,39 +477,40 @@ defines:     define
            ;
 
 define     : assignment_var BECOMES_Token formula ';'
-{
-  const irep_idt &identifier=stack_expr($1).get(ID_identifier);
-  smv_parse_treet::mc_vart &var=PARSER.module->vars[identifier];
+           {
+             const irep_idt &identifier=stack_expr($1).get(ID_identifier);
+             smv_parse_treet::mc_vart &var=PARSER.module->vars[identifier];
 
-  switch(var.var_class)
-  {
-  case smv_parse_treet::mc_vart::UNKNOWN:
-    var.type.make_nil();
-    var.var_class=smv_parse_treet::mc_vart::DEFINED;
-    break;
+             switch(var.var_class)
+             {
+             case smv_parse_treet::mc_vart::UNKNOWN:
+               var.type.make_nil();
+               var.var_class=smv_parse_treet::mc_vart::DEFINED;
+               break;
 
-  case smv_parse_treet::mc_vart::DECLARED:
-    var.var_class=smv_parse_treet::mc_vart::DEFINED;
-    break;
+             case smv_parse_treet::mc_vart::DECLARED:
+               yyerror("variable `"+id2string(identifier)+"' already declared");
+               YYERROR;
+               break;
 
-  case smv_parse_treet::mc_vart::DEFINED:
-    yyerror("variable `"+id2string(identifier)+"' already defined");
-    YYERROR;
-    break;
-  
-  case smv_parse_treet::mc_vart::ARGUMENT:
-    yyerror("variable `"+id2string(identifier)+"' already declared as argument");
-    YYERROR;
-    break;
-  
-  default:
-    DATA_INVARIANT(false, "unexpected variable class");
-  }
+             case smv_parse_treet::mc_vart::DEFINED:
+               yyerror("variable `"+id2string(identifier)+"' already defined");
+               YYERROR;
+               break;
 
-  binary($$, $1, ID_equal, $3);
-  PARSER.module->add_define(to_equal_expr(stack_expr($$)));
-}
-;
+             case smv_parse_treet::mc_vart::ARGUMENT:
+               yyerror("variable `"+id2string(identifier)+"' already declared as argument");
+               YYERROR;
+               break;
+
+             default:
+               DATA_INVARIANT(false, "unexpected variable class");
+             }
+
+             binary($$, $1, ID_equal, $3);
+             PARSER.module->add_define(to_equal_expr(stack_expr($$)));
+           }
+           ;
 
 formula    : term
            ;