Skip to content

Commit

Permalink
Add basic tests for LLVM through crucible-c
Browse files Browse the repository at this point in the history
Now, tests for the LLVM memory model can be written in C.
  • Loading branch information
david-christiansen committed Dec 5, 2018
1 parent c2612d5 commit b17bdb7
Show file tree
Hide file tree
Showing 24 changed files with 726 additions and 482 deletions.
1 change: 1 addition & 0 deletions .gitignore
Original file line number Diff line number Diff line change
Expand Up @@ -11,3 +11,4 @@ stack.yaml
/dist-newstyle
.*.swp
cabal.project.local
*.tix
71 changes: 69 additions & 2 deletions crucible-c/crucible-c.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -13,19 +13,57 @@ Description:
This tool (and corresponding C library) are intended for writing Crucible
specifications by using C as the specification language.

library

hs-source-dirs: src

exposed-modules: CrucibleCMain

other-modules:
Overrides

build-depends:
base >= 4.8 && < 4.13,
ansi-wl-pprint,
containers,
data-binary-ieee754,
lens,
mtl,
bytestring,
crucible,
crucible-llvm,
what4,
llvm-pretty,
llvm-pretty-bc-parser,
parameterized-utils,
filepath,
process,
directory,
template-haskell,
text,
ansi-terminal,
crux

ghc-options: -Wall
ghc-prof-options: -O2 -fprof-auto-top

default-language: Haskell2010



executable crucible-c

hs-source-dirs: src
main-is: Main.hs

other-modules:
Overrides
Overrides,
CrucibleCMain

build-depends:
base >= 4.8 && < 4.13,
ansi-wl-pprint,
containers,
crucible-c,
data-binary-ieee754,
lens,
mtl,
Expand All @@ -50,3 +88,32 @@ executable crucible-c
default-language: Haskell2010


test-suite crucible-c-test
type: exitcode-stdio-1.0
hs-source-dirs: test

ghc-options: -Wall
ghc-prof-options: -fprof-auto -O2

main-is: Test.hs

build-depends:
base >= 4.7,
containers,
crucible,
crucible-c,
deepseq,
directory,
filepath,
parsec,
process,
saw-core,
QuickCheck,
tasty >= 0.10,
tasty-hunit >= 0.10,
tasty-golden >= 2.3,
text,
what4

default-language: Haskell2010

Loading

0 comments on commit b17bdb7

Please sign in to comment.