SMV: move checks for duplicate declarations into type checker

regression/smv/define/define3.desc

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

regression/smv/var/already_declared1.desc

@@ -0,0 +1,8 @@
+CORE
+already_declared1.smv
+
+^file .* line 6: variable x already declared, at file .* line 3$
+^EXIT=2$
+^SIGNAL=0$
+--
+--

regression/smv/var/already_declared1.smv

@@ -0,0 +1,6 @@
+MODULE main
+
+VAR x : 1..10;
+
+-- x again
+VAR x : 1..10;

regression/smv/var/already_declared2.desc

@@ -0,0 +1,8 @@
+CORE
+already_declared2.smv
+
+^file .* line 6: variable x already declared, at file .* line 3$
+^EXIT=2$
+^SIGNAL=0$
+--
+--

regression/smv/var/already_declared2.smv

@@ -0,0 +1,6 @@
+MODULE main
+
+DEFINE x := 1;
+
+-- x again
+VAR x : 1..10;

regression/smv/var/already_declared3.desc

@@ -0,0 +1,8 @@
+CORE
+already_declared3.smv
+
+^file .* line 8: variable x already declared, at file .* line 5$
+^EXIT=2$
+^SIGNAL=0$
+--
+--

regression/smv/var/already_declared3.smv

@@ -0,0 +1,8 @@
+MODULE some_module
+
+MODULE main
+
+VAR x : some_module;
+
+-- x again
+VAR x : 1..10;

regression/smv/var/already_declared4.desc

@@ -0,0 +1,8 @@
+KNOWNBUG
+already_declared4.smv
+
+^EXIT=2$
+^SIGNAL=0$
+--
+--
+This should be errored.

regression/smv/var/already_declared4.smv

@@ -0,0 +1,8 @@
+MODULE some_module(x)
+
+-- already used as module parameter
+VAR x : 1..10;
+
+MODULE main
+
+VAR m : some_module(1);

regression/smv/var/already_declared5.desc

@@ -0,0 +1,8 @@
+KNOWNBUG
+already_declared5.smv
+
+^EXIT=2$
+^SIGNAL=0$
+--
+--
+This crashes.

regression/smv/var/already_declared5.smv

@@ -0,0 +1,6 @@
+MODULE main
+
+VAR some_enum : {x, y, z};
+
+-- x is already declared
+VAR x : boolean;

src/smvlang/parser.y

@@ -673,13 +673,7 @@ var_decl   : variable_identifier ':' type_specifier ';'
                break;
 
              case smv_parse_treet::mc_vart::DEFINED:
-               yyerror("variable `"+id2string(identifier)+"' already defined");
-               YYERROR;
-               break;
-
              case smv_parse_treet::mc_vart::DECLARED:
-               yyerror("variable `"+id2string(identifier)+"' already declared as variable");
-               YYERROR;
                break;
 
              case smv_parse_treet::mc_vart::ARGUMENT:

src/smvlang/smv_typecheck.cpp

@@ -1916,6 +1916,14 @@ void smv_typecheckt::create_var_symbols(
       irep_idt base_name = to_symbol_expr(item.expr).get_identifier();
       irep_idt identifier = module + "::var::" + id2string(base_name);
 
+      auto symbol_ptr = symbol_table.lookup(identifier);
+      if(symbol_ptr != nullptr)
+      {
+        throw errort{}.with_location(item.expr.source_location())
+          << "variable " << base_name << " already declared, at "
+          << symbol_ptr->location;
+      }
+
       typet type = item.expr.type();
 
       // check the type
@@ -1934,13 +1942,14 @@ void smv_typecheckt::create_var_symbols(
       symbol.value = nil_exprt{};
       symbol.is_input = true;
       symbol.is_state_var = false;
+      symbol.location = item.expr.source_location();
 
       symbol_table.insert(std::move(symbol));
     }
     else if(item.is_define())
     {
-      irep_idt base_name =
-        to_symbol_expr(to_equal_expr(item.expr).lhs()).get_identifier();
+      const auto &symbol_expr = to_symbol_expr(to_equal_expr(item.expr).lhs());
+      irep_idt base_name = symbol_expr.get_identifier();
       irep_idt identifier = module + "::var::" + id2string(base_name);
       typet type;
       type.make_nil();
@@ -1959,6 +1968,7 @@ void smv_typecheckt::create_var_symbols(
       symbol.value = nil_exprt{};
       symbol.is_input = true;
       symbol.is_state_var = false;
+      symbol.location = symbol_expr.source_location();
 
       symbol_table.insert(std::move(symbol));
     }