Update and adapt to GaloisInc/crucible#886 "dbg-def-use".

This adds a new translation-warnings output to function `translateModule`. Currently the translation warnings are ignored.
GaloisInc · Nov 12, 2021 · 28aff7c · 28aff7c
1 parent 99b783a
commit 28aff7c
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 2 deletions.
diff --git a/deps/crucible b/deps/crucible
diff --git a/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs b/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs
@@ -258,7 +258,8 @@ loadLLVMModule file halloc =
        Left err -> return (Left err)
        Right llvm_mod ->
          do memVar <- CL.mkMemVar (Text.pack "saw:llvm_memory") halloc
-            Some mtrans <- CL.translateModule halloc memVar llvm_mod
+            -- FIXME: do something with the translation warnings
+            (Some mtrans, _warnings) <- CL.translateModule halloc memVar llvm_mod
             return (Right (Some (LLVMModule file llvm_mod mtrans)))
 
 instance TestEquality LLVMModule where
+1 −0		crucible-llvm/crucible-llvm.cabal
+7 −2		crucible-llvm/src/Lang/Crucible/LLVM/Ctors.hs
+57 −20		crucible-llvm/src/Lang/Crucible/LLVM/Translation.hs
+285 −0		crucible-llvm/src/Lang/Crucible/LLVM/Translation/BlockInfo.hs
+59 −46		crucible-llvm/src/Lang/Crucible/LLVM/Translation/Instruction.hs
+47 −55		crucible-llvm/src/Lang/Crucible/LLVM/Translation/Monad.hs
+1 −1		crucible-llvm/test/MemSetup.hs
+3 −2		crucible-llvm/test/Tests.hs
+11 −0		crux-llvm/src/Crux/LLVM/Log.hs
+15 −4		crux-llvm/src/Crux/LLVM/Simulate.hs
+0 −3		crux-llvm/test-data/golden/T778.config
+0 −1		crux-llvm/test-data/golden/T778.good
+0 −0		crux-llvm/test-data/golden/T778.result
+7 −2		crux-llvm/test-data/golden/shrink.c.orig
+1 −0		crux-llvm/test-data/golden/shrink.config
+2 −0		crux-llvm/test-data/golden/shrink.good
+90 −0		crux-llvm/test-data/golden/shrink.ll
+1 −1		uc-crux-llvm/src/UCCrux/LLVM/Main.hs