Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
This module is responsible for finding annotated program units, and running the functionality in Camfort.Specification.Hoare.CheckBackend on each of them.
Invariant Checking
invariantChecking :: PrimReprSpec -> ProgramFile HA -> HoareAnalysis [HoareCheckResult] Source #
Runs invariant checking on every annotated program unit in the given program file. Expects the program file to have basic block and unique analysis information.
The PrimReprSpec
argument controls how Fortran data types are treated
symbolically. See the documentation in Language.Fortran.Mode.Repr.Prim for a
detailed explanation.
Analysis Types
data HoareFrontendError Source #
ParseError (SpecParseError HoareParseError) | |
InvalidPUConditions ProgramUnitName [SpecOrDecl InnerHA] | |
BackendError HoareBackendError |
Instances
Describe HoareFrontendError Source # | |
Defined in Camfort.Specification.Hoare.CheckFrontend | |
NFData HoareFrontendError Source # | |
Defined in Camfort.Specification.Hoare.CheckFrontend rnf :: HoareFrontendError -> () # |
data HoareFrontendWarning Source #