Module Asllib.SideEffectSource

Sourcetype identifier = string
Sourcemodule TimeFrame : sig ... end
Sourcetype read = {
  1. name : identifier;
  2. time_frame : TimeFrame.t;
  3. immutable : bool;
}
Sourcetype t =
  1. | ReadsLocal of read
    (*

    Reads the local storage element indicated by its argument.

    *)
  2. | WritesLocal of identifier
    (*

    Writes to the local variable indicated by its argument.

    *)
  3. | ReadsGlobal of read
    (*

    Reads the global storage element indicated by its argument.

    *)
  4. | WritesGlobal of identifier
    (*

    Writes to the global variable indicated by its argument.

    *)
  5. | ThrowsException of identifier
    (*

    Throws the exception indicated by its argument.

    *)
  6. | CallsRecursive of identifier
    (*

    Calls the function indicated by its argument. Can only happen in a strongly-connected component of mutually recursive functions.

    *)
  7. | PerformsAssertions
    (*

    Performs an assertion.

    *)
  8. | NonDeterministic
    (*

    Uses a non-deterministic construct such as ARBITRARY: ty.

    *)

Data type describing a potential side effect associated with an ASL piece of code.

Sourcetype side_effect = t
Sourceval equal : t -> t -> bool
Sourceval compare : t -> t -> int
Sourceval pp_print : Format.formatter -> t -> unit
Sourceval time_frame : t -> TimeFrame.t
Sourceval is_pure : t -> bool
Sourceval is_symbolically_evaluable : t -> bool
Sourcemodule SES : sig ... end

The module SES provides an abstraction over a set of side-effects.