package herdtools7

  1. Overview
  2. Docs
type identifier = string
module TimeFrame : sig ... end
type read = {
  1. name : identifier;
  2. time_frame : TimeFrame.t;
  3. immutable : bool;
}
type 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.

type side_effect = t
val equal : t -> t -> bool
val compare : t -> t -> int
val pp_print : Format.formatter -> t -> unit
val time_frame : t -> TimeFrame.t
val is_pure : t -> bool
val is_symbolically_evaluable : t -> bool
module SES : sig ... end

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

OCaml

Innovation. Community. Security.