saw-script.cabal

Cabal-version: 2.4
Name:          saw-script
Version:       1.2.0.99
Author:        Galois Inc.
Maintainer:    atomb@galois.com
Build-type:    Custom
License:       BSD-3-Clause
License-file:  LICENSE

extra-source-files:
    src/SAWScript/Parser.y
    src/SAWScript/Lexer.x

custom-setup
  setup-depends:
      Cabal >= 1.24
    , base
    , directory
    , filepath
    , process

library
  default-language: Haskell2010
  build-depends:
      base >= 4.9
    , aeson >= 2.0 && < 2.3
    , aig
    , array
    , binary
    , bimap
    , bytestring
    , bv-sized >= 1.0 && < 1.1
    , cborg-json
    , containers
    , constraints >= 0.6
    , cryptohash-sha256 >= 0.11.102.1
    , cryptol
    , cryptol-saw-core
    , crucible >= 0.4
    , crucible-jvm
    , crucible-llvm >= 0.2
    , crucible-mir
    , deepseq
    , either
    , elf-edit
    , exceptions
    , executable-path
    , extra
    , directory >= 1.2.4.0
    , fgl
    , filepath
    , flexdis86
    , free
    , haskeline
    , heapster-saw
    , hobbits >= 1.3.1
    , indexed-traversable
    , galois-dwarf >= 0.2.2
    , IfElse
    , jvm-parser
    , language-sally
    , lens
    , llvm-pretty >= 0.8
    , llvm-pretty-bc-parser >= 0.1.3.1
    , lmdb-simple
    , macaw-base
    , macaw-x86
    , macaw-symbolic
    , macaw-x86-symbolic
    , modern-uri >= 0.3.2 && < 0.4
    , mtl >= 2.1
    , old-locale
    , old-time
    , panic
    , parameterized-utils
    , parsec
    , pretty
    , prettyprinter
    , pretty-show
    , process
    , reflection
    , rme
    , saw-core
    , saw-core-aig
    , saw-core-coq
    , saw-core-sbv
    , saw-core-what4
    , sbv >= 9.1 && < 10.11
    , serialise
    , split
    , temporary
    , template-haskell
    , terminal-size
    , text
    , time
    , transformers
    , transformers-compat
    , unordered-containers
    , utf8-string
    , vector
    , what4 >= 0.4
    , what4-transition-system
    , zenc

  hs-source-dirs: src

  exposed-modules:
    SAWScript.AST
    SAWScript.AutoMatch
    SAWScript.AutoMatch.Interaction
    SAWScript.AutoMatch.ArgMapping
    SAWScript.AutoMatch.Declaration
    SAWScript.AutoMatch.Cryptol
    SAWScript.AutoMatch.LLVM
    SAWScript.AutoMatch.JVM
    SAWScript.AutoMatch.Util
    SAWScript.Bisimulation
    SAWScript.Bisimulation.BisimTheorem
    SAWScript.Builtins
    SAWScript.CongruenceClosure
    SAWScript.Exceptions
    SAWScript.Import
    SAWScript.ImportAIG
    SAWScript.Interpreter
    SAWScript.JavaExpr
    SAWScript.JavaPretty
    SAWScript.Lexer
    SAWScript.LLVMBuiltins
    SAWScript.Options
    SAWScript.Panic
    SAWScript.Parser
    SAWScript.Proof
    SAWScript.Position
    SAWScript.SBVParser
    SAWScript.SBVModel
    SAWScript.SolverCache
    SAWScript.SolverVersions
    SAWScript.Token
    SAWScript.TopLevel
    SAWScript.MGU
    SAWScript.Utils
    SAWScript.Value

    SAWScript.HeapsterBuiltins

    SAWScript.Crucible.Common
    SAWScript.Crucible.Common.MethodSpec
    SAWScript.Crucible.Common.Override
    SAWScript.Crucible.Common.ResolveSetupValue
    SAWScript.Crucible.Common.Setup.Builtins
    SAWScript.Crucible.Common.Setup.Type
    SAWScript.Crucible.Common.Setup.Value

    SAWScript.Crucible.LLVM.Builtins
    SAWScript.Crucible.LLVM.Boilerplate
    SAWScript.Crucible.LLVM.CrucibleLLVM
    SAWScript.Crucible.LLVM.FFI
    SAWScript.Crucible.LLVM.Override
    SAWScript.Crucible.LLVM.MethodSpecIR
    SAWScript.Crucible.LLVM.ResolveSetupValue
    SAWScript.Crucible.LLVM.Setup.Value
    SAWScript.Crucible.LLVM.Skeleton
    SAWScript.Crucible.LLVM.Skeleton.Builtins
    SAWScript.Crucible.LLVM.X86

    SAWScript.Crucible.JVM.Builtins
    SAWScript.Crucible.JVM.BuiltinsJVM
    SAWScript.Crucible.JVM.MethodSpecIR
    SAWScript.Crucible.JVM.Override
    SAWScript.Crucible.JVM.ResolveSetupValue
    SAWScript.Crucible.JVM.Setup.Value

    SAWScript.Crucible.MIR.Builtins
    SAWScript.Crucible.MIR.MethodSpecIR
    SAWScript.Crucible.MIR.Override
    SAWScript.Crucible.MIR.ResolveSetupValue
    SAWScript.Crucible.MIR.Setup.Value
    SAWScript.Crucible.MIR.TypeShape

    SAWScript.Prover.Mode
    SAWScript.Prover.Rewrite
    SAWScript.Prover.SolverStats
    SAWScript.Prover.Util
    SAWScript.Prover.SBV
    SAWScript.Prover.MRSolver
    SAWScript.Prover.MRSolver.Monad
    SAWScript.Prover.MRSolver.SMT
    SAWScript.Prover.MRSolver.Solver
    SAWScript.Prover.MRSolver.Evidence
    SAWScript.Prover.MRSolver.Term
    SAWScript.Prover.RME
    SAWScript.Prover.ABC
    SAWScript.Prover.What4
    SAWScript.Prover.Exporter
    SAWScript.Prover.Versions

    SAWScript.VerificationSummary

    SAWScript.X86
    SAWScript.X86Spec

    SAWScript.Yosys
    SAWScript.Yosys.Cell
    SAWScript.Yosys.IR
    SAWScript.Yosys.Netgraph
    SAWScript.Yosys.State
    SAWScript.Yosys.Theorem
    SAWScript.Yosys.TransitionSystem
    SAWScript.Yosys.Utils

  other-modules:
    GitRev
  autogen-modules:
    GitRev

  GHC-options: -O2 -Wall -fno-ignore-asserts -fno-spec-constr-count
  if impl(ghc == 8.0.1)
    ghc-options: -Wno-redundant-constraints

  build-tool-depends:
    alex:alex >= 3.1.3,
    happy:happy >= 1.9.4

