diff --git a/.travis.yml b/.travis.yml index 3bb979391d..eaf9c6a17f 100644 --- a/.travis.yml +++ b/.travis.yml @@ -72,15 +72,13 @@ jobs: addons: apt: packages: - - clang-3.8 - - llvm-3.8 + - clang-3.9 + - llvm-3.9 install: - # - git clone https://github.com/awslabs/s2n.git - - git clone https://github.com/GaloisInc/s2n.git + - git clone https://github.com/awslabs/s2n.git - mkdir -p s2n/test-deps/saw/bin - cp bin/saw s2n/test-deps/saw/bin - cd s2n - - git checkout bump-saw before_script: - export TESTS=sawHMAC - export SAW_HMAC_TEST=md5 diff --git a/src/SAWScript/Crucible/LLVM/Builtins.hs b/src/SAWScript/Crucible/LLVM/Builtins.hs index 56030ffe2b..f7265393ab 100644 --- a/src/SAWScript/Crucible/LLVM/Builtins.hs +++ b/src/SAWScript/Crucible/LLVM/Builtins.hs @@ -120,7 +120,6 @@ import qualified Lang.Crucible.Simulator as Crucible import qualified Lang.Crucible.Simulator.Breakpoint as Crucible import qualified Lang.Crucible.Simulator.GlobalState as Crucible import qualified Lang.Crucible.Simulator.PathSatisfiability as Crucible -import qualified Lang.Crucible.Simulator.SimError as Crucible -- crucible-llvm import qualified Lang.Crucible.LLVM.ArraySizeProfile as Crucible @@ -968,11 +967,11 @@ verifyPoststate opts sc cc mspec env0 globals ret = where sym = cc^.ccBackend - verifyObligation (Crucible.ProofGoal hyps (Crucible.LabeledPred concl (Crucible.SimError _loc err))) = do + verifyObligation (Crucible.ProofGoal hyps (Crucible.LabeledPred concl err)) = do hypTerm <- CrucibleSAW.toSC sym =<< W4.andAllOf sym (folded . Crucible.labeledPred) hyps conclTerm <- CrucibleSAW.toSC sym concl obligation <- scImplies sc hypTerm conclTerm - return ("safety assertion: " ++ Crucible.simErrorReasonMsg err, obligation) + return (unlines ["safety assertion:", show err], obligation) matchResult = case (ret, mspec ^. MS.csRetValue) of