ErlangBlock (infer.ErlangFrontend.ErlangBlock)

module Env = ErlangEnvironment

type t = {

start : IR.Procdesc.Node.t;
exit_success : IR.Procdesc.Node.t;
exit_failure : IR.Procdesc.Node.t option;

}

val (|~~>) : IR.Procdesc.Node.t -> IR.Procdesc.Node.t list -> unit

val (|?~>) : IR.Procdesc.Node.t option -> 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 ->
  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.Sil.instr list ->
  IR.Exp.t ->
  t

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

val join_failures : 
  (IR.Procdesc.t Env.present, _) Env.t ->
  t list ->
  IR.Procdesc.Node.t option