diff --git a/deps/crucible b/deps/crucible index b4422dd2f7..a18468dfd2 160000 --- a/deps/crucible +++ b/deps/crucible @@ -1 +1 @@ -Subproject commit b4422dd2f75f5a7310bc038a6ca67a91f3692a42 +Subproject commit a18468dfd2e48b3287d6d276faf6c7ecd33f3a8b diff --git a/deps/llvm-pretty b/deps/llvm-pretty index d099d5d0fe..16bc5bd5a0 160000 --- a/deps/llvm-pretty +++ b/deps/llvm-pretty @@ -1 +1 @@ -Subproject commit d099d5d0feab8066bc682f11c8a46c82fb7166b5 +Subproject commit 16bc5bd5a07d6e5d99c1c0f3a57b8eca2ecc944e diff --git a/deps/llvm-pretty-bc-parser b/deps/llvm-pretty-bc-parser index 59e6991e1b..9ba94bb3d7 160000 --- a/deps/llvm-pretty-bc-parser +++ b/deps/llvm-pretty-bc-parser @@ -1 +1 @@ -Subproject commit 59e6991e1b89252d4a4aa28a84ab1ac022c18b8d +Subproject commit 9ba94bb3d7e01d710c1eea364ab0b84045c9df78 diff --git a/heapster-saw/src/Verifier/SAW/Heapster/LLVMGlobalConst.hs b/heapster-saw/src/Verifier/SAW/Heapster/LLVMGlobalConst.hs index 7dea55bbb7..be82b7ebc8 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/LLVMGlobalConst.hs +++ b/heapster-saw/src/Verifier/SAW/Heapster/LLVMGlobalConst.hs @@ -178,7 +178,7 @@ translateLLVMType _ tp = -- | Helper function for 'translateLLVMValue' applied to a constant expression translateLLVMConstExpr :: (1 <= w, KnownNat w) => NatRepr w -> L.ConstExpr -> LLVMTransM (PermExpr (LLVMShapeType w), OpenTerm) -translateLLVMConstExpr w (L.ConstGEP _ _ _ (L.Typed tp ptr : ixs)) = +translateLLVMConstExpr w (L.ConstGEP _ _ _ (L.Typed tp ptr) ixs) = translateLLVMValue w tp ptr >>= \ptr_trans -> translateLLVMGEP w tp ptr_trans ixs translateLLVMConstExpr w (L.ConstConv L.BitCast