Bump submodules (more special function support)

This bumps several submodules: * `what4` (to include GaloisInc/what4#153 and GaloisInc/what4#164) * `crucible` (to include GaloisInc/crucible#901) * `copilot` (to include GaloisInc/copilot-1#2)
Copilot-Language · Oct 29, 2021 · 02799d5 · 02799d5
1 parent a4a3cc5
commit 02799d5
Show file tree

Hide file tree

Showing 4 changed files with 5 additions and 5 deletions.
diff --git a/copilot-verifier/src/Copilot/Verifier.hs b/copilot-verifier/src/Copilot/Verifier.hs
@@ -144,7 +144,7 @@ verify csettings0 properties prefix spec =
           let csrc = odir </> prefix ++ ".c"
           let cruxOpts1 = cruxOpts0{ outDir = odir, bldDir = odir, inputFiles = [csrc] }
           ocfg <- defaultOutputConfig cruxLogMessageToSayWhat
-          let ?outputConfig = ocfg (Just cruxOpts1)
+          let ?outputConfig = ocfg (Just (outputOptions cruxOpts1))
           cruxOpts2 <- withCruxLogMessage (postprocessOptions cruxOpts1)
           (cruxOpts3, llvmOpts2) <- processLLVMOptions (cruxOpts2, llvmOpts0{ optLevel = 0 })
           return (cruxOpts3, llvmOpts2, csettings, csrc)
@@ -153,7 +153,7 @@ verify csettings0 properties prefix spec =
      putStrLn ("Generated " ++ show csrc)
 
      ocfg <- defaultOutputConfig cruxLLVMLoggingToSayWhat
-     let ?outputConfig = ocfg (Just cruxOpts)
+     let ?outputConfig = ocfg (Just (outputOptions cruxOpts))
      bcFile <- withCruxLLVMLogging (genBitCode cruxOpts llvmOpts)
      putStrLn ("Compiled " ++ prefix ++ " into " ++ bcFile)
 

diff --git a/deps/copilot b/deps/copilot
diff --git a/deps/crucible b/deps/crucible
diff --git a/deps/what4 b/deps/what4
+2 −1		copilot-theorem/copilot-theorem.cabal
+15 −14		copilot-theorem/src/Copilot/Theorem/What4.hs
+191 −179		copilot-theorem/src/Copilot/Theorem/What4/Translate.hs
+7 −1		.github/Dockerfile-crux-llvm
+110 −0		.github/workflows/crucible-jvm-build.yml
+1 −0		crucible-concurrency/crucible-concurrency.cabal
+32 −13		crucible-concurrency/src/Cruces/ExploreCrux.hs
+2 −1		crucible-go/tool/Main.hs
+0 −1		crucible-jvm/crucible-jvm.cabal
+31 −22		crucible-jvm/tool/Main.hs
+4 −0		crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics.hs
+18 −0		crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/LLVM.hs
+21 −1		crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Libc.hs
+18 −1		crucible-llvm/src/Lang/Crucible/LLVM/Translation/BlockInfo.hs
+29 −17		crucible-wasm/tool/Main.hs
+2 −2		crux-llvm/for-ide/Main.hs
+2 −2		crux-llvm/for-ide/unix/RealMain.hs
+18 −8		crux-llvm/src/Crux/LLVM/Simulate.hs
+3 −3		crux-llvm/src/CruxLLVMMain.hs
+2 −2		crux-llvm/svcomp/Main.hs
+2 −0		crux-llvm/test-data/golden/golden/invoke-test.config
+77 −0		crux-llvm/test-data/golden/golden/invoke-test.good
+1,005 −0		crux-llvm/test-data/golden/golden/invoke-test.ll
+1 −0		crux-llvm/test-data/golden/golden/invoke-test.result
+5 −1		crux-llvm/test-data/golden/special-functions-fast-math.c
+4 −2		crux-llvm/test-data/golden/special-functions.c
+24 −16		crux-mir/src/Mir/Language.hs
+7 −4		crux-mir/test/Test.hs
+1 −0		crux/crux.cabal
+55 −33		crux/src/Crux.hs
+62 −37		crux/src/Crux/Config/Common.hs
+62 −21		crux/src/Crux/Config/Load.hs
+1 −1		dependencies/what4
+2 −2		uc-crux-llvm/src/UCCrux/LLVM/Main.hs
+75 −0		uc-crux-llvm/src/UCCrux/LLVM/Overrides/Polymorphic.hs
+24 −22		uc-crux-llvm/src/UCCrux/LLVM/Overrides/Skip.hs
+23 −21		uc-crux-llvm/src/UCCrux/LLVM/Overrides/Unsound.hs
+4 −2		uc-crux-llvm/src/UCCrux/LLVM/Run/Loop.hs
+258 −129		uc-crux-llvm/src/UCCrux/LLVM/Run/Simulate.hs
+9 −7		uc-crux-llvm/test/Utils.hs
+1 −0		uc-crux-llvm/uc-crux-llvm.cabal
+11 −6		what4/src/What4/Expr/Builder.hs
+10 −6		what4/src/What4/Expr/GroundEval.hs
+7 −1		what4/src/What4/SpecialFunctions.hs