Camfort.Specification.Hoare.CheckFrontend

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]

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

type HoareAnalysis = AnalysisT HoareFrontendError HoareFrontendWarning IO

data HoareFrontendError

Constructors

ParseError (SpecParseError HoareParseError)

InvalidPUConditions ProgramUnitName [SpecOrDecl InnerHA]

BackendError HoareBackendError

Instances

NFData HoareFrontendError

Defined in Camfort.Specification.Hoare.CheckFrontend

Methods

rnf :: HoareFrontendError -> ()

Describe HoareFrontendError

Defined in Camfort.Specification.Hoare.CheckFrontend

Methods

describe :: HoareFrontendError -> Text

describeBuilder :: HoareFrontendError -> Builder

data HoareFrontendWarning

Constructors

OrphanDecls ProgramUnitName

Instances

NFData HoareFrontendWarning

Defined in Camfort.Specification.Hoare.CheckFrontend

Methods

rnf :: HoareFrontendWarning -> ()

Describe HoareFrontendWarning

Defined in Camfort.Specification.Hoare.CheckFrontend

Methods

describe :: HoareFrontendWarning -> Text

describeBuilder :: HoareFrontendWarning -> Builder