Module Zero_alloc_utils.Make_value

Parameters

module Witnesses : WS
module V : Component with type witnesses := Witnesses.t

Signature

type t = {
  1. nor : V.t;
    (*

    Property about all paths from this program location that may reach a Normal Return

    *)
  2. exn : V.t;
    (*

    Property about all paths from this program point that may reach a Return with Exception

    *)
  3. div : V.t;
    (*

    Property about all paths from this program point that may diverge.

    *)
}

Abstract value associated with each program location in a function.

val lessequal : t -> t -> bool
val join : t -> t -> t
val meet : t -> t -> t
val top : Witnesses.t -> t
val bot : t
val normal_return : t

normal_return means property holds on paths to normal return, exceptional return is not reachable and execution will not diverge.

val exn_escape : t

exn_escape means the property holds on paths to exceptional return, normal return is not reachable and execution will not diverge.

val diverges : t

diverges means the execution may diverge without violating the property, but normal and exceptional return are not reachable (i.e., div is Safe, `nor` and `exn` are Bot).

val safe : t

safe means the property holds on all paths (i.e., all three components are set to Safe).

val relaxed : Witnesses.t -> t

relaxed means the property holds on paths that lead to normal returns only (i.e., nor component is Safe, others are Top.

val of_annotation : strict:bool -> never_returns_normally:bool -> never_raises:bool -> t

Constructs a value from a user annotation. The witness will be empty.

val print : witnesses:bool -> Format.formatter -> t -> unit
val compare : t -> t -> int

Use compare for structural comparison of terms, for example to store them in a set. Use lessequal for checking fixed point of the abstract domain.

compare must be consistent with lessthan order of the abstract domain, i.e., if compare t1 t2 <= 0 then lessequal v1 v2 = true.

compare may distinguish terms that are equivalent w.r.t. the abstraction, i.e., lessequal v1 v2 = true does not always imply compare t1 t2 <= 0. In particular, compare distinguishes between two "Top" values with different witnesses.