Merge branch 'master' into highprecision

nickbattle · Nov 1, 2024 · 229a6ac · 229a6ac
2 parents 65014d8 + 2b093ad
commit 229a6ac
Show file tree

Hide file tree

Showing 2 changed files with 17 additions and 2 deletions.
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
@@ -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
@@ -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 = ", ";
 			}