Bump submodules to allow building with what4-1.6.*

This bumps the `what4` submodule to the 1.6.* version series and updates the `.cabal` files in the `macaw` repo accordingly. Bumping the `what4` submodule also requires bringing in corresponding changes in the `crucible`, `llvm-pretty`, and `llvm-pretty-bc-parser` submodules, so I have done that as well.
GaloisInc · Jun 13, 2024 · 4db0341 · 4db0341
1 parent d04f097
commit 4db0341
Show file tree

Hide file tree

Showing 6 changed files with 6 additions and 6 deletions.
diff --git a/deps/crucible b/deps/crucible
diff --git a/deps/llvm-pretty b/deps/llvm-pretty
diff --git a/deps/llvm-pretty-bc-parser b/deps/llvm-pretty-bc-parser
diff --git a/deps/what4 b/deps/what4
diff --git a/macaw-semmc/macaw-semmc.cabal b/macaw-semmc/macaw-semmc.cabal
@@ -39,7 +39,7 @@ library
                        semmc,
                        bv-sized >= 1 && < 1.1,
                        libBF >= 0.6 && < 0.7,
-                       what4 >= 1.1 && < 1.6
+                       what4 >= 1.1 && < 1.7
   hs-source-dirs:      src
   default-language:    Haskell2010
   ghc-options:         -Wall -Wcompat
diff --git a/symbolic/macaw-symbolic.cabal b/symbolic/macaw-symbolic.cabal
@@ -27,7 +27,7 @@ library
     text,
     vector,
     bytestring,
-    what4 >= 1.1 && < 1.6
+    what4 >= 1.1 && < 1.7
 
   hs-source-dirs: src
+6 −2		.gitignore
+5 −0		CHANGELOG.md
+36 −0		README.md
+12 −6		llvm-pretty.cabal
+36 −6		src/Text/LLVM/AST.hs
+1 −0		src/Text/LLVM/Labels.hs
+1 −1		src/Text/LLVM/Lens.hs
+298 −195		src/Text/LLVM/PP.hs
+6 −1		test/Main.hs
+343 −0		test/Output.hs
+62 −0		test/TQQDefs.hs
+1 −1		.github/workflows/build.yml
+17 −5		.github/workflows/llvm-quick-fuzz.yml
+1 −1		.github/workflows/nix-ci.yml
+1 −1		.gitmodules
+20 −0		CHANGELOG.md
+1 −1		README.md
+163 −82		disasm-test/Main.hs
+53 −0		disasm-test/bc_src_tests/README.md
+ −		disasm-test/bc_src_tests/apple-llvm.bc
+927 −0		disasm-test/bc_src_tests/apple-llvm.ll
+ −		disasm-test/bc_src_tests/hello-world.bc
+4 −0		disasm-test/bc_src_tests/hello-world.ll
+8 −2		disasm-test/known_bugs/README.md
+0 −10		disasm-test/known_bugs/llvm-pretty_issue114
+0 −6		disasm-test/known_bugs/pr223pr228.txt
+7 −0		disasm-test/known_bugs/pr247
+1 −1		disasm-test/llvm-tests/README.md
+7 −0		disasm-test/tests/T266-constant-icmp.ll
+7 −0		disasm-test/tests/T266-constant-icmp.pre-llvm15.ll
+9 −0		disasm-test/tests/cmpxchg.c
+73 −0		disasm-test/tests/cmpxchg.ll
+5 −0		disasm-test/tests/derivedtype.c
+52 −0		disasm-test/tests/derivedtype.ll
+7 −0		disasm-test/tests/global-var-extern.c
+32 −0		disasm-test/tests/global-var-extern.ll
+7 −0		disasm-test/tests/global-var.c
+13 −0		disasm-test/tests/global-var.ll
+33 −0		disasm-test/tests/instrmd.ll
+41 −0		disasm-test/tests/smallprog.c
+226 −0		disasm-test/tests/smallprog.ll
+1 −0		doc/developing.md
+29 −15		flake.lock
+21 −6		flake.nix
+24 −26		llvm-disasm/LLVMDis.hs
+1 −1		llvm-pretty
+9 −4		llvm-pretty-bc-parser.cabal
+6 −4		src/Data/LLVM/BitCode/IR/Constants.hs
+23 −4		src/Data/LLVM/BitCode/IR/Function.hs
+352 −286		src/Data/LLVM/BitCode/IR/Metadata.hs
+0 −18		src/Data/LLVM/BitCode/IR/Values.hs
+1 −1		src/Data/LLVM/BitCode/Parse.hs
+1 −1		unit-test/Tests/ExpressionInstances.hs
+7 −3		.github/workflows/gen_matrix.pl
+24 −0		.github/workflows/lint.yml
+4 −1		.github/workflows/test.yml
+11 −72		.hlint.yaml
+5 −5		README.md
+1 −1		dependencies/aig
+1 −1		what4-abc/what4-abc.cabal
+1 −1		what4-blt/what4-blt.cabal
+2 −2		what4-transition-system/what4-transition-system.cabal
+32 −0		what4/CHANGES.md
+1 −0		what4/README.md
+1 −0		what4/src/What4/Expr.hs
+2 −2		what4/src/What4/Expr/App.hs
+542 −45		what4/src/What4/Expr/Builder.hs
+36 −0		what4/src/What4/Expr/GroundEval.hs
+2 −2		what4/src/What4/Expr/MATLAB.hs
+46 −5		what4/src/What4/Interface.hs
+56 −4		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
+8 −0		what4/src/What4/Solver/CVC4.hs
+0 −8		what4/src/What4/Solver/CVC5.hs
+88 −9		what4/src/What4/Solver/Z3.hs
+0 −6		what4/src/What4/Utils/Versions.hs
+50 −3		what4/test/AdapterTest.hs
+3 −1		what4/test/ConfigTest.hs
+55 −25		what4/test/ExprBuilderSMTLib2.hs
+4 −3		what4/test/InvariantSynthesis.hs
+3 −0		what4/test/OnlineSolverTest.hs
+3 −1		what4/test/ProbeSolvers.hs
+5 −4		what4/what4.cabal