Documentation

stencilChecking :: NameMap -> ProgramFile (Analysis A) -> [String] Source #

type LogLine = (SrcSpan, String) Source #

type Checker a = WriterT [LogLine] (State ((RegionEnv, Maybe ProgramUnitName), InductionVarMapByASTBlock)) a Source #

parseCommentToAST :: Analysis A -> SrcSpan -> Checker (Analysis A) Source #

updateRegionEnv :: Analysis A -> Checker () Source #

compareInferredToDeclared :: [([Name], Specification)] -> SpecDecls -> Bool Source #

perProgramUnitCheck :: (?nameMap :: NameMap, ?flowsGraph :: FlowsGraph A) => ProgramUnit (Analysis A) -> Checker (ProgramUnit (Analysis A)) Source #

perBlockCheck :: (?nameMap :: NameMap, ?flowsGraph :: FlowsGraph A) => Block (Analysis A) -> Checker (Block (Analysis A)) Source #