jon.recoil.org

Module Assume_info.ValueSource

Sourcetype t : immutable_data = Make_value(Witnesses)(V).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.

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

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

Sourceval exn_escape : t

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

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

Sourceval safe : t

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

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

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

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

Sourceval print : witnesses:bool -> Format.formatter -> t -> unit
Sourceval 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.