-- Initial G2.cabal generated by cabal init. For further documentation,
-- see http://haskell.org/cabal/users-guide/
name: g2
version: 0.1.0.2
synopsis: Haskell symbolic execution engine.
description: A Haskell symbolic execution engine.
For details, please see: <https://github.com/BillHallahan/G2>
License: BSD3
License-file: LICENSE
author: William Hallahan, Anton Xue
maintainer: whallahan@binghamton.edu
-- copyright:
category: Formal Methods, Symbolic Computation
build-type: Simple
extra-source-files: README.md
cabal-version: 1.24
Flag support-lh
Description: Build modules for reasoning about LiquidHaskell
Default: True
source-repository head
type: git
location: https://github.com/BillHallahan/G2.git
library
exposed-modules:
G2.Config
, G2.Config.Config
, G2.Config.Interface
, G2.Config.ParseConfig
, G2.Data.Timer
, G2.Data.UFMap
, G2.Data.UnionFind
, G2.Data.Utils
, G2.Equiv.Approximation
, G2.Equiv.Config
, G2.Equiv.InitRewrite
, G2.Equiv.EquivADT
, G2.Equiv.G2Calls
, G2.Equiv.Verifier
, G2.Equiv.Tactics
, G2.Equiv.Types
, G2.Equiv.Generalize
, G2.Equiv.Summary
, G2.Equiv.Uninterpreted
, G2.Execution
, G2.Execution.HPC
, G2.Execution.Interface
, G2.Execution.Memory
, G2.Execution.NewPC
, G2.Execution.NormalForms
, G2.Execution.PrimitiveEval
, G2.Execution.Reducer
, G2.Execution.Rules
, G2.Execution.RuleTypes
, G2.Initialization.Interface
, G2.Initialization.DeepSeqWalks
, G2.Initialization.ElimTicks
, G2.Initialization.ElimTypeSynonyms
, G2.Initialization.InitVarLocs
, G2.Initialization.KnownValues
, G2.Initialization.MkCurrExpr
, G2.Initialization.Types
, G2.Interface
, G2.Interface.Interface
, G2.Interface.OutputTypes
, G2.Language
, G2.Language.AlgDataTy
, G2.Language.Approximation
, G2.Language.ArbValueGen
, G2.Language.AST
, G2.Language.CallGraph
, G2.Language.Casts
, G2.Language.CreateFuncs
, G2.Language.Expr
, G2.Language.ExprEnv
, G2.Language.Ids
, G2.Language.KnownValues
, G2.Language.Located
, G2.Language.Monad
, G2.Language.Monad.AST
, G2.Language.Monad.CreateFuncs
, G2.Language.Monad.Expr
, G2.Language.Monad.ExprEnv
, G2.Language.Monad.Naming
, G2.Language.Monad.Primitives
, G2.Language.Monad.Support
, G2.Language.Monad.TypeClasses
, G2.Language.Monad.TypeEnv
, G2.Language.Monad.Typing
, G2.Language.Naming
, G2.Language.PathConds
, G2.Language.Primitives
, G2.Language.Simplification
, G2.Language.Stack
, G2.Language.Support
, G2.Language.Syntax
, G2.Language.TypeClasses
, G2.Language.TypeClasses.Extra
, G2.Language.TypeClasses.TypeClasses
, G2.Language.TypeEnv
, G2.Language.Typing
, G2.Lib.Printers
, G2.Nebula
, G2.Postprocessing.Interface
, G2.Preprocessing.AdjustTypes
, G2.Preprocessing.Interface
, G2.Preprocessing.NameCleaner
, G2.Postprocessing.NameSwitcher
, G2.Solver
, G2.Solver.ADTNumericalSolver
, G2.Solver.Converters
, G2.Solver.Interface
, G2.Solver.Language
, G2.Solver.Maximize
, G2.Solver.ParseSMT
, G2.Solver.Simplifier
, G2.Solver.SMT2
, G2.Solver.Solver
, G2.QuasiQuotes.Internals.G2Rep
, G2.QuasiQuotes.FloodConsts
, G2.QuasiQuotes.G2Rep
, G2.QuasiQuotes.Parser
, G2.QuasiQuotes.QuasiQuotes
, G2.QuasiQuotes.Support
, G2.Translation
, G2.Translation.Cabal.Cabal
, G2.Translation.GHC
, G2.Translation.Haskell
, G2.Translation.HaskellCheck
, G2.Translation.InjectSpecials
, G2.Translation.Interface
, G2.Translation.PrimInject
, G2.Translation.TransTypes
if flag(support-lh) && impl(ghc < 9.2)
exposed-modules:
G2.Liquid.AddCFBranch
, G2.Liquid.AddLHTC
, G2.Liquid.AddOrdToNum
, G2.Liquid.AddTyVars
, G2.Liquid.Annotations
, G2.Liquid.Config
, G2.Liquid.Conversion
, G2.Liquid.ConvertCurrExpr
, G2.Liquid.Helpers
, G2.Liquid.Interface
, G2.Liquid.LHReducers
, G2.Liquid.Measures
, G2.Liquid.MkLHVals
, G2.Liquid.Simplify
, G2.Liquid.SpecialAsserts
, G2.Liquid.TCGen
, G2.Liquid.TCValues
, G2.Liquid.Types
, G2.Liquid.TyVarBags
, G2.Liquid.G2Calls
, G2.Liquid.Inference.Config
, G2.Liquid.Inference.FuncConstraint
, G2.Liquid.Inference.G2Calls
, G2.Liquid.Inference.InfStack
, G2.Liquid.Inference.Initalization
, G2.Liquid.Inference.Interface
, G2.Liquid.Inference.PolyRef
, G2.Liquid.Inference.Sygus.UnsatCoreElim
, G2.Liquid.Inference.Sygus
, G2.Liquid.Inference.Sygus.FCConverter
, G2.Liquid.Inference.Sygus.RefSynth
, G2.Liquid.Inference.Sygus.LiaSynth
, G2.Liquid.Inference.Sygus.SimplifySygus
, G2.Liquid.Inference.Sygus.SpecInfo
, G2.Liquid.Inference.Sygus.Sygus
, G2.Liquid.Inference.UnionPoly
, G2.Liquid.Inference.Verify
, G2.Liquid.Inference.GeneratedSpecs
, G2.Liquid.Inference.QualifGen
build-depends: array >= 0.5.1.1 && <= 0.5.5.0
, Cabal >= 2.0.1.0 && < 3.11
, base >= 4.8 && < 4.19
, bimap == 0.3.3
, bytestring >= 0.10.8.0 && < 0.11.5
, clock >= 0.8 && < 0.9
, concurrent-extra >= 0.7 && < 0.8
, containers >= 0.5 && < 0.7
, directory >= 1.3.0.2 && <= 1.3.8.1
, extra >= 1.6.14 && < 1.7.13
, filepath >= 1.4 && <= 1.5
, ghc-paths >= 0.1 && < 0.2
, ghc (>= 8.2.2 && < 8.4) || (>= 8.6 && < 8.7) || (>= 8.10 && < 9.7)
, hashable >= 1.2.6.0 && <= 1.4.2.0
, HTTP >= 4000.3.0 && < 4001.0
, language-sygus >= 0.1.1.3 && < 0.2
, MissingH >= 1.4.0.0 && < 1.7
, mtl >= 2.2 && < 2.4
, random >= 1.1 && < 1.3
, reducers >= 3.12 && < 3.13
, regex-compat >= 0.95 && < 0.96
, regex-base >= 0.93 && < 0.94.0.3
, parsec >= 3.1 && < 3.2
, pretty >= 1.1 && < 1.4
, process >=1.6 && < 1.7
, optparse-applicative >=0.15.0.0 && < 0.18.0.0
, split >= 0.2.3 && < 0.2.4
, tasty-quickcheck >= 0.10.1.1 && < 0.11
, template-haskell >= 2.12.0.0 && <= 2.20.0.0
, temporary-rc >= 1.2 && < 1.3
, text >= 1.2.3.1 && <= 2.1
, text-builder >= 0.6.6.1 && < 0.7
, time >= 1.6 && <= 1.13
, unordered-containers >= 0.2.10.0 && < 0.3
-- remove this eventually
, deferred-folds <= 0.9.18.3
if flag(support-lh) && impl(ghc < 9.2)
build-depends: liquidhaskell >= 0.8.10.2 && <= 0.9.0.2.1
, liquid-fixpoint >= 0.8.10.2 && < 0.10
, Diff == 0.3.4
if flag(support-lh) && impl(ghc < 9)
build-depends: liquidhaskell == 0.8.10.2
, liquid-fixpoint == 0.8.10.2
default-language: Haskell2010
ghc-options: -Wall
-- -O1
-fno-ignore-asserts
-- -ddump-rule-rewrites
-- -ddump-splices
-- -fexternal-interpreter
-- ghc-prof-options: -fprof-auto
other-extensions: CPP
if flag(support-lh) && impl(ghc < 9)
cpp-options: -DSUPPORT_LH
hs-source-dirs: src
executable G2
-- other-modules:
-- other-extensions:
build-depends: g2
, base >= 4.8 && < 5
, containers
, filepath >= 1.4 && <= 1.5
, ghc
, text
, unordered-containers >= 0.2 && < 0.3
default-language: Haskell2010
ghc-options: -threaded -Wall
-- -fexternal-interpreter -opti+RTS -opti-p
-- ghc-prof-options: -fprof-auto "-with-rtsopts=-p"
hs-source-dirs: exe
main-is: Main.hs
executable G2LH
if flag(support-lh) && impl(ghc < 9.2)
buildable: True
else
buildable: False
-- other-modules:
-- other-extensions:
build-depends: g2
, base >= 4.8 && < 5
, containers
, filepath >= 1.4 && <= 1.5
, ghc
, text
, unordered-containers >= 0.2 && < 0.3
default-language: Haskell2010
ghc-options: -threaded -Wall
-- -fprof-auto "-with-rtsopts=-p"
-- -fexternal-interpreter -opti+RTS -opti-p
-- ghc-prof-options: -fprof-auto "-with-rtsopts=-p"
hs-source-dirs: lh
main-is: Main.hs
executable Inference
if flag(support-lh) && impl(ghc < 9.2)
buildable: True
else
buildable: False
-- other-modules:
-- other-extensions:
build-depends: g2
, base >= 4.8 && < 5
, containers
, deepseq >= 1.4 && < 2
, liquid-fixpoint
, liquidhaskell
, text
, time
default-language: Haskell2010
ghc-options: -threaded -Wall
-- -O1
-- ghc-prof-options: -fprof-auto "-with-rtsopts=-p"
hs-source-dirs: inference
main-is: Main.hs
executable Nebula
-- other-modules:
-- other-extensions:
build-depends: g2
, base >= 4.8 && < 5
, containers
, filepath >= 1.4 && <= 1.5
, ghc
, text
, unordered-containers >= 0.2 && < 0.3
default-language: Haskell2010
ghc-options: -threaded -Wall
-- ghc-prof-options: -fprof-auto "-with-rtsopts=-p"
hs-source-dirs: nebula
main-is: Main.hs
test-suite test
build-depends: g2
, base >= 4.8 && < 5
, containers
, directory
, filepath
, ghc-paths
, ghc
, hashable
, tagged
, tasty >= 1.0 && < 2.0
, tasty-hunit >= 0.10 && < 0.10.0.3
, tasty-quickcheck
, text
, time
, unordered-containers
default-language: Haskell2010
hs-source-dirs: tests
main-is: Test.hs
other-modules: CaseTest
, DefuncTest
, Expr
, GetNthTest
, HigherOrderMathTest
, InputOutputTest
, PeanoTest
, Reqs
, Simplifications
, TestUtils
, Typing
, UFMapTests
, UnionFindTests
, RewriteVerify.RewriteVerifyTest
ghc-options: -Wall
-threaded
-- ghc-prof-options: -fprof-auto "-with-rtsopts=-p"
type: exitcode-stdio-1.0
test-suite test-lh
if flag(support-lh) && impl(ghc < 9.2)
buildable: True
else
buildable: False
build-depends: g2
, base >= 4.8 && < 5
, containers
, directory
, filepath
, ghc-paths
, ghc
, hashable
, liquidhaskell
, tagged
, tasty >= 1.0 && < 2.0
, tasty-hunit >= 0.10 && < 0.10.0.3
, tasty-quickcheck
, text
, time
, unordered-containers
default-language: Haskell2010
hs-source-dirs: tests_lh, tests
main-is: LHTest.hs
other-modules: GetNthTest
, PeanoTest
, Reqs
, TestUtils
, UnionPoly
ghc-options: -Wall
-threaded
-- ghc-prof-options: -fprof-auto "-with-rtsopts=-p"
type: exitcode-stdio-1.0
test-suite test-g2q
-- other-extensions:
build-depends: g2
, base >= 4.8 && < 5
, tasty >= 1.0 && < 2.0
, tasty-hunit >= 0.10 && < 0.10.0.3
, time
default-language: Haskell2010
ghc-options: -Wall
-- -ddump-splices
-- -fprof-auto "-with-rtsopts=-p"
hs-source-dirs: tests_quasiquote
main-is: Main.hs
other-modules: Arithmetics.Interpreter
, Arithmetics.Test
, DeBruijn.Interpreter
, DeBruijn.Test
, Evaluations
, Lambda.Interpreter
, Lambda.Test
, NQueens.Encoding
, NQueens.Test
, RegEx.RegEx
, RegEx.Test
, Simple.Simple1
, Simple.SimpleTest1
ghc-options: -Wall
-threaded
-- ghc-prof-options: -fprof-auto "-with-rtsopts=-p"
type: exitcode-stdio-1.0
test-suite test-nebula-plugin
build-depends: base >= 4.8 && < 5
, process
, tasty >= 1.0 && < 2.0
, tasty-hunit >= 0.10 && < 0.10.0.3
default-language: Haskell2010
hs-source-dirs: tests_nebula_plugin
main-is: Main.hs
-- other-modules:
ghc-options: -Wall
-threaded
-- ghc-prof-options: -fprof-auto "-with-rtsopts=-p"
type: exitcode-stdio-1.0