Skip to content

Commit

Permalink
Merge branch 'master' into bh-alignment
Browse files Browse the repository at this point in the history
  • Loading branch information
Brian Huffman committed Jan 24, 2020
2 parents 950f106 + 4077704 commit cfead3e
Show file tree
Hide file tree
Showing 2 changed files with 5 additions and 8 deletions.
8 changes: 3 additions & 5 deletions .travis.yml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
5 changes: 2 additions & 3 deletions src/SAWScript/Crucible/LLVM/Builtins.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down

0 comments on commit cfead3e

Please sign in to comment.