crux-llvm-0.12: crux-llvm.cabal
Cabal-version: 2.2
Name: crux-llvm
Version: 0.12
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