module Cil2cfg:sig
..end
Build a CFG of a function keeping some information of the initial structure.
type
t
abstract type of a cfg
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
abstract type of the cfg nodes
val pp_node : Stdlib.Format.formatter -> node -> unit
val same_node : node -> node -> bool
type
edge
abstract type of the cfg edges
val pp_edge : Stdlib.Format.formatter -> edge -> unit
val same_edge : edge -> edge -> bool
val start_edge : t -> edge
get the starting edges
module Eset:FCSet.S
with type elt = edge
set of edges
val edge_src : edge -> node
node and edges relations
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
iterators
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
Be careful that only Bstmt are real Block statements
type
call_type =
| |
Dynamic of |
| |
Static of |
val pp_call_type : Stdlib.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 : Stdlib.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
similar to 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
Invalid_argument
if the node is not a test.val get_switch_edges : t ->
node -> (Cil_types.exp list * edge) list * edge
similar to succ_e g v
but give the switch cases and the default edge
val get_call_out_edges : t -> node -> edge * edge
similar to 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
detect is there are non natural loops or natural loops where we didn't
manage to compute back edges (see mark_loops
). Must be empty in the mode
-wp-no-invariants
. (see also very_strange_loops
)
val very_strange_loops : t -> node list
detect is there are natural loops where we didn't manage to compute
back edges (see 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_stmt : edge -> Cil_types.stmt option
Complete get_edge_labels and returns the associated stmt, if any.
val get_edge_next_stmt : t -> edge -> Cil_types.stmt option
val has_exit : t -> bool
whether an exit edge exists or not
val get_pre_edges : t -> node -> edge list
Find the edges where the precondition of the node statement have to be checked.
val get_post_edges : t -> node -> edge list
Find the edges where the postconditions of the node statement have to be checked.
val get_post_label : t -> node -> Clabels.c_label option
Get the label to be used for the Post state of the node contract if any.
val get_exit_edges : t -> node -> edge list
Find the edges e
that goes to the Vexit
node inside the statement
beginning at node n
val get_internal_edges : t -> node -> edge list * Eset.t
Find the edges 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
returns true
is this CFG is degenerated (no code available)
module type HEsig =sig
..end
signature of a mapping table from cfg edges to some information.
module HE: