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 f92d17d69..c5c5d4ddb 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 @@ -50,7 +50,7 @@ public POBlockStatement(LexLocation location, PODefinitionList assignmentDefs, P @Override public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { - ProofObligationList obligations = assignmentDefs.getProofObligations(ctxt, pogState, env); + ProofObligationList obligations = assignmentDefs.getDefProofObligations(ctxt, pogState, env); POGState dclState = pogState.getLink(); diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/POLetDefContext.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/POLetDefContext.java index 90626b8bc..22a70db7d 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/POLetDefContext.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/POLetDefContext.java @@ -24,6 +24,7 @@ package com.fujitsu.vdmj.pog; +import com.fujitsu.vdmj.po.definitions.POAssignmentDefinition; import com.fujitsu.vdmj.po.definitions.PODefinition; import com.fujitsu.vdmj.po.definitions.PODefinitionList; @@ -61,7 +62,21 @@ public String getSource() for (PODefinition def: localDefs) { sb.append(sep); - sb.append(def.toExplicitString(def.location)); + + if (def instanceof POAssignmentDefinition) + { + POAssignmentDefinition ass = (POAssignmentDefinition)def; + sb.append(ass.name); + sb.append(":"); + sb.append(ass.expType); + sb.append(" = "); + sb.append(ass.expression); + } + else // POValueDefinition + { + sb.append(def.toExplicitString(def.location)); + } + sep = ", "; }