-- Initial G2.cabal generated by cabal init. For further documentation, -- see http://haskell.org/cabal/users-guide/ name: g2 version: 0.2.0.0 x-revision: 1 synopsis: Haskell symbolic execution engine. description: A Haskell symbolic execution engine. For details, please see: 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.6 , 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