module Cil2cfg:sig
..end
Build a CFG of a function keeping some information of the initial structure.
type
t
The final CFG is composed of the graph, but also :
the function that it represents,
an hashtable to find a CFG node knowing its hashcode
val get : Kernel_function.t -> t
Log.FeatureRequest
for non natural loops and 'exception' stmts.type
node
val pp_node : Format.formatter -> node -> unit
val same_node : node -> node -> bool
type
edge
val pp_edge : Format.formatter -> edge -> unit
val same_edge : edge -> edge -> bool
val start_edge : t -> edge
module Eset:FCSet.S
with type elt = edge
val edge_src : edge -> node
val edge_dst : edge -> node
val pred_e : t -> node -> edge list
val succ_e : t -> node -> edge list
val fold_nodes : (node -> 'a -> 'a) -> t -> 'a -> 'a
val iter_nodes : (node -> unit) -> t -> unit
val iter_edges : (edge -> unit) -> t -> unit
type
block_type = private
| |
Bstmt of |
| |
Bthen of |
| |
Belse of |
| |
Bloop of |
| |
Bfct |
Be careful that only Bstmt are real Block statements
type
call_type =
| |
Dynamic of |
| |
Static of |
val pp_call_type : Format.formatter -> call_type -> unit
val get_call_type : Cil_types.exp -> call_type
type
node_type = private
| |
Vstart |
|||
| |
Vend |
|||
| |
Vexit |
|||
| |
VfctIn |
|||
| |
VfctOut |
|||
| |
VblkIn of |
|||
| |
VblkOut of |
|||
| |
Vstmt of |
|||
| |
Vcall of |
|||
| |
Vtest of |
(* |
bool=true for In and false for Out
| *) |
| |
Vswitch of |
|||
| |
Vloop of |
(* |
boolean is is_natural. None means the node has not been
detected as a loop.
boolean is is_natural. None means the node has not been detected
as a loop | *) |
| |
Vloop2 of |
val node_type : node -> node_type
val pp_node_type : Format.formatter -> node_type -> unit
val node_stmt_opt : node -> Cil_types.stmt option
val start_stmt_of_node : node -> Cil_types.stmt option
val unreachable_nodes : t -> node_type list
val get_test_edges : t -> node -> edge * edge
succ_e g v
but tests the branch to return (then-edge, else-edge)
Get the edges going out a test node with the then branch first
Raises Invalid_argument
if the node is not a test.
val get_switch_edges : t ->
node -> (Cil_types.exp list * edge) list * edge
succ_e g v
but give the switch cases and the default edgeval get_call_out_edges : t -> node -> edge * edge
succ_e g v
but gives the edge to VcallOut first and the edge to Vexit second.val blocks_closed_by_edge : t -> edge -> Cil_types.block list
val is_back_edge : edge -> bool
val strange_loops : t -> node list
mark_loops
). Must be empty in the mode
-wp-no-invariants
. (see also very_strange_loops
)val very_strange_loops : t -> node list
mark_loops
). At the moment, we are not able to handle those
loops.val get_edge_labels : edge -> Clabels.c_label list
val get_edge_next_stmt : t -> edge -> Cil_types.stmt option
val has_exit : t -> bool
val get_pre_edges : t -> node -> edge list
val get_post_edges : t -> node -> edge list
val get_post_logic_label : t -> node -> Cil_types.logic_label option
val get_exit_edges : t -> node -> edge list
e
that goes to the Vexit
node inside the statement
beginning at node n
val get_internal_edges : t -> node -> edge list * Eset.t
e
of the statement node n
postcondition
and the set of edges that are inside the statement (e
excluded).
For instance, for a single statement node, e
is succ_e n
,
and the set is empty. For a test node, e
are the last edges of the 2
branches, and the set contains all the edges between n
and the e
edges.
val cfg_kf : t -> Kernel_function.t
val cfg_spec_only : t -> bool
true
is this CFG is degenerated (no code available)module type HEsig =sig
..end
module HE: