voogie.cabal

cabal-version: 3.0
name: voogie
version: 0.1.0.0
synopsis: A verification conditions generator for simple Boogie programs
description:
  Voogie reads simple Boogie programs and generates their verification
  conditions as formulas in the FOOL logic. These formulas are written in the
  TPTP language and can be checked by automated first-order theorem provers.
  Currently, only the Vampire theorem prover fully supports FOOL.
homepage: https://github.com/aztek/voogie
bug-reports: https://github.com/aztek/voogie/issues
license: GPL-3.0-only
license-file: LICENSE
author: Evgenii Kotelnikov
maintainer: evgeny.kotelnikov@gmail.com
category: Language
build-type: Simple
extra-source-files: README.md
tested-with:
  GHC == 7.10.3,
  GHC == 8.0.2,
  GHC == 8.2.2,
  GHC == 8.4.4,
  GHC == 8.6.5,
  GHC == 8.8.1

source-repository head
  type: git
  location: git://github.com/aztek/voogie.git

flag Werror
  default: False
  manual: True

common ghc-warnings
  ghc-options:
    -Wall
  if flag(Werror)
    ghc-options: -Werror
  if impl(ghc < 8)
    ghc-options:
      -fwarn-incomplete-record-updates -fwarn-incomplete-uni-patterns
      -fno-warn-orphans
    build-depends:
      semigroups >= 0.18 && < 1.0
  if impl(ghc >= 8)
    ghc-options:
      -Wcompat -Wincomplete-record-updates -Wincomplete-uni-patterns
      -Wredundant-constraints -Wno-orphans

executable voogie
  import: ghc-warnings
  default-language: Haskell2010
  hs-source-dirs: src/Voogie/Executable
  main-is: Main.hs
  other-modules:
    CmdArgs
    Paths_voogie
  autogen-modules:
    Paths_voogie
  ghc-options:
    -threaded
  build-depends:
    base,
    text,
    optparse-applicative >= 0.14.3 && <= 0.15.1,
    unix                 >= 2.7    && <  2.8,
    voogie-internal
  if impl(ghc >= 8)
    default-extensions: Safe

library voogie-internal
  import: ghc-warnings
  default-language: Haskell2010
  hs-source-dirs: src
  exposed-modules:
    Data.List.NonUnit
    Voogie.AST
    Voogie.AST.Boogie
    Voogie.AST.FOOL
    Voogie.Back
    Voogie.Boogie
    Voogie.Boogie.Smart
    Voogie.Boogie.Syntax
    Voogie.Error
    Voogie.FOOL
    Voogie.FOOL.ArrayTheory
    Voogie.FOOL.Traverse
    Voogie.FOOL.Smart
    Voogie.Front
    Voogie.Language
    Voogie.Parse
    Voogie.Parse.Boogie
    Voogie.Parse.FOOL
    Voogie.Pretty
    Voogie.Pretty.Boogie
    Voogie.Pretty.Boogie.Boogie
    Voogie.Pretty.Boogie.FOOL
    Voogie.Pretty.TPTP
    Voogie.Pretty.TPTP.FOOL
    Voogie.TPTP
    Voogie.TPTP.Syntax
  other-modules:
    Data.List.NonEmpty
  build-depends:
    base           >= 4.8    && < 5.0,
    containers     >= 0.6.0  && < 0.7,
    extra          >= 1.6    && < 1.7,
    mtl            >= 2.2    && < 3.0,
    parsec         >= 3.1    && < 3.2,
    text           >= 0.11.3 && < 1.3,
    ansi-wl-pprint >= 0.6.6  && < 0.7
  if impl(ghc >= 8)
    default-extensions: Safe

test-suite test-idempotent-parsing-pretty-printing
  import: ghc-warnings
  default-language: Haskell2010
  type: exitcode-stdio-1.0
  main-is: tests/IdempotentParsingPrettyPrinting.hs
  ghc-options:
    -threaded
  build-depends:
    base,
    process

test-suite test-quickcheck-generators
  import: ghc-warnings
  default-language: Haskell2010
  type: exitcode-stdio-1.0
  hs-source-dirs: tests
  main-is: Generators.hs
  ghc-options:
    -threaded -main-is Generators
  build-depends:
    base,
    voogie-internal,
    QuickCheck

test-suite test-quickcheck-back
  import: ghc-warnings
  default-language: Haskell2010
  type: exitcode-stdio-1.0
  hs-source-dirs: tests
  main-is: Back.hs
  ghc-options:
    -threaded -main-is Back
  other-modules:
    Generators
  build-depends:
    base,
    voogie-internal,
    QuickCheck