Module Mlsem_system.Analyzer

type severity =
  1. | Message
  2. | Notice
  3. | Warning
  4. | Error
type msg = {
  1. eid : Mlsem_common.Eid.t;
  2. severity : severity;
  3. title : string;
  4. descr : string option;
}
module Visited : sig ... end

Sub-expressions reached by analyze.

val analyze : Ast.t -> Annot.Annot.t -> msg list * Visited.t

analyze e a reports the notices raised by the annotated expression e, together with the sub-expressions of e that a covers. The annotation must already have been type-checked, since the analysis reads the types cached in it.

  • raises Failure

    if a node of the annotation has no cached type.

val get_unreachable : Visited.t -> Ast.t -> msg list

get_unreachable visited e reports the sub-expressions of e that are not in visited, i.e. that no annotation covers. A same expression may be analyzed under several annotations (typically once per signature of a definition); visited must then be the union of the sets returned by the corresponding calls to analyze, otherwise the parts that only some of them reached are wrongly reported as unreachable.