diff --git a/src/plugins/dive/build.ml b/src/plugins/dive/build.ml
index bef29cb7ace6d40f0300f154b1214d1678525c43..bb310e803a8123e0ae712a0ec7d3107947c804b7 100644
--- a/src/plugins/dive/build.ml
+++ b/src/plugins/dive/build.ml
@@ -197,7 +197,7 @@ let build_node_kind ~is_folded_base lval kinstr =
let default_node_locality callstack =
match callstack with
- | [] ->
+ | [] ->
(* The empty callstack can be used for global lvalues *)
{ loc_file="" ; loc_callstack=[] }
| (kf,_kinstr) :: _ ->
@@ -409,12 +409,12 @@ let build_node_deps context node =
and build_call_deps callstack stmt callee args =
begin match callee.enode with
- | Lval (Var _vi, _offset) -> ()
- | Lval (Mem exp, _offset) ->
- build_exp_deps callstack stmt Callee exp
- | _ ->
- Self.warning "Cannot compute all callee dependencies for %a"
- Cil_printer.pp_stmt stmt;
+ | Lval (Var _vi, _offset) -> ()
+ | Lval (Mem exp, _offset) ->
+ build_exp_deps callstack stmt Callee exp
+ | _ ->
+ Self.warning "Cannot compute all callee dependencies for %a"
+ Cil_printer.pp_stmt stmt;
end;
let kinstr = Kstmt stmt in
let _,set = !Db.Value.expr_to_kernel_function kinstr ~deps:None callee in
@@ -433,7 +433,7 @@ let build_node_deps context node =
| Differing_blocks (e1,e2) -> for_exp e1; for_exp e2
| Memory_access _ | Not_separated _ | Overlap _
| Uninitialized _ | Dangling _ | Uninitialized_union _ -> ()
- (* TODO: adress depencies inside lval *)
+ (* TODO: adress depencies inside lval *)
| Invalid_bool lv -> build_lval_deps callstack stmt Data lv
and build_instr_deps callstack stmt = function
@@ -554,8 +554,8 @@ let explore ~depth context root =
let should_auto_explore node =
let is_root = Graph.Node.equal node root (* the root is always explored *)
and is_intersting_kind = match node.node_kind with
- | Scalar _ | Composite _ | Alarm _ -> true
- | Scattered _ -> false
+ | Scalar _ | Composite _ | Alarm _ -> true
+ | Scattered _ -> false
in
is_root || (not node.node_hidden && is_intersting_kind)
in
@@ -566,16 +566,16 @@ let explore ~depth context root =
let (n,d) = Queue.take queue in
if d < depth then begin
if not (n.node_deps_computed) && should_auto_explore n then
- begin
- begin try
- build_node_deps context n;
- with Too_many_deps ->
- (* TODO: give a mean to explore more dependencies *)
- Self.warning "Too many dependencies for %a ; throwing them out"
- Node_kind.pretty n.node_kind;
+ begin
+ begin try
+ build_node_deps context n;
+ with Too_many_deps ->
+ (* TODO: give a mean to explore more dependencies *)
+ Self.warning "Too many dependencies for %a ; throwing them out"
+ Node_kind.pretty n.node_kind;
+ end;
+ n.node_deps_computed <- true;
end;
- n.node_deps_computed <- true;
- end;
Graph.iter_pred (fun n' -> Queue.add (n',d+1) queue) context.graph n
end;
done
diff --git a/src/plugins/dive/imprecision_graph.ml b/src/plugins/dive/imprecision_graph.ml
index 9efa403a9715b24e7caee60682161d619b1d0895..c6295bc88ec41ae5c187a847f13a4d2515e35228 100644
--- a/src/plugins/dive/imprecision_graph.ml
+++ b/src/plugins/dive/imprecision_graph.ml
@@ -91,7 +91,7 @@ let merge_int_values p1 p2 =
{
values_interval = union_int_interval p1.values_interval p2.values_interval;
values_limits = p1.values_limits;
- values_grade = worst_precision_grade p1.values_grade p2.values_grade;
+ values_grade = worst_precision_grade p1.values_grade p2.values_grade;
}
let merge_float_values p1 p2 =
@@ -100,7 +100,7 @@ let merge_float_values p1 p2 =
{
values_interval = union_float_interval p1.values_interval p2.values_interval;
values_limits = p1.values_limits;
- values_grade = worst_precision_grade p1.values_grade p2.values_grade;
+ values_grade = worst_precision_grade p1.values_grade p2.values_grade;
}
let update_node_int_values node new_values =
@@ -125,7 +125,7 @@ let create_dependency ~allow_folding g v1 dependency_kind v2 =
with Not_found -> None
in
match matching_edge with
- | Some (_,e,_) ->
+ | Some (_,e,_) ->
e.dependency_multiple <- true
| None ->
let e = {
@@ -229,9 +229,9 @@ let ouptput_to_dot out_channel g =
!l
let get_subgraph v =
let {loc_file ; loc_callstack} = v.node_locality in
- match loc_callstack with
- | [] -> Some (get_file_subgraph loc_file)
- | cs -> get_callstack_subgraph cs
+ match loc_callstack with
+ | [] -> Some (get_file_subgraph loc_file)
+ | cs -> get_callstack_subgraph cs
let default_edge_attributes _g = []
let edge_attributes (_v1,e,_v2) =
let kind_attribute = match e.dependency_kind with
@@ -240,7 +240,7 @@ let ouptput_to_dot out_channel g =
and folding_attribute = match e.dependency_multiple with
| true -> [ `Style `Bold ]
| false -> []
- in kind_attribute @ folding_attribute
+ in kind_attribute @ folding_attribute
end)
in
Dot.output_graph out_channel g
@@ -317,20 +317,20 @@ struct
let output_node_float_values values =
`Assoc [
- ("computed", output_float_interval values.values_interval) ;
- ("limits", output_float_interval values.values_limits) ;
- ("grade", output_node_precision_grade values.values_grade) ;
- ]
+ ("computed", output_float_interval values.values_interval) ;
+ ("limits", output_float_interval values.values_limits) ;
+ ("grade", output_node_precision_grade values.values_grade) ;
+ ]
let output_node node =
let label = Pretty_utils.to_string Node_kind.pretty node.node_kind in
`Assoc ([
- ("id", `Int node.node_key) ;
- ("label", `String label) ;
- ("kind", output_node_kind node.node_kind) ;
- ("locality", output_node_locality node.node_locality) ;
- ("explored", `Bool node.node_deps_computed) ;
- ] @
+ ("id", `Int node.node_key) ;
+ ("label", `String label) ;
+ ("kind", output_node_kind node.node_kind) ;
+ ("locality", output_node_locality node.node_locality) ;
+ ("explored", `Bool node.node_deps_computed) ;
+ ] @
begin match node.node_int_values with
| None -> []
| Some node_values ->
diff --git a/src/plugins/dive/main.ml b/src/plugins/dive/main.ml
index e18fc5b0ef82969c0a4b0fe114b27087791aed24..b2a4407c21d7bc0c3db73f30743a22620df8d4a8 100644
--- a/src/plugins/dive/main.ml
+++ b/src/plugins/dive/main.ml
@@ -59,4 +59,3 @@ let main () =
let () =
Db.Main.extend main
-
diff --git a/src/plugins/dive/self.ml b/src/plugins/dive/self.ml
index a93edff327e193c646000824cb87ada6ba30d340..6fcd44e15a52a57b8f42d349cdf7ecebb002e613 100644
--- a/src/plugins/dive/self.ml
+++ b/src/plugins/dive/self.ml
@@ -68,7 +68,7 @@ struct
let function_name = Str.matched_group 1 s
and variable_name = Str.matched_group 2 s in
let kf = try Globals.Functions.find_by_name function_name
- with Not_found ->
+ with Not_found ->
raise (Cannot_build ("no function '" ^ function_name ^ "'"))
in
try Globals.Vars.find_from_astinfo variable_name (VLocal kf)
@@ -100,12 +100,12 @@ module type Varinfo_set = Parameter_sig.Set
module Varinfo_set (X: Parameter_sig.Input_with_arg) =
Make_set
- (Varinfo)
- (struct
- include X
- let dependencies = []
- let default = Cil_datatype.Varinfo.Set.empty
- end)
+ (Varinfo)
+ (struct
+ include X
+ let dependencies = []
+ let default = Cil_datatype.Varinfo.Set.empty
+ end)
module FromBases = Varinfo_set
(struct
diff --git a/src/plugins/dive/simple_deps.ml b/src/plugins/dive/simple_deps.ml
index 8baa89672fc3b8e173529be322bedb121200facf..f67f9e05d8153849c79969d1faae473b2f58d6a6 100644
--- a/src/plugins/dive/simple_deps.ml
+++ b/src/plugins/dive/simple_deps.ml
@@ -44,7 +44,7 @@ class find_write target_vi = object (self)
end;
Cil.SkipChildren
- method result = res
+ method result = res
end
let find_assignments kf vi =