Module ErlangFrontend.ErlangBlock

module Env = ErlangEnvironment
type t = {
  1. start : IR.Procdesc.Node.t;
  2. exit_success : IR.Procdesc.Node.t;
  3. exit_failure : IR.Procdesc.Node.t;
}
val (|~~>) : IR.Procdesc.Node.t -> IR.Procdesc.Node.t list -> unit
val make_success : (IR.Procdesc.t Env.present, _) Env.t -> t

Two nodes: start=exit_success, and exit_failure is distinct.

val make_stuck : (IR.Procdesc.t Env.present, _) Env.t -> t

Like make_success, but start/exit_success contains "prune false".

val make_fail : (IR.Procdesc.t Env.present, _) Env.t -> IR.Procname.t -> t

Like make_success, but start/exit_success calls the given function. The name is "fail" because the given function is supposed to be later (e.g., in Pulse) modeled by a crash.

val all : (IR.Procdesc.t Env.present, _) Env.t -> t list -> t

Chain a list of blocks together in a conjunctive style: a failure in any block leads to a global failure, and successes lead to the next block.

val any : (IR.Procdesc.t Env.present, _) Env.t -> t list -> t

Chain a list of blocks together in a disjunctive style: a success in any block leads to a global success, and failures lead to the next block.

val make_instruction : (IR.Procdesc.t Env.present, _) Env.t -> ?kind:IR.Procdesc.Node.stmt_nodekind -> IR.Sil.instr list -> t
val make_load : (IR.Procdesc.t Env.present, _) Env.t -> IR.Ident.t -> IR.Exp.t -> IR.Typ.t -> t
val make_branch : (IR.Procdesc.t Env.present, _) Env.t -> IR.Exp.t -> t

Make a branch based on the condition: go to success if true, go to failure if false