Check for non-static history operations in static sync clauses

nickbattle · Oct 1, 2015 · eb7ac0a · eb7ac0a
1 parent 32b25d1
commit eb7ac0a
Show file tree

Hide file tree

Showing 3 changed files with 12 additions and 0 deletions.
diff --git a/FJ-VDMJ/RELEASE_NOTES b/FJ-VDMJ/RELEASE_NOTES
@@ -5,6 +5,7 @@ https://github.com/nickbattle/vdmj/issues.
 
 Latest Changes in version 3.0.1
 
+2015-10-01 Check for non-static history operations in static sync clauses
 2015-07-28 Implicit compose types should have same access as the outer type
 2015-07-15 Added type checking for pure operations (RM#27)
 2015-07-10 Fix for invariants failing in some cases

diff --git a/FJ-VDMJ/documentation/MESSAGES b/FJ-VDMJ/documentation/MESSAGES
@@ -725,6 +725,7 @@ as the expected and actual values.
 3346, "Cannot use <statement/expression> in pure operations"
 3347, "Cannot have a pure operation as the body of a thread"
 3348, "Cannot use <expression> in a functional context"
+3349, "Cannot see non-static operation from static context"
 
 4000, "Cannot instantiate abstract class <class>"
 4002, "Expression value is not in set bind"

diff --git a/FJ-VDMJ/src/main/java/org/overturetool/vdmj/expressions/HistoryExpression.java b/FJ-VDMJ/src/main/java/org/overturetool/vdmj/expressions/HistoryExpression.java
@@ -31,6 +31,7 @@
 import org.overturetool.vdmj.lex.Token;
 import org.overturetool.vdmj.runtime.ClassContext;
 import org.overturetool.vdmj.runtime.Context;
+import org.overturetool.vdmj.runtime.ContextException;
 import org.overturetool.vdmj.runtime.ObjectContext;
 import org.overturetool.vdmj.runtime.ValueException;
 import org.overturetool.vdmj.typechecker.Environment;
@@ -142,6 +143,10 @@ else if (ctxt instanceof ClassContext)
 		{
 			return abort(e);
 		}
+		catch (ContextException e)
+		{
+			throw e;
+		}
 		catch (Exception e)
 		{
 			return abort(4065, e.getMessage(), ctxt);
@@ -198,6 +203,11 @@ public Type typeCheck(Environment env, TypeList qualifiers, NameScope scope, Typ
     				{
     					opname.report(3342, "Cannot use history counters for pure operations");
     				}
+
+    				if (!def.isStatic() && env.isStatic())
+    				{
+    					opname.report(3349, "Cannot see non-static operation from static context");
+    				}
     			}
     		}