Merge branch 'master' into highprecision

vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POApplyExpression.java

@@ -93,7 +93,7 @@ public ProofObligationList getProofObligations(POContextStack ctxt, POGState pog
 		{
 			if (type.isOperation(location))
 			{
-				pogState.didUpdateState();	// Operation calls assumed to update state
+				pogState.didUpdateState(location);	// Operation calls assumed to update state
 			}
 
 			if (type.isMap(location))

vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POBlockStatement.java

@@ -57,7 +57,7 @@ public ProofObligationList getProofObligations(POContextStack ctxt, POGState pog
 		for (PODefinition dcl: assignmentDefs)
 		{
 			POAssignmentDefinition adef = (POAssignmentDefinition)dcl;
-			dclState.addDclState(adef.name);
+			dclState.addDclLocal(adef.name);
 		}
 
 		ctxt.push(new PODclContext(assignmentDefs));

vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POCallObjectStatement.java

@@ -76,7 +76,7 @@ public ProofObligationList getProofObligations(POContextStack ctxt, POGState pog
 		}
 
 		// We have to assume the operation call accesses state
-		pogState.didUpdateState();
+		pogState.didUpdateState(location);
 
 		return obligations;
 	}

vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POCallStatement.java

@@ -64,7 +64,7 @@ public ProofObligationList getProofObligations(POContextStack ctxt, POGState pog
 		}
 
 		// We have to assume the operation call accesses state
-		pogState.didUpdateState();
+		pogState.didUpdateState(location);
 
 		return obligations;
 	}

vdmj/src/main/java/com/fujitsu/vdmj/pog/POGState.java

@@ -23,6 +23,7 @@
  ******************************************************************************/
 package com.fujitsu.vdmj.pog;
 
+import com.fujitsu.vdmj.lex.LexLocation;
 import com.fujitsu.vdmj.tc.lex.TCNameList;
 import com.fujitsu.vdmj.tc.lex.TCNameToken;
 import com.fujitsu.vdmj.util.Utils;
@@ -34,59 +35,91 @@
 public class POGState
 {
 	private boolean hasUpdatedState;
+	private LexLocation updatedFrom;
 	private POGState outerState;
 	private TCNameList locals;
 
 	public POGState()
 	{
 		hasUpdatedState = false;
+		updatedFrom = LexLocation.ANY;
 		outerState = null;
 		locals = new TCNameList();
 	}
 
-	private POGState(boolean hasUpdatedState, POGState outerState)
+	private POGState(boolean hasUpdatedState, LexLocation updatedFrom, POGState outerState, TCNameList locals)
 	{
 		this.hasUpdatedState = hasUpdatedState;
+		this.updatedFrom = updatedFrom;
 		this.outerState = outerState;
 		this.locals = new TCNameList();
+
+		this.locals.addAll(locals);
 	}
 
 	@Override
 	public String toString()
 	{
 		return (hasUpdatedState ?  "has" : "has not") + " updated state" +
-				(locals.isEmpty() ? "" : Utils.listToString("(locals ", locals, ", ", ")"));
+				(locals.isEmpty() ? "" : Utils.listToString(" (locals ", locals, ", ", ")"));
 	}
 
+	/**
+	 * Create a copy of the current state, to go into (say) the then/elseif/else branches
+	 * of a statement, before combining the results. Note this copies the locals.
+	 */
 	public POGState getCopy()
 	{
-		return new POGState(hasUpdatedState, outerState);
+		return new POGState(hasUpdatedState, updatedFrom, outerState, locals);
 	}
 
+	/**
+	 * Create a new chained POGState, linked to the current one. This is used to process
+	 * block statements that may contain "dcl" statements (ie. local state). The new local
+	 * state initially has no updates.
+	 */
 	public POGState getLink()
 	{
-		return new POGState(false, this);
+		return new POGState(false, LexLocation.ANY, this, new TCNameList());
 	}
 
 	public boolean hasUpdatedState()
 	{
 		return hasUpdatedState || (outerState != null && outerState.hasUpdatedState());
 	}
 
-	public void setUpdateState(boolean updatedState)
+	public void setUpdateState(boolean updatedState, LexLocation from)
 	{
 		hasUpdatedState = hasUpdatedState || updatedState;
+		updatedFrom = from;
 	}
 
-	public void didUpdateState()	// Used by call statements
+	public LexLocation getUpdatedFrom()
+	{
+		if (hasUpdatedState)
+		{
+			return updatedFrom;
+		}
+		else if (outerState != null)
+		{
+			return outerState.getUpdatedFrom();
+		}
+		else
+		{
+			return LexLocation.ANY;
+		}
+	}
+
+	public void didUpdateState(LexLocation from)	// Used by call statements
 	{
 		if (outerState != null)
 		{
-			outerState.didUpdateState();
+			outerState.didUpdateState(from);
 		}
 		else
 		{
 			hasUpdatedState = true;				// Module level
+			updatedFrom = from;
 		}
 	}
 
@@ -95,6 +128,7 @@ public void didUpdateState(TCNameToken name)
 		if (locals.contains(name))
 		{
 			hasUpdatedState = true;				// A local dcl update
+			updatedFrom = name.getLocation();
 		}
 		else if (outerState != null)
 		{
@@ -103,10 +137,11 @@ else if (outerState != null)
 		else
 		{
 			hasUpdatedState = true;				// A module state update
+			updatedFrom = name.getLocation();
 		}
 	}
 
-	public void addDclState(TCNameToken name)
+	public void addDclLocal(TCNameToken name)
 	{
 		locals.add(name);
 	}

vdmj/src/main/java/com/fujitsu/vdmj/pog/POGStateList.java

@@ -25,6 +25,8 @@
 
 import java.util.Vector;
 
+import com.fujitsu.vdmj.lex.LexLocation;
+
 /**
  * A list of POG states for the sub-clauses in a statements. These are combined when
  * the execution paths rejoin.
@@ -49,12 +51,17 @@ public POGState addCopy(POGState parent)
 	public void combineInto(POGState parent)
 	{
 		boolean hasUpdatedState = false;
+		LexLocation updatedFrom = LexLocation.ANY;
 
 		for (POGState state: this)
 		{
-			hasUpdatedState = hasUpdatedState || state.hasUpdatedState();
+			if (state.hasUpdatedState())
+			{
+				hasUpdatedState = true;
+				updatedFrom = state.getUpdatedFrom();
+			}
 		}
 
-		parent.setUpdateState(hasUpdatedState);
+		parent.setUpdateState(hasUpdatedState, updatedFrom);
 	}
 }

vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligation.java

@@ -54,12 +54,11 @@ abstract public class ProofObligation implements Comparable<ProofObligation>
 	// Arguments for the markUnchecked method.
 	public static final String NOT_YET_SUPPORTED	= "Not yet supported for operations";
 	public static final String MISSING_MEASURE		= "Obligation for missing measure function";
-	public static final String UNCHECKED_VDMPP		= "Unchecked in VDM++";
+	public static final String UNCHECKED_VDMPP		= "Unchecked in VDM++/RT";
 	public static final String HIDDEN_VARIABLES		= "Obligation patterns contain hidden variables";
 	public static final String REQUIRES_VDM10		= "Obligation requires VDM10";
-	public static final String BODY_UPDATES_STATE	= "Operation body updates state";
 	public static final String LOOP_STATEMENT		= "Loop modifies state";
-	public static final String HAS_UPDATED_STATE	= "Previous statements updated state";
+	public static final String HAS_UPDATED_STATE	= "Earlier statements updated state";
 	public static final String COMPLEX_ASSIGNMENT	= "Assignment too complex";
 
 	public final LexLocation location;

vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligationList.java

@@ -285,7 +285,7 @@ public void stateUpdate(POGState pstate, POExpression expression)
 
 		if (readsState && pstate.hasUpdatedState())
 		{
-			markUnchecked(ProofObligation.HAS_UPDATED_STATE);
+			markUnchecked(ProofObligation.HAS_UPDATED_STATE + " " + pstate.getUpdatedFrom().toShortString());
 		}
 	}
 }