Keep track of fields that were initialized with S::x = e in construct…

…ors to avoid giving spurious uninitialized field errors.
mcoblenz · Dec 4, 2019 · 1c23080 · 1c23080
1 parent abf02c3
commit 1c23080
Show file tree

Hide file tree

Showing 2 changed files with 14 additions and 0 deletions.
diff --git a/resources/tests/type_checker_tests/StateInitialization.obs b/resources/tests/type_checker_tests/StateInitialization.obs
@@ -55,3 +55,14 @@ main asset contract Wallet {
         ->S1(m = new Money()); // Error: double initialization
     }
 }
+
+contract HasField {
+    int x;
+
+    state S{}
+
+    HasField@Owned() {
+        S::x = 2;
+        ->S;
+    }
+}
diff --git a/src/main/scala/edu/cmu/cs/obsidian/typecheck/Checker.scala b/src/main/scala/edu/cmu/cs/obsidian/typecheck/Checker.scala
@@ -1755,6 +1755,9 @@ class Checker(globalTable: SymbolTable, verbose: Boolean = false) {
                         contextAfterTransition = contextAfterTransition.updatedWithFieldInitialization(update._1.name)
                     }
                 }
+                for (assignmentUpdate <- updatedViaAssignment) {
+                    contextAfterTransition = contextAfterTransition.updatedWithFieldInitialization(assignmentUpdate)
+                }
 
                 (contextAfterTransition, Transition(newStateName, newUpdatesOption, context.thisType.permission).setLoc(s))