Skip to content

Commit dbab6e9

Browse files
authored
Merge pull request #1614 from GaloisInc/fix-permForLLVMArrayBorrow
Fix error in `permForLLVMArrayBorrow`
2 parents bc564dd + 64fce85 commit dbab6e9

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs

+1-1
Original file line numberDiff line numberDiff line change
@@ -4575,7 +4575,7 @@ permForLLVMArrayBorrow ap (FieldBorrow cell) =
45754575
ValPerm_LLVMBlock $ llvmArrayCellPerm ap cell
45764576
permForLLVMArrayBorrow ap (RangeBorrow (BVRange off len)) =
45774577
ValPerm_Conj1 $ Perm_LLVMArray $
4578-
ap { llvmArrayOffset = llvmArrayCellToOffset ap off,
4578+
ap { llvmArrayOffset = llvmArrayCellToAbsOffset ap off,
45794579
llvmArrayLen = len,
45804580
llvmArrayBorrows = [] }
45814581

0 commit comments

Comments
 (0)