Fixed bug in datatypes; duplicate constructor names were not being de…

…tected.

Source/Core/Absy.cs

@@ -349,7 +349,7 @@ public void Emit(TokenTextWriter stream) {
       this.topLevelDeclarations.Emit(stream);
     }
 
-    public void ProcessDatatypeConstructors() {
+    public void ProcessDatatypeConstructors(Errors errors) {
       Dictionary<string, DatatypeConstructor> constructors = new Dictionary<string, DatatypeConstructor>();
       List<Declaration> prunedTopLevelDeclarations = new List<Declaration>();
       foreach (Declaration decl in TopLevelDeclarations) {
@@ -358,14 +358,22 @@ public void ProcessDatatypeConstructors() {
           prunedTopLevelDeclarations.Add(decl);
           continue;
         }
-        if (constructors.ContainsKey(func.Name)) continue;
+        if (constructors.ContainsKey(func.Name))
+        {
+          errors.SemErr(func.tok, string.Format("more than one declaration of datatype constructor name: {0}", func.Name));
+          continue;
+        }
         DatatypeConstructor constructor = new DatatypeConstructor(func);
         constructors.Add(func.Name, constructor);
         prunedTopLevelDeclarations.Add(constructor);
       }
+      if (errors.count > 0)
+      {
+        return;
+      }
+
       ClearTopLevelDeclarations();
       AddTopLevelDeclarations(prunedTopLevelDeclarations);
-
       foreach (DatatypeConstructor f in constructors.Values) {
         for (int i = 0; i < f.InParams.Count; i++) {
           DatatypeSelector selector = new DatatypeSelector(f, i);

Source/Core/Parser.cs

@@ -84,17 +84,18 @@ public static int Parse (string s, string/*!*/ filename, out /*maybe null*/ Prog
 
   Parser parser = new Parser(scanner, errors, false);
   parser.Parse();
-  if (parser.errors.count == 0)
+  if (errors.count == 0)
   {
-    program = parser.Pgm;
-    program.ProcessDatatypeConstructors();
-    return 0;
+    parser.Pgm.ProcessDatatypeConstructors(errors);
   }
-  else
+  if (errors.count == 0)
+  {
+    program = parser.Pgm;
+  } else
   {
     program = null;
-    return parser.errors.count;
   }
+  return errors.count;
 }
 
 public Parser(Scanner/*!*/ scanner, Errors/*!*/ errors, bool disambiguation)

Test/datatypes/t3.bpl

@@ -0,0 +1,7 @@
+// RUN: %boogie -typeEncoding:m "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+type {:datatype} Value;
+function {:constructor} Int(i: int): Value;
+
+type {:datatype} Path;
+function {:constructor} Int(i: int): Path;

Test/datatypes/t3.bpl.expect

@@ -0,0 +1,2 @@
+t3.bpl(7,25): error: more than one declaration of datatype constructor name: Int
+1 parse errors detected in t3.bpl