Rust: SSA: restrict mutablyBorrowed to variables with a 'mut' modifier

This commit is contained in:
Arthur Baars
2025-03-13 10:26:20 +01:00
parent 45db4ae7c6
commit 56574a15b7
2 changed files with 3 additions and 2 deletions

View File

@@ -212,7 +212,8 @@ predicate capturedCallWrite(Expr call, BasicBlock bb, int i, Variable v) {
/** Holds if `v` may be mutably borrowed in `e`. */
private predicate mutablyBorrows(Expr e, Variable v) {
e = any(MethodCallExpr mc).getReceiver() and
e.(VariableAccess).getVariable() = v
e.(VariableAccess).getVariable() = v and
v.isMutable()
or
exists(RefExpr re | re = e and re.isMut() and re.getExpr().(VariableAccess).getVariable() = v)
}

View File

@@ -161,7 +161,7 @@ module Impl {
}
/** Hold is this variable is mutable. */
predicate isMutable() { this.getPat().isMut() }
predicate isMutable() { this.getPat().isMut() or this.getSelfParam().isMut() }
/** Hold is this variable is immutable. */
predicate isImmutable() { not this.isMutable() }