@ -53,71 +53,6 @@ let iter_all_nodes ?(sorted= false) cfg ~f =
| > List . iter ~ f : ( fun ( _ , d , n ) -> f d n )
| > List . iter ~ f : ( fun ( _ , d , n ) -> f d n )
let proc_cfg_broken_for_node proc_desc =
let is_exit_node n =
match Procdesc . Node . get_kind n with Procdesc . Node . Exit_node _ -> true | _ -> false
in
let is_between_join_and_exit_node n =
match Procdesc . Node . get_kind n with
| Procdesc . Node . Stmt_node " between_join_and_exit " | Procdesc . Node . Stmt_node " Destruction " -> (
match Procdesc . Node . get_succs n with [ n' ] when is_exit_node n' -> true | _ -> false )
| _ ->
false
in
let rec is_consecutive_join_nodes n visited =
match Procdesc . Node . get_kind n with
| Procdesc . Node . Join_node
-> (
if Procdesc . NodeSet . mem n visited then false
else
let succs = Procdesc . Node . get_succs n in
match succs with
| [ n' ] ->
is_consecutive_join_nodes n' ( Procdesc . NodeSet . add n visited )
| _ ->
false )
| _ ->
is_between_join_and_exit_node n
in
let find_broken_node n =
let succs = Procdesc . Node . get_succs n in
let preds = Procdesc . Node . get_preds n in
match Procdesc . Node . get_kind n with
| Procdesc . Node . Start_node _ ->
if List . is_empty succs | | not ( List . is_empty preds ) then Some ` Other else None
| Procdesc . Node . Exit_node _ ->
if not ( List . is_empty succs ) | | List . is_empty preds then Some ` Other else None
| Procdesc . Node . Stmt_node _ | Procdesc . Node . Prune_node _ | Procdesc . Node . Skip_node _ ->
if List . is_empty succs | | List . is_empty preds then Some ` Other else None
| Procdesc . Node . Join_node ->
(* Join node has the exception that it may be without predecessors
and pointing to between_join_and_exit which points to an exit node .
This happens when the if branches end with a return .
Nested if statements , where all branches have return statements ,
introduce a sequence of join nodes * )
if
( List . is_empty preds && not ( is_consecutive_join_nodes n Procdesc . NodeSet . empty ) )
| | ( not ( List . is_empty preds ) && List . is_empty succs )
then Some ` Join
else None
in
let rec find_first_broken nodes res_broken_node =
match nodes with
| [] ->
res_broken_node
| n :: nodes' ->
let broken_node = find_broken_node n in
match broken_node with
| None ->
find_first_broken nodes' res_broken_node
| Some ` Join ->
find_first_broken nodes' broken_node
| Some ` Other ->
broken_node
in
find_first_broken ( Procdesc . get_nodes proc_desc ) None
let load_statement =
let load_statement =
ResultsDatabase . register_statement " SELECT cfgs FROM source_files WHERE source_file = :k "
ResultsDatabase . register_statement " SELECT cfgs FROM source_files WHERE source_file = :k "