saw-script.cabal

Name:          saw-script
Version:       0.8.0.99
Author:        Galois Inc.
Maintainer:    atomb@galois.com
Build-type:    Custom
Cabal-version: >= 1.24
License:       BSD3
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

flag builtin-abc
  description: Link with ABC as a static library
  default: True

library
  default-language: Haskell2010
  build-depends:
      base >= 4
    , aig
    , array
    , binary
    , bimap
    , bytestring
    , bv-sized >= 1.0 && < 1.1
    , containers
    , constraints >= 0.6
    , cryptol
    , cryptol-saw-core
    , crucible >= 0.4
    , crucible-jvm
    , crucible-llvm >= 0.2
    , deepseq
    , either
    , exceptions
    , executable-path
    , extra
    , directory >= 1.2.4.0
    , fgl
    , filepath
    , free
    , haskeline
    , IfElse
    , jvm-parser
    , lens
    , llvm-pretty >= 0.8
    , llvm-pretty-bc-parser >= 0.1.3.1
    , modern-uri >= 0.3.2 && < 0.4
    , mtl >= 2.1
    , old-locale
    , old-time
    , panic
    , parameterized-utils
    , parsec
    , pretty
    , prettyprinter
    , pretty-show
    , process
    , rme
    , saw-core
    , saw-core-aig
    , saw-core-coq
    , saw-core-sbv
    , saw-core-what4
    , sbv >= 8.6 && < 8.8
    , split
    , temporary
    , template-haskell
    , terminal-size
    , text
    , time
    , transformers
    , transformers-compat
    , unordered-containers
    , utf8-string
    , what4 >= 0.4
    , vector
    , GraphSCC
    , macaw-base
    , macaw-x86
    , macaw-symbolic
    , macaw-x86-symbolic
    , flexdis86
    , elf-edit
    , reflection
    , aeson

  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.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.PathVC
    SAWScript.Proof
    SAWScript.Position
    SAWScript.SBVParser
    SAWScript.SBVModel
    SAWScript.Token
    SAWScript.TopLevel
    SAWScript.MGU
    SAWScript.Utils
    SAWScript.Value
    SAWScript.VerificationCheck

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

    SAWScript.Crucible.LLVM.Builtins
    SAWScript.Crucible.LLVM.Boilerplate
    SAWScript.Crucible.LLVM.CrucibleLLVM
    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
    SAWScript.Crucible.JVM.BuiltinsJVM
    SAWScript.Crucible.JVM.MethodSpecIR
    SAWScript.Crucible.JVM.Override
    SAWScript.Crucible.JVM.ResolveSetupValue

    SAWScript.Prover.Mode
    SAWScript.Prover.Rewrite
    SAWScript.Prover.SolverStats
    SAWScript.Prover.Util
    SAWScript.Prover.SBV
    SAWScript.Prover.MRSolver
    SAWScript.Prover.RME
    SAWScript.Prover.ABC
    SAWScript.Prover.What4
    SAWScript.Prover.Exporter
    SAWScript.Prover.Versions

    SAWScript.VerificationSummary

    SAWScript.X86
    SAWScript.X86Spec

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

  build-tools:
    alex >= 3.1.3,
    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
    , QuickCheck
    , transformers
    , saw-script
    , saw-core
    , cryptol-saw-core

  if flag(builtin-abc)
    cpp-options: -DUSE_BUILTIN_ABC
    build-depends: abcBridge
    GHC-options: -O2 -Wall -Werror -fno-ignore-asserts -fno-spec-constr-count -pgmlc++
    extra-libraries:      stdc++
  else
    build-depends: aig
    GHC-options: -O2 -Wall -Werror -fno-ignore-asserts -fno-spec-constr-count

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

  ghc-options: -Wall
  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