Bump crucible, what4 submodules

This bumps: * The `crucible` submodule to bring in the changes from GaloisInc/crucible#1178 * The `what4` submodule to bring in the changes from GaloisInc/what4#256
GaloisInc · Mar 1, 2024 · c300e51 · c300e51
1 parent 392e3ca
commit c300e51
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/deps/crucible b/deps/crucible
diff --git a/deps/what4 b/deps/what4
+4 −1		.github/Dockerfile-crux-llvm
+4 −1		.github/Dockerfile-crux-mir
+6 −2		.github/ci.sh
+14 −11		.github/workflows/README.md
+3 −2		.github/workflows/crucible-go-build.yml
+3 −2		.github/workflows/crucible-jvm-build.yml
+3 −2		.github/workflows/crucible-wasm-build.yml
+19 −69		.github/workflows/crux-llvm-build.yml
+28 −11		.github/workflows/crux-mir-build.yml
+0 −289		cabal.GHC-8.10.7.config
+1 −1		cabal.GHC-9.2.8.config
+1 −1		cabal.GHC-9.4.5.config
+1 −1		cabal.GHC-9.6.2.config
+0 −1		cabal.project
+1 −1		crucible-llvm/crucible-llvm.cabal
+5 −0		crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics.hs
+91 −3		crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Common.hs
+33 −9		crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Libc.hs
+3 −3		crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Options.hs
+37 −0		crucible-llvm/src/Lang/Crucible/LLVM/MemModel.hs
+143 −63		crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Generic.hs
+27 −8		crucible-llvm/src/Lang/Crucible/LLVM/MemModel/MemLog.hs
+8 −0		crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Options.hs
+921 −406		crucible-llvm/src/Lang/Crucible/LLVM/SimpleLoopFixpoint.hs
+6 −0		crucible-llvm/src/Lang/Crucible/LLVM/SimpleLoopInvariant.hs
+0 −1		crucible-llvm/src/Lang/Crucible/LLVM/Translation/Expr.hs
+0 −5		crucible-mc/CHANGELOG.md
+0 −13		crucible-mc/LICENSE
+0 −2		crucible-mc/README
+0 −2		crucible-mc/Setup.hs
+0 −33		crucible-mc/crucible-mc.cabal
+0 −96		crucible-mc/exe/Main.hs
+0 −28		crucible-mc/exe/Print.hs
+0 −12		crucible-mc/test/Makefile
+0 −7		crucible-mc/test/example.c
+1 −1		crucible-symio/crucible-symio.cabal
+5 −0		crucible/CHANGELOG.md
+1 −1		crucible/crucible.cabal
+18 −0		crucible/src/Lang/Crucible/Analysis/Fixpoint/Components.hs
+65 −0		crucible/src/Lang/Crucible/Backend.hs
+77 −49		crucible/src/Lang/Crucible/Backend/AssumptionStack.hs
+1 −1		crucible/src/Lang/Crucible/Backend/Online.hs
+31 −17		crucible/src/Lang/Crucible/Backend/ProofGoals.hs
+1 −1		crucible/src/Lang/Crucible/Backend/Simple.hs
+0 −1		crucible/src/Lang/Crucible/CFG/Expr.hs
+15 −0		crucible/src/Lang/Crucible/FunctionHandle.hs
+0 −1		crucible/src/Lang/Crucible/Simulator/EvalStmt.hs
+1 −10		crucible/src/Lang/Crucible/Types.hs
+2 −2		crux-llvm/README.md
+1 −1		crux-llvm/crux-llvm.cabal
+3 −0		crux-llvm/src/Crux/LLVM/Config.hs
+2 −1		crux-llvm/svcomp/mk-svcomp-bindist.sh
+6 −3		crux-llvm/test-data/golden/T785a.c
+9 −2		crux-llvm/test-data/golden/T785b.c
+1 −1		crux-llvm/test-data/golden/T785b.z3.good
+1 −1		crux-llvm/test-data/golden/golden/double_free.c
+35 −25		crux-llvm/test-data/golden/isinf.c
+9 −3		crux-llvm/test-data/golden/isnan.c
+5 −0		crux-llvm/test-data/golden/special-functions.c
+8 −1		crux-llvm/test/Test.hs
+1 −1		crux-mir/README.md
+1 −1		crux-mir/crux-mir.cabal
+1 −1		crux/crux.cabal
+0 −1		crux/src/Crux.hs
+1 −1		dependencies/mir-json
+1 −1		dependencies/what4
+2 −0		uc-crux-llvm/src/UCCrux/LLVM/Run/Simulate.hs
+4 −1		.github/workflows/gen_matrix.pl
+3 −1		.github/workflows/test.yml
+5 −5		README.md
+4 −0		what4/CHANGES.md
+1 −0		what4/README.md
+1 −0		what4/src/What4/Expr.hs
+524 −37		what4/src/What4/Expr/Builder.hs
+22 −0		what4/src/What4/Interface.hs
+29 −2		what4/src/What4/Protocol/SMTLib2.hs
+5 −3		what4/src/What4/Protocol/SMTWriter.hs
+11 −0		what4/src/What4/Solver.hs
+158 −0		what4/src/What4/Solver/Bitwuzla.hs
+88 −9		what4/src/What4/Solver/Z3.hs
+42 −1		what4/test/AdapterTest.hs
+2 −1		what4/test/InvariantSynthesis.hs
+3 −0		what4/test/OnlineSolverTest.hs
+3 −2		what4/what4.cabal