Skip to content

Commit

Permalink
Make operation apply calls set updated, to suppress QC
Browse files Browse the repository at this point in the history
  • Loading branch information
nickbattle committed Oct 27, 2024
1 parent a392994 commit a63d611
Showing 1 changed file with 4 additions and 1 deletion.
Original file line number Diff line number Diff line change
Expand Up @@ -96,7 +96,10 @@ public ProofObligationList getProofObligations(POContextStack ctxt, POGState pog
{
if (type.isOperation(location))
{
pogState.addOperation(location, opdef);
// We have to say that the POGState is as if the operation updates state, because
// it may read state even if pure, and an apply uses the return value. So QC can't
// evaluate them. This makes subsequent POs Unchecked.
pogState.setUpdateState(true, location);
}

if (type.isMap(location))
Expand Down

0 comments on commit a63d611

Please sign in to comment.