pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

[IR] Rearrange the cfg module to make nodes, procd descs, and cfgs independent types.

Browse Source 
Reviewed By: jberdine

Differential Revision: D4118243

fbshipit-source-id: 73c910c
master
Cristiano Calcagno 8 years ago committed by Facebook Github Bot
parent 7c4c40b6b0
commit e933ee958a
21 changed files with 746 additions and 777 deletions
Show Stats Download Patch File Download Diff File

971
infer/src/IR/Cfg.re
View File

File diff suppressed because it is too large Load Diff

310
infer/src/IR/Cfg.rei
Unescape View File

@ -15,125 +15,13 @@ open! Utils;
/** Control Flow Graph for Interprocedural Analysis */ /** Control Flow Graph for Interprocedural Analysis */
/** {2 ADT node and proc_desc} */ /** node of the control flow graph */
type node; let module Node: {
type cfg;
/** Load a cfg from a file */
let load_cfg_from_file: DB.filename => option cfg;
/** Save a cfg into a file, and save a copy of the source files if the boolean is true */
let store_cfg_to_file:
save_sources::bool? => source_file::DB.source_file => DB.filename => cfg => unit;
/** proc description */
let module Procdesc: {
/** proc description */ /** type of nodes */
type t; type t;
/** Compute the distance of each node to the exit node, if not computed already */ /** node id */
let compute_distance_to_exit_node: t => unit;
/** Create a procdesc */
let create: cfg => ProcAttributes.t => t;
/** true if we ran the preanalysis on the CFG associated with [t] */
let did_preanalysis: t => bool;
/** indicate that we have performed preanalysis on the CFG assoociated with [t] */
let signal_did_preanalysis: t => unit;
/** [remove cfg name remove_nodes] remove the procdesc [name]
from the control flow graph [cfg]. */
let remove: cfg => Procname.t => unit;
/** Find the procdesc given the proc name. Return None if not found. */
let find_from_name: cfg => Procname.t => option t;
/** Get the attributes of the procedure. */
let get_attributes: t => ProcAttributes.t;
let get_err_log: t => Errlog.t;
let get_exit_node: t => node;
/** Get flags for the proc desc */
let get_flags: t => proc_flags;
/** Return name and type of formal parameters */
let get_formals: t => list (Mangled.t, Typ.t);
/** Return loc information for the procedure */
let get_loc: t => Location.t;
/** Return name and type of local variables */
let get_locals: t => list (Mangled.t, Typ.t);
/** Return name and type of block's captured variables */
let get_captured: t => list (Mangled.t, Typ.t);
/** Return the visibility attribute */
let get_access: t => PredSymb.access;
let get_nodes: t => list node;
/** Get the procedure's nodes up until the first branching */
let get_slope: t => list node;
/** Get the sliced procedure's nodes up until the first branching */
let get_sliced_slope: t => (node => bool) => list node;
let get_proc_name: t => Procname.t;
/** Return the return type of the procedure and type string */
let get_ret_type: t => Typ.t;
let get_ret_var: t => Pvar.t;
let get_start_node: t => node;
/** Return [true] iff the procedure is defined, and not just declared */
let is_defined: t => bool;
/** Return [true] if the procedure signature has the Java synchronized keyword */
let is_java_synchronized: t => bool;
/** iterate over all the nodes of a procedure */
let iter_nodes: (node => unit) => t => unit;
/** fold over the calls from the procedure: (callee, location) pairs */
let fold_calls: ('a => (Procname.t, Location.t) => 'a) => 'a => t => 'a;
/** iterate over the calls from the procedure: (callee, location) pairs */
let iter_calls: ((Procname.t, Location.t) => unit) => t => unit;
/** iterate over all nodes and their instructions */
let iter_instrs: (node => Sil.instr => unit) => t => unit;
/** fold over all nodes and their instructions */
let fold_instrs: ('a => node => Sil.instr => 'a) => 'a => t => 'a;
/** iterate over all nodes until we reach a branching structure */
let iter_slope: (node => unit) => t => unit;
/** iterate over all calls until we reach a branching structure */
let iter_slope_calls: (Procname.t => unit) => t => unit;
/** iterate between two nodes or until we reach a branching structure */
let iter_slope_range: (node => unit) => node => node => unit;
let set_exit_node: t => node => unit;
/** Set a flag for the proc desc */
let set_flag: t => string => string => unit;
let set_start_node: t => node => unit;
/** append a list of new local variables to the existing list of local variables */
let append_locals: t => list (Mangled.t, Typ.t) => unit;
};
/** node of the control flow graph */
let module Node: {
type t = node; /** type of nodes */
type id = private int; type id = private int;
/** kind of cfg node */ /** kind of cfg node */
@ -154,25 +42,15 @@ let module Node: {
/** kind of Stmt_node for a throw instruction. */ /** kind of Stmt_node for a throw instruction. */
let throw_kind: nodekind; let throw_kind: nodekind;
/** Add declarations for local variables and return variable to the node */
let add_locals_ret_declaration: t => ProcAttributes.t => list (Mangled.t, Typ.t) => unit;
/** Append the instructions to the list of instructions to execute */ /** Append the instructions to the list of instructions to execute */
let append_instrs: t => list Sil.instr => unit; let append_instrs: t => list Sil.instr => unit;
/** Add the instructions at the beginning of the list of instructions to execute */
let prepend_instrs: t => list Sil.instr => unit;
/** Add declarations for local variables and return variable to the node */
let add_locals_ret_declaration: Procdesc.t => t => list (Mangled.t, Typ.t) => unit;
/** Compare two nodes */ /** Compare two nodes */
let compare: t => t => int; let compare: t => t => int;
/** Create a new cfg node with the given location, kind, list of instructions,
and add it to the procdesc. */
let create: Location.t => nodekind => list Sil.instr => Procdesc.t => t;
/** create a new empty cfg */
let create_cfg: unit => cfg;
/** Dump extended instructions for the node */ /** Dump extended instructions for the node */
let d_instrs: sub_instrs::bool => option Sil.instr => t => unit; let d_instrs: sub_instrs::bool => option Sil.instr => t => unit;
@ -182,63 +60,65 @@ let module Node: {
/** Check if two nodes are equal */ /** Check if two nodes are equal */
let equal: t => t => bool; let equal: t => t => bool;
/** Get the distance to the exit node, if it has been computed */ /** Get the list of callee procnames from the node */
let get_distance_to_exit: t => option int; let get_callees: t => list Procname.t;
/** Return a description of the node */ /** Return a description of the node */
let get_description: printenv => t => string; let get_description: printenv => t => string;
/** Get the distance to the exit node, if it has been computed */
let get_distance_to_exit: t => option int;
/** Get the exception nodes from the current node */ /** Get the exception nodes from the current node */
let get_exn: t => list t; let get_exn: t => list t;
/** Get a list of unique nodes until the first branch starting
from a node with subsequent applications of a generator function */
let get_generated_slope: t => (t => list t) => list t;
/** Get the unique id of the node */ /** Get the unique id of the node */
let get_id: t => id; let get_id: t => id;
/** compare node ids */ /** Get the instructions to be executed */
let id_compare: id => id => int; let get_instrs: t => list Sil.instr;
/** Get the source location of the node */ /** Get the kind of the current node */
let get_loc: t => Location.t; let get_kind: t => nodekind;
/** Get the source location of the last instruction in the node */ /** Get the source location of the last instruction in the node */
let get_last_loc: t => Location.t; let get_last_loc: t => Location.t;
/** Get the kind of the current node */ /** Get the source location of the node */
let get_kind: t => nodekind; let get_loc: t => Location.t;
/** Get the predecessor nodes of the current node */ /** Get the predecessor nodes of the current node */
let get_preds: t => list t; let get_preds: t => list t;
/** Get a list of unique nodes until the first branch starting
from a node with subsequent applications of a generator function */
let get_generated_slope: t => (t => list t) => list t;
/** Get the name of the procedure the node belongs to */ /** Get the name of the procedure the node belongs to */
let get_proc_name: t => Procname.t; let get_proc_name: t => Procname.t;
/** Get the instructions to be executed */ /** Get the predecessor nodes of a node where the given predicate evaluates to true */
let get_instrs: t => list Sil.instr; let get_sliced_preds: t => (t => bool) => list t;
/** Get the list of callee procnames from the node */
let get_callees: t => list Procname.t;
/** Get the successor nodes of the current node */
let get_succs: t => list t;
/** Get the successor nodes of a node where the given predicate evaluates to true */ /** Get the successor nodes of a node where the given predicate evaluates to true */
let get_sliced_succs: t => (t => bool) => list t; let get_sliced_succs: t => (t => bool) => list t;
/** Get the predecessor nodes of a node where the given predicate evaluates to true */ /** Get the successor nodes of the current node */
let get_sliced_preds: t => (t => bool) => list t; let get_succs: t => list t;
/** Hash function for nodes */ /** Hash function for nodes */
let hash: t => int; let hash: t => int;
/** compare node ids */
let id_compare: id => id => int;
/** Comparison for node kind */ /** Comparison for node kind */
let kind_compare: nodekind => nodekind => int; let kind_compare: nodekind => nodekind => int;
/** Pretty print the node */ /** Pretty print the node */
let pp: Format.formatter => t => unit; let pp: Format.formatter => t => unit;
/** Pretty print a node id */
let pp_id: Format.formatter => id => unit; let pp_id: Format.formatter => id => unit;
/** Print extended instructions for the node, /** Print extended instructions for the node,
@ -247,12 +127,122 @@ let module Node: {
/** Replace the instructions to be executed. */ /** Replace the instructions to be executed. */
let replace_instrs: t => list Sil.instr => unit; let replace_instrs: t => list Sil.instr => unit;
};
/** procedure description */
let module Procdesc: {
/** proc description */
type t;
/** append a list of new local variables to the existing list of local variables */
let append_locals: t => list (Mangled.t, Typ.t) => unit;
/** Compute the distance of each node to the exit node, if not computed already */
let compute_distance_to_exit_node: t => unit;
/** Create a new cfg node with the given location, kind, list of instructions,
and add it to the procdesc. */
let create_node: t => Location.t => Node.nodekind => list Sil.instr => Node.t;
/** true if we ran the preanalysis on the CFG associated with [t] */
let did_preanalysis: t => bool;
/** fold over the calls from the procedure: (callee, location) pairs */
let fold_calls: ('a => (Procname.t, Location.t) => 'a) => 'a => t => 'a;
/** fold over all nodes and their instructions */
let fold_instrs: ('a => Node.t => Sil.instr => 'a) => 'a => t => 'a;
/** Return the visibility attribute */
let get_access: t => PredSymb.access;
/** Get the attributes of the procedure. */
let get_attributes: t => ProcAttributes.t;
/** Return name and type of block's captured variables */
let get_captured: t => list (Mangled.t, Typ.t);
let get_err_log: t => Errlog.t;
let get_exit_node: t => Node.t;
/** Get flags for the proc desc */
let get_flags: t => proc_flags;
/** Return name and type of formal parameters */
let get_formals: t => list (Mangled.t, Typ.t);
/** Return loc information for the procedure */
let get_loc: t => Location.t;
/** Return name and type of local variables */
let get_locals: t => list (Mangled.t, Typ.t);
let get_nodes: t => list Node.t;
let get_proc_name: t => Procname.t;
/** Return the return type of the procedure and type string */
let get_ret_type: t => Typ.t;
let get_ret_var: t => Pvar.t;
/** Get the sliced procedure's nodes up until the first branching */
let get_sliced_slope: t => (Node.t => bool) => list Node.t;
/** Get the procedure's nodes up until the first branching */
let get_slope: t => list Node.t;
let get_start_node: t => Node.t;
/** Return [true] iff the procedure is defined, and not just declared */
let is_defined: t => bool;
/** Return [true] if the procedure signature has the Java synchronized keyword */
let is_java_synchronized: t => bool;
/** iterate over the calls from the procedure: (callee, location) pairs */
let iter_calls: ((Procname.t, Location.t) => unit) => t => unit;
/** iterate over all nodes and their instructions */
let iter_instrs: (Node.t => Sil.instr => unit) => t => unit;
/** iterate over all the nodes of a procedure */
let iter_nodes: (Node.t => unit) => t => unit;
/** iterate over all nodes until we reach a branching structure */
let iter_slope: (Node.t => unit) => t => unit;
/** iterate over all calls until we reach a branching structure */
let iter_slope_calls: (Procname.t => unit) => t => unit;
/** iterate between two nodes or until we reach a branching structure */
let iter_slope_range: (Node.t => unit) => Node.t => Node.t => unit;
/** Set the successor nodes and exception nodes, and build predecessor links */ /** Set the successor nodes and exception nodes, and build predecessor links */
let set_succs_exn: Procdesc.t => t => list t => list t => unit; let node_set_succs_exn: t => Node.t => list Node.t => list Node.t => unit;
/** Set the exit node of the procedure */
let set_exit_node: t => Node.t => unit;
/** Set a flag for the proc desc */
let set_flag: t => string => string => unit;
let set_start_node: t => Node.t => unit;
/** indicate that we have performed preanalysis on the CFG assoociated with [t] */
let signal_did_preanalysis: t => unit;
}; };
/** A control-flow graph */
type cfg;
/** Load a cfg from a file */
let load_cfg_from_file: DB.filename => option cfg;
/** Save a cfg into a file, and save a copy of the source files if the boolean is true */
let store_cfg_to_file:
save_sources::bool? => source_file::DB.source_file => DB.filename => cfg => unit;
/** Hash table with nodes as keys. */ /** Hash table with nodes as keys. */
let module NodeHash: Hashtbl.S with type key = Node.t; let module NodeHash: Hashtbl.S with type key = Node.t;
@ -267,10 +257,22 @@ let module IdMap: Map.S with type key = Node.id;
/** {2 Functions for manipulating an interprocedural CFG} */ /** {2 Functions for manipulating an interprocedural CFG} */
/** create a new empty cfg */
let create_cfg: unit => cfg;
/** Create a new procdesc */
let create_proc_desc: cfg => ProcAttributes.t => Procdesc.t;
/** Iterate over all the procdesc's */ /** Iterate over all the procdesc's */
let iter_proc_desc: cfg => (Procname.t => Procdesc.t => unit) => unit; let iter_proc_desc: cfg => (Procname.t => Procdesc.t => unit) => unit;
/** Find the procdesc given the proc name. Return None if not found. */
let find_proc_desc_from_name: cfg => Procname.t => option Procdesc.t;
/** Get all the procedures (defined and declared) */ /** Get all the procedures (defined and declared) */
let get_all_procs: cfg => list Procdesc.t; let get_all_procs: cfg => list Procdesc.t;
@ -287,6 +289,10 @@ let iter_all_nodes: (Procdesc.t => Node.t => unit) => cfg => unit;
let check_cfg_connectedness: cfg => unit; let check_cfg_connectedness: cfg => unit;
/** Remove the procdesc from the control flow graph. */
let remove_proc_desc: cfg => Procname.t => unit;
/** Creates a copy of a procedure description and a list of type substitutions of the form /** Creates a copy of a procedure description and a list of type substitutions of the form
(name, typ) where name is a parameter. The resulting procdesc is isomorphic but (name, typ) where name is a parameter. The resulting procdesc is isomorphic but
all the type of the parameters are replaced in the instructions according to the list. all the type of the parameters are replaced in the instructions according to the list.

2
infer/src/backend/exe_env.ml
Unescape View File

@ -187,7 +187,7 @@ let get_cfg exe_env pname =
let get_proc_desc exe_env pname = let get_proc_desc exe_env pname =
match get_cfg exe_env pname with match get_cfg exe_env pname with
| Some cfg -> | Some cfg ->
Cfg.Procdesc.find_from_name cfg pname Cfg.find_proc_desc_from_name cfg pname
| None -> | None ->
None None

12
infer/src/backend/interproc.ml
Unescape View File

@ -99,7 +99,7 @@ module Worklist = struct
let is_empty (wl : t) : bool = let is_empty (wl : t) : bool =
NodeVisitSet.is_empty wl.todo_set NodeVisitSet.is_empty wl.todo_set
let add (wl : t) (node : Cfg.node) : unit = let add (wl : t) (node : Cfg.Node.t) : unit =
let visits = (* recover visit count if it was visited before *) let visits = (* recover visit count if it was visited before *)
try NodeMap.find node wl.visit_map with try NodeMap.find node wl.visit_map with
| Not_found -> 0 in | Not_found -> 0 in
@ -136,7 +136,7 @@ let htable_retrieve (htable : (Cfg.Node.id, Paths.PathSet.t) Hashtbl.t) (key : C
Paths.PathSet.empty Paths.PathSet.empty
(** Add [d] to the pathset todo at [node] returning true if changed *) (** Add [d] to the pathset todo at [node] returning true if changed *)
let path_set_put_todo (wl : Worklist.t) (node: Cfg.node) (d: Paths.PathSet.t) : bool = let path_set_put_todo (wl : Worklist.t) (node: Cfg.Node.t) (d: Paths.PathSet.t) : bool =
let changed = let changed =
if Paths.PathSet.is_empty d then false if Paths.PathSet.is_empty d then false
else else
@ -149,7 +149,7 @@ let path_set_put_todo (wl : Worklist.t) (node: Cfg.node) (d: Paths.PathSet.t) :
not (Paths.PathSet.equal old_todo todo_new) in not (Paths.PathSet.equal old_todo todo_new) in
changed changed
let path_set_checkout_todo (wl : Worklist.t) (node: Cfg.node) : Paths.PathSet.t = let path_set_checkout_todo (wl : Worklist.t) (node: Cfg.Node.t) : Paths.PathSet.t =
try try
let node_id = Cfg.Node.get_id node in let node_id = Cfg.Node.get_id node in
let todo = Hashtbl.find wl.Worklist.path_set_todo node_id in let todo = Hashtbl.find wl.Worklist.path_set_todo node_id in
@ -250,7 +250,7 @@ let collect_preconditions tenv proc_name : Prop.normal Specs.Jprop.t list =
(** propagate a set of results to the given node *) (** propagate a set of results to the given node *)
let propagate let propagate
(wl : Worklist.t) pname ~is_exception (pset: Paths.PathSet.t) (curr_node: Cfg.node) = (wl : Worklist.t) pname ~is_exception (pset: Paths.PathSet.t) (curr_node: Cfg.Node.t) =
let edgeset_todo = let edgeset_todo =
(* prop must be a renamed prop by the invariant preserved by PropSet *) (* prop must be a renamed prop by the invariant preserved by PropSet *)
let f prop path edgeset_curr = let f prop path edgeset_curr =
@ -270,7 +270,7 @@ let propagate
(** propagate a set of results, including exceptions and divergence *) (** propagate a set of results, including exceptions and divergence *)
let propagate_nodes_divergence let propagate_nodes_divergence
tenv (pdesc: Cfg.Procdesc.t) (pset: Paths.PathSet.t) tenv (pdesc: Cfg.Procdesc.t) (pset: Paths.PathSet.t)
(succ_nodes: Cfg.node list) (exn_nodes: Cfg.node list) (wl : Worklist.t) = (succ_nodes: Cfg.Node.t list) (exn_nodes: Cfg.Node.t list) (wl : Worklist.t) =
let pname = Cfg.Procdesc.get_proc_name pdesc in let pname = Cfg.Procdesc.get_proc_name pdesc in
let pset_exn, pset_ok = Paths.PathSet.partition (Tabulation.prop_is_exn pname) pset in let pset_exn, pset_ok = Paths.PathSet.partition (Tabulation.prop_is_exn pname) pset in
if !Config.footprint && not (Paths.PathSet.is_empty (State.get_diverging_states_node ())) then if !Config.footprint && not (Paths.PathSet.is_empty (State.get_diverging_states_node ())) then
@ -463,7 +463,7 @@ let check_assignement_guard pdesc node =
(** Perform symbolic execution for a node starting from an initial prop *) (** Perform symbolic execution for a node starting from an initial prop *)
let do_symbolic_execution pdesc handle_exn tenv let do_symbolic_execution pdesc handle_exn tenv
(node : Cfg.node) (prop: Prop.normal Prop.t) (path : Paths.Path.t) = (node : Cfg.Node.t) (prop: Prop.normal Prop.t) (path : Paths.Path.t) =
State.mark_execution_start node; State.mark_execution_start node;
(* build the const map lazily *) (* build the const map lazily *)
State.set_const_map (ConstantPropagation.build_const_map tenv pdesc); State.set_const_map (ConstantPropagation.build_const_map tenv pdesc);

14
infer/src/backend/paths.ml
Unescape View File

@ -36,7 +36,7 @@ module Path : sig
val create_loc_trace : t -> PredSymb.path_pos option -> Errlog.loc_trace val create_loc_trace : t -> PredSymb.path_pos option -> Errlog.loc_trace
(** return the current node of the path *) (** return the current node of the path *)
val curr_node : t -> Cfg.node option val curr_node : t -> Cfg.Node.t option
(** dump a path *) (** dump a path *)
val d : t -> unit val d : t -> unit
@ -45,13 +45,13 @@ module Path : sig
val d_stats : t -> unit val d_stats : t -> unit
(** extend a path with a new node reached from the given session, with an optional string for exceptions *) (** extend a path with a new node reached from the given session, with an optional string for exceptions *)
val extend : Cfg.node -> Typename.t option -> session -> t -> t val extend : Cfg.Node.t -> Typename.t option -> session -> t -> t
(** extend a path with a new node reached from the given session, with an optional string for exceptions *) (** extend a path with a new node reached from the given session, with an optional string for exceptions *)
val add_description : t -> string -> t val add_description : t -> string -> t
(** iterate over each node in the path, excluding calls, once *) (** iterate over each node in the path, excluding calls, once *)
val iter_all_nodes_nocalls : (Cfg.node -> unit) -> t -> unit val iter_all_nodes_nocalls : (Cfg.Node.t -> unit) -> t -> unit
(** iterate over the longest sequence belonging to the path, restricting to those containing the given position if given. (** iterate over the longest sequence belonging to the path, restricting to those containing the given position if given.
Do not iterate past the given position. Do not iterate past the given position.
@ -69,7 +69,7 @@ module Path : sig
val pp_stats : Format.formatter -> t -> unit val pp_stats : Format.formatter -> t -> unit
(** create a new path with given start node *) (** create a new path with given start node *)
val start : Cfg.node -> t val start : Cfg.Node.t -> t
(* (*
(** equality for paths *) (** equality for paths *)
@ -86,8 +86,8 @@ end = struct
type path = type path =
(* INVARIANT: stats are always set to dummy_stats unless we are in the middle of a traversal *) (* INVARIANT: stats are always set to dummy_stats unless we are in the middle of a traversal *)
(* in particular: a new traversal cannot be initiated during an existing traversal *) (* in particular: a new traversal cannot be initiated during an existing traversal *)
| Pstart of Cfg.node * stats (** start node *) | Pstart of Cfg.Node.t * stats (** start node *)
| Pnode of Cfg.node * Typename.t option * session * path * stats * string option | Pnode of Cfg.Node.t * Typename.t option * session * path * stats * string option
(** we got to [node] from last [session] perhaps propagating exception [exn_opt], (** we got to [node] from last [session] perhaps propagating exception [exn_opt],
and continue with [path]. *) and continue with [path]. *)
| Pjoin of path * path * stats (** join of two paths *) | Pjoin of path * path * stats (** join of two paths *)
@ -157,7 +157,7 @@ end = struct
let start node = Pstart (node, get_dummy_stats ()) let start node = Pstart (node, get_dummy_stats ())
let extend (node: Cfg.node) exn_opt session path = let extend (node: Cfg.Node.t) exn_opt session path =
Pnode (node, exn_opt, session, path, get_dummy_stats (), None) Pnode (node, exn_opt, session, path, get_dummy_stats (), None)
let join p1 p2 = let join p1 p2 =

8
infer/src/backend/paths.mli
Unescape View File

@ -31,7 +31,7 @@ module Path : sig
val create_loc_trace : t -> PredSymb.path_pos option -> Errlog.loc_trace val create_loc_trace : t -> PredSymb.path_pos option -> Errlog.loc_trace
(** return the current node of the path *) (** return the current node of the path *)
val curr_node : t -> Cfg.node option val curr_node : t -> Cfg.Node.t option
(** dump a path *) (** dump a path *)
val d : t -> unit val d : t -> unit
@ -40,12 +40,12 @@ module Path : sig
val d_stats : t -> unit val d_stats : t -> unit
(** extend a path with a new node reached from the given session, with an optional string for exceptions *) (** extend a path with a new node reached from the given session, with an optional string for exceptions *)
val extend : Cfg.node -> Typename.t option -> session -> t -> t val extend : Cfg.Node.t -> Typename.t option -> session -> t -> t
val add_description : t -> string -> t val add_description : t -> string -> t
(** iterate over each node in the path, excluding calls, once *) (** iterate over each node in the path, excluding calls, once *)
val iter_all_nodes_nocalls : (Cfg.node -> unit) -> t -> unit val iter_all_nodes_nocalls : (Cfg.Node.t -> unit) -> t -> unit
(** iterate over the longest sequence belonging to the path, restricting to those containing the given position if given. (** iterate over the longest sequence belonging to the path, restricting to those containing the given position if given.
Do not iterate past the given position. Do not iterate past the given position.
@ -63,7 +63,7 @@ module Path : sig
val pp_stats : Format.formatter -> t -> unit val pp_stats : Format.formatter -> t -> unit
(** create a new path with given start node *) (** create a new path with given start node *)
val start : Cfg.node -> t val start : Cfg.Node.t -> t
end end
(** Set of (prop,path) pairs, where the identity is given by prop *) (** Set of (prop,path) pairs, where the identity is given by prop *)

4
infer/src/backend/printer.ml
Unescape View File

@ -100,7 +100,7 @@ let is_visited proc_name node =
when starting and finishing the processing of a node *) when starting and finishing the processing of a node *)
module NodesHtml : sig module NodesHtml : sig
val start_node : val start_node :
int -> Location.t -> Procname.t -> Cfg.node list -> Cfg.node list -> Cfg.node list -> int -> Location.t -> Procname.t -> Cfg.Node.t list -> Cfg.Node.t list -> Cfg.Node.t list ->
DB.source_file -> bool DB.source_file -> bool
val finish_node : Procname.t -> int -> DB.source_file -> unit val finish_node : Procname.t -> int -> DB.source_file -> unit
end = struct end = struct
@ -237,7 +237,7 @@ let force_delayed_print fmt =
let (loc: Location.t) = Obj.obj loc in let (loc: Location.t) = Obj.obj loc in
Location.pp fmt loc Location.pp fmt loc
| (L.PTnode_instrs, b_n) -> | (L.PTnode_instrs, b_n) ->
let (b: bool), (io: Sil.instr option), (n: Cfg.node) = Obj.obj b_n in let (b: bool), (io: Sil.instr option), (n: Cfg.Node.t) = Obj.obj b_n in
if Config.write_html if Config.write_html
then then
F.fprintf fmt "%a%a%a" F.fprintf fmt "%a%a%a"

4
infer/src/backend/printer.mli
Unescape View File

@ -37,13 +37,13 @@ val curr_html_formatter : Format.formatter ref
val force_delayed_prints : unit -> unit val force_delayed_prints : unit -> unit
(** Finish a session, and perform delayed print actions if required *) (** Finish a session, and perform delayed print actions if required *)
val node_finish_session : Cfg.node -> DB.source_file -> unit val node_finish_session : Cfg.Node.t -> DB.source_file -> unit
(** Return true if the node was visited during footprint and during re-execution *) (** Return true if the node was visited during footprint and during re-execution *)
val node_is_visited : Procname.t -> Cfg.Node.t -> bool * bool val node_is_visited : Procname.t -> Cfg.Node.t -> bool * bool
(** Start a session, and create a new html fine for the node if it does not exist yet *) (** Start a session, and create a new html fine for the node if it does not exist yet *)
val node_start_session : Cfg.node -> Location.t -> Procname.t -> int -> DB.source_file -> unit val node_start_session : Cfg.Node.t -> Location.t -> Procname.t -> int -> DB.source_file -> unit
(** Write html file for the procedure. (** Write html file for the procedure.
The boolean indicates whether to print whole seconds only. *) The boolean indicates whether to print whole seconds only. *)

2
infer/src/backend/state.ml
Unescape View File

@ -336,7 +336,7 @@ let set_path path pos_opt =
let set_prop_tenv_pdesc prop tenv pdesc = let set_prop_tenv_pdesc prop tenv pdesc =
!gs.last_prop_tenv_pdesc <- Some (prop, tenv, pdesc) !gs.last_prop_tenv_pdesc <- Some (prop, tenv, pdesc)
let set_node (node: Cfg.node) = let set_node (node: Cfg.Node.t) =
!gs.last_instr <- None; !gs.last_instr <- None;
!gs.last_node <- node !gs.last_node <- node

2
infer/src/backend/state.mli
Unescape View File

@ -115,7 +115,7 @@ val set_const_map : const_map -> unit
val set_instr : Sil.instr -> unit val set_instr : Sil.instr -> unit
(** Set last node seen in symbolic execution *) (** Set last node seen in symbolic execution *)
val set_node : Cfg.node -> unit val set_node : Cfg.Node.t -> unit
(** Get last path seen in symbolic execution *) (** Get last path seen in symbolic execution *)
val set_path : Paths.Path.t -> PredSymb.path_pos option -> unit val set_path : Paths.Path.t -> PredSymb.path_pos option -> unit

2
infer/src/clang/cFrontend.ml
Unescape View File

@ -26,7 +26,7 @@ let compute_icfg trans_unit_ctx tenv ast =
CFrontend_config.global_translation_unit_decls := decl_list; CFrontend_config.global_translation_unit_decls := decl_list;
Logging.out_debug "@\n Start creating icfg@\n"; Logging.out_debug "@\n Start creating icfg@\n";
let cg = Cg.create (Some trans_unit_ctx.CFrontend_config.source_file) in let cg = Cg.create (Some trans_unit_ctx.CFrontend_config.source_file) in
let cfg = Cfg.Node.create_cfg () in let cfg = Cfg.create_cfg () in
IList.iter IList.iter
(CFrontend_declImpl.translate_one_declaration trans_unit_ctx tenv cg cfg `DeclTraversal) (CFrontend_declImpl.translate_one_declaration trans_unit_ctx tenv cg cfg `DeclTraversal)
decl_list; decl_list;

11
infer/src/clang/cFrontend_decl.ml
Unescape View File

@ -26,7 +26,7 @@ struct
Logging.out_debug Logging.out_debug
"@\n@\n>>---------- ADDING METHOD: '%s' ---------<<@\n@." (Procname.to_string procname); "@\n@\n>>---------- ADDING METHOD: '%s' ---------<<@\n@." (Procname.to_string procname);
try try
(match Cfg.Procdesc.find_from_name cfg procname with (match Cfg.find_proc_desc_from_name cfg procname with
| Some procdesc -> | Some procdesc ->
if (Cfg.Procdesc.is_defined procdesc && not (model_exists procname)) then if (Cfg.Procdesc.is_defined procdesc && not (model_exists procname)) then
(let context = (let context =
@ -38,9 +38,10 @@ struct
"\n\n>>---------- Start translating body of function: '%s' ---------<<\n@." "\n\n>>---------- Start translating body of function: '%s' ---------<<\n@."
(Procname.to_string procname); (Procname.to_string procname);
let meth_body_nodes = T.instructions_trans context body extra_instrs exit_node in let meth_body_nodes = T.instructions_trans context body extra_instrs exit_node in
let proc_attributes = Cfg.Procdesc.get_attributes procdesc in
Cfg.Node.add_locals_ret_declaration Cfg.Node.add_locals_ret_declaration
procdesc start_node (Cfg.Procdesc.get_locals procdesc); start_node proc_attributes (Cfg.Procdesc.get_locals procdesc);
Cfg.Node.set_succs_exn procdesc start_node meth_body_nodes []; Cfg.Procdesc.node_set_succs_exn procdesc start_node meth_body_nodes [];
Cg.add_defined_node (CContext.get_cg context) (Cfg.Procdesc.get_proc_name procdesc)) Cg.add_defined_node (CContext.get_cg context) (Cfg.Procdesc.get_proc_name procdesc))
| None -> ()) | None -> ())
with with
@ -51,7 +52,7 @@ struct
assert false assert false
| Assert_failure (file, line, column) -> | Assert_failure (file, line, column) ->
Logging.out "Fatal error: exception Assert_failure(%s, %d, %d)\n%!" file line column; Logging.out "Fatal error: exception Assert_failure(%s, %d, %d)\n%!" file line column;
Cfg.Procdesc.remove cfg procname; Cfg.remove_proc_desc cfg procname;
CMethod_trans.create_external_procdesc cfg procname is_objc_method None; CMethod_trans.create_external_procdesc cfg procname is_objc_method None;
() ()
@ -111,7 +112,7 @@ struct
let attrs = { (ProcAttributes.default procname Config.Clang) with let attrs = { (ProcAttributes.default procname Config.Clang) with
loc = loc; loc = loc;
objc_accessor = property_accessor; } in objc_accessor = property_accessor; } in
ignore (Cfg.Procdesc.create cfg attrs) ignore (Cfg.create_proc_desc cfg attrs)
| _ -> ()) in | _ -> ()) in
process_accessor obj_c_property_decl_info.Clang_ast_t.opdi_getter_method ~getter:true; process_accessor obj_c_property_decl_info.Clang_ast_t.opdi_getter_method ~getter:true;
process_accessor obj_c_property_decl_info.Clang_ast_t.opdi_setter_method ~getter:false process_accessor obj_c_property_decl_info.Clang_ast_t.opdi_setter_method ~getter:false

14
infer/src/clang/cMethod_trans.ml
Unescape View File

@ -328,11 +328,11 @@ let sil_func_attributes_of_attributes attrs =
do_translation [] attrs do_translation [] attrs
let should_create_procdesc cfg procname defined = let should_create_procdesc cfg procname defined =
match Cfg.Procdesc.find_from_name cfg procname with match Cfg.find_proc_desc_from_name cfg procname with
| Some previous_procdesc -> | Some previous_procdesc ->
let is_defined_previous = Cfg.Procdesc.is_defined previous_procdesc in let is_defined_previous = Cfg.Procdesc.is_defined previous_procdesc in
if defined && (not is_defined_previous) then if defined && (not is_defined_previous) then
(Cfg.Procdesc.remove cfg (Cfg.Procdesc.get_proc_name previous_procdesc); (Cfg.remove_proc_desc cfg (Cfg.Procdesc.get_proc_name previous_procdesc);
true) true)
else false else false
| None -> true | None -> true
@ -418,14 +418,14 @@ let create_local_procdesc trans_unit_ctx cfg tenv ms fbody captured is_objc_inst
method_annotation; method_annotation;
ret_type; ret_type;
} in } in
Cfg.Procdesc.create cfg proc_attributes in Cfg.create_proc_desc cfg proc_attributes in
if defined then if defined then
(if !Config.arc_mode then (if !Config.arc_mode then
Cfg.Procdesc.set_flag procdesc Mleak_buckets.objc_arc_flag "true"; Cfg.Procdesc.set_flag procdesc Mleak_buckets.objc_arc_flag "true";
let start_kind = Cfg.Node.Start_node proc_name in let start_kind = Cfg.Node.Start_node proc_name in
let start_node = Cfg.Node.create loc_start start_kind [] procdesc in let start_node = Cfg.Procdesc.create_node procdesc loc_start start_kind [] in
let exit_kind = Cfg.Node.Exit_node proc_name in let exit_kind = Cfg.Node.Exit_node proc_name in
let exit_node = Cfg.Node.create loc_exit exit_kind [] procdesc in let exit_node = Cfg.Procdesc.create_node procdesc loc_exit exit_kind [] in
Cfg.Procdesc.set_start_node procdesc start_node; Cfg.Procdesc.set_start_node procdesc start_node;
Cfg.Procdesc.set_exit_node procdesc exit_node) in Cfg.Procdesc.set_exit_node procdesc exit_node) in
if should_create_procdesc cfg proc_name defined then if should_create_procdesc cfg proc_name defined then
@ -434,7 +434,7 @@ let create_local_procdesc trans_unit_ctx cfg tenv ms fbody captured is_objc_inst
(** Create a procdesc for objc methods whose signature cannot be found. *) (** Create a procdesc for objc methods whose signature cannot be found. *)
let create_external_procdesc cfg proc_name is_objc_inst_method type_opt = let create_external_procdesc cfg proc_name is_objc_inst_method type_opt =
match Cfg.Procdesc.find_from_name cfg proc_name with match Cfg.find_proc_desc_from_name cfg proc_name with
| Some _ -> () | Some _ -> ()
| None -> | None ->
let ret_type, formals = let ret_type, formals =
@ -450,7 +450,7 @@ let create_external_procdesc cfg proc_name is_objc_inst_method type_opt =
loc; loc;
ret_type; ret_type;
} in } in
ignore (Cfg.Procdesc.create cfg proc_attributes) ignore (Cfg.create_proc_desc cfg proc_attributes)
let create_procdesc_with_pointer context pointer class_name_opt name = let create_procdesc_with_pointer context pointer class_name_opt name =
let open CContext in let open CContext in

40
infer/src/clang/cTrans.ml
Unescape View File

@ -600,7 +600,7 @@ struct
(* create the label root node into the hashtbl *) (* create the label root node into the hashtbl *)
let sil_loc = CLocation.get_sil_location stmt_info context in let sil_loc = CLocation.get_sil_location stmt_info context in
let root_node' = GotoLabel.find_goto_label trans_state.context label_name sil_loc in let root_node' = GotoLabel.find_goto_label trans_state.context label_name sil_loc in
Cfg.Node.set_succs_exn context.procdesc root_node' res_trans.root_nodes []; Cfg.Procdesc.node_set_succs_exn context.procdesc root_node' res_trans.root_nodes [];
{ empty_res_trans with root_nodes = [root_node']; leaf_nodes = trans_state.succ_nodes } { empty_res_trans with root_nodes = [root_node']; leaf_nodes = trans_state.succ_nodes }
and var_deref_trans trans_state stmt_info (decl_ref : Clang_ast_t.decl_ref) = and var_deref_trans trans_state stmt_info (decl_ref : Clang_ast_t.decl_ref) =
@ -750,7 +750,7 @@ struct
if res_trans_idx.root_nodes <> [] if res_trans_idx.root_nodes <> []
then then
IList.iter IList.iter
(fun n -> Cfg.Node.set_succs_exn context.procdesc n res_trans_idx.root_nodes []) (fun n -> Cfg.Procdesc.node_set_succs_exn context.procdesc n res_trans_idx.root_nodes [])
res_trans_a.leaf_nodes; res_trans_a.leaf_nodes;
(* Note the order of res_trans_idx.ids @ res_trans_a.ids is important. *) (* Note the order of res_trans_idx.ids @ res_trans_a.ids is important. *)
@ -1132,7 +1132,7 @@ struct
let prune_nodes_t, prune_nodes_f = IList.partition is_true_prune_node prune_nodes in let prune_nodes_t, prune_nodes_f = IList.partition is_true_prune_node prune_nodes in
let prune_nodes' = if branch then prune_nodes_t else prune_nodes_f in let prune_nodes' = if branch then prune_nodes_t else prune_nodes_f in
IList.iter IList.iter
(fun n -> Cfg.Node.set_succs_exn context.procdesc n res_trans.root_nodes []) (fun n -> Cfg.Procdesc.node_set_succs_exn context.procdesc n res_trans.root_nodes [])
prune_nodes' in prune_nodes' in
(match stmt_list with (match stmt_list with
| [cond; exp1; exp2] -> | [cond; exp1; exp2] ->
@ -1141,7 +1141,7 @@ struct
context.CContext.tenv expr_info.Clang_ast_t.ei_type_ptr in context.CContext.tenv expr_info.Clang_ast_t.ei_type_ptr in
let var_typ = add_reference_if_glvalue typ expr_info in let var_typ = add_reference_if_glvalue typ expr_info in
let join_node = create_node (Cfg.Node.Join_node) [] sil_loc context in let join_node = create_node (Cfg.Node.Join_node) [] sil_loc context in
Cfg.Node.set_succs_exn context.procdesc join_node succ_nodes []; Cfg.Procdesc.node_set_succs_exn context.procdesc join_node succ_nodes [];
let pvar = mk_temp_sil_var procdesc "SIL_temp_conditional___" in let pvar = mk_temp_sil_var procdesc "SIL_temp_conditional___" in
Cfg.Procdesc.append_locals procdesc [(Pvar.get_name pvar, var_typ)]; Cfg.Procdesc.append_locals procdesc [(Pvar.get_name pvar, var_typ)];
let continuation' = mk_cond_continuation trans_state.continuation in let continuation' = mk_cond_continuation trans_state.continuation in
@ -1214,7 +1214,7 @@ struct
let prune_t = mk_prune_node true e' instrs' in let prune_t = mk_prune_node true e' instrs' in
let prune_f = mk_prune_node false e' instrs' in let prune_f = mk_prune_node false e' instrs' in
IList.iter IList.iter
(fun n' -> Cfg.Node.set_succs_exn context.procdesc n' [prune_t; prune_f] []) (fun n' -> Cfg.Procdesc.node_set_succs_exn context.procdesc n' [prune_t; prune_f] [])
res_trans_cond.leaf_nodes; res_trans_cond.leaf_nodes;
let rnodes = if (IList.length res_trans_cond.root_nodes) = 0 then let rnodes = if (IList.length res_trans_cond.root_nodes) = 0 then
[prune_t; prune_f] [prune_t; prune_f]
@ -1247,7 +1247,7 @@ struct
| Binop.LOr -> prune_nodes_f, prune_nodes_t | Binop.LOr -> prune_nodes_f, prune_nodes_t
| _ -> assert false) in | _ -> assert false) in
IList.iter IList.iter
(fun n -> Cfg.Node.set_succs_exn context.procdesc n res_trans_s2.root_nodes []) (fun n -> Cfg.Procdesc.node_set_succs_exn context.procdesc n res_trans_s2.root_nodes [])
prune_to_s2; prune_to_s2;
let root_nodes_to_parent = let root_nodes_to_parent =
if (IList.length res_trans_s1.root_nodes) = 0 if (IList.length res_trans_s1.root_nodes) = 0
@ -1288,7 +1288,7 @@ struct
let succ_nodes = trans_state.succ_nodes in let succ_nodes = trans_state.succ_nodes in
let sil_loc = CLocation.get_sil_location stmt_info context in let sil_loc = CLocation.get_sil_location stmt_info context in
let join_node = create_node (Cfg.Node.Join_node) [] sil_loc context in let join_node = create_node (Cfg.Node.Join_node) [] sil_loc context in
Cfg.Node.set_succs_exn context.procdesc join_node succ_nodes []; Cfg.Procdesc.node_set_succs_exn context.procdesc join_node succ_nodes [];
let trans_state' = { trans_state with succ_nodes = [join_node] } in let trans_state' = { trans_state with succ_nodes = [join_node] } in
let do_branch branch stmt_branch prune_nodes = let do_branch branch stmt_branch prune_nodes =
(* leaf nodes are ignored here as they will be already attached to join_node *) (* leaf nodes are ignored here as they will be already attached to join_node *)
@ -1302,7 +1302,7 @@ struct
let prune_nodes_t, prune_nodes_f = IList.partition is_true_prune_node prune_nodes in let prune_nodes_t, prune_nodes_f = IList.partition is_true_prune_node prune_nodes in
let prune_nodes' = if branch then prune_nodes_t else prune_nodes_f in let prune_nodes' = if branch then prune_nodes_t else prune_nodes_f in
IList.iter IList.iter
(fun n -> Cfg.Node.set_succs_exn context.procdesc n nodes_branch []) (fun n -> Cfg.Procdesc.node_set_succs_exn context.procdesc n nodes_branch [])
prune_nodes' in prune_nodes' in
(match stmt_list with (match stmt_list with
| [_; decl_stmt; cond; stmt1; stmt2] -> | [_; decl_stmt; cond; stmt1; stmt2] ->
@ -1339,7 +1339,8 @@ struct
let node_kind = Cfg.Node.Stmt_node "Switch_stmt" in let node_kind = Cfg.Node.Stmt_node "Switch_stmt" in
create_node node_kind res_trans_cond_tmp.instrs sil_loc context in create_node node_kind res_trans_cond_tmp.instrs sil_loc context in
IList.iter IList.iter
(fun n' -> Cfg.Node.set_succs_exn context.procdesc n' [switch_special_cond_node] []) (fun n' ->
Cfg.Procdesc.node_set_succs_exn context.procdesc n' [switch_special_cond_node] [])
res_trans_cond_tmp.leaf_nodes; res_trans_cond_tmp.leaf_nodes;
let root_nodes = let root_nodes =
if res_trans_cond_tmp.root_nodes <> [] then res_trans_cond_tmp.root_nodes if res_trans_cond_tmp.root_nodes <> [] then res_trans_cond_tmp.root_nodes
@ -1437,8 +1438,8 @@ struct
let case_entry_point = connected_instruction (IList.rev case_content) last_nodes in let case_entry_point = connected_instruction (IList.rev case_content) last_nodes in
(* connects between cases, then continuation has priority about breaks *) (* connects between cases, then continuation has priority about breaks *)
let prune_node_t, prune_node_f = create_prune_nodes_for_case case in let prune_node_t, prune_node_f = create_prune_nodes_for_case case in
Cfg.Node.set_succs_exn context.procdesc prune_node_t case_entry_point []; Cfg.Procdesc.node_set_succs_exn context.procdesc prune_node_t case_entry_point [];
Cfg.Node.set_succs_exn context.procdesc prune_node_f last_prune_nodes []; Cfg.Procdesc.node_set_succs_exn context.procdesc prune_node_f last_prune_nodes [];
case_entry_point, [prune_node_t; prune_node_f] case_entry_point, [prune_node_t; prune_node_f]
| DefaultStmt(stmt_info, default_content) :: rest -> | DefaultStmt(stmt_info, default_content) :: rest ->
let sil_loc = CLocation.get_sil_location stmt_info context in let sil_loc = CLocation.get_sil_location stmt_info context in
@ -1448,14 +1449,15 @@ struct
translate_and_connect_cases rest next_nodes [placeholder_entry_point] in translate_and_connect_cases rest next_nodes [placeholder_entry_point] in
let default_entry_point = let default_entry_point =
connected_instruction (IList.rev default_content) last_nodes in connected_instruction (IList.rev default_content) last_nodes in
Cfg.Node.set_succs_exn Cfg.Procdesc.node_set_succs_exn
context.procdesc placeholder_entry_point default_entry_point []; context.procdesc placeholder_entry_point default_entry_point [];
default_entry_point, last_prune_nodes default_entry_point, last_prune_nodes
| _ -> assert false in | _ -> assert false in
let top_entry_point, top_prune_nodes = let top_entry_point, top_prune_nodes =
translate_and_connect_cases list_of_cases succ_nodes succ_nodes in translate_and_connect_cases list_of_cases succ_nodes succ_nodes in
let _ = connected_instruction (IList.rev pre_case_stmts) top_entry_point in let _ = connected_instruction (IList.rev pre_case_stmts) top_entry_point in
Cfg.Node.set_succs_exn context.procdesc switch_special_cond_node top_prune_nodes []; Cfg.Procdesc.node_set_succs_exn
context.procdesc switch_special_cond_node top_prune_nodes [];
let top_nodes = res_trans_decl.root_nodes in let top_nodes = res_trans_decl.root_nodes in
IList.iter IList.iter
(fun n' -> Cfg.Node.append_instrs n' []) succ_nodes; (fun n' -> Cfg.Node.append_instrs n' []) succ_nodes;
@ -1536,12 +1538,12 @@ struct
match loop_kind with match loop_kind with
| Loops.For _ | Loops.While _ -> res_trans_body.root_nodes | Loops.For _ | Loops.While _ -> res_trans_body.root_nodes
| Loops.DoWhile _ -> [join_node] in | Loops.DoWhile _ -> [join_node] in
Cfg.Node.set_succs_exn context.procdesc join_node join_succ_nodes []; Cfg.Procdesc.node_set_succs_exn context.procdesc join_node join_succ_nodes [];
IList.iter IList.iter
(fun n -> Cfg.Node.set_succs_exn context.procdesc n prune_t_succ_nodes []) (fun n -> Cfg.Procdesc.node_set_succs_exn context.procdesc n prune_t_succ_nodes [])
prune_nodes_t; prune_nodes_t;
IList.iter IList.iter
(fun n -> Cfg.Node.set_succs_exn context.procdesc n succ_nodes []) (fun n -> Cfg.Procdesc.node_set_succs_exn context.procdesc n succ_nodes [])
prune_nodes_f; prune_nodes_f;
let root_nodes = let root_nodes =
match loop_kind with match loop_kind with
@ -1890,7 +1892,7 @@ struct
let trans_state_pri = PriorityNode.try_claim_priority_node trans_state stmt_info in let trans_state_pri = PriorityNode.try_claim_priority_node trans_state stmt_info in
let mk_ret_node instrs = let mk_ret_node instrs =
let ret_node = create_node (Cfg.Node.Stmt_node "Return Stmt") instrs sil_loc context in let ret_node = create_node (Cfg.Node.Stmt_node "Return Stmt") instrs sil_loc context in
Cfg.Node.set_succs_exn Cfg.Procdesc.node_set_succs_exn
context.procdesc context.procdesc
ret_node [(Cfg.Procdesc.get_exit_node context.CContext.procdesc)] []; ret_node [(Cfg.Procdesc.get_exit_node context.CContext.procdesc)] [];
ret_node in ret_node in
@ -1924,7 +1926,7 @@ struct
let instrs = var_instrs @ res_trans_stmt.instrs @ ret_instrs @ autorelease_instrs in let instrs = var_instrs @ res_trans_stmt.instrs @ ret_instrs @ autorelease_instrs in
let ret_node = mk_ret_node instrs in let ret_node = mk_ret_node instrs in
IList.iter IList.iter
(fun n -> Cfg.Node.set_succs_exn procdesc n [ret_node] []) (fun n -> Cfg.Procdesc.node_set_succs_exn procdesc n [ret_node] [])
res_trans_stmt.leaf_nodes; res_trans_stmt.leaf_nodes;
let root_nodes_to_parent = let root_nodes_to_parent =
if IList.length res_trans_stmt.root_nodes >0 if IList.length res_trans_stmt.root_nodes >0
@ -2011,7 +2013,7 @@ struct
autorelease_pool_vars, sil_loc, CallFlags.default) in autorelease_pool_vars, sil_loc, CallFlags.default) in
let node_kind = Cfg.Node.Stmt_node ("Release the autorelease pool") in let node_kind = Cfg.Node.Stmt_node ("Release the autorelease pool") in
let call_node = create_node node_kind [stmt_call] sil_loc context in let call_node = create_node node_kind [stmt_call] sil_loc context in
Cfg.Node.set_succs_exn context.procdesc call_node trans_state.succ_nodes []; Cfg.Procdesc.node_set_succs_exn context.procdesc call_node trans_state.succ_nodes [];
let trans_state'={ trans_state with continuation = None; succ_nodes =[call_node] } in let trans_state'={ trans_state with continuation = None; succ_nodes =[call_node] } in
instructions trans_state' stmts instructions trans_state' stmts

14
infer/src/clang/cTrans_utils.ml
Unescape View File

@ -54,7 +54,7 @@ struct
let create_node node_kind instrs loc context = let create_node node_kind instrs loc context =
let procdesc = CContext.get_procdesc context in let procdesc = CContext.get_procdesc context in
Cfg.Node.create loc node_kind instrs procdesc Cfg.Procdesc.create_node procdesc loc node_kind instrs
let create_prune_node branch e_cond instrs_cond loc ik context = let create_prune_node branch e_cond instrs_cond loc ik context =
let (e_cond', _) = extract_exp_from_list e_cond let (e_cond', _) = extract_exp_from_list e_cond
@ -170,7 +170,9 @@ let collect_res_trans pdesc l =
if rt'.leaf_nodes <> [] then rt'.leaf_nodes if rt'.leaf_nodes <> [] then rt'.leaf_nodes
else rt.leaf_nodes in else rt.leaf_nodes in
if rt'.root_nodes <> [] then if rt'.root_nodes <> [] then
IList.iter (fun n -> Cfg.Node.set_succs_exn pdesc n rt'.root_nodes []) rt.leaf_nodes; IList.iter
(fun n -> Cfg.Procdesc.node_set_succs_exn pdesc n rt'.root_nodes [])
rt.leaf_nodes;
collect l' collect l'
{ root_nodes = root_nodes; { root_nodes = root_nodes;
leaf_nodes = leaf_nodes; leaf_nodes = leaf_nodes;
@ -244,9 +246,9 @@ struct
(* We need to create a node *) (* We need to create a node *)
let node_kind = Cfg.Node.Stmt_node (nd_name) in let node_kind = Cfg.Node.Stmt_node (nd_name) in
let node = Nodes.create_node node_kind res_state.instrs loc trans_state.context in let node = Nodes.create_node node_kind res_state.instrs loc trans_state.context in
Cfg.Node.set_succs_exn trans_state.context.procdesc node trans_state.succ_nodes []; Cfg.Procdesc.node_set_succs_exn trans_state.context.procdesc node trans_state.succ_nodes [];
IList.iter IList.iter
(fun leaf -> Cfg.Node.set_succs_exn trans_state.context.procdesc leaf [node] []) (fun leaf -> Cfg.Procdesc.node_set_succs_exn trans_state.context.procdesc leaf [node] [])
res_state.leaf_nodes; res_state.leaf_nodes;
(* Invariant: if root_nodes is empty then the params have not created a node.*) (* Invariant: if root_nodes is empty then the params have not created a node.*)
let root_nodes = (if res_state.root_nodes <> [] then res_state.root_nodes let root_nodes = (if res_state.root_nodes <> [] then res_state.root_nodes
@ -447,13 +449,13 @@ let trans_assertion_failure sil_loc (context : CContext.t) =
let exit_node = Cfg.Procdesc.get_exit_node (CContext.get_procdesc context) let exit_node = Cfg.Procdesc.get_exit_node (CContext.get_procdesc context)
and failure_node = and failure_node =
Nodes.create_node (Cfg.Node.Stmt_node "Assertion failure") [call_instr] sil_loc context in Nodes.create_node (Cfg.Node.Stmt_node "Assertion failure") [call_instr] sil_loc context in
Cfg.Node.set_succs_exn context.procdesc failure_node [exit_node] []; Cfg.Procdesc.node_set_succs_exn context.procdesc failure_node [exit_node] [];
{ empty_res_trans with root_nodes = [failure_node]; } { empty_res_trans with root_nodes = [failure_node]; }
let trans_assume_false sil_loc (context : CContext.t) succ_nodes = let trans_assume_false sil_loc (context : CContext.t) succ_nodes =
let instrs_cond = [Sil.Prune (Exp.zero, sil_loc, true, Sil.Ik_land_lor)] in let instrs_cond = [Sil.Prune (Exp.zero, sil_loc, true, Sil.Ik_land_lor)] in
let prune_node = Nodes.create_node (Nodes.prune_kind true) instrs_cond sil_loc context in let prune_node = Nodes.create_node (Nodes.prune_kind true) instrs_cond sil_loc context in
Cfg.Node.set_succs_exn context.procdesc prune_node succ_nodes []; Cfg.Procdesc.node_set_succs_exn context.procdesc prune_node succ_nodes [];
{ empty_res_trans with root_nodes = [prune_node]; leaf_nodes = [prune_node] } { empty_res_trans with root_nodes = [prune_node]; leaf_nodes = [prune_node] }
let trans_assertion trans_state sil_loc = let trans_assertion trans_state sil_loc =

22
infer/src/harness/inhabit.ml
Unescape View File

@ -238,28 +238,28 @@ let setup_harness_cfg harness_name env cg cfg =
(* each procedure has different scope: start names from id 0 *) (* each procedure has different scope: start names from id 0 *)
Ident.NameGenerator.reset (); Ident.NameGenerator.reset ();
let procname = Procname.Java harness_name in let procname = Procname.Java harness_name in
let proc_attributes =
{ (ProcAttributes.default procname Config.Java) with
ProcAttributes.is_defined = true;
loc = env.pc;
} in
let procdesc = let procdesc =
let proc_attributes = Cfg.create_proc_desc cfg proc_attributes in
{ (ProcAttributes.default procname Config.Java) with
ProcAttributes.is_defined = true;
loc = env.pc;
} in
Cfg.Procdesc.create cfg proc_attributes in
let harness_node = let harness_node =
(* important to reverse the list or there will be scoping issues! *) (* important to reverse the list or there will be scoping issues! *)
let instrs = (IList.rev env.instrs) in let instrs = (IList.rev env.instrs) in
let nodekind = Cfg.Node.Stmt_node "method_body" in let nodekind = Cfg.Node.Stmt_node "method_body" in
Cfg.Node.create env.pc nodekind instrs procdesc in Cfg.Procdesc.create_node procdesc env.pc nodekind instrs in
let (start_node, exit_node) = let (start_node, exit_node) =
let create_node kind = Cfg.Node.create env.pc kind [] procdesc in let create_node kind = Cfg.Procdesc.create_node procdesc env.pc kind [] in
let start_kind = Cfg.Node.Start_node procname in let start_kind = Cfg.Node.Start_node procname in
let exit_kind = Cfg.Node.Exit_node procname in let exit_kind = Cfg.Node.Exit_node procname in
(create_node start_kind, create_node exit_kind) in (create_node start_kind, create_node exit_kind) in
Cfg.Procdesc.set_start_node procdesc start_node; Cfg.Procdesc.set_start_node procdesc start_node;
Cfg.Procdesc.set_exit_node procdesc exit_node; Cfg.Procdesc.set_exit_node procdesc exit_node;
Cfg.Node.add_locals_ret_declaration procdesc start_node []; Cfg.Node.add_locals_ret_declaration start_node proc_attributes [];
Cfg.Node.set_succs_exn procdesc start_node [harness_node] [exit_node]; Cfg.Procdesc.node_set_succs_exn procdesc start_node [harness_node] [exit_node];
Cfg.Node.set_succs_exn procdesc harness_node [exit_node] [exit_node]; Cfg.Procdesc.node_set_succs_exn procdesc harness_node [exit_node] [exit_node];
add_harness_to_cg harness_name harness_node cg add_harness_to_cg harness_name harness_node cg
(** create a procedure named harness_name that calls each of the methods in trace in the specified (** create a procedure named harness_name that calls each of the methods in trace in the specified

13
infer/src/java/jFrontend.ml
Unescape View File

@ -48,7 +48,8 @@ let add_edges
if super_call then (fun _ -> exit_nodes) if super_call then (fun _ -> exit_nodes)
else JTransExn.create_exception_handlers context [exn_node] get_body_nodes impl in else JTransExn.create_exception_handlers context [exn_node] get_body_nodes impl in
let connect node pc = let connect node pc =
Cfg.Node.set_succs_exn context.procdesc node (get_succ_nodes node pc) (get_exn_nodes pc) in Cfg.Procdesc.node_set_succs_exn
context.procdesc node (get_succ_nodes node pc) (get_exn_nodes pc) in
let connect_nodes pc translated_instruction = let connect_nodes pc translated_instruction =
match translated_instruction with match translated_instruction with
| JTrans.Skip -> () | JTrans.Skip -> ()
@ -57,7 +58,7 @@ let add_edges
connect node_true pc; connect node_true pc;
connect node_false pc connect node_false pc
| JTrans.Loop (join_node, node_true, node_false) -> | JTrans.Loop (join_node, node_true, node_false) ->
Cfg.Node.set_succs_exn context.procdesc join_node [node_true; node_false] []; Cfg.Procdesc.node_set_succs_exn context.procdesc join_node [node_true; node_false] [];
connect node_true pc; connect node_true pc;
connect node_false pc in connect node_false pc in
let first_nodes = let first_nodes =
@ -65,11 +66,11 @@ let add_edges
direct_successors (-1) in direct_successors (-1) in
(* the exceptions edges here are going directly to the exit node *) (* the exceptions edges here are going directly to the exit node *)
Cfg.Node.set_succs_exn context.procdesc start_node first_nodes exit_nodes; Cfg.Procdesc.node_set_succs_exn context.procdesc start_node first_nodes exit_nodes;
if not super_call then if not super_call then
(* the exceptions node is just before the exit node *) (* the exceptions node is just before the exit node *)
Cfg.Node.set_succs_exn context.procdesc exn_node exit_nodes exit_nodes; Cfg.Procdesc.node_set_succs_exn context.procdesc exn_node exit_nodes exit_nodes;
Array.iteri connect_nodes method_body_nodes Array.iteri connect_nodes method_body_nodes
@ -192,7 +193,7 @@ let compute_source_icfg
source_basename package_opt source_file = source_basename package_opt source_file =
let icfg = let icfg =
{ JContext.cg = Cg.create (Some source_file); { JContext.cg = Cg.create (Some source_file);
JContext.cfg = Cfg.Node.create_cfg (); JContext.cfg = Cfg.create_cfg ();
JContext.tenv = tenv } in JContext.tenv = tenv } in
let select test procedure cn node = let select test procedure cn node =
if test node then if test node then
@ -212,7 +213,7 @@ let compute_source_icfg
let compute_class_icfg source_file linereader program tenv node = let compute_class_icfg source_file linereader program tenv node =
let icfg = let icfg =
{ JContext.cg = Cg.create (Some source_file); { JContext.cg = Cg.create (Some source_file);
JContext.cfg = Cfg.Node.create_cfg (); JContext.cfg = Cfg.create_cfg ();
JContext.tenv = tenv } in JContext.tenv = tenv } in
begin begin
try try

50
infer/src/java/jTrans.ml
Unescape View File

@ -267,12 +267,12 @@ let create_procdesc source_file program linereader icfg m : Cfg.Procdesc.t optio
method_annotation; method_annotation;
ret_type = JTransType.return_type program tenv ms; ret_type = JTransType.return_type program tenv ms;
} in } in
Cfg.Procdesc.create cfg proc_attributes in Cfg.create_proc_desc cfg proc_attributes in
let start_kind = Cfg.Node.Start_node proc_name in let start_kind = Cfg.Node.Start_node proc_name in
let start_node = Cfg.Node.create Location.dummy start_kind [] procdesc in let start_node = Cfg.Procdesc.create_node procdesc Location.dummy start_kind [] in
let exit_kind = (Cfg.Node.Exit_node proc_name) in let exit_kind = (Cfg.Node.Exit_node proc_name) in
let exit_node = Cfg.Node.create Location.dummy exit_kind [] procdesc in let exit_node = Cfg.Procdesc.create_node procdesc Location.dummy exit_kind [] in
Cfg.Node.set_succs_exn procdesc start_node [exit_node] [exit_node]; Cfg.Procdesc.node_set_succs_exn procdesc start_node [exit_node] [exit_node];
Cfg.Procdesc.set_start_node procdesc start_node; Cfg.Procdesc.set_start_node procdesc start_node;
Cfg.Procdesc.set_exit_node procdesc exit_node; Cfg.Procdesc.set_exit_node procdesc exit_node;
procdesc procdesc
@ -291,7 +291,7 @@ let create_procdesc source_file program linereader icfg m : Cfg.Procdesc.t optio
method_annotation; method_annotation;
ret_type = JTransType.return_type program tenv ms; ret_type = JTransType.return_type program tenv ms;
} in } in
Cfg.Procdesc.create cfg proc_attributes; Cfg.create_proc_desc cfg proc_attributes;
| Javalib.ConcreteMethod cm -> | Javalib.ConcreteMethod cm ->
let impl = get_implementation cm in let impl = get_implementation cm in
let locals, formals = locals_formals program tenv cn impl in let locals, formals = locals_formals program tenv cn impl in
@ -304,32 +304,32 @@ let create_procdesc source_file program linereader icfg m : Cfg.Procdesc.t optio
JAnnotation.translate_method proc_name_java cm.Javalib.cm_annotations in JAnnotation.translate_method proc_name_java cm.Javalib.cm_annotations in
update_constr_loc cn ms loc_start; update_constr_loc cn ms loc_start;
update_init_loc cn ms loc_exit; update_init_loc cn ms loc_exit;
let proc_attributes =
{ (ProcAttributes.default proc_name Config.Java) with
ProcAttributes.access = trans_access cm.Javalib.cm_access;
exceptions = IList.map JBasics.cn_name cm.Javalib.cm_exceptions;
formals;
is_bridge_method = cm.Javalib.cm_bridge;
is_defined = true;
is_synthetic_method = cm.Javalib.cm_synthetic;
is_java_synchronized_method = cm.Javalib.cm_synchronized;
loc = loc_start;
locals;
method_annotation;
ret_type = JTransType.return_type program tenv ms;
} in
let procdesc = let procdesc =
let proc_attributes = Cfg.create_proc_desc cfg proc_attributes in
{ (ProcAttributes.default proc_name Config.Java) with
ProcAttributes.access = trans_access cm.Javalib.cm_access;
exceptions = IList.map JBasics.cn_name cm.Javalib.cm_exceptions;
formals;
is_bridge_method = cm.Javalib.cm_bridge;
is_defined = true;
is_synthetic_method = cm.Javalib.cm_synthetic;
is_java_synchronized_method = cm.Javalib.cm_synchronized;
loc = loc_start;
locals;
method_annotation;
ret_type = JTransType.return_type program tenv ms;
} in
Cfg.Procdesc.create cfg proc_attributes in
let start_kind = Cfg.Node.Start_node proc_name in let start_kind = Cfg.Node.Start_node proc_name in
let start_node = Cfg.Node.create loc_start start_kind [] procdesc in let start_node = Cfg.Procdesc.create_node procdesc loc_start start_kind [] in
let exit_kind = (Cfg.Node.Exit_node proc_name) in let exit_kind = (Cfg.Node.Exit_node proc_name) in
let exit_node = Cfg.Node.create loc_exit exit_kind [] procdesc in let exit_node = Cfg.Procdesc.create_node procdesc loc_exit exit_kind [] in
let exn_kind = Cfg.Node.exn_sink_kind in let exn_kind = Cfg.Node.exn_sink_kind in
let exn_node = Cfg.Node.create loc_exit exn_kind [] procdesc in let exn_node = Cfg.Procdesc.create_node procdesc loc_exit exn_kind [] in
JContext.add_exn_node proc_name exn_node; JContext.add_exn_node proc_name exn_node;
Cfg.Procdesc.set_start_node procdesc start_node; Cfg.Procdesc.set_start_node procdesc start_node;
Cfg.Procdesc.set_exit_node procdesc exit_node; Cfg.Procdesc.set_exit_node procdesc exit_node;
Cfg.Node.add_locals_ret_declaration procdesc start_node locals; Cfg.Node.add_locals_ret_declaration start_node proc_attributes locals;
procdesc in procdesc in
Some procdesc Some procdesc
with JBir.Subroutine | JBasics.Class_structure_error _ -> with JBir.Subroutine | JBasics.Class_structure_error _ ->
@ -709,7 +709,7 @@ let rec instruction (context : JContext.t) pc instr : translation =
let file = loc.Location.file in let file = loc.Location.file in
let match_never_null = Inferconfig.never_return_null_matcher in let match_never_null = Inferconfig.never_return_null_matcher in
let create_node node_kind sil_instrs = let create_node node_kind sil_instrs =
Cfg.Node.create loc node_kind sil_instrs context.procdesc in Cfg.Procdesc.create_node context.procdesc loc node_kind sil_instrs in
let return_not_null () = let return_not_null () =
match_never_null loc.Location.file proc_name in match_never_null loc.Location.file proc_name in
let trans_monitor_enter_exit context expr pc loc builtin node_desc = let trans_monitor_enter_exit context expr pc loc builtin node_desc =

8
infer/src/java/jTransExn.ml
Unescape View File

@ -30,7 +30,7 @@ let translate_exceptions (context : JContext.t) exit_nodes get_body_nodes handle
let catch_block_table = Hashtbl.create 1 in let catch_block_table = Hashtbl.create 1 in
let exn_message = "exception handler" in let exn_message = "exception handler" in
let procdesc = context.procdesc in let procdesc = context.procdesc in
let create_node loc node_kind instrs = Cfg.Node.create loc node_kind instrs procdesc in let create_node loc node_kind instrs = Cfg.Procdesc.create_node procdesc loc node_kind instrs in
let ret_var = Cfg.Procdesc.get_ret_var procdesc in let ret_var = Cfg.Procdesc.get_ret_var procdesc in
let ret_type = Cfg.Procdesc.get_ret_type procdesc in let ret_type = Cfg.Procdesc.get_ret_type procdesc in
let id_ret_val = Ident.create_fresh Ident.knormal in let id_ret_val = Ident.create_fresh Ident.knormal in
@ -91,8 +91,8 @@ let translate_exceptions (context : JContext.t) exit_nodes get_body_nodes handle
let node_false = let node_false =
let instrs_false = [instr_call_instanceof; instr_prune_false] @ (if rethrow_exception then [instr_rethrow_exn] else []) in let instrs_false = [instr_call_instanceof; instr_prune_false] @ (if rethrow_exception then [instr_rethrow_exn] else []) in
create_node loc node_kind_false instrs_false in create_node loc node_kind_false instrs_false in
Cfg.Node.set_succs_exn procdesc node_true catch_nodes exit_nodes; Cfg.Procdesc.node_set_succs_exn procdesc node_true catch_nodes exit_nodes;
Cfg.Node.set_succs_exn procdesc node_false succ_nodes exit_nodes; Cfg.Procdesc.node_set_succs_exn procdesc node_false succ_nodes exit_nodes;
let is_finally = handler.JBir.e_catch_type = None in let is_finally = handler.JBir.e_catch_type = None in
if is_finally if is_finally
then [node_true] (* TODO (#4759480): clean up the translation so prune nodes are not created at all *) then [node_true] (* TODO (#4759480): clean up the translation so prune nodes are not created at all *)
@ -109,7 +109,7 @@ let translate_exceptions (context : JContext.t) exit_nodes get_body_nodes handle
| n:: _ -> Cfg.Node.get_loc n | n:: _ -> Cfg.Node.get_loc n
| [] -> Location.dummy in | [] -> Location.dummy in
let entry_node = create_entry_node loc in let entry_node = create_entry_node loc in
Cfg.Node.set_succs_exn procdesc entry_node nodes_first_handler exit_nodes; Cfg.Procdesc.node_set_succs_exn procdesc entry_node nodes_first_handler exit_nodes;
Hashtbl.add catch_block_table handler_list [entry_node] in Hashtbl.add catch_block_table handler_list [entry_node] in
Hashtbl.iter (fun _ handler_list -> create_entry_block handler_list) handler_table; Hashtbl.iter (fun _ handler_list -> create_entry_block handler_list) handler_table;
catch_block_table catch_block_table

8
infer/src/unit/analyzerTester.ml
Unescape View File

@ -168,15 +168,15 @@ module Make
type assert_map = string M.t type assert_map = string M.t
let structured_program_to_cfg program test_pname = let structured_program_to_cfg program test_pname =
let cfg = Cfg.Node.create_cfg () in let cfg = Cfg.create_cfg () in
let pdesc = let pdesc =
Cfg.Procdesc.create cfg (ProcAttributes.default test_pname !Config.curr_language) in Cfg.create_proc_desc cfg (ProcAttributes.default test_pname !Config.curr_language) in
let pname = Cfg.Procdesc.get_proc_name pdesc in let pname = Cfg.Procdesc.get_proc_name pdesc in
let create_node kind cmds = let create_node kind cmds =
Cfg.Node.create dummy_loc kind cmds pdesc in Cfg.Procdesc.create_node pdesc dummy_loc kind cmds in
let set_succs cur_node succs ~exn_handlers= let set_succs cur_node succs ~exn_handlers=
Cfg.Node.set_succs_exn pdesc cur_node succs exn_handlers in Cfg.Procdesc.node_set_succs_exn pdesc cur_node succs exn_handlers in
let mk_prune_nodes_for_cond cond_exp if_kind = let mk_prune_nodes_for_cond cond_exp if_kind =
let mk_prune_node cond_exp if_kind true_branch = let mk_prune_node cond_exp if_kind true_branch =
let prune_instr = Sil.Prune (cond_exp, dummy_loc, true_branch, if_kind) in let prune_instr = Sil.Prune (cond_exp, dummy_loc, true_branch, if_kind) in

12
infer/src/unit/procCfgTests.ml
Unescape View File

@ -16,9 +16,9 @@ module InstrCfg = ProcCfg.OneInstrPerNode (ProcCfg.Normal)
module BackwardInstrCfg = ProcCfg.Backward (InstrCfg) module BackwardInstrCfg = ProcCfg.Backward (InstrCfg)
let tests = let tests =
let cfg = Cfg.Node.create_cfg () in let cfg = Cfg.create_cfg () in
let test_pdesc = let test_pdesc =
Cfg.Procdesc.create cfg (ProcAttributes.default Procname.empty_block !Config.curr_language) in Cfg.create_proc_desc cfg (ProcAttributes.default Procname.empty_block !Config.curr_language) in
let dummy_instr1 = Sil.Remove_temps ([], Location.dummy) in let dummy_instr1 = Sil.Remove_temps ([], Location.dummy) in
let dummy_instr2 = Sil.Abstract Location.dummy in let dummy_instr2 = Sil.Abstract Location.dummy in
let dummy_instr3 = Sil.Remove_temps ([Ident.create_fresh Ident.knormal], Location.dummy) in let dummy_instr3 = Sil.Remove_temps ([Ident.create_fresh Ident.knormal], Location.dummy) in
@ -28,7 +28,7 @@ let tests =
let instrs3 = [dummy_instr4] in let instrs3 = [dummy_instr4] in
let instrs4 = [] in let instrs4 = [] in
let create_node instrs = let create_node instrs =
Cfg.Node.create Location.dummy (Cfg.Node.Stmt_node "") instrs test_pdesc in Cfg.Procdesc.create_node test_pdesc Location.dummy (Cfg.Node.Stmt_node "") instrs in
let n1 = create_node instrs1 in let n1 = create_node instrs1 in
let n2 = create_node instrs2 in let n2 = create_node instrs2 in
let n3 = create_node instrs3 in let n3 = create_node instrs3 in
@ -37,9 +37,9 @@ let tests =
Cfg.Procdesc.set_start_node test_pdesc n1; Cfg.Procdesc.set_start_node test_pdesc n1;
(* let -> represent normal transitions and -*-> represent exceptional transitions *) (* let -> represent normal transitions and -*-> represent exceptional transitions *)
(* creating graph n1 -> n2, n1 -*-> n3, n2 -> n4, n2 -*-> n3, n3 -> n4 , n3 -*> n4 *) (* creating graph n1 -> n2, n1 -*-> n3, n2 -> n4, n2 -*-> n3, n3 -> n4 , n3 -*> n4 *)
Cfg.Node.set_succs_exn test_pdesc n1 [n2] [n3]; Cfg.Procdesc.node_set_succs_exn test_pdesc n1 [n2] [n3];
Cfg.Node.set_succs_exn test_pdesc n2 [n4] [n3]; Cfg.Procdesc.node_set_succs_exn test_pdesc n2 [n4] [n3];
Cfg.Node.set_succs_exn test_pdesc n3 [n4] [n4]; Cfg.Procdesc.node_set_succs_exn test_pdesc n3 [n4] [n4];
let normal_proc_cfg = ProcCfg.Normal.from_pdesc test_pdesc in let normal_proc_cfg = ProcCfg.Normal.from_pdesc test_pdesc in
let exceptional_proc_cfg = ProcCfg.Exceptional.from_pdesc test_pdesc in let exceptional_proc_cfg = ProcCfg.Exceptional.from_pdesc test_pdesc in

Write Preview
Loading…
Cancel
Save