Module Cil2cfg

module Cil2cfg: sig .. end
abstract type of a cfg

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
Raises Log.FeatureRequest for non natural loops and 'exception' stmts.
Returns the graph and the list of unreachable nodes.
type node 
abstract type of the cfg nodes
val pp_node : Format.formatter -> node -> unit
val same_node : node -> node -> bool
type edge 
abstract type of the cfg edges
val pp_edge : Format.formatter -> edge -> unit
val same_edge : edge -> edge -> bool
val start_edge : t -> edge
get the starting edges
module Eset: Set.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 Cil_types.stmt
| Bthen of Cil_types.stmt
| Belse of Cil_types.stmt
| Bloop of Cil_types.stmt
| Bfct
Be careful that only Bstmt are real Block statements

Be careful that only Bstmt are real Block statements

type call_type = 
| Dynamic of Cil_types.exp
| Static of Cil_types.kernel_function
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 block_type * Cil_types.block
| VblkOut of block_type * Cil_types.block
| Vstmt of Cil_types.stmt
| Vcall of Cil_types.stmt * Cil_types.lval option * call_type
* Cil_types.exp list
| Vtest of bool * Cil_types.stmt * Cil_types.exp (*
bool=true for In and false for Out
*)
| Vswitch of Cil_types.stmt * Cil_types.exp
| Vloop of bool option * Cil_types.stmt (*
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 bool * int
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
Returns the nodes that are unreachable from the 'start' node. These nodes have been removed from the cfg already.
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
Raises 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.
type block_scope = {
   b_opened : Cil_types.block list;
   b_closed : Cil_types.block list;
}
val block_scope_for_edge : t -> edge -> block_scope
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
Returns the (normalized) labels at the program point of the edge.
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
Returns None when the edge leads to the end of the function.
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: 
functor (I : sig
type t 
end-> HEsig  with type ti = I.t