jon.recoil.org

Module Assume_info.Value

type t = Zero_alloc_utils.Make_value(Zero_alloc_utils.Assume_info.Witnesses)(Zero_alloc_utils.Assume_info.V).t = {
  1. nor : Zero_alloc_utils.Assume_info.V.t;
    (*

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

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

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

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

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

    *)
}

Abstract value associated with each program location in a function.

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

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

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).

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

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 -> Zero_alloc_utils.Assume_info.Value.t

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

val print : witnesses:bool -> Stdlib.Format.formatter -> Zero_alloc_utils.Assume_info.Value.t -> unit

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.