From 36d218a4a46dcbfeb31823e248f3a5b366b4cd03 Mon Sep 17 00:00:00 2001
From: Nick Battle <nick.battle@gmail.com>
Date: Sat, 22 Aug 2015 15:11:57 +0100
Subject: [PATCH] Prevent new expressions in functions

---
 .../org/overturetool/vdmj/expressions/NewExpression.java   | 7 +++++++
 .../overturetool/vdmj/expressions/ThreadIdExpression.java  | 4 ++--
 .../org/overturetool/vdmj/expressions/TimeExpression.java  | 4 ++--
 .../src/test/resources/Overture/typecheck/puretest.assert  | 2 +-
 FJ-VDMJ/src/test/resources/Overture/typecheck/puretest.vpp | 4 ++--
 5 files changed, 14 insertions(+), 7 deletions(-)

diff --git a/FJ-VDMJ/src/main/java/org/overturetool/vdmj/expressions/NewExpression.java b/FJ-VDMJ/src/main/java/org/overturetool/vdmj/expressions/NewExpression.java
index a2867469f..77c01345e 100644
--- a/FJ-VDMJ/src/main/java/org/overturetool/vdmj/expressions/NewExpression.java
+++ b/FJ-VDMJ/src/main/java/org/overturetool/vdmj/expressions/NewExpression.java
@@ -23,6 +23,8 @@
 
 package org.overturetool.vdmj.expressions;
 
+import org.overturetool.vdmj.Release;
+import org.overturetool.vdmj.Settings;
 import org.overturetool.vdmj.definitions.BUSClassDefinition;
 import org.overturetool.vdmj.definitions.CPUClassDefinition;
 import org.overturetool.vdmj.definitions.ClassDefinition;
@@ -79,6 +81,11 @@ public Type typeCheck(Environment env, TypeList qualifiers, NameScope scope, Typ
 			report(3133, "Class name " + classname + " not in scope");
 			return new UnknownType(location);
 		}
+		
+		if (Settings.release == Release.VDM_10 && env.isFunctional())
+		{
+			report(3348, "Cannot use 'new' in a functional context");
+		}
 
 		classdef = (ClassDefinition)cdef;
 
diff --git a/FJ-VDMJ/src/main/java/org/overturetool/vdmj/expressions/ThreadIdExpression.java b/FJ-VDMJ/src/main/java/org/overturetool/vdmj/expressions/ThreadIdExpression.java
index cd6212ca0..334e0c2ac 100644
--- a/FJ-VDMJ/src/main/java/org/overturetool/vdmj/expressions/ThreadIdExpression.java
+++ b/FJ-VDMJ/src/main/java/org/overturetool/vdmj/expressions/ThreadIdExpression.java
@@ -78,12 +78,12 @@ public Type typeCheck(Environment env, TypeList qualifiers, NameScope scope, Typ
 		
 		if (encl != null && encl.isPure())
 		{
-			report(3346, "Cannot use threadid in pure operations");
+			report(3346, "Cannot use 'threadid' in pure operations");
 		}
 
 		if (Settings.release == Release.VDM_10 && env.isFunctional())
 		{
-			report(3348, "Cannot use threadid in a functional context");
+			report(3348, "Cannot use 'threadid' in a functional context");
 		}
 
 		return checkConstraint(constraint, new NaturalType(location));
diff --git a/FJ-VDMJ/src/main/java/org/overturetool/vdmj/expressions/TimeExpression.java b/FJ-VDMJ/src/main/java/org/overturetool/vdmj/expressions/TimeExpression.java
index 7fcf97e85..1a3d9712c 100644
--- a/FJ-VDMJ/src/main/java/org/overturetool/vdmj/expressions/TimeExpression.java
+++ b/FJ-VDMJ/src/main/java/org/overturetool/vdmj/expressions/TimeExpression.java
@@ -80,12 +80,12 @@ public Type typeCheck(Environment env, TypeList qualifiers, NameScope scope, Typ
 		
 		if (encl != null && encl.isPure())
 		{
-			report(3346, "Cannot use time in pure operations");
+			report(3346, "Cannot use 'time' in pure operations");
 		}
 		
 		if (Settings.release == Release.VDM_10 && env.isFunctional())
 		{
-			report(3348, "Cannot use time in a functional context");
+			report(3348, "Cannot use 'time' in a functional context");
 		}
 
 		return checkConstraint(constraint, new NaturalType(location));
diff --git a/FJ-VDMJ/src/test/resources/Overture/typecheck/puretest.assert b/FJ-VDMJ/src/test/resources/Overture/typecheck/puretest.assert
index 9ea01cc63..d64042726 100644
--- a/FJ-VDMJ/src/test/resources/Overture/typecheck/puretest.assert
+++ b/FJ-VDMJ/src/test/resources/Overture/typecheck/puretest.assert
@@ -1 +1 @@
-[3341, 3300, 3286, 3346, 3300, 3346, 3346, 3346, 3346, 3346, 3300, 3338, 3339, 3293, 3345, 3344, 3340, 3342, 3343, 3300, 3347, 3300, 3091, 3348, 3348, 5017]
\ No newline at end of file
+[3341, 3300, 3286, 3346, 3300, 3346, 3346, 3346, 3346, 3346, 3300, 3338, 3339, 3293, 3345, 3344, 3340, 3342, 3343, 3300, 3347, 3300, 3091, 3348, 3348, 3348, 5017]
\ No newline at end of file
diff --git a/FJ-VDMJ/src/test/resources/Overture/typecheck/puretest.vpp b/FJ-VDMJ/src/test/resources/Overture/typecheck/puretest.vpp
index 7886ac5ae..1d2d7e394 100644
--- a/FJ-VDMJ/src/test/resources/Overture/typecheck/puretest.vpp
+++ b/FJ-VDMJ/src/test/resources/Overture/typecheck/puretest.vpp
@@ -7,7 +7,7 @@ values
 	v = 123;
 
 operations
-	pure A: () ==> A
+	public pure A: () ==> A
 	A() == 
 	(
 		dcl z:nat := 0;
@@ -55,6 +55,6 @@ functions
 	f(a) == a.impop() + a.pre_impop(a) + a.op();
 	
 	g:() -> nat
-	g() == time + threadid;
+	g() == time + threadid + new A().x;
 
 end Test
\ No newline at end of file