executable saw
  default-language: Haskell2010
  hs-source-dirs: saw

  main-is: Main.hs

  other-modules:
    Paths_saw_script
    GitRev
    SAWScript.REPL
    SAWScript.REPL.Command
    SAWScript.REPL.Haskeline
    SAWScript.REPL.Logo
    SAWScript.REPL.Monad
    SAWScript.REPL.Trie
    SAWScript.Version

  autogen-modules:
    Paths_saw_script
    GitRev

  build-depends:
      base >= 4
    , ansi-terminal
    , containers
    , cryptol
    , directory
    , either
    , exceptions
    , filepath
    , haskeline
    , mtl
    , QuickCheck
    , transformers
    , saw-script
    , saw-core
    , heapster-saw
    , cryptol-saw-core
    , aig

  GHC-options: -O2 -Wall -Werror -threaded -fno-ignore-asserts -fno-spec-constr-count -rtsopts

test-suite integration_tests
  type: exitcode-stdio-1.0
  hs-source-dirs: intTests

  ghc-options: -Wall -threaded
  default-language: Haskell2010

  main-is: IntegrationTest.hs

  build-depends: base
               , directory
               , filemanip
               , filepath
               , process
               , tasty
               , tasty-hunit
               , tasty-expected-failure

  build-tool-depends: saw-script:saw