Skip to content

Commit

Permalink
Update Evaluator.scala
Browse files Browse the repository at this point in the history
  • Loading branch information
marcoeilers authored Jul 15, 2023
1 parent 4d7e88f commit eb6130e
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/main/scala/rules/Evaluator.scala
Original file line number Diff line number Diff line change
Expand Up @@ -214,7 +214,7 @@ object evaluator extends EvaluationRules {
case pa: ast.PredicateAccess if Verifier.config.maskHeapMode() && s.qpPredicates.contains(pa.res(s.program).asInstanceOf[ast.Predicate]) =>
val pvef: ast.Exp => PartialVerificationError = _ => pve
evals(s, pa.args, pvef, v)((s1, tArgs, v1) => {
val resChunk = s.h.values.find(c => c.asInstanceOf[MaskHeapChunk].resource == pa.res(s.program)).get.asInstanceOf[BasicMaskHeapChunk]
val resChunk = s.h.values.find(c => c.isInstanceOf[MaskHeapChunk] && c.asInstanceOf[MaskHeapChunk].resource == pa.res(s.program)).get.asInstanceOf[BasicMaskHeapChunk]
val ve = pve dueTo InsufficientPermission(pa)
val maskValue = HeapLookup(resChunk.mask, toSnapTree(tArgs))
v1.decider.assert(perms.IsPositive(maskValue)) {
Expand Down

0 comments on commit eb6130e

Please sign in to comment.