Module Linter.Annotation

type 'domain annotation =
  1. | Empty
  2. | Annotation of 'domain

Annotation type. Used to wrap domain with a minimal Empty value.

val pp : (Format.formatter -> (Jasmin.Location.i_loc * 'domain) -> unit) -> Format.formatter -> (Jasmin.Location.i_loc * 'domain annotation) -> unit

Pretty printer wraper function for the annotation type following Jasmin.Printer.pp_iprog interface.

val merge : 'domain annotation -> 'domain annotation -> ('domain -> 'domain -> 'domain) -> 'domain annotation

Wrapper for domain merge functions. merge a Empty f

val included : 'domain annotation -> 'domain annotation -> ('domain -> 'domain -> bool) -> bool

Inclusion test for annotations. included a b f return :

  • true if a is Empty
  • false if b is Empty and a is not Empty
  • true if inner domain a is included in inner domain b according to the function f otherwise
val bind : 'domain annotation -> ('domain -> 'domain annotation) -> 'domain annotation

bind a f applies the function f to the value contained in the annotation a and return a new annotation. If a is Empty, it returns Empty.

val unwrap : 'domain annotation -> 'domain

Unwrapping function for annotation. It should only be used on annotations that are not Empty. It will otherwise raise an Invalid_argument exception.

val map : 'a annotation -> ('a -> 'b) -> 'b annotation

map a f applies the function f to the value contained in the annotation a. If a is Empty, it returns Empty.