Cabal revisions of crux-llvm-0.11.0.0
Hackage metadata revisions edit the .cabal file after upload; each diff below is one revision.
revision 1
-Cabal-version: 2.2-Name: crux-llvm-Version: 0.11.0.0-Author: Galois Inc.-Maintainer: rscott@galois.com, kquick@galois.com, langston@galois.com-Copyright: (c) Galois, Inc 2014-2022-License: BSD-3-Clause-License-file: LICENSE-Build-type: Simple-Category: Language-Synopsis: A verification tool for C programs.-Description:- .- This tool (and corresponding C library) are intended for verifying C- programs using verification specifications embedded in the input- source files (i.e. it allows for writing Crucible specifications- by using C as the specification language).- .- This tool provides:- .- * a Haskell library with the core functionality,- .- * a @crux-llvm@ executable used to run the verification when given one- or more C or C++ source files- .- * a set of supplemental C source files, include files, and LLVM- runtime library bitcode files to use for building the input C- files into verifiable LLVM BC files.- .- * a @crux-llvm-svcomp@ executable that is designed to run verification- of challenge inputs for the SV-COMP competition, generating- results tailored to the format that SV-COMP expects.---data-files:- c-src/includes/crucible.h- c-src/includes/crucible-model.h- c-src/concrete-backend.c- c-src/print-model.c- c-src/libcxx-3.6.2.bc- c-src/libcxx-7.1.0.bc-extra-doc-files: CHANGELOG.md, README.md--source-repository head- type: git- location: https://github.com/GaloisInc/crucible- subdir: crux-llvm--common bldflags- ghc-options: -Wall- -Werror=incomplete-patterns- -Werror=missing-methods- -Werror=overlapping-patterns- -Wpartial-fields- -Wincomplete-uni-patterns- ghc-prof-options: -O2- default-language: Haskell2010- build-depends: base >= 4.8 && < 4.21- , bytestring- , containers- , crucible- , crucible-symio- , crucible-llvm- , crux- , directory- , filepath- , lens- , process- , text- , what4--common warns- -- Specifying -Wall and -Werror can cause the project to fail to build on- -- newer versions of GHC simply due to new warnings being added to -Wall. To- -- prevent this from happening we manually list which warnings should be- -- considered errors. We also list some warnings that are not in -Wall, though- -- try to avoid "opinionated" warnings (though this judgement is clearly- -- subjective).- --- -- Warnings are grouped by the GHC version that introduced them, and then- -- alphabetically.- --- -- A list of warnings and the GHC version in which they were introduced is- -- available here:- -- https://ghc.gitlab.haskell.org/ghc/doc/users_guide/using-warnings.html-- -- Since GHC 9.6 or earlier:- ghc-options:- -Wall- -Werror=ambiguous-fields- -Werror=compat-unqualified-imports- -Werror=deferred-type-errors- -Werror=deprecated-flags- -Werror=deprecations- -Werror=deriving-defaults- -Werror=deriving-typeable- -Werror=dodgy-foreign-imports- -Werror=duplicate-exports- -Werror=empty-enumerations- -Werror=gadt-mono-local-binds- -Werror=identities- -Werror=inaccessible-code- -Werror=incomplete-patterns- -Werror=incomplete-record-updates- -Werror=incomplete-uni-patterns- -Werror=inline-rule-shadowing- -Werror=misplaced-pragmas- -Werror=missed-extra-shared-lib- -Werror=missing-exported-signatures- -Werror=missing-fields- -Werror=missing-home-modules- -Werror=missing-methods- -Werror=missing-pattern-synonym-signatures- -Werror=missing-signatures- -Werror=name-shadowing- -Werror=noncanonical-monad-instances- -Werror=noncanonical-monoid-instances- -Werror=operator-whitespace- -Werror=operator-whitespace-ext-conflict- -Werror=orphans- -Werror=overflowed-literals- -Werror=overlapping-patterns- -Werror=partial-fields- -Werror=partial-type-signatures- -Werror=redundant-bang-patterns- -Werror=redundant-record-wildcards- -Werror=redundant-strictness-flags- -Werror=simplifiable-class-constraints- -Werror=star-binder- -Werror=star-is-type- -Werror=tabs- -Werror=type-defaults- -Werror=typed-holes- -Werror=type-equality-out-of-scope- -Werror=type-equality-requires-operators- -Werror=unicode-bidirectional-format-characters- -Werror=unrecognised-pragmas- -Werror=unrecognised-warning-flags- -Werror=unsupported-calling-conventions- -Werror=unsupported-llvm-version- -Werror=unused-do-bind- -Werror=unused-imports- -Werror=unused-record-wildcards- -Werror=warnings-deprecations- -Werror=wrong-do-bind-- if impl(ghc < 9.8)- ghc-options:- -Werror=forall-identifier-- if impl(ghc >= 9.8)- ghc-options:- -Werror=incomplete-export-warnings- -Werror=inconsistent-flags-- if impl(ghc >= 9.10)- ghc-options:- -Werror=badly-staged-types- -Werror=data-kinds-tc- -Werror=deprecated-type-abstractions- -Werror=incomplete-record-selectors--common testdefs- build-depends: tasty >= 0.10- , tasty-hunit >= 0.10- , tasty-sugar >= 2.2 && < 2.3---library- import: bldflags- hs-source-dirs: src-- exposed-modules:- CruxLLVMMain- Crux.LLVM.Compile- Crux.LLVM.Config- Crux.LLVM.Log- Crux.LLVM.Overrides- Crux.LLVM.Simulate- Paths_crux_llvm-- autogen-modules:- Paths_crux_llvm-- build-depends:- aeson,- bv-sized,- config-schema >= 1.2.2.0,- crucible-debug,- logict,- llvm-pretty,- llvm-pretty-bc-parser >= 0.5,- mtl,- parameterized-utils,- prettyprinter >= 1.7.0---executable crux-llvm- import: bldflags-- hs-source-dirs: exe-- build-depends:- crux-llvm-- main-is: Main.hs-- if os(windows)- hs-source-dirs: exe/windows- else- hs-source-dirs: exe/unix- build-depends: unix-- other-modules: RealMain---executable crux-llvm-for-ide- import: bldflags-- hs-source-dirs: for-ide-- build-depends:- aeson,- crux-llvm,- lumberjack,- websockets >= 0.12-- main-is: Main.hs-- if os(windows)- hs-source-dirs: for-ide/windows- else- hs-source-dirs: for-ide/unix- build-depends: unix-- other-modules:- Paths_crux_llvm- RealMain-- autogen-modules:- Paths_crux_llvm---executable crux-llvm-svcomp- import: bldflags- hs-source-dirs: svcomp- main-is: Main.hs-- build-depends:- aeson,- attoparsec,- base16-bytestring,- crux-llvm,- cryptohash-sha256,- extra,- indexed-traversable,- time-- other-modules:- SVComp.Log- Paths_crux_llvm-- autogen-modules:- Paths_crux_llvm---test-suite crux-llvm-test- import: bldflags, testdefs- import: warns- type: exitcode-stdio-1.0- hs-source-dirs: test-- main-is: Test.hs-- build-depends:- crux-llvm,- extra,- regex-base,- regex-posix,- versions+Cabal-version: 2.2 +Name: crux-llvm +Version: 0.11.0.0 +x-revision: 1 +Author: Galois Inc. +Maintainer: rscott@galois.com, kquick@galois.com, langston@galois.com +Copyright: (c) Galois, Inc 2014-2022 +License: BSD-3-Clause +License-file: LICENSE +Build-type: Simple +Category: Language +Synopsis: A verification tool for C programs. +Description: + . + This tool (and corresponding C library) are intended for verifying C + programs using verification specifications embedded in the input + source files (i.e. it allows for writing Crucible specifications + by using C as the specification language). + . + This tool provides: + . + * a Haskell library with the core functionality, + . + * a @crux-llvm@ executable used to run the verification when given one + or more C or C++ source files + . + * a set of supplemental C source files, include files, and LLVM + runtime library bitcode files to use for building the input C + files into verifiable LLVM BC files. + . + * a @crux-llvm-svcomp@ executable that is designed to run verification + of challenge inputs for the SV-COMP competition, generating + results tailored to the format that SV-COMP expects. + + +data-files: + c-src/includes/crucible.h + c-src/includes/crucible-model.h + c-src/concrete-backend.c + c-src/print-model.c + c-src/libcxx-3.6.2.bc + c-src/libcxx-7.1.0.bc +extra-doc-files: CHANGELOG.md, README.md + +source-repository head + type: git + location: https://github.com/GaloisInc/crucible + subdir: crux-llvm + +common bldflags + ghc-options: -Wall + -Werror=incomplete-patterns + -Werror=missing-methods + -Werror=overlapping-patterns + -Wpartial-fields + -Wincomplete-uni-patterns + ghc-prof-options: -O2 + default-language: Haskell2010 + build-depends: base >= 4.8 && < 4.21 + , bytestring + , containers + , crucible + , crucible-symio + , crucible-llvm + , crux == 0.8.* + , directory + , filepath + , lens + , process + , text + , what4 + +common warns + -- Specifying -Wall and -Werror can cause the project to fail to build on + -- newer versions of GHC simply due to new warnings being added to -Wall. To + -- prevent this from happening we manually list which warnings should be + -- considered errors. We also list some warnings that are not in -Wall, though + -- try to avoid "opinionated" warnings (though this judgement is clearly + -- subjective). + -- + -- Warnings are grouped by the GHC version that introduced them, and then + -- alphabetically. + -- + -- A list of warnings and the GHC version in which they were introduced is + -- available here: + -- https://ghc.gitlab.haskell.org/ghc/doc/users_guide/using-warnings.html + + -- Since GHC 9.6 or earlier: + ghc-options: + -Wall + -Werror=ambiguous-fields + -Werror=compat-unqualified-imports + -Werror=deferred-type-errors + -Werror=deprecated-flags + -Werror=deprecations + -Werror=deriving-defaults + -Werror=deriving-typeable + -Werror=dodgy-foreign-imports + -Werror=duplicate-exports + -Werror=empty-enumerations + -Werror=gadt-mono-local-binds + -Werror=identities + -Werror=inaccessible-code + -Werror=incomplete-patterns + -Werror=incomplete-record-updates + -Werror=incomplete-uni-patterns + -Werror=inline-rule-shadowing + -Werror=misplaced-pragmas + -Werror=missed-extra-shared-lib + -Werror=missing-exported-signatures + -Werror=missing-fields + -Werror=missing-home-modules + -Werror=missing-methods + -Werror=missing-pattern-synonym-signatures + -Werror=missing-signatures + -Werror=name-shadowing + -Werror=noncanonical-monad-instances + -Werror=noncanonical-monoid-instances + -Werror=operator-whitespace + -Werror=operator-whitespace-ext-conflict + -Werror=orphans + -Werror=overflowed-literals + -Werror=overlapping-patterns + -Werror=partial-fields + -Werror=partial-type-signatures + -Werror=redundant-bang-patterns + -Werror=redundant-record-wildcards + -Werror=redundant-strictness-flags + -Werror=simplifiable-class-constraints + -Werror=star-binder + -Werror=star-is-type + -Werror=tabs + -Werror=type-defaults + -Werror=typed-holes + -Werror=type-equality-out-of-scope + -Werror=type-equality-requires-operators + -Werror=unicode-bidirectional-format-characters + -Werror=unrecognised-pragmas + -Werror=unrecognised-warning-flags + -Werror=unsupported-calling-conventions + -Werror=unsupported-llvm-version + -Werror=unused-do-bind + -Werror=unused-imports + -Werror=unused-record-wildcards + -Werror=warnings-deprecations + -Werror=wrong-do-bind + + if impl(ghc < 9.8) + ghc-options: + -Werror=forall-identifier + + if impl(ghc >= 9.8) + ghc-options: + -Werror=incomplete-export-warnings + -Werror=inconsistent-flags + + if impl(ghc >= 9.10) + ghc-options: + -Werror=badly-staged-types + -Werror=data-kinds-tc + -Werror=deprecated-type-abstractions + -Werror=incomplete-record-selectors + +common testdefs + build-depends: tasty >= 0.10 + , tasty-hunit >= 0.10 + , tasty-sugar >= 2.2 && < 2.3 + + +library + import: bldflags + hs-source-dirs: src + + exposed-modules: + CruxLLVMMain + Crux.LLVM.Compile + Crux.LLVM.Config + Crux.LLVM.Log + Crux.LLVM.Overrides + Crux.LLVM.Simulate + Paths_crux_llvm + + autogen-modules: + Paths_crux_llvm + + build-depends: + aeson, + bv-sized, + config-schema >= 1.2.2.0, + crucible-debug, + logict, + llvm-pretty, + llvm-pretty-bc-parser >= 0.5, + mtl, + parameterized-utils, + prettyprinter >= 1.7.0 + + +executable crux-llvm + import: bldflags + + hs-source-dirs: exe + + build-depends: + crux-llvm + + main-is: Main.hs + + if os(windows) + hs-source-dirs: exe/windows + else + hs-source-dirs: exe/unix + build-depends: unix + + other-modules: RealMain + + +executable crux-llvm-for-ide + import: bldflags + + hs-source-dirs: for-ide + + build-depends: + aeson, + crux-llvm, + lumberjack, + websockets >= 0.12 + + main-is: Main.hs + + if os(windows) + hs-source-dirs: for-ide/windows + else + hs-source-dirs: for-ide/unix + build-depends: unix + + other-modules: + Paths_crux_llvm + RealMain + + autogen-modules: + Paths_crux_llvm + + +executable crux-llvm-svcomp + import: bldflags + hs-source-dirs: svcomp + main-is: Main.hs + + build-depends: + aeson, + attoparsec, + base16-bytestring, + crux-llvm, + cryptohash-sha256, + extra, + indexed-traversable, + time + + other-modules: + SVComp.Log + Paths_crux_llvm + + autogen-modules: + Paths_crux_llvm + + +test-suite crux-llvm-test + import: bldflags, testdefs + import: warns + type: exitcode-stdio-1.0 + hs-source-dirs: test + + main-is: Test.hs + + build-depends: + crux-llvm, + extra, + regex-base, + regex-posix, + versions