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