Previous  Up  Next

Module Cil2cfg

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
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: 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 : Stdlib.Format.formatter -> call_type -> unit
val get_call_type : Cil_types.exp -> call_type
type node_type = private
| Vstart
| Vend
| VfctIn
| VfctOut
| VfctErr
| 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 : 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

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
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: 
functor (I : sig
type t 
end) -> HEsig  with type ti = I.t
module Dump: sig .. end