| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Camfort.Specification.Hoare.CheckFrontend
Contents
Description
This module is responsible for finding annotated program units, and running the functionality in Camfort.Specification.Hoare.CheckBackend on each of them.
Synopsis
- invariantChecking :: PrimReprSpec -> ProgramFile HA -> HoareAnalysis [HoareCheckResult]
- type HoareAnalysis = AnalysisT HoareFrontendError HoareFrontendWarning IO
- data HoareFrontendError
- = ParseError (SpecParseError HoareParseError)
- | InvalidPUConditions ProgramUnitName [SpecOrDecl InnerHA]
- | BackendError HoareBackendError
- data HoareFrontendWarning = OrphanDecls ProgramUnitName
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 #
Constructors
| ParseError (SpecParseError HoareParseError) | |
| InvalidPUConditions ProgramUnitName [SpecOrDecl InnerHA] | |
| BackendError HoareBackendError |
Instances
| NFData HoareFrontendError Source # | |
Defined in Camfort.Specification.Hoare.CheckFrontend Methods rnf :: HoareFrontendError -> () # | |
| Describe HoareFrontendError Source # | |
Defined in Camfort.Specification.Hoare.CheckFrontend Methods describe :: HoareFrontendError -> Text Source # | |
data HoareFrontendWarning Source #
Constructors
| OrphanDecls ProgramUnitName |
Instances
| NFData HoareFrontendWarning Source # | |
Defined in Camfort.Specification.Hoare.CheckFrontend Methods rnf :: HoareFrontendWarning -> () # | |
| Describe HoareFrontendWarning Source # | |
Defined in Camfort.Specification.Hoare.CheckFrontend Methods describe :: HoareFrontendWarning -> Text Source # | |