Merge remote-tracking branch 'origin/skeleton' into cex-errors2

GaloisInc · Sep 11, 2020 · a896d3a · a896d3a
2 parents 9c6d6ab + 5c410fd
commit a896d3a
Show file tree

Hide file tree

Showing 13 changed files with 934 additions and 421 deletions.
diff --git a/deps/crucible b/deps/crucible
diff --git a/deps/macaw b/deps/macaw
diff --git a/intTests/disabled_tests.txt b/intTests/disabled_tests.txt
@@ -12,3 +12,6 @@ test0010_jss_cnf_exp
 
 # Missing LLVM intrinsic
 test0039_rust
+
+# Boilerplate generation has been overhauled
+test_boilerplate
diff --git a/saw-script.cabal b/saw-script.cabal
@@ -143,6 +143,8 @@ library
     SAWScript.Crucible.LLVM.Override
     SAWScript.Crucible.LLVM.MethodSpecIR
     SAWScript.Crucible.LLVM.ResolveSetupValue
+    SAWScript.Crucible.LLVM.Skeleton
+    SAWScript.Crucible.LLVM.Skeleton.Builtins
     SAWScript.Crucible.LLVM.X86
 
     SAWScript.Crucible.JVM.Builtins
+0 −3		.gitmodules
+1 −1		cabal.project
+1 −1		crucible-llvm/crucible-llvm.cabal
+126 −77		crucible-llvm/src/Lang/Crucible/LLVM/ArraySizeProfile.hs
+2 −2		crucible-llvm/src/Lang/Crucible/LLVM/Errors.hs
+25 −21		crucible-llvm/src/Lang/Crucible/LLVM/Errors/UndefinedBehavior.hs
+2 −1		crucible-llvm/src/Lang/Crucible/LLVM/Eval.hs
+3 −0		crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics.hs
+24 −0		crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/LLVM.hs
+5 −4		crucible-llvm/src/Lang/Crucible/LLVM/MemModel.hs
+62 −40		crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Partial.hs
+2 −2		crucible-llvm/src/Lang/Crucible/LLVM/MemType.hs
+1 −1		crucible-llvm/src/Lang/Crucible/LLVM/Printf.hs
+2 −2		crucible-server/crucible-server.cabal
+9 −0		crucible/src/Lang/Crucible/CFG/Expr.hs
+3 −0		crucible/src/Lang/Crucible/CFG/Generator.hs
+1 −0		crucible/src/Lang/Crucible/Simulator/SimError.hs
+11 −0		crucible/src/Lang/Crucible/Utils/StateContT.hs
+6 −8		crux-llvm/c-src/print-model.c
+23 −13		crux-llvm/src/Crux/LLVM/Compile.hs
+8 −1		crux-llvm/src/Crux/LLVM/Simulate.hs
+0 −1		crux-llvm/src/CruxLLVMMain.hs
+4 −5		crux/src/Crux.hs
+13 −9		crux/src/Crux/Goal.hs
+63 −31		crux/src/Crux/Model.hs
+58 −34		crux/src/Crux/Report.hs
+31 −7		crux/src/Crux/UI/IndexHtml.hs
+15 −13		crux/src/Crux/UI/JS.hs
+1 −1		dependencies/cryptol
+0 −1		dependencies/cryptol-verifier
+1 −1		dependencies/saw-core
+1 −1		dependencies/what4
+1 −1		deps/asl-translator
+1 −1		deps/crucible
+1 −1		deps/dismantle
+1 −1		deps/semmc
+1 −0		refinement/src/Data/Macaw/Refinement/SymbolicExecution.hs
+2 −2		refinement/tests/RefinementTests.hs
+1 −1		symbolic/src/Data/Macaw/Symbolic/Memory.hs
+3 −1		x86/src/Data/Macaw/X86/ArchTypes.hs
+8 −0		x86/src/Data/Macaw/X86/Semantics.hs
+5 −1		x86/src/Data/Macaw/X86/Semantics/AVX.hs
+4 −0		x86_symbolic/src/Data/Macaw/X86/Crucible.hs