Skip to content

Commit

Permalink
Remove unused function.
Browse files Browse the repository at this point in the history
  • Loading branch information
abakst committed Mar 24, 2022
1 parent a415019 commit 590265a
Showing 1 changed file with 0 additions and 13 deletions.
13 changes: 0 additions & 13 deletions heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs
Original file line number Diff line number Diff line change
Expand Up @@ -3723,19 +3723,6 @@ llvmPtr0EqExPerm :: (1 <= w, KnownNat w, 1 <= sz, KnownNat sz) => prx sz ->
(ValuePerm (LLVMPointerType w))
llvmPtr0EqExPerm = fmap (ValPerm_Conj1 . Perm_LLVMField) . llvmPtr0EqEx

llvmExBlock :: (1 <= w, KnownNat w) =>
PermExpr (BVType w) -> PermExpr (BVType w) ->
PermExpr (LLVMShapeType w) ->
Mb (RNil :> RWModalityType :> LifetimeType)
(LLVMBlockPerm w)
llvmExBlock off len shape =
nuMulti (MNil :>: Proxy :>: Proxy) $ \(_ :>: rw :>: l) ->
LLVMBlockPerm { llvmBlockRW = PExpr_Var rw,
llvmBlockLifetime = PExpr_Var l,
llvmBlockOffset = off,
llvmBlockLen = len,
llvmBlockShape = shape }

-- | Create a permission to read a known value from offset 0 of an LLVM pointer
-- in the given lifetime, i.e., return @exists y.[l]ptr ((0,R) |-> eq(e))@
llvmRead0EqPerm :: (1 <= w, KnownNat w) => PermExpr LifetimeType ->
Expand Down

0 comments on commit 590265a

Please sign in to comment.