Merge pull request #1215 from diffblue/duplicate-declaration-errors

SMV: move checks for duplicate declarations into type checker

Author: tautschnig

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.