wip

GaloisInc · Jan 19, 2024 · 803a8be · 803a8be
1 parent 34651c6
commit 803a8be
Show file tree

Hide file tree

Showing 5 changed files with 954 additions and 409 deletions.
diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Generic.hs b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Generic.hs
@@ -790,9 +790,10 @@ readMem' sym w end gsym l0 origMem tp0 alignment (MemWrites ws) =
         else do -- We're playing a trick here.  By making a fresh constant a proof obligation, we can be
                 -- sure it always fails.  But, because it's a variable, it won't be constant-folded away
                 -- and we can be relatively sure the annotation will survive.
-                b <- freshConstant sym (safeSymbol "noSatisfyingWrite") BaseBoolRepr
-                Partial.Err <$>
-                  Partial.annotateME sym mop (NoSatisfyingWrite tp) b
+                -- b <- freshConstant sym (safeSymbol "noSatisfyingWrite") BaseBoolRepr
+                -- Partial.Err <$>
+                --   Partial.annotateME sym mop (NoSatisfyingWrite tp) b
+                Partial.partErr sym mop (NoSatisfyingWrite tp)
 
     go :: (StorageType -> LLVMPtr sym w -> ReadMem sym (PartLLVMVal sym)) ->
           LLVMPtr sym w ->