Fix PP PO names

nickbattle · Oct 24, 2024 · 6ba09b3 · 6ba09b3
1 parent 94f0ebe
commit 6ba09b3
Showing 1 changed file with 4 additions and 1 deletion.
diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POClassDefinition.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POClassDefinition.java
@@ -29,6 +29,7 @@
 import com.fujitsu.vdmj.po.statements.POClassInvariantStatement;
 import com.fujitsu.vdmj.pog.POContextStack;
 import com.fujitsu.vdmj.pog.POGState;
+import com.fujitsu.vdmj.pog.PONameContext;
 import com.fujitsu.vdmj.pog.ProofObligationList;
 import com.fujitsu.vdmj.tc.definitions.TCClassDefinition;
 import com.fujitsu.vdmj.tc.lex.TCNameToken;
@@ -183,7 +184,9 @@ public ProofObligationList getProofObligations(POContextStack ctxt, POGState pog
 
 		for (PODefinition def: definitions)
 		{
-			list.addAll(def.getProofObligations(new POContextStack(), new POGState(), local));
+			ctxt.push(new PONameContext(def.getVariableNames()));
+			list.addAll(def.getProofObligations(ctxt, new POGState(), local));
+			ctxt.pop();
 		}
 
 		list.typeCheck(tcdef.name, local);