diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POApplyExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POApplyExpression.java index e51c34529..bf7862d89 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POApplyExpression.java +++ b/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)) diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POBlockStatement.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POBlockStatement.java index 6eaab6b3c..f92d17d69 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POBlockStatement.java +++ b/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)); diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POCallObjectStatement.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POCallObjectStatement.java index 248cd6787..5f31d8f81 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POCallObjectStatement.java +++ b/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; } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POCallStatement.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POCallStatement.java index 91bf391e2..866fd2c81 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POCallStatement.java +++ b/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; } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/POGState.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/POGState.java index adc89f5c7..aa76f1976 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/POGState.java +++ b/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,38 +35,52 @@ 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() @@ -73,20 +88,38 @@ 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); } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/POGStateList.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/POGStateList.java index 31683bd92..4dbeef67a 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/POGStateList.java +++ b/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); } } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligation.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligation.java index b80855701..3e1466bfb 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligation.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligation.java @@ -54,12 +54,11 @@ abstract public class ProofObligation implements Comparable // 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; diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligationList.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligationList.java index 0365de1d7..487857f8b 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligationList.java +++ b/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()); } } }