Skip to content

Commit 236c269

Browse files
committed
fix: update array type checks for pointer offset calculations
1 parent 27434bd commit 236c269

1 file changed

Lines changed: 4 additions & 4 deletions

File tree

  • kmir/src/kmir/kdist/mir-semantics/rt

kmir/src/kmir/kdist/mir-semantics/rt/data.md

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1465,12 +1465,12 @@ Transmuting a pointer to an integer discards provenance and reinterprets the poi
14651465
rule #ptrOffsetBytes(PTR_OFFSET, TY:Ty)
14661466
=> PTR_OFFSET *Int #elemSize(#lookupMaybeTy(elemTy(lookupTy(TY))))
14671467
requires PTR_OFFSET =/=Int 0
1468-
andBool #isUnsizedArrayType(lookupTy(TY))
1468+
andBool #isArrayType(lookupTy(TY))
14691469
rule #ptrOffsetBytes(_, _) => -1 [owise] // should not happen
14701470
1471-
syntax Bool ::= #isUnsizedArrayType ( TypeInfo ) [function, total]
1472-
rule #isUnsizedArrayType(typeInfoArrayType(_, noTyConst)) => true
1473-
rule #isUnsizedArrayType(_) => false [owise]
1471+
syntax Bool ::= #isArrayType ( TypeInfo ) [function, total]
1472+
rule #isArrayType(typeInfoArrayType(_, _)) => true
1473+
rule #isArrayType(_) => false [owise]
14741474
```
14751475

14761476
```k

0 commit comments

Comments
 (0)