From 70c84946255d030d2bd8c0af46d11edc68d02c62 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Thu, 14 Apr 2016 15:29:51 -0700 Subject: [PATCH] opacify the type of node ids Summary:Make node ids be `private int` to make sure we don't mix them with random integers from other sources. Reviewed By: sblackshear, cristianoc Differential Revision: D3179670 fb-gh-sync-id: 4bcf4f0 fbshipit-source-id: 4bcf4f0 --- infer/src/IR/cfg.ml | 7 ++- infer/src/IR/cfg.mli | 7 ++- infer/src/backend/dotty.ml | 9 ++-- infer/src/backend/errdesc.ml | 4 +- infer/src/backend/interproc.ml | 28 +++++------ infer/src/backend/paths.ml | 13 +++-- infer/src/backend/printer.ml | 50 ++++++++++---------- infer/src/backend/reporting.ml | 4 +- infer/src/backend/specs.ml | 6 +-- infer/src/backend/specs.mli | 6 +-- infer/src/backend/state.ml | 7 +-- infer/src/backend/state.mli | 4 +- infer/src/checkers/checkDeadCode.ml | 2 +- infer/src/checkers/checkTraceCallSequence.ml | 2 +- infer/src/checkers/constantPropagation.ml | 2 +- infer/src/checkers/procCfg.ml | 6 +-- infer/src/clang/cTrans.ml | 2 +- 17 files changed, 86 insertions(+), 73 deletions(-) diff --git a/infer/src/IR/cfg.ml b/infer/src/IR/cfg.ml index e19ab4d5e..167187ffd 100644 --- a/infer/src/IR/cfg.ml +++ b/infer/src/IR/cfg.ml @@ -17,6 +17,8 @@ module F = Format (* =============== START of module Node =============== *) module Node = struct + type id = int + type nodekind = | Start_node of proc_desc | Exit_node of proc_desc @@ -27,7 +29,7 @@ module Node = struct and t = { (** a node *) (** unique id of the node *) - nd_id : int; + nd_id : id; (** distance to the exit node *) mutable nd_dist_exit : int option; @@ -204,6 +206,9 @@ module Node = struct (** Get the unique id of the node *) let get_id node = node.nd_id + (** compare node ids *) + let id_compare = int_compare + let get_succs node = node.nd_succs type node = t diff --git a/infer/src/IR/cfg.mli b/infer/src/IR/cfg.mli index 872395313..3d17182da 100644 --- a/infer/src/IR/cfg.mli +++ b/infer/src/IR/cfg.mli @@ -127,6 +127,8 @@ end module Node : sig type t = node (** type of nodes *) + type id = private int + (** kind of cfg node *) type nodekind = | Start_node of Procdesc.t @@ -192,7 +194,10 @@ module Node : sig val get_exn : t -> t list (** Get the unique id of the node *) - val get_id : t -> int + val get_id : t -> id + + (** compare node ids *) + val id_compare : id -> id -> int (** Get the source location of the node *) val get_loc : t -> Location.t diff --git a/infer/src/backend/dotty.ml b/infer/src/backend/dotty.ml index 337fd8a32..6195035f9 100644 --- a/infer/src/backend/dotty.ml +++ b/infer/src/backend/dotty.ml @@ -924,7 +924,7 @@ let pp_proplist_parsed2dotty_file filename plist = (* channel. You have to compute an interprocedural cfg first *) let pp_cfgnodename fmt (n : Cfg.Node.t) = - F.fprintf fmt "%d" (Cfg.Node.get_id n) + F.fprintf fmt "%d" (Cfg.Node.get_id n :> int) let pp_etlist fmt etl = IList.iter (fun (id, ty) -> @@ -962,7 +962,7 @@ let pp_cfgnodelabel fmt (n : Cfg.Node.t) = let pp_instrs fmt instrs = IList.iter (fun i -> F.fprintf fmt " %s\\n " (instr_string i)) instrs in let instrs = Cfg.Node.get_instrs n in - F.fprintf fmt "%d: %a \\n %a" (Cfg.Node.get_id n) pp_label n pp_instrs instrs + F.fprintf fmt "%d: %a \\n %a" (Cfg.Node.get_id n :> int) pp_label n pp_instrs instrs let pp_cfgnodeshape fmt (n: Cfg.Node.t) = match Cfg.Node.get_kind n with @@ -987,7 +987,10 @@ let pp_cfgnode fmt (n: Cfg.Node.t) = | Cfg.Node.Exit_node _ when is_exn = true -> (* don't print exception edges to the exit node *) () | _ -> - F.fprintf fmt "\n\t %d -> %d %s;" (Cfg.Node.get_id n1) (Cfg.Node.get_id n2) color in + F.fprintf fmt "\n\t %d -> %d %s;" + (Cfg.Node.get_id n1 :> int) + (Cfg.Node.get_id n2 :> int) + color in IList.iter (fun n' -> print_edge n n' false) (Cfg.Node.get_succs n); IList.iter (fun n' -> print_edge n n' true) (Cfg.Node.get_exn n) diff --git a/infer/src/backend/errdesc.ml b/infer/src/backend/errdesc.ml index 8f6ab03ed..26fd92a89 100644 --- a/infer/src/backend/errdesc.ml +++ b/infer/src/backend/errdesc.ml @@ -115,7 +115,7 @@ let find_normal_variable_funcall ("find_normal_variable_funcall could not find " ^ Ident.to_string id ^ " in node " ^ - string_of_int (Cfg.Node.get_id node)); + string_of_int (Cfg.Node.get_id node :> int)); L.d_ln ()); !res @@ -257,7 +257,7 @@ let rec _find_normal_variable_letderef (seen : Sil.ExpSet.t) node id : Sil.dexp ("find_normal_variable_letderef could not find " ^ Ident.to_string id ^ " in node " ^ - string_of_int (Cfg.Node.get_id node)); + string_of_int (Cfg.Node.get_id node :> int)); L.d_ln ()); !res diff --git a/infer/src/backend/interproc.ml b/infer/src/backend/interproc.ml index 31bc28826..370c9f736 100644 --- a/infer/src/backend/interproc.ml +++ b/infer/src/backend/interproc.ml @@ -58,15 +58,12 @@ module NodeVisitSet = (** Table for the results of the join operation on nodes. *) module Join_table : sig type t - type node_id = int - val add : t -> node_id -> Paths.PathSet.t -> unit + val add : t -> Cfg.Node.id -> Paths.PathSet.t -> unit val create : unit -> t - val find : t -> node_id -> Paths.PathSet.t + val find : t -> Cfg.Node.id -> Paths.PathSet.t end = struct - type t = (int, Paths.PathSet.t) Hashtbl.t - - type node_id = int + type t = (Cfg.Node.id, Paths.PathSet.t) Hashtbl.t let create () : t = Hashtbl.create 11 @@ -83,14 +80,12 @@ end module Worklist = struct module NodeMap = Map.Make(Cfg.Node) - type node_id = int - type t = { join_table : Join_table.t; (** Table of join results *) - path_set_todo : (node_id, Paths.PathSet.t) Hashtbl.t; (** Pathset todo *) - path_set_visited : (node_id, Paths.PathSet.t) Hashtbl.t; (** Pathset visited *) + path_set_todo : (Cfg.Node.id, Paths.PathSet.t) Hashtbl.t; (** Pathset todo *) + path_set_visited : (Cfg.Node.id, Paths.PathSet.t) Hashtbl.t; (** Pathset visited *) mutable todo_set : NodeVisitSet.t; (** Set of nodes still to do, with visit count *) - mutable visit_map : node_id NodeMap.t; (** Map from nodes done to visit count *) + mutable visit_map : int NodeMap.t; (** Map from nodes done to visit count *) } let create () = { @@ -132,7 +127,8 @@ let path_set_create_worklist pdesc = Cfg.Procdesc.compute_distance_to_exit_node pdesc; Worklist.create () -let htable_retrieve (htable : (int, Paths.PathSet.t) Hashtbl.t) (key : int) : Paths.PathSet.t = +let htable_retrieve (htable : (Cfg.Node.id, Paths.PathSet.t) Hashtbl.t) (key : Cfg.Node.id) + : Paths.PathSet.t = try Hashtbl.find htable key with Not_found -> @@ -344,7 +340,7 @@ let do_before_node session node = State.set_node node; State.set_session session; L.reset_delayed_prints (); - Printer.node_start_session node loc proc_name session + Printer.node_start_session node loc proc_name (session :> int) let do_after_node node = Printer.node_finish_session node @@ -493,9 +489,9 @@ let mark_visited summary node = let stats = summary.Specs.stats in if !Config.footprint then - stats.Specs.nodes_visited_fp <- IntSet.add node_id stats.Specs.nodes_visited_fp + stats.Specs.nodes_visited_fp <- IntSet.add (node_id :> int) stats.Specs.nodes_visited_fp else - stats.Specs.nodes_visited_re <- IntSet.add node_id stats.Specs.nodes_visited_re + stats.Specs.nodes_visited_re <- IntSet.add (node_id :> int) stats.Specs.nodes_visited_re let forward_tabulate tenv wl = let handled_some_exception = ref false in @@ -549,7 +545,7 @@ let forward_tabulate tenv wl = handled_some_exception := false; check_prop_size pathset_todo; L.d_strln ("**** " ^ (log_string proc_name) ^ " " ^ - "Node: " ^ string_of_int curr_node_id ^ ", " ^ + "Node: " ^ string_of_int (curr_node_id :> int) ^ ", " ^ "Procedure: " ^ Procname.to_string proc_name ^ ", " ^ "Session: " ^ string_of_int session ^ ", " ^ "Todo: " ^ string_of_int (Paths.PathSet.size pathset_todo) ^ " ****"); diff --git a/infer/src/backend/paths.ml b/infer/src/backend/paths.ml index f1bae8ffd..ba03fb5ab 100644 --- a/infer/src/backend/paths.ml +++ b/infer/src/backend/paths.ml @@ -271,7 +271,7 @@ end = struct let get_path_pos node = let pn = Cfg.Procdesc.get_proc_name (Cfg.Node.get_proc_desc node) in let n_id = Cfg.Node.get_id node in - (pn, n_id) + (pn, (n_id :> int)) let contains_position path pos = let found = ref false in @@ -291,10 +291,13 @@ end = struct | Pstart _ -> f level path session prev_exn_opt | Pnode (_, exn_opt, session', p, _, _) -> let next_exn_opt = if prev_exn_opt <> None then None else exn_opt in (* no two consecutive exceptions *) - doit level session' p next_exn_opt; + doit level (session' :> int) p next_exn_opt; f level path session prev_exn_opt | Pjoin (p1, p2, _) -> - if (Invariant.get_stats p1).max_length >= (Invariant.get_stats p2).max_length then doit level session p1 prev_exn_opt else doit level session p2 prev_exn_opt + if (Invariant.get_stats p1).max_length >= (Invariant.get_stats p2).max_length then + doit level session p1 prev_exn_opt + else + doit level session p2 prev_exn_opt | Pcall (p1, _, p2, _) -> let next_exn_opt = None in (* exn must already be inside the call *) doit level session p1 next_exn_opt; @@ -367,7 +370,7 @@ end = struct "linear paths: " ^ string_of_float (Invariant.get_stats path).linear_num ^ " max length: " ^ string_of_int (Invariant.get_stats path).max_length ^ " has repetitions: " ^ string_of_int repetitions ^ - " of node " ^ (string_of_int (Cfg.Node.get_id node)) in + " of node " ^ (string_of_int (Cfg.Node.get_id node :> int)) in Invariant.reset_stats path; str @@ -411,7 +414,7 @@ end = struct | Pstart (node, _) -> F.fprintf fmt "n%a" Cfg.Node.pp node | Pnode (node, _, session, path, _, _) -> - F.fprintf fmt "%a(s%d).n%a" (doit (n - 1)) path session Cfg.Node.pp node + F.fprintf fmt "%a(s%d).n%a" (doit (n - 1)) path (session :> int) Cfg.Node.pp node | Pjoin (path1, path2, _) -> F.fprintf fmt "(%a + %a)" (doit (n - 1)) path1 (doit (n - 1)) path2 | Pcall (path1, _, path2, _) -> diff --git a/infer/src/backend/printer.ml b/infer/src/backend/printer.ml index 0cc5344fb..987844ea6 100644 --- a/infer/src/backend/printer.ml +++ b/infer/src/backend/printer.ml @@ -86,9 +86,9 @@ let node_is_visited node = | Some summary -> let stats = summary.Specs.stats in let is_visited_fp = - IntSet.mem (Cfg.Node.get_id node) stats.Specs.nodes_visited_fp in + IntSet.mem (Cfg.Node.get_id node :> int) stats.Specs.nodes_visited_fp in let is_visited_re = - IntSet.mem (Cfg.Node.get_id node) stats.Specs.nodes_visited_re in + IntSet.mem (Cfg.Node.get_id node :> int) stats.Specs.nodes_visited_re in is_visited_fp, is_visited_re (** Return true if the node was visited during analysis *) @@ -130,24 +130,24 @@ end = struct F.fprintf fmt "
PREDS:@\n"; IList.iter (fun node -> Io_infer.Html.pp_node_link [".."] "" - (IList.map Cfg.Node.get_id (Cfg.Node.get_preds node)) - (IList.map Cfg.Node.get_id (Cfg.Node.get_succs node)) - (IList.map Cfg.Node.get_id (Cfg.Node.get_exn node)) - (is_visited node) false fmt (Cfg.Node.get_id node)) preds; + (IList.map Cfg.Node.get_id (Cfg.Node.get_preds node) :> int list) + (IList.map Cfg.Node.get_id (Cfg.Node.get_succs node) :> int list) + (IList.map Cfg.Node.get_id (Cfg.Node.get_exn node) :> int list) + (is_visited node) false fmt (Cfg.Node.get_id node :> int)) preds; F.fprintf fmt "
SUCCS: @\n"; IList.iter (fun node -> Io_infer.Html.pp_node_link [".."] "" - (IList.map Cfg.Node.get_id (Cfg.Node.get_preds node)) - (IList.map Cfg.Node.get_id (Cfg.Node.get_succs node)) - (IList.map Cfg.Node.get_id (Cfg.Node.get_exn node)) - (is_visited node) false fmt (Cfg.Node.get_id node)) succs; + (IList.map Cfg.Node.get_id (Cfg.Node.get_preds node) :> int list) + (IList.map Cfg.Node.get_id (Cfg.Node.get_succs node) :> int list) + (IList.map Cfg.Node.get_id (Cfg.Node.get_exn node) :> int list) + (is_visited node) false fmt (Cfg.Node.get_id node :> int)) succs; F.fprintf fmt "
EXN: @\n"; IList.iter (fun node -> Io_infer.Html.pp_node_link [".."] "" - (IList.map Cfg.Node.get_id (Cfg.Node.get_preds node)) - (IList.map Cfg.Node.get_id (Cfg.Node.get_succs node)) - (IList.map Cfg.Node.get_id (Cfg.Node.get_exn node)) - (is_visited node) false fmt (Cfg.Node.get_id node)) exn; + (IList.map Cfg.Node.get_id (Cfg.Node.get_preds node) :> int list) + (IList.map Cfg.Node.get_id (Cfg.Node.get_succs node) :> int list) + (IList.map Cfg.Node.get_id (Cfg.Node.get_exn node) :> int list) + (is_visited node) false fmt (Cfg.Node.get_id node :> int)) exn; F.fprintf fmt "
@\n"; F.pp_print_flush fmt (); true @@ -360,7 +360,7 @@ let force_delayed_prints () = let start_session node (loc: Location.t) proc_name session = let node_id = Cfg.Node.get_id node in (if NodesHtml.start_node - node_id loc proc_name + (node_id :> int) loc proc_name (Cfg.Node.get_preds node) (Cfg.Node.get_succs node) (Cfg.Node.get_exn node) @@ -372,7 +372,7 @@ let start_session node (loc: Location.t) proc_name session = F.fprintf !curr_html_formatter "%a%a" Io_infer.Html.pp_hline () (Io_infer.Html.pp_session_link ~with_name: true [".."]) - (node_id, session, loc.Location.line); + ((node_id :> int), session, loc.Location.line); F.fprintf !curr_html_formatter "%a" Io_infer.Html.pp_start_color Black @@ -387,7 +387,7 @@ let node_finish_session node = if !Config.write_html then begin F.fprintf !curr_html_formatter "%a" Io_infer.Html.pp_end_color (); - NodesHtml.finish_node (Cfg.Node.get_id node) + NodesHtml.finish_node (Cfg.Node.get_id node :> int) end (** Write html file for the procedure. @@ -409,10 +409,10 @@ let write_proc_html whole_seconds pdesc = (fun n -> Io_infer.Html.pp_node_link [] (Cfg.Node.get_description (pe_html Black) n) - (IList.map Cfg.Node.get_id (Cfg.Node.get_preds n)) - (IList.map Cfg.Node.get_id (Cfg.Node.get_succs n)) - (IList.map Cfg.Node.get_id (Cfg.Node.get_exn n)) - (is_visited n) false fmt (Cfg.Node.get_id n)) + (IList.map Cfg.Node.get_id (Cfg.Node.get_preds n) :> int list) + (IList.map Cfg.Node.get_id (Cfg.Node.get_succs n) :> int list) + (IList.map Cfg.Node.get_id (Cfg.Node.get_exn n) :> int list) + (is_visited n) false fmt (Cfg.Node.get_id n :> int)) nodes; (match Specs.get_summary pname with | None -> @@ -512,13 +512,13 @@ let write_html_file linereader filename cfg = Io_infer.Html.pp_node_link [fname_encoding] (Cfg.Node.get_description (pe_html Black) n) - (IList.map Cfg.Node.get_id (Cfg.Node.get_preds n)) - (IList.map Cfg.Node.get_id (Cfg.Node.get_succs n)) - (IList.map Cfg.Node.get_id (Cfg.Node.get_exn n)) + (IList.map Cfg.Node.get_id (Cfg.Node.get_preds n) :> int list) + (IList.map Cfg.Node.get_id (Cfg.Node.get_succs n) :> int list) + (IList.map Cfg.Node.get_id (Cfg.Node.get_exn n) :> int list) (is_visited n) isproof fmt - (Cfg.Node.get_id n)) + (Cfg.Node.get_id n :> int)) nodes_at_linenum; IList.iter (fun n -> diff --git a/infer/src/backend/reporting.ml b/infer/src/backend/reporting.ml index 0b01d7b72..3a6c8cbdf 100644 --- a/infer/src/backend/reporting.ml +++ b/infer/src/backend/reporting.ml @@ -37,10 +37,10 @@ let log_issue_from_errlog | None -> State.get_loc () | Some loc -> loc in let node_id = match node_id with - | None -> State.get_node_id_key () + | None -> (State.get_node_id_key () :> int * int) | Some node_id -> node_id in let session = match session with - | None -> State.get_session () + | None -> (State.get_session () :> int) | Some session -> session in let ltr = match ltr with | None -> State.get_loc_trace () diff --git a/infer/src/backend/specs.ml b/infer/src/backend/specs.ml index 340ffc31b..ed148f28d 100644 --- a/infer/src/backend/specs.ml +++ b/infer/src/backend/specs.ml @@ -143,8 +143,8 @@ end module Visitedset = Set.Make (struct - type t = int * int list - let compare (node_id1, _) (node_id2, _) = int_compare node_id1 node_id2 + type t = Cfg.Node.id * int list + let compare (node_id1, _) (node_id2, _) = Cfg.Node.id_compare node_id1 node_id2 end) let visited_str vis = @@ -324,7 +324,7 @@ type payload = type summary = { dependency_map: dependency_map_t; (** maps children procs to timestamp as last seen at the start of an analysys phase for this proc *) - nodes: int list; (** ids of cfg nodes of the procedure *) + nodes: Cfg.Node.id list; (** ids of cfg nodes of the procedure *) phase: phase; (** in FOOTPRINT phase or in RE_EXECUTION PHASE *) payload: payload; (** payload containing the result of some analysis *) sessions: int ref; (** Session number: how many nodes went trough symbolic execution *) diff --git a/infer/src/backend/specs.mli b/infer/src/backend/specs.mli index a7398fbd7..967fedd4c 100644 --- a/infer/src/backend/specs.mli +++ b/infer/src/backend/specs.mli @@ -61,7 +61,7 @@ module Jprop : sig end (** set of visited nodes: node id and list of lines of all the instructions *) -module Visitedset : Set.S with type elt = int * int list +module Visitedset : Set.S with type elt = Cfg.Node.id * int list (** convert a Visitedset to a string *) val visited_str : Visitedset.t -> string @@ -137,7 +137,7 @@ type payload = (** Procedure summary *) type summary = { dependency_map: dependency_map_t; (** maps children procs to timestamp as last seen at the start of an analysys phase for this proc *) - nodes: int list; (** ids of cfg nodes of the procedure *) + nodes: Cfg.Node.id list; (** ids of cfg nodes of the procedure *) phase: phase; (** in FOOTPRINT phase or in RE_EXECUTION PHASE *) payload: payload; (** payload containing the result of some analysis *) sessions: int ref; (** Session number: how many nodes went trough symbolic execution *) @@ -220,7 +220,7 @@ val is_inactive : Procname.t -> bool Do nothing if a summary exists already. *) val init_summary : (Procname.t list * (** depend list *) - int list * (** nodes *) + Cfg.Node.id list * (** nodes *) proc_flags * (** procedure flags *) (Procname.t * Location.t) list * (** calls *) (Cg.in_out_calls option) * (** in and out calls *) diff --git a/infer/src/backend/state.ml b/infer/src/backend/state.ml index b2e15f54d..fc2bfaaa0 100644 --- a/infer/src/backend/state.ml +++ b/infer/src/backend/state.ml @@ -277,7 +277,7 @@ let get_path_pos () = | Some (_, _, pdesc) -> Cfg.Procdesc.get_proc_name pdesc | None -> Procname.from_string_c_fun "unknown_procedure" in let nid = get_node_id () in - (pname, nid) + (pname, (nid :> int)) let mark_execution_start node = let fs = get_failure_stats node in @@ -298,11 +298,12 @@ let mark_instr_ok () = let mark_instr_fail pre_opt exn = let loc = get_loc () in - let key = get_node_id_key () in + let key = (get_node_id_key () :> int * int) in let session = get_session () in let loc_trace = get_loc_trace () in let fs = get_failure_stats (get_node ()) in - if fs.first_failure = None then fs.first_failure <- Some (loc, key, session, loc_trace, pre_opt, exn); + if fs.first_failure = None then + fs.first_failure <- Some (loc, key, (session :> int), loc_trace, pre_opt, exn); fs.instr_fail <- fs.instr_fail + 1 type log_issue = diff --git a/infer/src/backend/state.mli b/infer/src/backend/state.mli index ca08e54ed..705aba8ce 100644 --- a/infer/src/backend/state.mli +++ b/infer/src/backend/state.mli @@ -45,10 +45,10 @@ val get_loc_trace : unit -> Errlog.loc_trace val get_node : unit -> Cfg.Node.t (** Get id of last node seen in symbolic execution *) -val get_node_id : unit -> int +val get_node_id : unit -> Cfg.Node.id (** Get id and key of last node seen in symbolic execution *) -val get_node_id_key : unit -> int * int +val get_node_id_key : unit -> Cfg.Node.id * int (** return the normalized precondition extracted form the last prop seen, if any the abstraction function is a parameter to get around module dependencies *) diff --git a/infer/src/checkers/checkDeadCode.ml b/infer/src/checkers/checkDeadCode.ml index 14f1f38b9..3348310e8 100644 --- a/infer/src/checkers/checkDeadCode.ml +++ b/infer/src/checkers/checkDeadCode.ml @@ -78,7 +78,7 @@ let check_final_state proc_name proc_desc final_s = IList.filter (fun n -> not (Cfg.NodeSet.mem n (State.get_visited final_s))) proc_nodes in let do_node n = let loc = Cfg.Node.get_loc n in - let description = Format.sprintf "Node not visited: %d" (Cfg.Node.get_id n) in + let description = Format.sprintf "Node not visited: %d" (Cfg.Node.get_id n :> int) in let report = match Cfg.Node.get_kind n with | Cfg.Node.Join_node -> false | k when k = Cfg.Node.exn_sink_kind -> false diff --git a/infer/src/checkers/checkTraceCallSequence.ml b/infer/src/checkers/checkTraceCallSequence.ml index bc31d043d..dc744a9f1 100644 --- a/infer/src/checkers/checkTraceCallSequence.ml +++ b/infer/src/checkers/checkTraceCallSequence.ml @@ -303,7 +303,7 @@ end (** State transformation for a cfg node. *) let do_node pn pd idenv _ node (s : State.t) : (State.t list) * (State.t list) = - if verbose then L.stderr "N:%d S:%s@." (Cfg.Node.get_id node) (State.to_string s); + if verbose then L.stderr "N:%d S:%s@." (Cfg.Node.get_id node :> int) (State.to_string s); let curr_state = ref s in diff --git a/infer/src/checkers/constantPropagation.ml b/infer/src/checkers/constantPropagation.ml index 86eff5656..986d55fbd 100644 --- a/infer/src/checkers/constantPropagation.ml +++ b/infer/src/checkers/constantPropagation.ml @@ -112,7 +112,7 @@ module ConstantFlow = Dataflow.MakeDF(struct if verbose then begin - L.stdout "Node %i:" (Cfg.Node.get_id node); + L.stdout "Node %i:" (Cfg.Node.get_id node :> int); L.stdout "%a" pp constants; IList.iter (fun instr -> L.stdout "%a@." (Sil.pp_instr pe_text) instr) diff --git a/infer/src/checkers/procCfg.ml b/infer/src/checkers/procCfg.ml index 112430bd4..5cc03a0c7 100644 --- a/infer/src/checkers/procCfg.ml +++ b/infer/src/checkers/procCfg.ml @@ -48,7 +48,7 @@ end module Forward : Wrapper with type node = Cfg.node = struct type t = Cfg.Procdesc.t type node = Cfg.node - type node_id = int + type node_id = Cfg.Node.id let node_id = Cfg.Node.get_id let succs _ n = Cfg.Node.get_succs n @@ -63,10 +63,10 @@ module Forward : Wrapper with type node = Cfg.node = struct let from_pdesc pdesc = pdesc - let node_id_compare = int_compare + let node_id_compare = Cfg.Node.id_compare let pp_node = Cfg.Node.pp - let pp_node_id fmt n = F.fprintf fmt "%d" n + let pp_node_id fmt (n : Cfg.Node.id) = F.fprintf fmt "%d" (n :> int) end diff --git a/infer/src/clang/cTrans.ml b/infer/src/clang/cTrans.ml index 5edee143a..5af4f7d7a 100644 --- a/infer/src/clang/cTrans.ml +++ b/infer/src/clang/cTrans.ml @@ -1153,7 +1153,7 @@ struct let var_typ = add_reference_if_glvalue typ expr_info in let join_node = create_node (Cfg.Node.Join_node) [] [] sil_loc context in Cfg.Node.set_succs_exn cfg join_node succ_nodes []; - let pvar = mk_temp_var (Cfg.Node.get_id join_node) in + let pvar = mk_temp_var (Cfg.Node.get_id join_node :> int) in let continuation' = mk_cond_continuation trans_state.continuation in let trans_state' = { trans_state with continuation = continuation'; succ_nodes = [] } in let res_trans_cond = exec_with_priority_exception trans_state' cond cond_trans in