| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Camfort.Specification.Hoare.CheckBackend
Documentation
data AnnotatedProgramUnit Source #
Constructors
| AnnotatedProgramUnit | |
Fields
| |
apuPreconditions :: Lens' AnnotatedProgramUnit [PrimFormula InnerHA] Source #
apuPostconditions :: Lens' AnnotatedProgramUnit [PrimFormula InnerHA] Source #
apuPU :: Lens' AnnotatedProgramUnit (ProgramUnit HA) Source #
apuAuxDecls :: Lens' AnnotatedProgramUnit [AuxDecl InnerHA] Source #
type BackendAnalysis = AnalysisT HoareBackendError HoareBackendWarning IO Source #
data HoareCheckResult Source #
Constructors
| HoareCheckResult (ProgramUnit HA) Bool |
Instances
| Show HoareCheckResult Source # | |
Defined in Camfort.Specification.Hoare.CheckBackend Methods showsPrec :: Int -> HoareCheckResult -> ShowS # show :: HoareCheckResult -> String # showList :: [HoareCheckResult] -> ShowS # | |
| Describe HoareCheckResult Source # | |
Defined in Camfort.Specification.Hoare.CheckBackend Methods describe :: HoareCheckResult -> Text Source # | |
| ExitCodeOfReport HoareCheckResult Source # | |
Defined in Camfort.Specification.Hoare.CheckBackend Methods exitCodeOf :: HoareCheckResult -> Int Source # exitCodeOfSet :: [HoareCheckResult] -> Int Source # | |
data HoareBackendError Source #
Constructors
| VerifierError (VerifierError FortranVar) | |
| TranslateErrorAnn TranslateError | Unit errors come from translating annotation formulae |
| TranslateErrorSrc TranslateError | HA errors come from translating actual source Fortran |
| InvalidSourceName SourceName | A program source name had no unique name |
| UnsupportedBlock (Block HA) | Found a block that we don't know how to deal with |
| UnexpectedBlock (Block HA) | Found a block in an illegal place |
| ArgWithoutDecl NamePair | Found an argument that didn't come with a variable declaration |
| AuxVarConflict Name | An auxiliary variable name conflicted with a program source name |
| AssignVarNotInScope NamePair | The variable was referenced in an assignment but not in scope |
| WrongAssignmentType Text SomeType | Expected array type but got the given type instead |
| NonLValueAssignment | Assigning to an expression that isn't an lvalue |
| UnsupportedAssignment Text | Tried to assign to something that's valid Fortran but unsupported |
| AnnotationError AnnotationError | There was a problem with the annotations |
Instances
| Describe HoareBackendError Source # | |
Defined in Camfort.Specification.Hoare.CheckBackend Methods describe :: HoareBackendError -> Text Source # | |