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