From eb7ac0a07605fdeaf11f4006ec5d9173cb5910be Mon Sep 17 00:00:00 2001
From: Nick Battle <nick.battle@gmail.com>
Date: Thu, 1 Oct 2015 13:34:30 +0100
Subject: [PATCH] Check for non-static history operations in static sync
 clauses

---
 FJ-VDMJ/RELEASE_NOTES                                  |  1 +
 FJ-VDMJ/documentation/MESSAGES                         |  1 +
 .../vdmj/expressions/HistoryExpression.java            | 10 ++++++++++
 3 files changed, 12 insertions(+)

diff --git a/FJ-VDMJ/RELEASE_NOTES b/FJ-VDMJ/RELEASE_NOTES
index 24e240d2d..4951e31da 100644
--- 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
index d2b46258f..6d2e81a1d 100644
--- 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
index 3bc10d13a..6f4fe7adb 100644
--- 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");
+    				}
     			}
     		}