diff --git a/src/plugins/pdg/api.ml b/src/plugins/pdg/api.ml
index 2dcc57f4a5c8126f0d553176daf8f57559e37333..6f6df8d3b0a4987dd8b32a4feb3d7cd3ca020564 100644
--- a/src/plugins/pdg/api.ml
+++ b/src/plugins/pdg/api.ml
@@ -70,7 +70,7 @@ let find_fun_variant_nodes = Annot.find_fun_variant_nodes
let find_call_out_nodes_to_select = Sets.find_call_out_nodes_to_select
let find_in_nodes_to_select_for_this_call =
- Sets.find_in_nodes_to_select_for_this_call
+ Sets.find_in_nodes_to_select_for_this_call
(**************************************************************************)
diff --git a/src/plugins/pdg/api.mli b/src/plugins/pdg/api.mli
index c0a8fcf858c1d78103b5b166178774c58abad318..89b6912d3f1bfa8bc154de77f8ccc33ceb35bfcf 100644
--- a/src/plugins/pdg/api.mli
+++ b/src/plugins/pdg/api.mli
@@ -221,7 +221,7 @@ val find_fun_variant_nodes : t -> Cil_types.term ->
they use polymorphic types. **)
val find_call_out_nodes_to_select :
- t -> PdgTypes.NodeSet.t -> t -> Cil_types.stmt -> PdgTypes.Node.t list
+ t -> PdgTypes.NodeSet.t -> t -> Cil_types.stmt -> PdgTypes.Node.t list
(** [find_call_out_nodes_to_select pdg_called called_selected_nodes
pdg_caller call_stmt]
@return the call outputs nodes [out] such that
@@ -229,7 +229,7 @@ val find_call_out_nodes_to_select :
intersects [called_selected_nodes]. *)
val find_in_nodes_to_select_for_this_call :
- t -> PdgTypes.NodeSet.t -> Cil_types.stmt -> t -> PdgTypes.Node.t list
+ t -> PdgTypes.NodeSet.t -> Cil_types.stmt -> t -> PdgTypes.Node.t list
(** [find_in_nodes_to_select_for_this_call
pdg_caller caller_selected_nodes call_stmt pdg_called]
@return the called input nodes such that the corresponding nodes
diff --git a/src/plugins/wp/tests/wp_bts/bts_1586.i b/src/plugins/wp/tests/wp_bts/bts_1586.i
index dab7fc01fe3489960e604ec1a582048561820a0e..510137770e7c34d8dcec9e29899e910519cbaa7e 100644
--- a/src/plugins/wp/tests/wp_bts/bts_1586.i
+++ b/src/plugins/wp/tests/wp_bts/bts_1586.i
@@ -1,54 +1,54 @@
-
-/*@ behavior Bizarre:
- assumes x;
- ensures TRANS: x ==> \result==1 ;
- */
-int compute_bizarre(int x)
-{
- if (x)
- return 1;
- else
- return 2;
-}
-
-/*@ behavior Normal:
- assumes x;
- ensures TRANS: x <==> \result==1 ;
- */
-int compute_normal(int x)
-{
- if (x)
- return 1;
- else
- return 2;
-}
-
-int main_bizarre_KO(int x)
-{
- int trans = compute_bizarre(x);
-
- switch(trans) {
- case 0:
- //@ assert FALSE: \false;
- return -1;
- break;
- default:
- return -1;
- break;
- }
-}
-
-int main_normal_KO(int x)
-{
- int trans = compute_normal(x);
-
- switch(trans) {
- case 0:
- //@ assert FALSE: \false;
- return -1;
- break;
- default:
- return -1;
- break;
- }
-}
+
+/*@ behavior Bizarre:
+ assumes x;
+ ensures TRANS: x ==> \result==1 ;
+ */
+int compute_bizarre(int x)
+{
+ if (x)
+ return 1;
+ else
+ return 2;
+}
+
+/*@ behavior Normal:
+ assumes x;
+ ensures TRANS: x <==> \result==1 ;
+ */
+int compute_normal(int x)
+{
+ if (x)
+ return 1;
+ else
+ return 2;
+}
+
+int main_bizarre_KO(int x)
+{
+ int trans = compute_bizarre(x);
+
+ switch(trans) {
+ case 0:
+ //@ assert FALSE: \false;
+ return -1;
+ break;
+ default:
+ return -1;
+ break;
+ }
+}
+
+int main_normal_KO(int x)
+{
+ int trans = compute_normal(x);
+
+ switch(trans) {
+ case 0:
+ //@ assert FALSE: \false;
+ return -1;
+ break;
+ default:
+ return -1;
+ break;
+ }
+}
diff --git a/src/plugins/wp/tests/wp_bts/ergo_typecheck.i b/src/plugins/wp/tests/wp_bts/ergo_typecheck.i
index 27786043f20fd6d2e90613e767fd3de0deed156c..3a05b9220dd03e2b1b1444e202df0a8a79ab2978 100644
--- a/src/plugins/wp/tests/wp_bts/ergo_typecheck.i
+++ b/src/plugins/wp/tests/wp_bts/ergo_typecheck.i
@@ -1,44 +1,44 @@
-typedef struct
-{
- unsigned int a[2];
- unsigned int b[2];
- unsigned int c;
-} my_type;
-
-my_type var = {0};
-
-/*@
- @ ensures var_divded : var == {\old(var) \with
- @ .a = {\old(var.a) \with
- @ [0] = (unsigned int) 0,
- @ [1] = (unsigned int) 1},
- @ .b = {\old(var.b) \with
- @ [0] = (unsigned int)(\old(var.b[0]) + 1),
- @ [1] = (unsigned int)(\old(var.b[1]) + 2)},
- @ .c = (unsigned int) 5
- @ };
- @
- @ ensures var_inline : var == {\old(var) \with
- @ .a[0] = (unsigned int) 0,
- @ .a[1] = (unsigned int) 1,
- @ .b[0] = (unsigned int)(\old(var.b[0]) + 1),
- @ .b[1] = (unsigned int)(\old(var.b[1]) + 2),
- @ .c = (unsigned int) 5
- @ };
- @
- @ ensures var_unit0 : var.a[0] == 0;
- @ ensures var_unit1 : var.a[1] == 1;
- @ ensures var_unit2 : var.b[0] == (unsigned int)(\old(var.b[0]) + 1);
- @ ensures var_unit3 : var.b[1] == (unsigned int)(\old(var.b[1]) + 2);
- @ ensures var_unit4 : var.c == 5;
- @ assigns var;
- @
- */
-void f()
-{
- var.a[0] = 0u;
- var.a[1] = 1u;
- var.b[0] ++;
- var.b[1] += 2;
- var.c = 5u;
-}
+typedef struct
+{
+ unsigned int a[2];
+ unsigned int b[2];
+ unsigned int c;
+} my_type;
+
+my_type var = {0};
+
+/*@
+ @ ensures var_divded : var == {\old(var) \with
+ @ .a = {\old(var.a) \with
+ @ [0] = (unsigned int) 0,
+ @ [1] = (unsigned int) 1},
+ @ .b = {\old(var.b) \with
+ @ [0] = (unsigned int)(\old(var.b[0]) + 1),
+ @ [1] = (unsigned int)(\old(var.b[1]) + 2)},
+ @ .c = (unsigned int) 5
+ @ };
+ @
+ @ ensures var_inline : var == {\old(var) \with
+ @ .a[0] = (unsigned int) 0,
+ @ .a[1] = (unsigned int) 1,
+ @ .b[0] = (unsigned int)(\old(var.b[0]) + 1),
+ @ .b[1] = (unsigned int)(\old(var.b[1]) + 2),
+ @ .c = (unsigned int) 5
+ @ };
+ @
+ @ ensures var_unit0 : var.a[0] == 0;
+ @ ensures var_unit1 : var.a[1] == 1;
+ @ ensures var_unit2 : var.b[0] == (unsigned int)(\old(var.b[0]) + 1);
+ @ ensures var_unit3 : var.b[1] == (unsigned int)(\old(var.b[1]) + 2);
+ @ ensures var_unit4 : var.c == 5;
+ @ assigns var;
+ @
+ */
+void f()
+{
+ var.a[0] = 0u;
+ var.a[1] = 1u;
+ var.b[0] ++;
+ var.b[1] += 2;
+ var.c = 5u;
+}
diff --git a/tests/pdg/sets.ml b/tests/pdg/sets.ml
index 8ebb56e106c19aca5a76f2a18d0001e7fdd14fd8..23c627b3a5bb207fb6a40a3d1ec5fcd793dfbe3e 100644
--- a/tests/pdg/sets.ml
+++ b/tests/pdg/sets.ml
@@ -1,57 +1,57 @@
-open Cil_types;;
-
-let pp_nodes msg nodes =
- Kernel.result "%s" msg ;
- List.iter (fun n -> Kernel.result "%a" (Pdg.Api.pretty_node false) n) nodes;;
-
-exception Find of varinfo;;
-
-let main _ =
- let f = Globals.Functions.find_by_name "f" in
- let pdg = Pdg.Api.get f in
-
- (* Uncomment to retrieve sid *)
- (*Kernel.Debug.set 1;;
- Format.eprintf "@[%a@]@." Printer.pp_global (Kernel_function.get_global f);;
- *)
- (*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
- let stmt_1 = fst (Kernel_function.find_from_sid 1) in (* y = 0 *)
- let node = Pdg.Api.find_stmt_node pdg stmt_1 in
- let nodes = Pdg.Api.all_uses pdg [node] in
- pp_nodes "Test [all_uses] stmt1" nodes;
-
- (*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
- let y =
- try
- Globals.Vars.iter (fun v _ -> if v.vname = "y" then raise (Find v));
- assert false
- with Find v ->
- v
- in
-
- let y_zone = Locations.(enumerate_valid_bits Read (loc_of_varinfo y)) in
- let y_at_11_nodes, undef = (* y=5 *)
- Pdg.Api.find_location_nodes_at_stmt
- pdg (fst (Kernel_function.find_from_sid 11)) ~before:false y_zone
- in
-
- assert (undef = None);
- let y_at_11_nodes = List.map (fun (n,_z) -> n) y_at_11_nodes in
-
- let () = pp_nodes "Test [find_location_nodes_at_stmt] y@11" y_at_11_nodes in
- (*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
- let nodes = Pdg.Api.all_dpds pdg y_at_11_nodes in
- let () = pp_nodes "Test [all_dpds] y@11" nodes in
- (*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
- let nodes = Pdg.Api.all_uses pdg y_at_11_nodes in
- let () = pp_nodes "Test [all_uses] y@11" nodes in
- (*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
- let all_related_nodes pdg =
- let all n = (Pdg.Api.direct_uses pdg n) @ (Pdg.Api.direct_dpds pdg n) in
- Pdg.Api.custom_related_nodes all
- in
- let nodes = all_related_nodes pdg y_at_11_nodes in
- pp_nodes "Test [all_related_nodes] y@11" nodes
-(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
-
-let () = Db.Main.extend main
+open Cil_types;;
+
+let pp_nodes msg nodes =
+ Kernel.result "%s" msg ;
+ List.iter (fun n -> Kernel.result "%a" (Pdg.Api.pretty_node false) n) nodes;;
+
+exception Find of varinfo;;
+
+let main _ =
+ let f = Globals.Functions.find_by_name "f" in
+ let pdg = Pdg.Api.get f in
+
+ (* Uncomment to retrieve sid *)
+ (*Kernel.Debug.set 1;;
+ Format.eprintf "@[%a@]@." Printer.pp_global (Kernel_function.get_global f);;
+ *)
+ (*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
+ let stmt_1 = fst (Kernel_function.find_from_sid 1) in (* y = 0 *)
+ let node = Pdg.Api.find_stmt_node pdg stmt_1 in
+ let nodes = Pdg.Api.all_uses pdg [node] in
+ pp_nodes "Test [all_uses] stmt1" nodes;
+
+ (*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
+ let y =
+ try
+ Globals.Vars.iter (fun v _ -> if v.vname = "y" then raise (Find v));
+ assert false
+ with Find v ->
+ v
+ in
+
+ let y_zone = Locations.(enumerate_valid_bits Read (loc_of_varinfo y)) in
+ let y_at_11_nodes, undef = (* y=5 *)
+ Pdg.Api.find_location_nodes_at_stmt
+ pdg (fst (Kernel_function.find_from_sid 11)) ~before:false y_zone
+ in
+
+ assert (undef = None);
+ let y_at_11_nodes = List.map (fun (n,_z) -> n) y_at_11_nodes in
+
+ let () = pp_nodes "Test [find_location_nodes_at_stmt] y@11" y_at_11_nodes in
+ (*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
+ let nodes = Pdg.Api.all_dpds pdg y_at_11_nodes in
+ let () = pp_nodes "Test [all_dpds] y@11" nodes in
+ (*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
+ let nodes = Pdg.Api.all_uses pdg y_at_11_nodes in
+ let () = pp_nodes "Test [all_uses] y@11" nodes in
+ (*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
+ let all_related_nodes pdg =
+ let all n = (Pdg.Api.direct_uses pdg n) @ (Pdg.Api.direct_dpds pdg n) in
+ Pdg.Api.custom_related_nodes all
+ in
+ let nodes = all_related_nodes pdg y_at_11_nodes in
+ pp_nodes "Test [all_related_nodes] y@11" nodes
+(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
+
+let () = Db.Main.extend main
diff --git a/tests/spec/const_ptr_bts1729.i b/tests/spec/const_ptr_bts1729.i
index e2231335e0454d2586897f1552b3eac698e88e87..cb6ef2c2f0fe442b5bcd69f4714ec14f65cd0c73 100644
--- a/tests/spec/const_ptr_bts1729.i
+++ b/tests/spec/const_ptr_bts1729.i
@@ -1,4 +1,4 @@
-
-static void elem_size(void) {
- //@ assert \valid_read((char const * const *)0);
-}
+
+static void elem_size(void) {
+ //@ assert \valid_read((char const * const *)0);
+}
diff --git a/tests/syntax/copy_visitor_bts_1073_bis.ml b/tests/syntax/copy_visitor_bts_1073_bis.ml
index d26b1010abf5ca0abdc6ed8c1f089c43bc39291c..7f6abc845200d0eceff40365c3c812cd702b3632 100644
--- a/tests/syntax/copy_visitor_bts_1073_bis.ml
+++ b/tests/syntax/copy_visitor_bts_1073_bis.ml
@@ -1,55 +1,55 @@
-(*============================================================================*)
-module P = Plugin.Register
- (struct
- let name = "Testing plugin"
- let shortname = "test"
- let help = "Just to test Filter..."
- end)
-module Opt = P.False
- (struct
- let option_name = "-test"
- let help = "switch the plug-in on"
- end)
-(*============================================================================*)
-module Visi = struct
- exception EraseAssigns
- exception EraseAllocation
+(*============================================================================*)
+module P = Plugin.Register
+ (struct
+ let name = "Testing plugin"
+ let shortname = "test"
+ let help = "Just to test Filter..."
+ end)
+module Opt = P.False
+ (struct
+ let option_name = "-test"
+ let help = "switch the plug-in on"
+ end)
+(*============================================================================*)
+module Visi = struct
+ exception EraseAssigns
+ exception EraseAllocation
- type fct = unit
- type proj = unit
+ type fct = unit
+ type proj = unit
- let fct_name vf _fi = vf.Cil_types.vname
- let fct_info () _ = [ () ]
- let param_visible _ _ = true
- let body_visible _fi = true
- let loc_var_visible _ _ = true
- let inst_visible _ _ = true
- let label_visible _ _ _ = true
- let annotation_visible _ _ _ = true
- let fun_precond_visible _ _ = true
- let fun_postcond_visible _ _ = true
- let fun_variant_visible _ _ = true
- let fun_frees_visible _ _ = true
- let fun_allocates_visible _ _ = true
- let fun_assign_visible _ _ = true
- let fun_deps_visible _ _ = true
- let called_info _ _ = None
- let res_call_visible _ _ = true
- let result_visible _ _ = true
- let cond_edge_visible _ _ = true, true
-end
-(*============================================================================*)
-let main () =
- if Opt.get () then
- begin
- let _ast = Ast.get () in
- P.feedback "start compute";
- let new_proj_name = "filtered" in
- let module Transform = Filter.F (Visi) in
- let new_prj = Transform.build_cil_file new_proj_name () in
- Project.on new_prj Opt.clear ();
- P.feedback "exported in new project : %s" new_proj_name
- end
+ let fct_name vf _fi = vf.Cil_types.vname
+ let fct_info () _ = [ () ]
+ let param_visible _ _ = true
+ let body_visible _fi = true
+ let loc_var_visible _ _ = true
+ let inst_visible _ _ = true
+ let label_visible _ _ _ = true
+ let annotation_visible _ _ _ = true
+ let fun_precond_visible _ _ = true
+ let fun_postcond_visible _ _ = true
+ let fun_variant_visible _ _ = true
+ let fun_frees_visible _ _ = true
+ let fun_allocates_visible _ _ = true
+ let fun_assign_visible _ _ = true
+ let fun_deps_visible _ _ = true
+ let called_info _ _ = None
+ let res_call_visible _ _ = true
+ let result_visible _ _ = true
+ let cond_edge_visible _ _ = true, true
+end
+(*============================================================================*)
+let main () =
+ if Opt.get () then
+ begin
+ let _ast = Ast.get () in
+ P.feedback "start compute";
+ let new_proj_name = "filtered" in
+ let module Transform = Filter.F (Visi) in
+ let new_prj = Transform.build_cil_file new_proj_name () in
+ Project.on new_prj Opt.clear ();
+ P.feedback "exported in new project : %s" new_proj_name
+ end
-let () = Db.Main.extend main
-(*============================================================================*)
+let () = Db.Main.extend main
+(*============================================================================*)
diff --git a/tests/syntax/duplicated_global_bts1129.i b/tests/syntax/duplicated_global_bts1129.i
index b95f7dfed63c40ac468c5af75edf3b4f1d7ef84b..b8ac93ff233a19e3dcd95c1d12e7297ff4c9668e 100644
--- a/tests/syntax/duplicated_global_bts1129.i
+++ b/tests/syntax/duplicated_global_bts1129.i
@@ -1,7 +1,7 @@
-void f(int* x);
-
-void f(int* x) { *x++; }
-
-int X;
-//@ ensures X==1;
-void f(int* x);
+void f(int* x);
+
+void f(int* x) { *x++; }
+
+int X;
+//@ ensures X==1;
+void f(int* x);