diff --git a/.git-blame-ignore-revs b/.git-blame-ignore-revs
index 3196956b2af09a6bee69aae4c36836f0a84d489c..279efd6d84f6d50d28ca9a6bf8a2431ba7bf6016 100644
--- a/.git-blame-ignore-revs
+++ b/.git-blame-ignore-revs
@@ -31,3 +31,4 @@ dc99367c8f4a95d53ec7ce6187892b91fbfd4c1f
0e05285bd47c752f57c190683608527599fa5afb
a767fdcb7adda81a5ef192733ef7c62fd56b30e2
4130bab7a8b59d0c94a22d792b2a7d5a26d3484d
+6cc1a6f2036b75c6b2451518ffbfbe025eb1a1f8
diff --git a/Makefile b/Makefile
index 422f3709cbabf495152eeb0e5d56ae39d225388e..d623999aff5a7a242d2178e6024abcdb8528b33c 100644
--- a/Makefile
+++ b/Makefile
@@ -1810,11 +1810,12 @@ ifneq ($(strip $(ML_LINT_MISSING)),)
exit 1
endif
-INDENT_TARGET= $(patsubst %,%.indent,$(ML_LINT_CHECK))
+ML_LINT_CHECK_LIST=$(wildcard $(ML_LINT_CHECK))
+INDENT_TARGET= $(patsubst %,%.indent,$(ML_LINT_CHECK_LIST))
-LINT_TARGET= $(patsubst %,%.lint,$(ML_LINT_CHECK))
+LINT_TARGET= $(patsubst %,%.lint,$(ML_LINT_CHECK_LIST))
-FIX_SYNTAX_TARGET=$(patsubst %,%.fix-syntax,$(ML_LINT_CHECK))
+FIX_SYNTAX_TARGET=$(patsubst %,%.fix-syntax,$(ML_LINT_CHECK_LIST))
.PHONY: $(INDENT_TARGET) $(LINT_TARGET) $(FIX_SYNTAX_TARGET) \
indent lint fix-syntax
diff --git a/devel_tools/size.ml b/devel_tools/size.ml
index e73417a893eb05620619b34deb42aac98a73276c..bd24feec4f33c718189a759be496d3abe39047f6 100644
--- a/devel_tools/size.ml
+++ b/devel_tools/size.ml
@@ -25,12 +25,12 @@ open Obj
external address_of_value: 'a -> int = "address_of_value"
module H = Hashtbl.Make(
- struct
- type t = Obj.t
- let equal = (==)
+ struct
+ type t = Obj.t
+ let equal = (==)
let hash = address_of_value
end)
-
+
let node_table = (H.create 257 : unit H.t)
let in_table o = try H.find node_table o; true with Not_found -> false
@@ -53,19 +53,19 @@ let rec traverse t =
let n = size t in
let tag = tag t in
if tag < no_scan_tag then begin
- count := !count + 1 + n;
- for i = 0 to n - 1 do
- let f = field t i in
- if is_block f then traverse f
- done
+ count := !count + 1 + n;
+ for i = 0 to n - 1 do
+ let f = field t i in
+ if is_block f then traverse f
+ done
end else if tag = string_tag then
- count := !count + 1 + n
+ count := !count + 1 + n
else if tag = double_tag then
- count := !count + size_of_double
+ count := !count + size_of_double
else if tag = double_array_tag then
- count := !count + 1 + size_of_double * n
+ count := !count + 1 + size_of_double * n
else
- incr count
+ incr count
end
end
@@ -86,10 +86,8 @@ let size_w ?except o =
count := 0;
traverse (repr o);
res ()
-
+
let size_b ?except o = (size_w ?except o) * (Sys.word_size / 8)
let size_kb ?except o = (size_w ?except o) / (8192 / Sys.word_size)
-
-
diff --git a/devel_tools/size.mli b/devel_tools/size.mli
index 037d5b4a707c50988c444da0c7179ff193cc5a3a..9d67f0a8da54ae7c88ff0d3e5fa369503bb1d7a2 100644
--- a/devel_tools/size.mli
+++ b/devel_tools/size.mli
@@ -18,7 +18,7 @@
(*i $Id: size.mli,v 1.1 2007-11-28 12:52:04 uid568 Exp $ i*)
-(* Sizes of ocaml values (in their memory representation).
+(* Sizes of ocaml values (in their memory representation).
Sizes are given in words ([size_w]), bytes ([size_b]) or kilobytes
([size_kb]), in a system-independent way. *)
diff --git a/devel_tools/size_states.ml b/devel_tools/size_states.ml
index 36bd41b32ca057fa5d9d3866d5406ffc5bc638e7..2cdec788b99c6ab76f53c26f12003c31c5e116ed 100644
--- a/devel_tools/size_states.ml
+++ b/devel_tools/size_states.ml
@@ -23,9 +23,9 @@ open Obj
external address_of_value: 'a -> int = "address_of_value"
module H = Hashtbl.Make(
- struct
- type t = Obj.t
- let equal = (==)
+ struct
+ type t = Obj.t
+ let equal = (==)
let hash = address_of_value
end)
@@ -57,19 +57,19 @@ let rec traverse t =
let n = size t in
let tag = tag t in
if tag < no_scan_tag then begin
- count := !count + 1 + n;
- for i = 0 to n - 1 do
- let f = field t i in
- if is_block f then traverse f
- done
+ count := !count + 1 + n;
+ for i = 0 to n - 1 do
+ let f = field t i in
+ if is_block f then traverse f
+ done
end else if tag = string_tag then
- count := !count + 1 + n
+ count := !count + 1 + n
else if tag = double_tag then
- count := !count + size_of_double
+ count := !count + size_of_double
else if tag = double_array_tag then
- count := !count + 1 + size_of_double * n
+ count := !count + 1 + size_of_double * n
else
- incr count
+ incr count
end
end
@@ -108,5 +108,5 @@ let all_sizes () =
let pp fmt (size, name) = Format.fprintf fmt "@[%d kW, %s@]" size name in
Kernel.result "## Sizes ##@.%a"
(Pretty_utils.pp_list ~pre:"@[<v>" ~suf:"@]" ~sep:"@ " pp) res
-
+
let () = Db.Main.extend all_sizes
diff --git a/src/plugins/report/tests/report/one_hyp.ml b/src/plugins/report/tests/report/one_hyp.ml
index 7ee46906e36c0e49e9fc580d1531176baf6d87a1..e8c5b05c742e6e397fb98694cafe65358a78b6e8 100644
--- a/src/plugins/report/tests/report/one_hyp.ml
+++ b/src/plugins/report/tests/report/one_hyp.ml
@@ -1,13 +1,13 @@
open Cil_types
-let emitter =
+let emitter =
Emitter.create "Test" [ Emitter.Property_status ] ~correctness:[] ~tuning:[]
-let emitter2 =
+let emitter2 =
Emitter.create "Test2" [ Emitter.Property_status ] ~correctness:[] ~tuning:[]
let set_status ?(emitter=emitter) p hyps s =
- Kernel.feedback "SETTING STATUS OF %a TO %a"
+ Kernel.feedback "SETTING STATUS OF %a TO %a"
Property.pretty p
Property_status.Emitted_status.pretty s;
Property_status.emit emitter p ~hyps s
@@ -15,7 +15,7 @@ let set_status ?(emitter=emitter) p hyps s =
let print_status =
Dynamic.get
~plugin:"Report"
- "print"
+ "print"
(Datatype.func Datatype.unit Datatype.unit)
let clear () =
@@ -30,13 +30,13 @@ let main () =
let main, _, _, h, g =
let l =
Annotations.fold_all_code_annot
- (fun stmt _ ca acc ->
- let kf = Kernel_function.find_englobing_kf stmt in
- let ps = Property.ip_of_code_annot kf stmt ca in
- match ps with
- | [ p ] -> p :: acc
- | _ -> assert false)
- []
+ (fun stmt _ ca acc ->
+ let kf = Kernel_function.find_englobing_kf stmt in
+ let ps = Property.ip_of_code_annot kf stmt ca in
+ match ps with
+ | [ p ] -> p :: acc
+ | _ -> assert false)
+ []
in
match l with
| [ p1; p2; p3; p4; p5 ] -> p1, p2, p3, p4, p5
@@ -223,4 +223,3 @@ let main () =
()
let () = Db.Main.extend main
-
diff --git a/src/plugins/report/tests/report/projectified_status.ml b/src/plugins/report/tests/report/projectified_status.ml
index 986d3a2a2e01effd514621ac90224e668a2d9c61..643fbd6057e6cd512bce729b09b029f65113d122 100644
--- a/src/plugins/report/tests/report/projectified_status.ml
+++ b/src/plugins/report/tests/report/projectified_status.ml
@@ -1,21 +1,21 @@
-let emitter =
+let emitter =
Emitter.create
- "Test"
- [ Emitter.Property_status ]
- ~correctness:[ Kernel.LibEntry.parameter ]
+ "Test"
+ [ Emitter.Property_status ]
+ ~correctness:[ Kernel.LibEntry.parameter ]
~tuning:[ Kernel.SafeArrays.parameter ]
let set_status s =
Annotations.iter_all_code_annot
(fun stmt _ ca ->
- let kf = Kernel_function.find_englobing_kf stmt in
- let ps = Property.ip_of_code_annot kf stmt ca in
- List.iter (fun p -> Property_status.emit emitter p ~hyps:[] s) ps)
+ let kf = Kernel_function.find_englobing_kf stmt in
+ let ps = Property.ip_of_code_annot kf stmt ca in
+ List.iter (fun p -> Property_status.emit emitter p ~hyps:[] s) ps)
let print_status =
Dynamic.get
~plugin:"Report"
- "print"
+ "print"
(Datatype.func Datatype.unit Datatype.unit)
let main () =
@@ -40,7 +40,7 @@ let main () =
set_status Property_status.False_and_reachable;
print_status ();
Kernel.feedback "CHANGING DEFAULT PROJECT TO p";
- Project.set_current p;
+ Project.set_current p;
print_status ();
Kernel.feedback "SETTING A CORRECTNESS PARAMETER";
Kernel.LibEntry.on ();
diff --git a/tests/cil/Change_formals.ml b/tests/cil/Change_formals.ml
index 3ed509cbbe9a90d0a789d62f77eacd24e0df3140..f224e4bcfca28421dbd9967f5624a0e485d8cccb 100644
--- a/tests/cil/Change_formals.ml
+++ b/tests/cil/Change_formals.ml
@@ -2,89 +2,89 @@ open Cil_types
module Options =
Plugin.Register(struct let name = "Test"
- let shortname= "test"
- let help = "test" end)
-
+ let shortname= "test"
+ let help = "test" end)
+
class transform prj = object(_self)
- inherit Visitor.frama_c_copy prj
-
+ inherit Visitor.frama_c_copy prj
+
method! vglob_aux = function
- | GFun (_fdec, _loc) as g ->
+ | GFun (_fdec, _loc) as g ->
let mk_formal = function l -> begin match l with
- | GFun (fundec, loc) :: [] ->
- Project.on
- prj
- (fun () ->
- Options.feedback "current prj = %a"
- Project.pretty (Project.current ());
- ignore(Cil.makeFormalVar fundec "ok" Cil.intType))
- ();
- let g = GFun({ fundec with svar = fundec.svar }, loc) in
- [g]
- | _ -> assert false
- end
- in
+ | GFun (fundec, loc) :: [] ->
+ Project.on
+ prj
+ (fun () ->
+ Options.feedback "current prj = %a"
+ Project.pretty (Project.current ());
+ ignore(Cil.makeFormalVar fundec "ok" Cil.intType))
+ ();
+ let g = GFun({ fundec with svar = fundec.svar }, loc) in
+ [g]
+ | _ -> assert false
+ end
+ in
Cil.ChangeDoChildrenPost( [g], mk_formal)
-
+
| GFunDecl (_fspec, _vi, _loc) as g ->
- let mk_gvar_decl = function l ->
- begin match l with
- | (GFunDecl (_fspec, vi, _loc) as g) :: [] ->
- if not (Cil_builtins.Frama_c_builtins.mem vi.vname) then
- begin match vi.vtype with
- | TFun(typ, args, varity, attr) ->
- let vtype = Cil.argsToList args in
- let new_fun_typ = TFun(
- typ, Some (vtype @ [ "ok", Cil.intType, [] ]),
- varity, attr)
- in
+ let mk_gvar_decl = function l ->
+ begin match l with
+ | (GFunDecl (_fspec, vi, _loc) as g) :: [] ->
+ if not (Cil_builtins.Frama_c_builtins.mem vi.vname) then
+ begin match vi.vtype with
+ | TFun(typ, args, varity, attr) ->
+ let vtype = Cil.argsToList args in
+ let new_fun_typ = TFun(
+ typ, Some (vtype @ [ "ok", Cil.intType, [] ]),
+ varity, attr)
+ in
Cil.update_var_type vi new_fun_typ;
- Project.on
- prj
- (fun () -> Cil.setFormalsDecl vi new_fun_typ;) ();
- [ g ]
- | _ -> assert false
- end
- else
- [g]
- | _ -> assert false
- end
+ Project.on
+ prj
+ (fun () -> Cil.setFormalsDecl vi new_fun_typ;) ();
+ [ g ]
+ | _ -> assert false
+ end
+ else
+ [g]
+ | _ -> assert false
+ end
in
Cil.ChangeDoChildrenPost ([g], mk_gvar_decl)
- | GVarDecl _
- | GVar _
- | GType _
- | GCompTag _
- | GCompTagDecl _
- | GEnumTag _
- | GEnumTagDecl _
- | GAsm _
- | GPragma _
- | GText _
- | GAnnot _ -> Cil.DoChildren
+ | GVarDecl _
+ | GVar _
+ | GType _
+ | GCompTag _
+ | GCompTagDecl _
+ | GEnumTag _
+ | GEnumTagDecl _
+ | GAsm _
+ | GPragma _
+ | GText _
+ | GAnnot _ -> Cil.DoChildren
method! vinst = function
| Call(_,{ Cil_types.enode = Lval (Var _, NoOffset)},_,_) as i ->
- let add_zero = function
- | [Call(res,f,args,loc)] ->
- let args =
- args @ [ Cil.zero ~loc ]
- in
- [Call(res,f,args,loc)]
- | _ -> assert false
- in
- Cil.ChangeDoChildrenPost([i], add_zero)
+ let add_zero = function
+ | [Call(res,f,args,loc)] ->
+ let args =
+ args @ [ Cil.zero ~loc ]
+ in
+ [Call(res,f,args,loc)]
+ | _ -> assert false
+ in
+ Cil.ChangeDoChildrenPost([i], add_zero)
| _ -> Cil.DoChildren
-
- end
+
+end
let generate_code name =
let transform prj = new transform prj in
File.create_project_from_visitor name transform
-let main () =
+let main () =
if Project.get_name (Project.current()) <> "test" then
ignore (generate_code "test")
diff --git a/tests/cil/queue_ghost_instr.ml b/tests/cil/queue_ghost_instr.ml
index 22fcc753adaeea44ff4733b3971b4b2d53f12bce..f8a486d3fe77663beff1fa0c8e18168a44c1bf7d 100644
--- a/tests/cil/queue_ghost_instr.ml
+++ b/tests/cil/queue_ghost_instr.ml
@@ -8,9 +8,9 @@ class add_skip = object(this)
method! vstmt s =
let open Cil_types in
begin match s.skind with
- | If(_) ->
- this#queueInstr([Skip(Cil.CurrentLoc.get())])
- | _ -> ()
+ | If(_) ->
+ this#queueInstr([Skip(Cil.CurrentLoc.get())])
+ | _ -> ()
end ;
Cil.DoChildren
diff --git a/tests/constant_propagation/introduction_of_non_explicit_cast.ml b/tests/constant_propagation/introduction_of_non_explicit_cast.ml
index b35466333f6fe2af94cefa38d3cd816aea663dd5..2d20a43cb00819d2370fd19c4a2e2db7e2b4f880 100644
--- a/tests/constant_propagation/introduction_of_non_explicit_cast.ml
+++ b/tests/constant_propagation/introduction_of_non_explicit_cast.ml
@@ -5,8 +5,8 @@ let main _ =
Project.on
new_proj
(fun () ->
- Kernel.CodeOutput.output
- (fun fmt -> Format.fprintf fmt "After Constant propagation :@."))
+ Kernel.CodeOutput.output
+ (fun fmt -> Format.fprintf fmt "After Constant propagation :@."))
();
File.pretty_ast ~prj:new_proj ();;
diff --git a/tests/crowbar/complete_type.ml b/tests/crowbar/complete_type.ml
index dec73a79cc1c746fef65bdf4ad218d157f2ee6f0..39dc30e45bc0257958644136f7e24c296fe17611 100644
--- a/tests/crowbar/complete_type.ml
+++ b/tests/crowbar/complete_type.ml
@@ -66,18 +66,18 @@ let mk_comp_type
Cil_const.mkCompInfo cstruct (type_name()) mk_fields []
in
let kind =
- match cstruct, nb_fields, kind1, kind2 with
- | _, 0, _, _ -> Incomplete
- | _, _, Incomplete, _ -> Incomplete
- | _, _, FAM_struct, _ -> Incomplete
- | _, 1, Complete, _ -> Complete
- | true, 1, FAM_array, _ -> Incomplete
- | _, _, FAM_array, _ -> Incomplete
- | _, _, _, Incomplete -> Incomplete
- | _, _, _, FAM_struct -> Incomplete
- | true, _, Complete, FAM_array -> FAM_struct
- | _, _, _, FAM_array -> Incomplete
- | _, _, Complete, Complete -> Complete
+ match cstruct, nb_fields, kind1, kind2 with
+ | _, 0, _, _ -> Incomplete
+ | _, _, Incomplete, _ -> Incomplete
+ | _, _, FAM_struct, _ -> Incomplete
+ | _, 1, Complete, _ -> Complete
+ | true, 1, FAM_array, _ -> Incomplete
+ | _, _, FAM_array, _ -> Incomplete
+ | _, _, _, Incomplete -> Incomplete
+ | _, _, _, FAM_struct -> Incomplete
+ | true, _, Complete, FAM_array -> FAM_struct
+ | _, _, _, FAM_array -> Incomplete
+ | _, _, Complete, Complete -> Complete
in
let types =
match nb_fields with
diff --git a/tests/crowbar/constfold.ml b/tests/crowbar/constfold.ml
index 91de9a16715a5ca908c76349ab5a0cc727b47c78..8b176ca248d07f6ebbba36d8f2e7daff1fdb0325 100644
--- a/tests/crowbar/constfold.ml
+++ b/tests/crowbar/constfold.ml
@@ -133,35 +133,35 @@ let gen_cabs typ expr =
DECDEF(None,([SpecType Tint],[("result", JUSTBASE,[],loc),NO_INIT]),loc);
false,
FUNDEF(
- None,([SpecType Tvoid],("f", PROTO(JUSTBASE,[],[],false),[],loc)),
- { blabels = [];
- battrs = [];
- bstmts = [
- { stmt_ghost = false;
- stmt_node =
- DEFINITION(
- DECDEF(
- None,
- ([SpecType typ], [("x",JUSTBASE,[],loc),SINGLE_INIT expr]),
- loc))};
- { stmt_ghost = false;
- stmt_node =
- COMPUTATION(
- mk_exp(
- BINARY(
- ASSIGN,
- mk_exp (VARIABLE "result"),
- mk_exp (
- BINARY(
- EQ,
- mk_exp (VARIABLE "x"),
- mk_exp(
- INDEX(
- mk_exp (VARIABLE "a"),
- mk_exp (CONSTANT (CONST_INT "0")))))))), loc)}
- ]
- },
- loc,loc)])
+ None,([SpecType Tvoid],("f", PROTO(JUSTBASE,[],[],false),[],loc)),
+ { blabels = [];
+ battrs = [];
+ bstmts = [
+ { stmt_ghost = false;
+ stmt_node =
+ DEFINITION(
+ DECDEF(
+ None,
+ ([SpecType typ], [("x",JUSTBASE,[],loc),SINGLE_INIT expr]),
+ loc))};
+ { stmt_ghost = false;
+ stmt_node =
+ COMPUTATION(
+ mk_exp(
+ BINARY(
+ ASSIGN,
+ mk_exp (VARIABLE "result"),
+ mk_exp (
+ BINARY(
+ EQ,
+ mk_exp (VARIABLE "x"),
+ mk_exp(
+ INDEX(
+ mk_exp (VARIABLE "a"),
+ mk_exp (CONSTANT (CONST_INT "0")))))))), loc)}
+ ]
+ },
+ loc,loc)])
let () = Kernel.AutoLoadPlugins.off()
diff --git a/tests/crowbar/integer_bb_pretty.ml b/tests/crowbar/integer_bb_pretty.ml
index 2c6ec812e2968f282f1efb3e3cb19a7c45c9ef0a..686b6fac115d93ed0d7a818fcb3569ee2c818c44 100644
--- a/tests/crowbar/integer_bb_pretty.ml
+++ b/tests/crowbar/integer_bb_pretty.ml
@@ -22,10 +22,10 @@ let reparse v s =
let v' = Z.of_string ("0x" ^ remains) in
4 * (String.length remains), v'
end else begin
- let remains = String.sub s idx (String.length s - idx) in
- let v' = Z.of_string ("0b" ^ remains) in
- String.length remains, v'
- end
+ let remains = String.sub s idx (String.length s - idx) in
+ let v' = Z.of_string ("0b" ^ remains) in
+ String.length remains, v'
+ end
in
let m = Z.(one lsl len) in
let m = Z.pred m in
diff --git a/tests/crowbar/offset_anonymous_field.ml b/tests/crowbar/offset_anonymous_field.ml
index f62efd3a1f9724256d417a984f5143ffa9470da6..973cfc07ea8ce9c7e11a38546ebef287e3dbcf37 100644
--- a/tests/crowbar/offset_anonymous_field.ml
+++ b/tests/crowbar/offset_anonymous_field.ml
@@ -201,9 +201,9 @@ let test { designator; offsets; structs } =
"fieldsToInit didn't find appropriate offset for %s in %s.\n\
expected offsets were %a\n\
returned offsets are %a"
- field filename
- (Format.pp_print_list ~pp_sep Cil_printer.pp_offset) expected
- (Format.pp_print_list ~pp_sep Cil_printer.pp_offset) result)
+ field filename
+ (Format.pp_print_list ~pp_sep Cil_printer.pp_offset) expected
+ (Format.pp_print_list ~pp_sep Cil_printer.pp_offset) result)
end
with Log.AbortFatal _ ->
let filename = generate_failure_file offset structs in
diff --git a/tests/crowbar/test_ghost_cfg.ml b/tests/crowbar/test_ghost_cfg.ml
index 5f67349aee7aec87e003b56d33b1dac317de6964..7cc14d11f1955493274dfab77be7c66717271fcc 100644
--- a/tests/crowbar/test_ghost_cfg.ml
+++ b/tests/crowbar/test_ghost_cfg.ml
@@ -25,11 +25,11 @@ type stmt_pos =
type switch_or_loop = Is_switch | Is_loop
type env = {
- switch_or_loop: (switch_or_loop * bool) list;
- should_fail: bool;
- in_ghost: bool;
- stmt_stack: stmt list;
- stmt_pos: stmt_pos;
+ switch_or_loop: (switch_or_loop * bool) list;
+ should_fail: bool;
+ in_ghost: bool;
+ stmt_stack: stmt list;
+ stmt_pos: stmt_pos;
}
let empty_env =
@@ -41,7 +41,7 @@ let merge old_env new_env =
{ old_env with
should_fail = old_env.should_fail || new_env.should_fail;
stmt_stack = new_env.stmt_stack;
- }
+ }
let add_stack stmt env = { env with stmt_stack = stmt :: env.stmt_stack }
@@ -74,18 +74,18 @@ let end_of_body = [ incr_stmt; return; forward_goto_target ]
let ghost_status env ghost =
match env.stmt_pos with
- | Normal -> env.in_ghost || ghost
- | _ -> env.in_ghost
+ | Normal -> env.in_ghost || ghost
+ | _ -> env.in_ghost
let block env stmts = env, Cil.mkBlock stmts
let gen_stmts gen_stmt =
fix
(fun gen_stmts ->
- choose [
- const (fun env -> env,[]);
- map [gen_stmt; gen_stmts]
- (fun f1 f2 env ->
+ choose [
+ const (fun env -> env,[]);
+ map [gen_stmt; gen_stmts]
+ (fun f1 f2 env ->
let (new_env, stmt) = f1 env in
let env = merge env new_env in
let (new_env, stmts) = f2 env in
@@ -129,21 +129,21 @@ let gen_return ghost env =
let mk_label =
let nb = ref 0 in
fun stmt ->
- match List.filter (function Label _ -> true | _ -> false) stmt.labels with
+ match List.filter (function Label _ -> true | _ -> false) stmt.labels with
| [] ->
- incr nb;
- let name = "L" ^ (string_of_int !nb) in
- stmt.labels <- [ Label (name, Loc.unknown, true) ]
+ incr nb;
+ let name = "L" ^ (string_of_int !nb) in
+ stmt.labels <- [ Label (name, Loc.unknown, true) ]
| _ -> ()
(* approximation for gotos: if all the statements we jump over are ghost, we
consider that we stay inside a ghost block. Might not be completely accurate.
- *)
+*)
let rec all_ghosts n l =
match l with
- | [] -> assert false
- | s :: _ when n = 0 -> s.ghost
- | s :: tl -> s.ghost && all_ghosts (n-1) tl
+ | [] -> assert false
+ | s :: _ when n = 0 -> s.ghost
+ | s :: tl -> s.ghost && all_ghosts (n-1) tl
let gen_goto ghost tgt env =
let loc = Loc.unknown in
@@ -183,16 +183,16 @@ let gen_break ghost env =
let ghost = ghost_status env ghost in
let skind, should_fail =
match env.switch_or_loop with
- | [] -> Instr (Skip Loc.unknown), false
- | (Is_loop,g) :: _ -> Break Loc.unknown, not g && ghost
- | (Is_switch,g)::_ ->
- (match env.stmt_pos with
- | Normal -> Break Loc.unknown, not g && ghost
- | Case g1 -> Break Loc.unknown, not g && (g1 || ghost)
- | Case_no_default _ -> Break Loc.unknown, false
- | Last_case g1 -> Break Loc.unknown, not g && (g1 || ghost)
- | Last_case_no_default _ -> Break Loc.unknown, false
- | Default g1 -> Break Loc.unknown, not g && not g1 && ghost)
+ | [] -> Instr (Skip Loc.unknown), false
+ | (Is_loop,g) :: _ -> Break Loc.unknown, not g && ghost
+ | (Is_switch,g)::_ ->
+ (match env.stmt_pos with
+ | Normal -> Break Loc.unknown, not g && ghost
+ | Case g1 -> Break Loc.unknown, not g && (g1 || ghost)
+ | Case_no_default _ -> Break Loc.unknown, false
+ | Last_case g1 -> Break Loc.unknown, not g && (g1 || ghost)
+ | Last_case_no_default _ -> Break Loc.unknown, false
+ | Default g1 -> Break Loc.unknown, not g && not g1 && ghost)
in
let should_fail = env.should_fail || should_fail in
let stmt = Cil.mkStmt ~ghost skind in
@@ -208,8 +208,8 @@ let gen_continue ghost env =
let is_loop = function (Is_loop,_) -> true | (Is_switch,_) -> false in
let skind, should_fail =
match List.find_opt is_loop env.switch_or_loop with
- | None -> Instr (Skip Loc.unknown), false
- | Some (_,g) -> Continue Loc.unknown, not g && ghost
+ | None -> Instr (Skip Loc.unknown), false
+ | Some (_,g) -> Continue Loc.unknown, not g && ghost
in
let should_fail = should_fail || env.should_fail in
let stmt = Cil.mkStmt ~ghost skind in
@@ -236,9 +236,9 @@ let gen_if ghost ghost_else stmt_then stmt_else env =
let env = merge env new_env in
let else_b = Cil.mkBlock else_s in
if (not ghost) && ghoste then begin
- let attr = Attr (Cil.frama_c_ghost_else,[]) in
- else_b.battrs <- Cil.addAttribute attr else_b.battrs;
- end;
+ let attr = Attr (Cil.frama_c_ghost_else,[]) in
+ else_b.battrs <- Cil.addAttribute attr else_b.battrs;
+ end;
stmt.skind <- If(e,Cil.mkBlock then_s, Cil.mkBlock else_s,loc);
env, stmt
@@ -246,13 +246,13 @@ let gen_default should_break stmts env =
let ghost = env.in_ghost in
(* default clause always has the same status as underlying switch.
This simplifies deciding whether the check should fail or not.
- *)
+ *)
let new_env = { env with stmt_pos = Default ghost } in
let new_env, stmts = stmts new_env in
(* Don't make the statements in the default branch potential goto targets:
they could be picked up by gotos inside case branches, which would become
forward gotos, complicating the should_fail oracle computation.
- *)
+ *)
let new_env = { new_env with stmt_stack = env.stmt_stack } in
let _,s1 = gen_inst ghost env in
let epilogue =
@@ -270,12 +270,12 @@ let gen_default should_break stmts env =
let ghost_case_breaks has_default other_cases =
let rec find_ghost_seq seq = function
- (* if there's a (non-ghost by definition) default, inspect the ghost
- cases. Otherwise, non-ghost exits the switch anyway, ghost can break
- at any time. *)
+ (* if there's a (non-ghost by definition) default, inspect the ghost
+ cases. Otherwise, non-ghost exits the switch anyway, ghost can break
+ at any time. *)
| [] -> if has_default then seq else []
| hd :: tl ->
- if (List.hd hd).ghost then find_ghost_seq (hd :: seq) tl else seq
+ if (List.hd hd).ghost then find_ghost_seq (hd :: seq) tl else seq
in
let seq = find_ghost_seq [] other_cases in
let module M = struct exception Has_break end in
@@ -284,10 +284,10 @@ let ghost_case_breaks has_default other_cases =
inherit Cil.nopCilVisitor
method! vstmt s =
match s.skind with
- | Break _ -> raise M.Has_break
- | Loop _ | Switch _ -> (* a break there won't break the switch *)
- Cil.SkipChildren
- | _ -> Cil.DoChildren
+ | Break _ -> raise M.Has_break
+ | Loop _ | Switch _ -> (* a break there won't break the switch *)
+ Cil.SkipChildren
+ | _ -> Cil.DoChildren
end
in
try
@@ -300,12 +300,12 @@ let rec no_ghost_case_breaks = function
| [] -> false (* should not happen, we have at least one non-ghost case before
default. *)
| stmts :: others ->
- if (List.hd stmts).ghost then
- begin
- match (Extlib.last stmts).skind with
- | Break _ -> false
- | _ -> no_ghost_case_breaks others
- end else true
+ if (List.hd stmts).ghost then
+ begin
+ match (Extlib.last stmts).skind with
+ | Break _ -> false
+ | _ -> no_ghost_case_breaks others
+ end else true
@@ -319,32 +319,32 @@ let gen_case ghost should_break my_case cases env =
let has_default = match default with None -> false | Some _ -> true in
let stmt_pos =
match non_ghost_cases with
- | [] ->
- if has_default then Last_case ghost else Last_case_no_default ghost
- | _ -> if has_default then Case ghost else Case_no_default ghost
+ | [] ->
+ if has_default then Last_case ghost else Last_case_no_default ghost
+ | _ -> if has_default then Case ghost else Case_no_default ghost
in
let should_fail =
match stmt_pos, env.switch_or_loop with
- | (Normal | Default _),_ -> assert false
- | _,[] -> assert false
- | Last_case_no_default _,_ -> false
- | Last_case g1, (_,g2)::_ ->
- (* if the switch is non-ghost, but the last case is, and ends with
- a break, the default clause won't be taken. *)
- not g2 && g1 && should_break
- | Case_no_default g1, (_, g2)::_ ->
- (* fails iff switch is non-ghost, current case is, and doesn't break,
- going to the next case. *)
- not g2 && g1 && not should_break && no_ghost_case_breaks others
- | Case g1, (_,g2) :: _ ->
- not g2 && g1 (* prevents taking the default clause.*)
+ | (Normal | Default _),_ -> assert false
+ | _,[] -> assert false
+ | Last_case_no_default _,_ -> false
+ | Last_case g1, (_,g2)::_ ->
+ (* if the switch is non-ghost, but the last case is, and ends with
+ a break, the default clause won't be taken. *)
+ not g2 && g1 && should_break
+ | Case_no_default g1, (_, g2)::_ ->
+ (* fails iff switch is non-ghost, current case is, and doesn't break,
+ going to the next case. *)
+ not g2 && g1 && not should_break && no_ghost_case_breaks others
+ | Case g1, (_,g2) :: _ ->
+ not g2 && g1 (* prevents taking the default clause.*)
in
let should_fail =
should_fail ||
- (* if non-ghost case is supposed to fall through another non-ghost case,
- we have to inspect all ghost cases in between to search for a
- break, which would indicate a failure. *)
- (not ghost && not should_break && ghost_case_breaks has_default others)
+ (* if non-ghost case is supposed to fall through another non-ghost case,
+ we have to inspect all ghost cases in between to search for a
+ break, which would indicate a failure. *)
+ (not ghost && not should_break && ghost_case_breaks has_default others)
in
let should_fail = env.should_fail || should_fail in
let new_env = { env with in_ghost = ghost; stmt_pos; should_fail } in
@@ -364,11 +364,11 @@ let gen_case ghost should_break my_case cases env =
let gen_cases gen_stmt =
fix
(fun gen_cases ->
- choose [
- const (fun env -> env,None,[]);
- map [ bool; gen_stmts gen_stmt ] gen_default;
- map [ bool; bool; gen_stmts gen_stmt; gen_cases ] gen_case
- ])
+ choose [
+ const (fun env -> env,None,[]);
+ map [ bool; gen_stmts gen_stmt ] gen_default;
+ map [ bool; bool; gen_stmts gen_stmt; gen_cases ] gen_case
+ ])
let gen_switch ghost cases env =
let loc = Loc.unknown in
@@ -384,17 +384,17 @@ let gen_switch ghost cases env =
let (new_env, default, cases) = cases new_env in
let acc =
match default with
- | None -> [],[]
- | Some stmts -> [List.hd stmts],stmts
+ | None -> [],[]
+ | Some stmts -> [List.hd stmts],stmts
in
let count_case = ref 0 in
let mk_switch case (labels, stmts) =
- let h = List.hd case in
- h.labels <-
- Cil_types.Case (Cil.integer Loc.unknown !count_case, Loc.unknown)
- :: h.labels;
- incr count_case;
- (h::labels, case @ stmts)
+ let h = List.hd case in
+ h.labels <-
+ Cil_types.Case (Cil.integer Loc.unknown !count_case, Loc.unknown)
+ :: h.labels;
+ incr count_case;
+ (h::labels, case @ stmts)
in
let (labels, stmts) = List.fold_right mk_switch cases acc in
let block = Cil.mkBlock stmts in
@@ -435,40 +435,40 @@ let gen_loop ghost stmts env =
let gen_stmt =
fix (fun gen_stmt ->
choose [
- map [bool] gen_inst;
- map [bool; gen_stmts gen_stmt] gen_block;
- map [bool] gen_return;
- map [bool; uint16] gen_goto;
- map [bool] gen_break;
- map [bool] gen_continue;
- map [bool; bool; gen_stmts gen_stmt; gen_stmts gen_stmt] gen_if;
- map [bool; gen_cases gen_stmt] gen_switch;
- map [bool; gen_stmts gen_stmt] gen_loop;
- ])
+ map [bool] gen_inst;
+ map [bool; gen_stmts gen_stmt] gen_block;
+ map [bool] gen_return;
+ map [bool; uint16] gen_goto;
+ map [bool] gen_break;
+ map [bool] gen_continue;
+ map [bool; bool; gen_stmts gen_stmt; gen_stmts gen_stmt] gen_if;
+ map [bool; gen_cases gen_stmt] gen_switch;
+ map [bool; gen_stmts gen_stmt] gen_loop;
+ ])
let gen_body =
map [gen_stmts gen_stmt]
(fun f ->
- let (env, stmts) = f empty_env in
- let stmts = stmts @ end_of_body in
- env, Cil.mkBlock stmts)
+ let (env, stmts) = f empty_env in
+ let stmts = stmts @ end_of_body in
+ env, Cil.mkBlock stmts)
let gen_file =
map [gen_body]
(fun (env, body) ->
- let f = Cil.emptyFunctionFromVI f in
- f.svar.vdefined <- true;
- f.sbody <- body;
- (env,
- { fileName = Filepath.Normalized.empty;
- globals = [
- GVarDecl (x,Cil_datatype.Location.unknown);
- GVarDecl (y,Cil_datatype.Location.unknown);
- GFun (f, Cil_datatype.Location.unknown)
- ];
- globinit = None;
- globinitcalled = false
- }))
+ let f = Cil.emptyFunctionFromVI f in
+ f.svar.vdefined <- true;
+ f.sbody <- body;
+ (env,
+ { fileName = Filepath.Normalized.empty;
+ globals = [
+ GVarDecl (x,Cil_datatype.Location.unknown);
+ GVarDecl (y,Cil_datatype.Location.unknown);
+ GFun (f, Cil_datatype.Location.unknown)
+ ];
+ globinit = None;
+ globinitcalled = false
+ }))
let ignore_deferred_errors () =
try Log.treat_deferred_error () with Log.AbortError _ -> ()
@@ -495,56 +495,56 @@ let check_file (env, file) =
Log.treat_deferred_error ();
true
with
- | Log.AbortError _ ->
- ignore_deferred_errors ();
- false
- | exn ->
- Printf.printf
- "Uncaught exception: %s\n%t\nFile saved in %s\n%!"
- (Printexc.to_string exn) Printexc.print_backtrace file_name;
- ignore_deferred_errors ();
- report file_name "Found code leading to an unknown exception"
+ | Log.AbortError _ ->
+ ignore_deferred_errors ();
+ false
+ | exn ->
+ Printf.printf
+ "Uncaught exception: %s\n%t\nFile saved in %s\n%!"
+ (Printexc.to_string exn) Printexc.print_backtrace file_name;
+ ignore_deferred_errors ();
+ report file_name "Found code leading to an unknown exception"
in
if env.should_fail && success then
report file_name "Found ghost code that should not have been accepted"
else if not (env.should_fail) then begin
- if success then begin
- let norm_buf = Buffer.create 150 in
- let fmt = Format.formatter_of_buffer norm_buf in
- let f = Globals.Functions.find_by_name "f" in
- Kernel_function.pretty fmt f;
- let prj2 = Project.create "copy" in
- Project.set_current prj2;
- Kernel.Files.set [ Filepath.Normalized.of_string file_name ];
- let parse_success =
- try
- File.init_from_cmdline (); true
- with
- Log.AbortError _ -> ignore_deferred_errors (); false
- in
- if parse_success then begin
- let copy_buf = Buffer.create 150 in
- let fmt = Format.formatter_of_buffer copy_buf in
- let f = Globals.Functions.find_by_name "f" in
- Kernel_function.pretty fmt f;
- if Buffer.contents norm_buf <> Buffer.contents copy_buf then begin
- let norm = open_out (file_name ^ ".norm.c") in
- Buffer.output_buffer norm norm_buf;
- flush norm;
- close_out norm;
- let copy = open_out (file_name ^ ".copy.c") in
- Buffer.output_buffer copy copy_buf;
- flush copy;
- close_out copy;
- report file_name "Found ghost code not well pretty-printed"
- end else true
- end else begin
- report file_name "Error during re-parsing of pretty-printed code"
- end
- end
- else
- report file_name "Found ghost code that should have been accepted"
+ if success then begin
+ let norm_buf = Buffer.create 150 in
+ let fmt = Format.formatter_of_buffer norm_buf in
+ let f = Globals.Functions.find_by_name "f" in
+ Kernel_function.pretty fmt f;
+ let prj2 = Project.create "copy" in
+ Project.set_current prj2;
+ Kernel.Files.set [ Filepath.Normalized.of_string file_name ];
+ let parse_success =
+ try
+ File.init_from_cmdline (); true
+ with
+ Log.AbortError _ -> ignore_deferred_errors (); false
+ in
+ if parse_success then begin
+ let copy_buf = Buffer.create 150 in
+ let fmt = Format.formatter_of_buffer copy_buf in
+ let f = Globals.Functions.find_by_name "f" in
+ Kernel_function.pretty fmt f;
+ if Buffer.contents norm_buf <> Buffer.contents copy_buf then begin
+ let norm = open_out (file_name ^ ".norm.c") in
+ Buffer.output_buffer norm norm_buf;
+ flush norm;
+ close_out norm;
+ let copy = open_out (file_name ^ ".copy.c") in
+ Buffer.output_buffer copy copy_buf;
+ flush copy;
+ close_out copy;
+ report file_name "Found ghost code not well pretty-printed"
+ end else true
+ end else begin
+ report file_name "Error during re-parsing of pretty-printed code"
+ end
end
+ else
+ report file_name "Found ghost code that should have been accepted"
+ end
else true
let () =
diff --git a/tests/dynamic/abstract.ml b/tests/dynamic/abstract.ml
index 54a14984bb33114aa4d2d04a2f500c3fc8ddb40a..f0a45ba0e7f428d6185895bdae134eb6078034f6 100644
--- a/tests/dynamic/abstract.ml
+++ b/tests/dynamic/abstract.ml
@@ -42,9 +42,9 @@ module A : sig end = struct
Dynamic.register ~plugin:"A" "h"
(Datatype.func t (Datatype.func u Datatype.bool))
(fun x y ->
- match x with A x ->
- Format.printf "params = %d %f@." x y;
- x = int_of_float y | B _ -> false)
+ match x with A x ->
+ Format.printf "params = %d %f@." x y;
+ x = int_of_float y | B _ -> false)
let _ =
Dynamic.register ~plugin:"A" "succ"
(Datatype.func Datatype.int Datatype.int) succ
@@ -104,28 +104,28 @@ module B = struct
let ho =
Dynamic.get ~plugin:"A" "ho"
(Datatype.func
- (Datatype.func Datatype.int Datatype.int) (Datatype.func ty ty'))
+ (Datatype.func Datatype.int Datatype.int) (Datatype.func ty ty'))
let ppu = Dynamic.get ~plugin:"A" "ppu" (Datatype.func ty' Datatype.unit)
let res =
ho (Dynamic.get ~plugin:"A" "succ"
- (Datatype.func Datatype.int Datatype.int)) v2
+ (Datatype.func Datatype.int Datatype.int)) v2
let () = Format.printf "print:@."; ppu res
let ho_bug =
try
ignore
- (Dynamic.get ~plugin:"A" "ho"
- (Datatype.func
- (Datatype.func ty Datatype.int) (Datatype.func ty ty')) f v2);
+ (Dynamic.get ~plugin:"A" "ho"
+ (Datatype.func
+ (Datatype.func ty Datatype.int) (Datatype.func ty ty')) f v2);
assert false
with Dynamic.Incompatible_type s ->
print_endline s
(* let () = (* is now statically checked and no more dynamically *)
- try
+ try
List.iter
- (Dynamic.get ~plugin:"A" "ppu" (Datatype.func ty' Datatype.unit))
- (Dynamic.get ~plugin:"A" "poly" (Datatype.list ty'));
+ (Dynamic.get ~plugin:"A" "ppu" (Datatype.func ty' Datatype.unit))
+ (Dynamic.get ~plugin:"A" "poly" (Datatype.list ty'));
assert false
- with Dynamic.Incompatible_type s ->
+ with Dynamic.Incompatible_type s ->
print_endline s*)
let () =
List.iter
diff --git a/tests/dynamic/abstract2.ml b/tests/dynamic/abstract2.ml
index 461f2dfbfc15096526e514857aafdddc475ee34a..73293f6f62db4ff66140644d78c423ab6c181980 100644
--- a/tests/dynamic/abstract2.ml
+++ b/tests/dynamic/abstract2.ml
@@ -26,7 +26,7 @@ let main () =
let _b = B.ty in
let _s = Dynamic.get ~plugin:"AA" "mk" (Datatype.func Datatype.unit a) () in
(* is now statically checked and no more dynamically *)
-(* Dynamic.get ~plugin:"BB" "print" (Datatype.func b Datatype.unit) s;*)
+ (* Dynamic.get ~plugin:"BB" "print" (Datatype.func b Datatype.unit) s;*)
()
diff --git a/tests/float/fval_test.ml b/tests/float/fval_test.ml
index 9197808e84e9d6fe49772f489013b393485a1e3e..6ce0dc57be049a58c3884d46b551637628452564 100644
--- a/tests/float/fval_test.ml
+++ b/tests/float/fval_test.ml
@@ -50,11 +50,11 @@ let inject_range f1 f2 = join (inject f1) (inject f2)
values. *)
let interesting_double =
[-.infinity; -1.2e307; -120.; -1.2e-323; -0.;
- infinity; 1.3e308; 130.; 1.3e-323; +0.; ]
+ infinity; 1.3e308; 130.; 1.3e-323; +0.; ]
let interesting_float =
[-.infinity; -2.2e37; -120.; -1.5e-33; -0.;
- infinity; 2.3e37; 130.; 1.6e-33; +0.; ]
+ infinity; 2.3e37; 130.; 1.6e-33; +0.; ]
let product itvs =
let l = Extlib.product (fun a b -> (a, b)) itvs itvs in
diff --git a/tests/libc/check_compliance.ml b/tests/libc/check_compliance.ml
index fabf605d2b8d14f9aa8503e6553d945e16256a37..542109885e37bf262e67cbf9f93275d9b27c91a4 100644
--- a/tests/libc/check_compliance.ml
+++ b/tests/libc/check_compliance.ml
@@ -77,7 +77,7 @@ struct
fun format json ->
let table = Hashtbl.create 500 in
json |> to_assoc |> List.iter (fun (ident, values) ->
- Hashtbl.replace table ident (convert values format));
+ Hashtbl.replace table ident (convert values format));
table
end
diff --git a/tests/libc/check_const.ml b/tests/libc/check_const.ml
index 710373708e0e41f8b386ecc4773030c6e56ba713..807c878a6602a9517375fea1b008ffec61cff2d7 100644
--- a/tests/libc/check_const.ml
+++ b/tests/libc/check_const.ml
@@ -10,7 +10,7 @@ let warn_if_const string typ vi loc =
if Cil.typeHasQualifier "const" typ then
Kernel.result ~source:(fst loc)
"'requires %svalid%s' of a const variable %a. \
- You probably meant '%svalid_read%s' instead"
+ You probably meant '%svalid_read%s' instead"
bs string Printer.pp_varinfo vi bs string
let warn_if_not_const kf string typ vi loc =
@@ -28,43 +28,43 @@ let check_annot kf _ (a: identified_predicate) =
| Papp ({l_var_info={lv_name=("valid_string"|"valid_read_string")}},
_, [t]) ->
begin
- let warn = match p with
- | Pvalid _ ->
- warn_if_const ""
- | Papp ({l_var_info={lv_name="valid_string"}},_,_) ->
- warn_if_const "_string"
- | Pvalid_read _ ->
- warn_if_not_const kf ""
- | Papp ({l_var_info={lv_name="valid_read_string"}},_,_) ->
- warn_if_not_const kf "_string"
- | _ -> assert false
- in
- match t.term_node with
- | TAddrOf (TVar lvi, _) -> begin
- match lvi.lv_origin with
- | Some ({vtype = typ} as vi) ->
- warn typ vi t.term_loc
+ let warn = match p with
+ | Pvalid _ ->
+ warn_if_const ""
+ | Papp ({l_var_info={lv_name="valid_string"}},_,_) ->
+ warn_if_const "_string"
+ | Pvalid_read _ ->
+ warn_if_not_const kf ""
+ | Papp ({l_var_info={lv_name="valid_read_string"}},_,_) ->
+ warn_if_not_const kf "_string"
+ | _ -> assert false
+ in
+ match t.term_node with
+ | TAddrOf (TVar lvi, _) -> begin
+ match lvi.lv_origin with
+ | Some ({vtype = typ} as vi) ->
+ warn typ vi t.term_loc
+ | _ -> ()
+ end
+ | TBinOp ((PlusPI | MinusPI),
+ ({term_node = TLval (TVar lvi, _)} |
+ {term_node = TCastE (_, {term_node = TLval (TVar lvi, _)})}),
+ _)
+ | TLval (TVar lvi, _) -> begin
+ match lvi.lv_origin with
+ | Some vi ->
+ warn (Cil.typeOf_pointed vi.vtype) vi t.term_loc
+ | _ -> ()
+ end
| _ -> ()
end
- | TBinOp ((PlusPI | MinusPI),
- ({term_node = TLval (TVar lvi, _)} |
- {term_node = TCastE (_, {term_node = TLval (TVar lvi, _)})}),
- _)
- | TLval (TVar lvi, _) -> begin
- match lvi.lv_origin with
- | Some vi ->
- warn (Cil.typeOf_pointed vi.vtype) vi t.term_loc
- | _ -> ()
- end
- | _ -> ()
- end
| _ -> ()
let check () =
let check_kf kf =
let bhvs = Annotations.behaviors ~populate:false kf in
List.iter (fun bhv ->
- Annotations.iter_requires (check_annot kf) kf bhv.b_name) bhvs
+ Annotations.iter_requires (check_annot kf) kf bhv.b_name) bhvs
in
Globals.Functions.iter check_kf
diff --git a/tests/misc/Debug_category.ml b/tests/misc/Debug_category.ml
index 04016b428c3bba1c1f93b1490dd23bef0533d7ed..c3ab6699cdcf5d62e36ddf353bf4201f736b5f77 100644
--- a/tests/misc/Debug_category.ml
+++ b/tests/misc/Debug_category.ml
@@ -1,10 +1,10 @@
include
Plugin.Register(
- struct
- let name = "test"
- let shortname = "test"
- let help = "test"
- end)
+ struct
+ let name = "test"
+ let shortname = "test"
+ let help = "test"
+ end)
let akey = register_category "a"
let ckey = register_category "a:b:c"
diff --git a/tests/misc/add_assigns.ml b/tests/misc/add_assigns.ml
index 7cf5569c55135d17e737453d3a6ac86bea968a46..11df28607ac8e92edffb3d1ef12b31e1b4f8440d 100644
--- a/tests/misc/add_assigns.ml
+++ b/tests/misc/add_assigns.ml
@@ -5,7 +5,7 @@ let emitter =
create "assigns" [ Property_status; Funspec ] ~correctness:[] ~tuning:[])
let computed = ref false
-
+
let main () =
if not !computed then begin
computed := true;
diff --git a/tests/misc/bts0452.ml b/tests/misc/bts0452.ml
index 6d5e9b6238e489a84838712e63812b27d8124cde..70a185bd243a2a7d04fce958c1776abb8362a524 100644
--- a/tests/misc/bts0452.ml
+++ b/tests/misc/bts0452.ml
@@ -1,4 +1,4 @@
(* Checks that even Jessie-specific normalization does not create spurious
warnings.
- *)
+*)
Cabs2cil.setDoAlternateConditional ();;
diff --git a/tests/misc/bts0489.ml b/tests/misc/bts0489.ml
index a8c15b449e9a549a58d888a348f2d4996978d304..224c74f4289c413958bf7e141380d34e00949465 100644
--- a/tests/misc/bts0489.ml
+++ b/tests/misc/bts0489.ml
@@ -1,17 +1,17 @@
open Cil_types
class visitor =
-object
- inherit Visitor.frama_c_inplace
- method! vexpr e =
- match e.enode with
+ object
+ inherit Visitor.frama_c_inplace
+ method! vexpr e =
+ match e.enode with
| Const(CInt64 (_,_,Some s)) ->
- Format.printf "Found representation %s@." s; Cil.SkipChildren
+ Format.printf "Found representation %s@." s; Cil.SkipChildren
| Const(CInt64(n,_,None)) ->
- Format.printf "No representation for %s@." (Integer.to_string n);
- Cil.SkipChildren
+ Format.printf "No representation for %s@." (Integer.to_string n);
+ Cil.SkipChildren
| _ -> Cil.DoChildren
-end
+ end
let run () =
let file = Ast.get () in
diff --git a/tests/misc/bts1347.ml b/tests/misc/bts1347.ml
index e1336805421fcbd1b834358ed9209b9e67520e53..d7196ae5940a4fc1316bb328207cfdc4044e0803 100644
--- a/tests/misc/bts1347.ml
+++ b/tests/misc/bts1347.ml
@@ -1,28 +1,28 @@
-let emitter =
+let emitter =
Emitter.create "emitter" ~correctness:[] ~tuning:[]
- [ Emitter.Code_annot; Emitter.Property_status ]
+ [ Emitter.Code_annot; Emitter.Property_status ]
let run () =
Globals.Functions.iter
(fun kf ->
- if not (Cil_builtins.is_builtin (Kernel_function.get_vi kf)) then begin
- Globals.set_entry_point (Kernel_function.get_name kf) true;
- Eva.Analysis.compute();
- let hyps =
- Alarms.fold
- (fun _ kf' s ~rank:_ _ a l ->
- if Kernel_function.equal kf kf' then
- Property.ip_of_code_annot_single kf s a :: l
- else
- l)
- []
- in
- let s = Kernel_function.find_return kf in
- let ca = !Db.Properties.Interp.code_annot kf s "assert 32.5>=10.;" in
- Annotations.add_code_annot emitter ~kf s ca;
- let ip = Property.ip_of_code_annot_single kf s ca in
- Property_status.emit emitter ~hyps ip Property_status.True
- end)
+ if not (Cil_builtins.is_builtin (Kernel_function.get_vi kf)) then begin
+ Globals.set_entry_point (Kernel_function.get_name kf) true;
+ Eva.Analysis.compute();
+ let hyps =
+ Alarms.fold
+ (fun _ kf' s ~rank:_ _ a l ->
+ if Kernel_function.equal kf kf' then
+ Property.ip_of_code_annot_single kf s a :: l
+ else
+ l)
+ []
+ in
+ let s = Kernel_function.find_return kf in
+ let ca = !Db.Properties.Interp.code_annot kf s "assert 32.5>=10.;" in
+ Annotations.add_code_annot emitter ~kf s ca;
+ let ip = Property.ip_of_code_annot_single kf s ca in
+ Property_status.emit emitter ~hyps ip Property_status.True
+ end)
-let () =
+let () =
Db.Main.extend run
diff --git a/tests/misc/callsite.ml b/tests/misc/callsite.ml
index e6f44481254a6e48f3c0522e1821e9d86c11fbee..c906a333c79cdbc7b004e95ccfe1496de65f0cf6 100644
--- a/tests/misc/callsite.ml
+++ b/tests/misc/callsite.ml
@@ -7,10 +7,10 @@ let dump f =
(fun fmt ->
Format.fprintf fmt "Call Sites for %s:@\n" f ;
List.iter
- (fun (ckf,stmt) ->
- Format.fprintf fmt " - From %s at #%03d@\n"
- (Kernel_function.get_name ckf) stmt.sid)
- csites)
+ (fun (ckf,stmt) ->
+ Format.fprintf fmt " - From %s at #%03d@\n"
+ (Kernel_function.get_name ckf) stmt.sid)
+ csites)
let main () =
Ast.compute () ;
diff --git a/tests/misc/change_main.ml b/tests/misc/change_main.ml
index e66b62ec5b04903483bf8bec2a2e8447444603d0..ac7fba803c66a0b3a6d79d93cdda3118cb3d19db 100644
--- a/tests/misc/change_main.ml
+++ b/tests/misc/change_main.ml
@@ -8,7 +8,7 @@ class visitor prj =
let run () =
ignore
- (File.create_project_from_visitor
+ (File.create_project_from_visitor
"change_main" (fun prj -> new visitor prj))
let () = Db.Main.extend run
diff --git a/tests/misc/cli_string_multiple_map.ml b/tests/misc/cli_string_multiple_map.ml
index 2b2078c4bb7fe41c97b5482023e91596f6b4976f..e8f5b806e8358fdc021fe1977576213b1b93f109 100644
--- a/tests/misc/cli_string_multiple_map.ml
+++ b/tests/misc/cli_string_multiple_map.ml
@@ -33,4 +33,3 @@ let main () =
Datatype.String.Map.iter print (M.get ())
let () = Db.Main.extend main
-
diff --git a/tests/misc/copy_machdep.ml b/tests/misc/copy_machdep.ml
index b522f1e6664294053573765fbb0f8d72f4a9d058..9843d085b1e85bbb4cca3d1c49fdb0e15fcda88b 100644
--- a/tests/misc/copy_machdep.ml
+++ b/tests/misc/copy_machdep.ml
@@ -5,13 +5,12 @@ let run () =
in
Kernel.feedback "Machdep is %spreserved"
(if Kernel.Machdep.get () = Project.on proj Kernel.Machdep.get () then
- "" else "not ");
+ "" else "not ");
Kernel.feedback "Enums is %spreserved"
(if Kernel.Enums.get () = Project.on proj Kernel.Enums.get () then
- "" else "not ");
+ "" else "not ");
Kernel.feedback "Unicode is %spreserved"
(if Kernel.Unicode.get () = Project.on proj Kernel.Unicode.get () then
- "" else "not ")
+ "" else "not ")
let () = Db.Main.extend run
-
diff --git a/tests/misc/custom_machdep.ml b/tests/misc/custom_machdep.ml
index 8942b2b793acec940637c3194d331047d15762dd..503611ae1fec6f6b921e2d1cdeecfeae7fba075b 100644
--- a/tests/misc/custom_machdep.ml
+++ b/tests/misc/custom_machdep.ml
@@ -1,47 +1,47 @@
open Cil_types
let mach =
-{
- version = "foo";
- compiler = "bar";
- cpp_arch_flags = [];
- sizeof_short = 2;
- sizeof_int = 3;
- sizeof_long = 4;
- sizeof_longlong = 8;
- sizeof_ptr = 4;
- sizeof_float = 4;
- sizeof_double = 8;
- sizeof_longdouble = 12;
- sizeof_void = 1;
- sizeof_fun = 1;
- size_t = "unsigned long";
- wchar_t = "int";
- ptrdiff_t = "int";
- alignof_short = 2;
- alignof_int = 3;
- alignof_long = 4;
- alignof_longlong = 4;
- alignof_ptr = 4;
- alignof_float = 4;
- alignof_double = 4;
- alignof_longdouble = 4;
- alignof_str = 1;
- alignof_fun = 1;
- alignof_aligned= 16;
- char_is_unsigned = false;
- const_string_literals = true;
- little_endian = true;
- underscore_name = false ;
- has__builtin_va_list = true;
-}
+ {
+ version = "foo";
+ compiler = "bar";
+ cpp_arch_flags = [];
+ sizeof_short = 2;
+ sizeof_int = 3;
+ sizeof_long = 4;
+ sizeof_longlong = 8;
+ sizeof_ptr = 4;
+ sizeof_float = 4;
+ sizeof_double = 8;
+ sizeof_longdouble = 12;
+ sizeof_void = 1;
+ sizeof_fun = 1;
+ size_t = "unsigned long";
+ wchar_t = "int";
+ ptrdiff_t = "int";
+ alignof_short = 2;
+ alignof_int = 3;
+ alignof_long = 4;
+ alignof_longlong = 4;
+ alignof_ptr = 4;
+ alignof_float = 4;
+ alignof_double = 4;
+ alignof_longdouble = 4;
+ alignof_str = 1;
+ alignof_fun = 1;
+ alignof_aligned= 16;
+ char_is_unsigned = false;
+ const_string_literals = true;
+ little_endian = true;
+ underscore_name = false ;
+ has__builtin_va_list = true;
+ }
let mach2 = { mach with compiler = "baz" }
(* First run : register [mach] under name [custom].
Second run :
- - register [mach] under name [custom] again. This must work.
- - then register [mach2] under name [custom]. This must result in an error.
+ - register [mach] under name [custom] again. This must work.
+ - then register [mach2] under name [custom]. This must result in an error.
*)
let () =
let ran = ref false in
diff --git a/tests/misc/ensures.ml b/tests/misc/ensures.ml
index a08e28e31b1135d67ab1334b1c307a85b23a855f..56cb3e03cc2e0c4d4288d24001b22ecc6540c96a 100644
--- a/tests/misc/ensures.ml
+++ b/tests/misc/ensures.ml
@@ -16,8 +16,8 @@ let run () =
in
let function_name = kf_name ^ ": behavior " ^ bname in
let status = Property_status.get ip in
- Kernel.result "@[%s@ @[%a@]@]"
- function_name Property_status.pretty status)
+ Kernel.result "@[%s@ @[%a@]@]"
+ function_name Property_status.pretty status)
ip)
let () = Db.Main.extend run
diff --git a/tests/misc/exception.ml b/tests/misc/exception.ml
index 08de229679131457770c774e61e52cb739887789..b99e9b1122b729d9ef074b263684e8aff7cd06b0 100644
--- a/tests/misc/exception.ml
+++ b/tests/misc/exception.ml
@@ -3,15 +3,15 @@ open Cil_types
let rec init_exn exn init acc =
match init with
- | SingleInit init ->
- Cil.mkStmtOneInstr (Set(exn,init,Cil_datatype.Location.unknown))
- :: acc
- | CompoundInit (ct,initl) ->
- Cil.foldLeftCompound
- ~implicit:false
- ~doinit:(fun off' i' _ acc ->
- init_exn (Cil.addOffsetLval off' exn) i' acc)
- ~ct ~initl ~acc
+ | SingleInit init ->
+ Cil.mkStmtOneInstr (Set(exn,init,Cil_datatype.Location.unknown))
+ :: acc
+ | CompoundInit (ct,initl) ->
+ Cil.foldLeftCompound
+ ~implicit:false
+ ~doinit:(fun off' i' _ acc ->
+ init_exn (Cil.addOffsetLval off' exn) i' acc)
+ ~ct ~initl ~acc
let add_throw_test f exn_type test init =
let throw_block = Cil.mkBlock [] in
@@ -40,8 +40,8 @@ let add_my_exn my_exn f =
in
let init =
CompoundInit(
- exn_type,
- [Field(my_field, NoOffset), SingleInit (Cil.kinteger ~loc kind 0)])
+ exn_type,
+ [Field(my_field, NoOffset), SingleInit (Cil.kinteger ~loc kind 0)])
in
add_throw_test f exn_type c init
@@ -90,33 +90,33 @@ let add_catch my_exn my_exn2 f =
let catch_stmt =
Cil.mkStmt
(TryCatch(
- f.sbody,
- [ Catch_exn (v1,[(v3,id_block); (v4, convert_exn_block)]),
- Cil.mkBlock
- [ Cil.mkStmt
- (Return
- (Some (Cil.new_exp ~loc (Lval (Var v1,exn_field_offset))),
- loc))];
- Catch_exn (v2,[]),
- Cil.mkBlock
- [ Cil.mkStmt (Return (Some (Cil.evar ~loc v2),loc))];
- Catch_exn (v5,[]),
- Cil.mkBlock
- [ Cil.mkStmt (Return (Some (Cil.mone ~loc), loc))];
- Catch_all, Cil.mkBlock [ Cil.mkStmt (Throw (None, loc)) ]
- ],
- loc))
+ f.sbody,
+ [ Catch_exn (v1,[(v3,id_block); (v4, convert_exn_block)]),
+ Cil.mkBlock
+ [ Cil.mkStmt
+ (Return
+ (Some (Cil.new_exp ~loc (Lval (Var v1,exn_field_offset))),
+ loc))];
+ Catch_exn (v2,[]),
+ Cil.mkBlock
+ [ Cil.mkStmt (Return (Some (Cil.evar ~loc v2),loc))];
+ Catch_exn (v5,[]),
+ Cil.mkBlock
+ [ Cil.mkStmt (Return (Some (Cil.mone ~loc), loc))];
+ Catch_all, Cil.mkBlock [ Cil.mkStmt (Throw (None, loc)) ]
+ ],
+ loc))
in
f.sbody <- Cil.mkBlock [ catch_stmt ]
let change_body my_exn my_exn2 glob f =
match f.svar.vname with
- | "f1" -> add_my_exn my_exn f; File.must_recompute_cfg f
- | "f2" -> add_int_exn f; File.must_recompute_cfg f
- | "f3" -> add_int_ptr_exn glob f; File.must_recompute_cfg f
- | "f4" -> add_my_exn my_exn2 f; File.must_recompute_cfg f
- | "h" -> add_catch my_exn my_exn2 f; File.must_recompute_cfg f
- | _ -> ()
+ | "f1" -> add_my_exn my_exn f; File.must_recompute_cfg f
+ | "f2" -> add_int_exn f; File.must_recompute_cfg f
+ | "f3" -> add_int_ptr_exn glob f; File.must_recompute_cfg f
+ | "f4" -> add_my_exn my_exn2 f; File.must_recompute_cfg f
+ | "h" -> add_catch my_exn my_exn2 f; File.must_recompute_cfg f
+ | _ -> ()
let add_exn ast =
let my_exn = ref None in
@@ -125,13 +125,13 @@ let add_exn ast =
let treat_glob =
function
| GCompTag(ci,_) ->
- (match !my_exn with
- | None -> my_exn := Some ci
- | Some _ -> my_exn2 := Some ci)
+ (match !my_exn with
+ | None -> my_exn := Some ci
+ | Some _ -> my_exn2 := Some ci)
| GVar(v,_,_) when v.vname = "x" -> glob := Some v
| GFun(f,_) ->
- change_body
- (Option.get !my_exn) (Option.get !my_exn2) (Option.get !glob) f
+ change_body
+ (Option.get !my_exn) (Option.get !my_exn2) (Option.get !glob) f
| _ -> ()
in
List.iter treat_glob ast.globals
@@ -141,28 +141,28 @@ let stmt stmt_node = { stmt_ghost = false; stmt_node }
let var v = { expr_loc = loc; expr_node = VARIABLE v }
let mk_exn_cabs b =
- { blabels = []; Cabs.battrs = [];
- Cabs.bstmts =
- [ stmt
- (IF (var "c",
- stmt (THROW (Some (var "x"),loc)),
- stmt (BLOCK (b,loc,loc)),loc))] }
+ { blabels = []; Cabs.battrs = [];
+ Cabs.bstmts =
+ [ stmt
+ (IF (var "c",
+ stmt (THROW (Some (var "x"),loc)),
+ stmt (BLOCK (b,loc,loc)),loc))] }
let mk_catch_cabs b =
{ blabels = []; Cabs.battrs = [];
Cabs.bstmts =
[ stmt
- (TRY_CATCH
- (stmt (BLOCK (b,loc,loc)),
- [Some ([SpecType Tint],("x",JUSTBASE,[],loc)),
- stmt (
- RETURN (
- { expr_loc = loc; expr_node = CONSTANT (CONST_INT "3")}, loc));
- None,
- stmt (
- RETURN (
- { expr_loc = loc; expr_node = CONSTANT (CONST_INT "4")}, loc))],
- loc))]}
+ (TRY_CATCH
+ (stmt (BLOCK (b,loc,loc)),
+ [Some ([SpecType Tint],("x",JUSTBASE,[],loc)),
+ stmt (
+ RETURN (
+ { expr_loc = loc; expr_node = CONSTANT (CONST_INT "3")}, loc));
+ None,
+ stmt (
+ RETURN (
+ { expr_loc = loc; expr_node = CONSTANT (CONST_INT "4")}, loc))],
+ loc))]}
let add_exn_cabs (f,l) =
let treat_one_global (b,d) =
diff --git a/tests/misc/find_enclosing_loop.ml b/tests/misc/find_enclosing_loop.ml
index cc510ae91eb510e392f836f279022ba05f39aab0..bf97a89df6479fba8dcfeb7cb317fba07fb3f6cc 100644
--- a/tests/misc/find_enclosing_loop.ml
+++ b/tests/misc/find_enclosing_loop.ml
@@ -2,29 +2,29 @@ open Cil
open Cil_types
class check =
-object(self)
- inherit Visitor.frama_c_inplace
- val current_loop = Stack.create ()
- method! vstmt_aux s =
- let res =
- match s.skind with
- | Loop _ -> Stack.push s current_loop;
- ChangeDoChildrenPost
- (s,
- fun s -> ignore (Stack.pop current_loop); s)
+ object(self)
+ inherit Visitor.frama_c_inplace
+ val current_loop = Stack.create ()
+ method! vstmt_aux s =
+ let res =
+ match s.skind with
+ | Loop _ -> Stack.push s current_loop;
+ ChangeDoChildrenPost
+ (s,
+ fun s -> ignore (Stack.pop current_loop); s)
| _ -> DoChildren
- in
- let has_loop =
- try
- Some
- (Kernel_function.find_enclosing_loop (Option.get self#current_kf) s)
- with Not_found -> None
- in
- (match has_loop with
- | Some s -> assert (s == Stack.top current_loop)
- | None -> assert (Stack.is_empty current_loop));
- res
-end
+ in
+ let has_loop =
+ try
+ Some
+ (Kernel_function.find_enclosing_loop (Option.get self#current_kf) s)
+ with Not_found -> None
+ in
+ (match has_loop with
+ | Some s -> assert (s == Stack.top current_loop)
+ | None -> assert (Stack.is_empty current_loop));
+ res
+ end
let run () =
Visitor.visitFramacFileSameGlobals (new check) (Ast.get());
diff --git a/tests/misc/interpreted_automata_dataflow_backward.ml b/tests/misc/interpreted_automata_dataflow_backward.ml
index 5cdf8a97f7592ad5ca3687de223a98585a23e28f..43e96ba1a24aa9b14808047fb4b9f26b6b73f360 100644
--- a/tests/misc/interpreted_automata_dataflow_backward.ml
+++ b/tests/misc/interpreted_automata_dataflow_backward.ml
@@ -16,7 +16,7 @@ struct
let widen v1 v2 =
if Set.subset v2 v1 then
- None (* Inclusion *)
+ None (* Inclusion *)
else
Some v2 (* No widening necessary *)
@@ -37,19 +37,19 @@ struct
let transfer t v =
let open Interpreted_automata in
let r = match t with
- | Skip | Prop _ | Leave _ | Return (None,_) ->
- v (* Nothing to do *)
- | Enter b ->
- Set.diff v (Set.of_list b.blocals) (* If unconditionnaly initialized, they should not be there *)
- | Instr (Set ((Var vi, NoOffset), exp, _), _)
- | Instr (Local_init (vi, AssignInit (SingleInit exp), _), _) ->
- Set.union (Set.remove vi v) (vars exp)
- | Guard (exp,_,_)
- | Instr (Set (_, exp, _), _)
- | Return (Some exp, _) ->
- Set.union v (vars exp)
- | Instr _ ->
- v (* All remaining cases are incorrectly ignored *)
+ | Skip | Prop _ | Leave _ | Return (None,_) ->
+ v (* Nothing to do *)
+ | Enter b ->
+ Set.diff v (Set.of_list b.blocals) (* If unconditionnaly initialized, they should not be there *)
+ | Instr (Set ((Var vi, NoOffset), exp, _), _)
+ | Instr (Local_init (vi, AssignInit (SingleInit exp), _), _) ->
+ Set.union (Set.remove vi v) (vars exp)
+ | Guard (exp,_,_)
+ | Instr (Set (_, exp, _), _)
+ | Return (Some exp, _) ->
+ Set.union v (vars exp)
+ | Instr _ ->
+ v (* All remaining cases are incorrectly ignored *)
in
Some r
end
diff --git a/tests/misc/interpreted_automata_dataflow_forward.ml b/tests/misc/interpreted_automata_dataflow_forward.ml
index 562e940d333a4445ff3efee943ceb22fdec088b6..6470ee925904435745bd9ead0d9d7a33cf929d00 100644
--- a/tests/misc/interpreted_automata_dataflow_forward.ml
+++ b/tests/misc/interpreted_automata_dataflow_forward.ml
@@ -25,7 +25,7 @@ struct
Map.find_opt vi v2 = Some x
in
if Map.for_all same_entry v1 then
- None (* Inclusion *)
+ None (* Inclusion *)
else
Some v2 (* No widening necessary *)
@@ -113,7 +113,7 @@ let run () =
Dataflow.Result.to_dot_file ConstantsDomain.pretty results filepath;
(* Output result to stdout *)
match Dataflow.Result.at_return results with
- | None ->
+ | None ->
Kernel.result "No result at the end of function %s." main_name
| Some result ->
Kernel.result "Results at the end of function %s:@.%a" main_name
diff --git a/tests/misc/log_twice.ml b/tests/misc/log_twice.ml
index 15145a121857b9156787d96f5cf526a94f4e308d..73238757c077b193a9a5ea1cfd9be83778134585 100644
--- a/tests/misc/log_twice.ml
+++ b/tests/misc/log_twice.ml
@@ -13,4 +13,4 @@ let run () =
Eva.Analysis.compute ();
()
-let () = Db.Main.extend run
+let () = Db.Main.extend run
diff --git a/tests/misc/my_visitor.ml b/tests/misc/my_visitor.ml
index 250f4fead95f446e45aee9828a6e8dc9caba91c1..832c2104127e461c46e5e120a9e9868262897194 100644
--- a/tests/misc/my_visitor.ml
+++ b/tests/misc/my_visitor.ml
@@ -2,13 +2,13 @@ open Logic_const
open Cil
open Cil_types
-module P =
+module P =
Plugin.Register
(struct
let name = "My_visitor"
let shortname = "my_vis"
let help = ""
- end)
+ end)
module S =
P.True(struct let option_name = "-s" let help = "" end)
@@ -19,11 +19,11 @@ module S2 =
module Enabled =
P.True(struct let option_name = "-my-visitor" let help = "" end)
-let emitter1 =
+let emitter1 =
Emitter.create "emitter1" [ Emitter.Code_annot ]
~correctness:[ S.parameter ] ~tuning:[]
-let emitter2 =
+let emitter2 =
Emitter.create "emitter2" [ Emitter.Code_annot ]
~correctness:[ S2.parameter ] ~tuning:[]
diff --git a/tests/misc/orphan_emitter.ml b/tests/misc/orphan_emitter.ml
index 573894ba52e7d833dad60df9e527c724769e1e63..2fd3673ffa30e0005f7e38f8b3663104e5dce937 100644
--- a/tests/misc/orphan_emitter.ml
+++ b/tests/misc/orphan_emitter.ml
@@ -4,7 +4,7 @@ module P =
let name = "Orphan"
let shortname = "orphan"
let help = ""
- end)
+ end)
module S =
P.True(struct let option_name = "-orphan" let help = "" end)
diff --git a/tests/misc/plugin_log.ml b/tests/misc/plugin_log.ml
index b43fe6d2811838a7e59ce441063fbca14a0a3581..81908f382636d5494b21425fc938182ab0d00d38 100644
--- a/tests/misc/plugin_log.ml
+++ b/tests/misc/plugin_log.ml
@@ -13,8 +13,8 @@ let main () =
debug ~level:0 "debug (level 0)";
warning "warning";
(* temporarily disabled to avoid leaking version number in test oracle
- error "error";
- failure "failure";*)
+ error "error";
+ failure "failure";*)
()
let () = Db.Main.extend main
diff --git a/tests/misc/pp_bin_hex.ml b/tests/misc/pp_bin_hex.ml
index 736ad51ae24f6d05af7d70ef09ec58e507aa3c87..e2402a8bd0bbbb6cf3c653ae1067b588aaf94dac 100644
--- a/tests/misc/pp_bin_hex.ml
+++ b/tests/misc/pp_bin_hex.ml
@@ -21,17 +21,17 @@ let () =
if not (Integer.equal z Integer.zero) then
testcase (Integer.neg z)
) [
- Integer.of_string "0" ;
- Integer.of_string "1" ;
- Integer.of_string "2" ;
- Integer.of_string "5" ;
- Integer.of_string "9" ;
- Integer.of_string "16" ;
- Integer.of_string "127" ;
- Integer.of_string "128" ;
- Integer.of_string "0xFF" ;
- Integer.of_string "0xFF0F000F" ;
- Integer.of_string "0x17070007" ;
- ] ;
+ Integer.of_string "0" ;
+ Integer.of_string "1" ;
+ Integer.of_string "2" ;
+ Integer.of_string "5" ;
+ Integer.of_string "9" ;
+ Integer.of_string "16" ;
+ Integer.of_string "127" ;
+ Integer.of_string "128" ;
+ Integer.of_string "0xFF" ;
+ Integer.of_string "0xFF0F000F" ;
+ Integer.of_string "0x17070007" ;
+ ] ;
hrule () ;
end
diff --git a/tests/misc/pp_int.ml b/tests/misc/pp_int.ml
index ef2d83bd0b7037492702c6398e5a7f2252c753c3..43fca9d7fcaf077cb60a9a471b86583b7c8dad32 100644
--- a/tests/misc/pp_int.ml
+++ b/tests/misc/pp_int.ml
@@ -87,4 +87,3 @@ let () =
] ;
]
end
-
diff --git a/tests/misc/remove_status_hyps.ml b/tests/misc/remove_status_hyps.ml
index 062c1688500a0019013337cb6eb2977043ece613..c382ddaaabc0f7b7ba73f904d9ef5b7dbbbcea1a 100644
--- a/tests/misc/remove_status_hyps.ml
+++ b/tests/misc/remove_status_hyps.ml
@@ -13,7 +13,7 @@ let pretty_status fmt = function
Format.fprintf fmt "%a (hyps: %t)"
Property_status.Emitted_status.pretty s
(fun fmt ->
- Pretty_utils.pp_list Property.pretty fmt e.Property_status.properties)
+ Pretty_utils.pp_list Property.pretty fmt e.Property_status.properties)
| Property_status.Never_tried ->
Format.fprintf fmt "no try"
| Property_status.Inconsistent _
@@ -23,9 +23,9 @@ let report msg l =
P.feedback msg;
List.iter
(fun (_, _, p) ->
- P.feedback "%a: %a"
- Property.pretty p
- pretty_status (Property_status.get p))
+ P.feedback "%a: %a"
+ Property.pretty p
+ pretty_status (Property_status.get p))
l
let main () =
@@ -39,12 +39,12 @@ let main () =
Annotations.fold_all_code_annot
~sorted:true
(fun stmt _ ca (even, acc) ->
- let ppt = Property.ip_of_code_annot_single kf stmt ca in
- (if even then Property_status.(emit emitter ~hyps:[] ppt Dont_know)
- else
+ let ppt = Property.ip_of_code_annot_single kf stmt ca in
+ (if even then Property_status.(emit emitter ~hyps:[] ppt Dont_know)
+ else
let hyps = List.map (fun (_, _, ppt) -> ppt) acc in
Property_status.(emit emitter ~hyps ppt Dont_know));
- not even, (ca, stmt, ppt) :: acc)
+ not even, (ca, stmt, ppt) :: acc)
(true, [])
in
let l = List.rev l in
diff --git a/tests/misc/save_comments.ml b/tests/misc/save_comments.ml
index c885ff86e080ca3d2461d86ee4501046281cefba..0c9dea658b023a88f7be802b18c95c7de552edab 100644
--- a/tests/misc/save_comments.ml
+++ b/tests/misc/save_comments.ml
@@ -6,7 +6,7 @@ let find_comment () =
let loc1 = Kernel_function.get_location kf in
let loc2 = Cil_datatype.Stmt.loc (Kernel_function.find_return kf) in
let zone = (fst loc1, snd loc2) in
- Format.printf
+ Format.printf
"@[In project %s, searching for comments between %a and %a:@\n%a\
@\nEnd of comments@."
(Project.get_name (Project.current()))
@@ -18,8 +18,8 @@ let find_comment () =
let run () =
let ast = Ast.get () in
let vis = object
- inherit Visitor.frama_c_inplace
- method! vglob_aux g = match g with GText s -> Format.printf "got global comment %s@." s; SkipChildren | _ -> DoChildren
+ inherit Visitor.frama_c_inplace
+ method! vglob_aux g = match g with GText s -> Format.printf "got global comment %s@." s; SkipChildren | _ -> DoChildren
end
in
ignore (Visitor.visitFramacFile vis ast);
diff --git a/tests/misc/vis_spec.ml b/tests/misc/vis_spec.ml
index ec8a33e2c84821e0734a0b22d7e61a51c96bd235..dce3f9c206dc50599fd9f2159060d542661e1cb6 100644
--- a/tests/misc/vis_spec.ml
+++ b/tests/misc/vis_spec.ml
@@ -2,36 +2,36 @@ open Cil_types
open Cil
class pathcrawlerVisitor prj =
-object(self)
- inherit Visitor.frama_c_copy prj
+ object(self)
+ inherit Visitor.frama_c_copy prj
- method! vspec sp =
- Format.printf "Considering spec of function %s@."
- (Kernel_function.get_name (Option.get self#current_kf));
- (match self#current_func with
- | Some f ->
- if f.svar.vname ="f" then (
- Format.printf "@[Funspec of f is@ @['%a'@]@ through visitor@]@."
- Printer.pp_funspec sp;
- Format.printf "@[It is@ @['%a'@]@ through get_spec@]@."
- Printer.pp_funspec
- (Annotations.funspec (Globals.Functions.get f.svar));
- )
- | None ->
- Format.printf "@[Function prototype;@ Funspec is@ @['%a'@]@]@."
- Printer.pp_funspec sp;
- );
- DoChildren
-end
+ method! vspec sp =
+ Format.printf "Considering spec of function %s@."
+ (Kernel_function.get_name (Option.get self#current_kf));
+ (match self#current_func with
+ | Some f ->
+ if f.svar.vname ="f" then (
+ Format.printf "@[Funspec of f is@ @['%a'@]@ through visitor@]@."
+ Printer.pp_funspec sp;
+ Format.printf "@[It is@ @['%a'@]@ through get_spec@]@."
+ Printer.pp_funspec
+ (Annotations.funspec (Globals.Functions.get f.svar));
+ )
+ | None ->
+ Format.printf "@[Function prototype;@ Funspec is@ @['%a'@]@]@."
+ Printer.pp_funspec sp;
+ );
+ DoChildren
+ end
-let startup () =
- ignore(Ast.get ());
- Format.printf "Starting visit@.";
- let prj = File.create_project_from_visitor "pcanalyzer"
+let startup () =
+ ignore(Ast.get ());
+ Format.printf "Starting visit@.";
+ let prj = File.create_project_from_visitor "pcanalyzer"
(fun prj -> new pathcrawlerVisitor prj)
- in
- Format.printf "End visit@.";
- Project.set_current prj;
+ in
+ Format.printf "End visit@.";
+ Project.set_current prj;
;;
let () = Db.Main.extend startup
diff --git a/tests/misc/visitor_creates_func_bts_1349.ml b/tests/misc/visitor_creates_func_bts_1349.ml
index ceb3a8926630460d64387c0e74e2eb97b85f2fa6..44d7b7cae636a1d6aa880f2ff6c65c01bd1914a0 100644
--- a/tests/misc/visitor_creates_func_bts_1349.ml
+++ b/tests/misc/visitor_creates_func_bts_1349.ml
@@ -11,12 +11,12 @@ class test prj = object(self)
self#get_filling_actions;
f.sbody <-
Cil.mkBlock
- [Cil.mkStmt ~valid_sid:true
- (Return (Some (Cil.evar x),Cil_datatype.Location.unknown))];
+ [Cil.mkStmt ~valid_sid:true
+ (Return (Some (Cil.evar x),Cil_datatype.Location.unknown))];
Queue.add
(fun () ->
- Globals.Functions.replace_by_definition
- (Cil.empty_funspec()) f Cil_datatype.Location.unknown)
+ Globals.Functions.replace_by_definition
+ (Cil.empty_funspec()) f Cil_datatype.Location.unknown)
self#get_filling_actions
;
[GFunDecl(Cil.empty_funspec(),f.svar,Cil_datatype.Location.unknown);
@@ -24,19 +24,19 @@ class test prj = object(self)
method! vglob_aux = function
| GVar (v,i,loc) ->
- let v'=
- Visitor.visitFramacVarDecl (self:>Visitor.frama_c_visitor) v
- in
- let i'=
- match i.init with
- | None -> { init = None }
- | Some i ->
- { init =
- Some (Visitor.visitFramacInit
- (self:>Visitor.frama_c_visitor) v' NoOffset i) }
- in
- let g = GVar(v',i',loc) in
- Cil.ChangeToPost (g::self#create_f(),fun x -> x)
+ let v'=
+ Visitor.visitFramacVarDecl (self:>Visitor.frama_c_visitor) v
+ in
+ let i'=
+ match i.init with
+ | None -> { init = None }
+ | Some i ->
+ { init =
+ Some (Visitor.visitFramacInit
+ (self:>Visitor.frama_c_visitor) v' NoOffset i) }
+ in
+ let g = GVar(v',i',loc) in
+ Cil.ChangeToPost (g::self#create_f(),fun x -> x)
| _ -> Cil.DoChildren
end
diff --git a/tests/misc/wstring_phase6.ml b/tests/misc/wstring_phase6.ml
index eca6470862ddd8b9df431b10a7b99c6af4e808f1..a7a36476e7bd7baf11e9e893971bb13722ca783b 100644
--- a/tests/misc/wstring_phase6.ml
+++ b/tests/misc/wstring_phase6.ml
@@ -6,16 +6,16 @@ let print_loc fmt (b,e) =
b.pos_lnum (b.pos_cnum - b.pos_bol) e.pos_lnum (e.pos_cnum - e.pos_bol)
class vis =
-object
- inherit Visitor.frama_c_inplace
- method! vexpr e =
- (match e.enode with
- | Const (CStr _ | CWStr _ as c) ->
- Kernel.result "@[<hov 0>@[<h 0>Constant %a@]@ location: %a@]"
- Printer.pp_constant c print_loc e.eloc
- | _ -> ());
- Cil.DoChildren
-end
+ object
+ inherit Visitor.frama_c_inplace
+ method! vexpr e =
+ (match e.enode with
+ | Const (CStr _ | CWStr _ as c) ->
+ Kernel.result "@[<hov 0>@[<h 0>Constant %a@]@ location: %a@]"
+ Printer.pp_constant c print_loc e.eloc
+ | _ -> ());
+ Cil.DoChildren
+ end
let do_it () = Visitor.visitFramacFileSameGlobals (new vis) (Ast.get())
diff --git a/tests/pdg/sets.ml b/tests/pdg/sets.ml
index 5fcdf037acd216631a506f0a396eba8a772d0209..f9759901253978aef39e3675d91663df60b7587e 100644
--- a/tests/pdg/sets.ml
+++ b/tests/pdg/sets.ml
@@ -1,16 +1,16 @@
open Db;;
open Cil_types;;
-
+
let pp_nodes msg nodes =
Kernel.result "%s" msg ;
List.iter (fun n -> Kernel.result "%a" (!Pdg.pretty_node false) n) nodes;;
-
+
exception Find of varinfo;;
-
+
let main _ =
let f = Globals.Functions.find_by_name "f" in
let pdg = !Pdg.get f in
-
+
(* Uncomment to retrieve sid *)
(*Kernel.Debug.set 1;;
Format.eprintf "@[%a@]@." Printer.pp_global (Kernel_function.get_global f);;
@@ -20,7 +20,7 @@ let main _ =
let node = !Pdg.find_stmt_node pdg stmt_1 in
let nodes = !Pdg.all_uses pdg [node] in
pp_nodes "Test [all_uses] stmt1" nodes;
-
+
(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
let y =
try
@@ -29,16 +29,16 @@ let main _ =
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.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.all_dpds pdg y_at_11_nodes in
@@ -54,5 +54,5 @@ let main _ =
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/rte/compute_annot.ml b/tests/rte/compute_annot.ml
index f6ec511a975118c8daa9a01e1201e30204e96e4f..4ae1c287163e1fb7ffd7e8f924eda11192cfe982 100644
--- a/tests/rte/compute_annot.ml
+++ b/tests/rte/compute_annot.ml
@@ -7,9 +7,9 @@ let print_status () =
let _, _, get_signedOv_status = !Db.RteGen.get_signedOv_status () in
Globals.Functions.iter
(fun kf ->
- Kernel.log "kf = %s rte_gen_status = %b\n"
- (Kernel_function.get_name kf)
- (get_signedOv_status kf))
+ Kernel.log "kf = %s rte_gen_status = %b\n"
+ (Kernel_function.get_name kf)
+ (get_signedOv_status kf))
let main () =
Dynamic.Parameter.Bool.set "-rte-mem" false;
diff --git a/tests/rte/my_annot_proxy.ml b/tests/rte/my_annot_proxy.ml
index 9c3c22da3d7e0397334396ec5e3fb0f23442e28b..f4c4b44f5f61b9657d327fd751f50ceee62adcd6 100644
--- a/tests/rte/my_annot_proxy.ml
+++ b/tests/rte/my_annot_proxy.ml
@@ -5,13 +5,13 @@ let print () =
let print_status () =
Kernel.log "printing status";
let rte_state_getter_list = !Db.RteGen.get_all_status () in
- Globals.Functions.iter
- (fun kf ->
- Kernel.log "kf = %s" (Kernel_function.get_name kf) ;
- List.iter
- (fun (s, _, getter) -> Kernel.log "- %s = %b" s (getter kf))
- rte_state_getter_list);
- Kernel.log "================================"
+ Globals.Functions.iter
+ (fun kf ->
+ Kernel.log "kf = %s" (Kernel_function.get_name kf) ;
+ List.iter
+ (fun (s, _, getter) -> Kernel.log "- %s = %b" s (getter kf))
+ rte_state_getter_list);
+ Kernel.log "================================"
let main () =
Dynamic.Parameter.Bool.set "-rte-mem" true;
diff --git a/tests/rte/my_annotation.ml b/tests/rte/my_annotation.ml
index c20cb6ed00ffcbdcf5d8401e56ff63ba7d5fa870..1aff9c30ecbb73fa398f28109665cc76c5d38686 100644
--- a/tests/rte/my_annotation.ml
+++ b/tests/rte/my_annotation.ml
@@ -7,9 +7,9 @@ let print_status () =
let _, _, get_signedOv_status = !Db.RteGen.get_signedOv_status () in
Globals.Functions.iter
(fun kf ->
- Kernel.log "kf = %s rte_gen_status = %b\n"
- (Kernel_function.get_name kf)
- (get_signedOv_status kf))
+ Kernel.log "kf = %s rte_gen_status = %b\n"
+ (Kernel_function.get_name kf)
+ (get_signedOv_status kf))
let main () =
Dynamic.Parameter.Bool.set "-rte-mem" true;
@@ -37,15 +37,15 @@ let main () =
print ();
print_status ();
-(* Dynamic.Parameter.Bool.set "-rte-all" true;*)
+ (* Dynamic.Parameter.Bool.set "-rte-all" true;*)
let one_on_two = ref true in
Globals.Functions.iter
(fun kf ->
- if !one_on_two then begin
- set_signed kf false;
- !Db.RteGen.annotate_kf kf
- end;
- one_on_two := not !one_on_two);
+ if !one_on_two then begin
+ set_signed kf false;
+ !Db.RteGen.annotate_kf kf
+ end;
+ one_on_two := not !one_on_two);
print () ;
print_status ()
diff --git a/tests/rte/rte_get_annot.ml b/tests/rte/rte_get_annot.ml
index b82fc3c317c706ea32d71c3bd7f9412d5a12eb61..da89041557ec72d35613ba6ece2094df6b7773e8 100644
--- a/tests/rte/rte_get_annot.ml
+++ b/tests/rte/rte_get_annot.ml
@@ -5,8 +5,8 @@ let print () =
File.pretty_ast ();
Kernel.log "================================"
-let get_rte_annotations =
- Dynamic.get ~plugin:"RteGen" "get_rte_annotations"
+let get_rte_annotations =
+ Dynamic.get ~plugin:"RteGen" "get_rte_annotations"
(Datatype.func
Cil_datatype.Stmt.ty
(let module L = Datatype.List(Cil_datatype.Code_annotation) in L.ty))
@@ -18,33 +18,33 @@ let fetch_stmts_visitor () = object
method! vstmt stmt = stmts <- stmt :: stmts ; DoChildren
end
-let get_stmts kf =
- match kf.fundec with
+let get_stmts kf =
+ match kf.fundec with
| Definition (f,_) ->
let vis = fetch_stmts_visitor () in
let _ = visitCilFunction (vis :> cilVisitor) f in
vis#fetch_stmts ()
| _ -> []
-let show_rte_of_kf kf =
+let show_rte_of_kf kf =
let is_annot = ref false in
- Kernel.log "Rte-generated annotations for function %a"
+ Kernel.log "Rte-generated annotations for function %a"
Kernel_function.pretty kf ;
List.iter
(fun stmt ->
- let lannot = get_rte_annotations stmt in
- match lannot with
- | [] -> ()
- | lannot ->
- is_annot := true;
- Kernel.log "For Statement %a"
- (Printer.without_annot Printer.pp_stmt) stmt;
- List.iter
- (fun a -> Kernel.log "%a" Printer.pp_code_annotation a)
- lannot)
+ let lannot = get_rte_annotations stmt in
+ match lannot with
+ | [] -> ()
+ | lannot ->
+ is_annot := true;
+ Kernel.log "For Statement %a"
+ (Printer.without_annot Printer.pp_stmt) stmt;
+ List.iter
+ (fun a -> Kernel.log "%a" Printer.pp_code_annotation a)
+ lannot)
(get_stmts kf);
if not !is_annot then Kernel.log "None"
-
+
let main () =
Ast.compute () ;
Kernel.SignedOverflow.on ();
diff --git a/tests/saveload/basic.ml b/tests/saveload/basic.ml
index cd897a5ac7498ae0fdcfbe8986561ac40c5337f1..61f23aace11c8e57b7aaa1fb9455b32cc90513b8 100644
--- a/tests/saveload/basic.ml
+++ b/tests/saveload/basic.ml
@@ -1,5 +1,5 @@
(* This datatype tests the bug fix of BTS #1277 *)
-module A =
+module A =
Datatype.Pair
(Datatype.List(Datatype.String))
(Datatype.List(Datatype.String))
@@ -11,6 +11,6 @@ module StateA =
let name = "Project.Test.StateA"
let dependencies = []
let default () = 0
- end)
+ end)
let () = StateA.set 10
diff --git a/tests/saveload/deps_A.ml b/tests/saveload/deps_A.ml
index b993678766344292041d59708ac11dea3dc7c8d8..15d795bd49240202b8c10fe3d6948973cfc06146 100644
--- a/tests/saveload/deps_A.ml
+++ b/tests/saveload/deps_A.ml
@@ -2,29 +2,28 @@ module StateA =
State_builder.Ref
(Datatype.Int)
(struct
- let name = "Project.Test.StateA"
- let dependencies = []
- let default () = 0
- end)
+ let name = "Project.Test.StateA"
+ let dependencies = []
+ let default () = 0
+ end)
module StateB =
State_builder.Option_ref
(Datatype.Bool)
(struct
- let name = "Project.Test.StateB"
- let dependencies = [ StateA.self ]
- end)
+ let name = "Project.Test.StateB"
+ let dependencies = [ StateA.self ]
+ end)
module StateC =
State_builder.Option_ref
(Datatype.Int)
(struct
- let name = "Project.Test.StateC"
- let dependencies = [ StateB.self ]
- end)
+ let name = "Project.Test.StateC"
+ let dependencies = [ StateB.self ]
+ end)
let () = StateA.set 10
let () = StateB.set (if StateA.get () = 10 then true else false)
let () = assert (StateB.get ())
let () = StateC.set (if StateB.get () then 10 else 5)
-
diff --git a/tests/saveload/deps_B.ml b/tests/saveload/deps_B.ml
index da3fa1b802799308054d0fd6ad93043be1aec1d4..f6a1be54cae60eaa98b98d2219abf0f1d58ee8a9 100644
--- a/tests/saveload/deps_B.ml
+++ b/tests/saveload/deps_B.ml
@@ -4,15 +4,15 @@ module StateABis =
(struct
let name = "Project.Test.StateABis"
let dependencies = []
- end)
+ end)
module StateB =
State_builder.Option_ref
(Datatype.Bool)
(struct
- let name = "Project.Test.StateB"
- let dependencies = [ StateABis.self ]
- end)
+ let name = "Project.Test.StateB"
+ let dependencies = [ StateABis.self ]
+ end)
let () = StateABis.set 10
let () = StateB.set (if StateABis.get () = 10 then true else false)
diff --git a/tests/saveload/deps_C.ml b/tests/saveload/deps_C.ml
index 20737f80415817fbc49c1007f1bd6706171d8f51..4c34c7f651003c96ce996bce5aede864d2ae250d 100644
--- a/tests/saveload/deps_C.ml
+++ b/tests/saveload/deps_C.ml
@@ -5,7 +5,7 @@ module StateA =
let name = "Project.Test.StateA"
let dependencies = []
let default () = 0
- end)
+ end)
module StateABis =
State_builder.Option_ref
@@ -13,7 +13,7 @@ module StateABis =
(struct
let name = "Project.Test.StateABis"
let dependencies = []
- end)
+ end)
let () = StateA.set 5
let () = StateABis.set 10
diff --git a/tests/saveload/deps_D.ml b/tests/saveload/deps_D.ml
index e6f0db7c8604f14ec3145dfd964c0869c0f5f40e..ae5157e302c54524c9747e431ccfcc7e22b05ef5 100644
--- a/tests/saveload/deps_D.ml
+++ b/tests/saveload/deps_D.ml
@@ -5,32 +5,32 @@ module StateA =
let name = "Project.Test.StateA"
let dependencies = []
let default () = 0
- end)
+ end)
module StateB =
State_builder.Option_ref
(Datatype.Bool)
(struct
- let name = "Project.Test.StateB"
- let dependencies = [ StateA.self ]
- end)
+ let name = "Project.Test.StateB"
+ let dependencies = [ StateA.self ]
+ end)
module StateD =
State_builder.Ref
(Datatype.Int)
(struct
- let name = "Project.Test.StateD"
- let dependencies = [ StateA.self ]
- let default () = 0
- end)
+ let name = "Project.Test.StateD"
+ let dependencies = [ StateA.self ]
+ let default () = 0
+ end)
module StateC =
State_builder.Option_ref
(Datatype.Int)
(struct
- let name = "Project.Test.StateC"
- let dependencies = [ StateB.self; StateD.self ]
- end)
+ let name = "Project.Test.StateC"
+ let dependencies = [ StateB.self; StateD.self ]
+ end)
let () = StateA.set 10
let () = StateB.set (StateA.get () = 10)
diff --git a/tests/saveload/deps_E.ml b/tests/saveload/deps_E.ml
index 01334a6b3bc15a16e2156860df9ee8fb70574c32..1e5347ab012160175d918845265e2438e3ea3532 100644
--- a/tests/saveload/deps_E.ml
+++ b/tests/saveload/deps_E.ml
@@ -5,10 +5,10 @@ module StateA =
State_builder.Ref
(Datatype.Int)
(struct
- let name = "Project.Test.StateA"
- let dependencies = []
- let default () = 0
- end)
+ let name = "Project.Test.StateA"
+ let dependencies = []
+ let default () = 0
+ end)
(* same name but incompatible with deps_A.ml *)
module StateB =
@@ -17,16 +17,16 @@ module StateB =
(struct
let name = "Project.Test.StateB"
let dependencies = []
- end)
+ end)
(* the unchanged dependency of StateB *)
module StateC =
State_builder.Option_ref
(Datatype.Int)
(struct
- let name = "Project.Test.StateC"
- let dependencies = [ StateB.self ]
- end)
+ let name = "Project.Test.StateC"
+ let dependencies = [ StateB.self ]
+ end)
let () = StateA.set 5
let () = StateB.set 10.
@@ -36,5 +36,5 @@ let main () =
assert (StateA.get () = 10);
assert (StateB.get_option () = None); (* reset to default *)
assert (StateC.get_option () = None) (* reset because of dependency of B *)
-
+
let () = Db.Main.extend main
diff --git a/tests/saveload/segfault_datatypes_A.ml b/tests/saveload/segfault_datatypes_A.ml
index 06b7659e9f53672552b610f8131038da28377287..7199ea9b1cb33a6a2305d9f56b4bf56db7531829 100644
--- a/tests/saveload/segfault_datatypes_A.ml
+++ b/tests/saveload/segfault_datatypes_A.ml
@@ -5,6 +5,6 @@ module StateA =
let name = "Project.Test.StateA"
let dependencies = []
let default () = 0
- end)
+ end)
let () = StateA.set 10
diff --git a/tests/saveload/segfault_datatypes_B.ml b/tests/saveload/segfault_datatypes_B.ml
index 2f25f1a2cc66a792a86aa5e38f29835477ad6d9d..746436bcd001881a173ad0b6660954755ff78677 100644
--- a/tests/saveload/segfault_datatypes_B.ml
+++ b/tests/saveload/segfault_datatypes_B.ml
@@ -4,6 +4,6 @@ module StateA =
(struct
let name = "Project.Test.StateA"
let dependencies = []
- end)
+ end)
let () = StateA.set 3
diff --git a/tests/saveload/serialized_queue.ml b/tests/saveload/serialized_queue.ml
index 88874f39aa5ee278d234d5cab2c7f726831be7e9..f29aec47f0a4ccf4dcd54bdd5903517e21c61cfc 100644
--- a/tests/saveload/serialized_queue.ml
+++ b/tests/saveload/serialized_queue.ml
@@ -19,4 +19,3 @@ let run () =
Project.on prj pretty ()
let () = run ()
-
diff --git a/tests/saveload/status.ml b/tests/saveload/status.ml
index 893411de94973ecd23d0b0748628032d70949a48..5337381c38f61d7ebd21bfe3dd76abd77f937f0b 100644
--- a/tests/saveload/status.ml
+++ b/tests/saveload/status.ml
@@ -20,20 +20,20 @@ let main () =
method !vstmt_aux stmt =
Annotations.iter_code_annot
(fun _ ca ->
- let kf = Kernel_function.find_englobing_kf stmt in
- let ps = Property.ip_of_code_annot kf stmt ca in
- List.iter
- (fun p ->
- Property_status.emit
- emitter
- p
- ~hyps:[
- Property.(
- ip_other "Blob" (OLGlob Cil_datatype.Location.unknown))]
- Property_status.Dont_know;
- Format.printf "%a@."
- Property_status.pretty (Property_status.get p))
- ps)
+ let kf = Kernel_function.find_englobing_kf stmt in
+ let ps = Property.ip_of_code_annot kf stmt ca in
+ List.iter
+ (fun p ->
+ Property_status.emit
+ emitter
+ p
+ ~hyps:[
+ Property.(
+ ip_other "Blob" (OLGlob Cil_datatype.Location.unknown))]
+ Property_status.Dont_know;
+ Format.printf "%a@."
+ Property_status.pretty (Property_status.get p))
+ ps)
stmt;
Cil.DoChildren
end in
diff --git a/tests/scope/bts971.ml b/tests/scope/bts971.ml
index 89738f59cc02e3c8bb87283012e3947061099539..5a4231067b4463e3e5e1647b6eb1acdb39d278fc 100644
--- a/tests/scope/bts971.ml
+++ b/tests/scope/bts971.ml
@@ -1,30 +1,30 @@
let find_pp kf_name =
- let kf = Globals.Functions.find_by_name kf_name in
- let stmt = Kernel_function.find_first_stmt kf in
- Format.printf "Current program point = first one in function '%s'@\n"
- kf_name;
- stmt, kf
+ let kf = Globals.Functions.find_by_name kf_name in
+ let stmt = Kernel_function.find_first_stmt kf in
+ Format.printf "Current program point = first one in function '%s'@\n"
+ kf_name;
+ stmt, kf
let compute_and_print pp str_data =
let stmt, kf = pp in
let lval_term = !Db.Properties.Interp.term_lval kf str_data in
let lval = !Db.Properties.Interp.term_lval_to_lval ~result:None lval_term in
let defs = Scope.Defs.get_defs kf stmt lval in
- Format.printf "* @[<v 2>Defs for (%s) at current program point=@[<v 2>@."
- str_data;
+ Format.printf "* @[<v 2>Defs for (%s) at current program point=@[<v 2>@."
+ str_data;
let _ = match defs with
- | None -> Format.printf "computation problem.@."
- | Some (defs, _undef) when Cil_datatype.Stmt.Hptset.is_empty defs ->
- Format.printf "no Defs found@."
- | Some (defs, _undef) ->
- Cil_datatype.Stmt.Hptset.iter
- (fun s ->
- Format.printf "%a: %a@\n"
- Printer.pp_location (Cil_datatype.Stmt.loc s)
- (Printer.without_annot Printer.pp_stmt) s)
- defs
- in
+ | None -> Format.printf "computation problem.@."
+ | Some (defs, _undef) when Cil_datatype.Stmt.Hptset.is_empty defs ->
+ Format.printf "no Defs found@."
+ | Some (defs, _undef) ->
+ Cil_datatype.Stmt.Hptset.iter
+ (fun s ->
+ Format.printf "%a: %a@\n"
+ Printer.pp_location (Cil_datatype.Stmt.loc s)
+ (Printer.without_annot Printer.pp_stmt) s)
+ defs
+ in
Format.printf "@]@]@."
open Cil_types
@@ -64,4 +64,3 @@ let main _ =
;;
let _ = Db.Main.extend main
-
diff --git a/tests/scope/zones.ml b/tests/scope/zones.ml
index 19d3afc121119fb4bfbd343f526d57b9b91b33ec..1e06b3584e36988ad6886ac41835386b5d0a74f2 100644
--- a/tests/scope/zones.ml
+++ b/tests/scope/zones.ml
@@ -1,6 +1,6 @@
(* when using toplevel.top :
-bin/topleval.top -eva tests/scope/zones.c
-#directory "cil/src";;
+ bin/topleval.top -eva tests/scope/zones.c
+ #directory "cil/src";;
*)
let fmt = Format.std_formatter;;
@@ -15,31 +15,31 @@ Kernel.Debug.set old_debug;;
let find_ret kf_name =
let kf = Globals.Functions.find_by_name kf_name in
let stmt = Kernel_function.find_return kf in
- Format.printf "Current program point = return in function %s@\n" kf_name;
- stmt, kf
+ Format.printf "Current program point = return in function %s@\n" kf_name;
+ stmt, kf
;;
let find_sid sid =
let stmt, kf = Kernel_function.find_from_sid sid in
- Format.printf "Current program point = before stmt %d in function %a@\n"
- sid Kernel_function.pretty kf;
- stmt, kf
+ Format.printf "Current program point = before stmt %d in function %a@\n"
+ sid Kernel_function.pretty kf;
+ stmt, kf
;;
let find_label kf_name lab_name =
let kf = Globals.Functions.find_by_name kf_name in
let stmt = !(Kernel_function.find_label kf lab_name) in
- Format.printf "Current program point = label %s in function %s@\n"
- lab_name kf_name;
- stmt, kf
+ Format.printf "Current program point = label %s in function %s@\n"
+ lab_name kf_name;
+ stmt, kf
let compute_and_print pp str_data =
let stmt, kf = pp in
let lval_term = !Db.Properties.Interp.term_lval kf str_data in
let lval = !Db.Properties.Interp.term_lval_to_lval ~result:None lval_term in
let (_used_stmts, zones) = Scope.Zones.build_zones kf stmt lval in
- Format.printf "Zones for %s at current program point =@.%a\n@\n"
- str_data Scope.Zones.pretty_zones zones
+ Format.printf "Zones for %s at current program point =@.%a\n@\n"
+ str_data Scope.Zones.pretty_zones zones
;;
let main _ =
diff --git a/tests/slicing/adpcm.ml b/tests/slicing/adpcm.ml
index 0da186815d051e27681f0ed1f6c4cacb639bcdbb..ff6515dce26737dc4355e611a7eaeca836bd31d8 100644
--- a/tests/slicing/adpcm.ml
+++ b/tests/slicing/adpcm.ml
@@ -14,4 +14,3 @@ ignore (test "uppol2" ~do_prop_to_callers:true ~resname (select_retres));;
let () =
Db.Main.extend
(fun _ -> ignore (test "uppol2" ~do_prop_to_callers:true (select_retres)))
-
diff --git a/tests/slicing/anim.ml b/tests/slicing/anim.ml
index 845f8405af0070998708af054255c0d803f8ef9d..50e23891052592eb8f602c19bb18a5990e8c8740 100644
--- a/tests/slicing/anim.ml
+++ b/tests/slicing/anim.ml
@@ -1,4 +1,4 @@
-(*
+(*
* Small example to view graphically the building process of a slicing project.
* To try it, use the following commands :
@@ -14,8 +14,8 @@ let add_select_fun_calls kf =
let selections =
Slicing.Api.Select.select_func_calls_into selections ~spare:false kf
in Slicing.Api.Select.iter_selects_internal
- (fun s -> !Db.Slicing.Request.add_selection_internal s)
- selections
+ (fun s -> !Db.Slicing.Request.add_selection_internal s)
+ selections
(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
diff --git a/tests/slicing/ex_spec_interproc.ml b/tests/slicing/ex_spec_interproc.ml
index a97a0bbebbd542fce41da037a0f1dd13105e4f30..f378201635ea019df2276d1c0ec0c8bea7ed1952 100644
--- a/tests/slicing/ex_spec_interproc.ml
+++ b/tests/slicing/ex_spec_interproc.ml
@@ -1,7 +1,7 @@
(* ledit bin/toplevel.top -deps tests/slicing/ex_spec_interproc.c
- #use "tests/slicing/select.ml";;
-ou
- #use "tests/slicing/ex_spec_interproc.ml";;
+ #use "tests/slicing/select.ml";;
+ ou
+ #use "tests/slicing/ex_spec_interproc.ml";;
*)
diff --git a/tests/slicing/horwitz.ml b/tests/slicing/horwitz.ml
index f897fa15e85842c275955a33c927714f609adda0..f8034d2bb8bfe58794f7aee9d97fa09214159c64 100644
--- a/tests/slicing/horwitz.ml
+++ b/tests/slicing/horwitz.ml
@@ -1,4 +1,4 @@
-(*
+(*
ledit bin/toplevel.top -deps tests/slicing/horwitz.c
#use "tests/slicing/select.ml";;
@@ -11,5 +11,3 @@ let () =
Db.Main.extend
(fun _ ->
ignore (test_select_data ~do_prop_to_callers:true "incr" "*pi"));;
-
-
diff --git a/tests/slicing/libAnim.ml b/tests/slicing/libAnim.ml
index a71ec650781bd5f599018550b7da38dc79315fe3..23e7f12f78434464f18f5a5fb86dc79f65e54442 100644
--- a/tests/slicing/libAnim.ml
+++ b/tests/slicing/libAnim.ml
@@ -1,5 +1,5 @@
(* Some useful function to use the graphical representation of a slicing
-* project. (see tests/slicing/anim.ml for a test) *)
+ * project. (see tests/slicing/anim.ml for a test) *)
(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
let use_dot =
@@ -28,7 +28,7 @@ let print_proj basename title n =
;;
(* apply all requests of the project and generate a .jpg file for each step.
-* (begin at number [n])
+ * (begin at number [n])
*)
let build_all_graphs basename title first_n =
Format.printf "Processing %s : " basename;
diff --git a/tests/slicing/libSelect.ml b/tests/slicing/libSelect.ml
index 6149a8dd0c1feb11cc3747e35108dd1cd5957491..fae01cc8b503d8b9ea25207c7d62c2617596d3aa 100644
--- a/tests/slicing/libSelect.ml
+++ b/tests/slicing/libSelect.ml
@@ -1,6 +1,6 @@
(* To use this in interactive mode :
-#use "tests/slicing/select.ml";;
+ #use "tests/slicing/select.ml";;
*)
exception Break
@@ -51,8 +51,8 @@ let apply () = Slicing.Api.Request.apply_next_internal (); print_project ()
(*--------------------------*)
(** clear a previously computed project and load a new source file,
-* starting at [entry_point] to be specified iif it is different from [main].
-* DOESN'T WORK at the moment because CIL datas are not cleared...*)
+ * starting at [entry_point] to be specified iif it is different from [main].
+ * DOESN'T WORK at the moment because CIL datas are not cleared...*)
(* [Julien 25/06/2007:] Should be possible to do now (?) *)
(*
let load_source_file ?entry_point filename =
@@ -83,19 +83,19 @@ let get_zones str_data (kinst, kf) =
let select_data_before_stmt str_data kinst kf =
let mark = Slicing.Api.Mark.make ~data:true ~addr:false ~ctrl:false in
let zone = get_zones str_data (kinst, kf) in
- Slicing.Api.Select.select_stmt_zone_internal kf kinst ~before:true zone mark
+ Slicing.Api.Select.select_stmt_zone_internal kf kinst ~before:true zone mark
(** build the selection for returned value of the function *)
let select_retres kf =
let ki = Kernel_function.find_return kf in
- try
- let loc = Db.Value.find_return_loc kf in
- let zone = Locations.(enumerate_valid_bits Read loc) in
- let mark = Slicing.Api.Mark.make ~data:true ~addr:false ~ctrl:false in
- let before = false in
- Slicing.Api.Select.select_stmt_zone_internal kf ki ~before zone mark
- with Db.Value.Void_Function -> raise No_return
+ try
+ let loc = Db.Value.find_return_loc kf in
+ let zone = Locations.(enumerate_valid_bits Read loc) in
+ let mark = Slicing.Api.Mark.make ~data:true ~addr:false ~ctrl:false in
+ let before = false in
+ Slicing.Api.Select.select_stmt_zone_internal kf ki ~before zone mark
+ with Db.Value.Void_Function -> raise No_return
;;
(** build the selection for the [data] at the end of the function *)
@@ -104,13 +104,13 @@ let select_data data kf =
let ki = Kernel_function.find_return kf in
let mark = Slicing.Api.Mark.make ~data:true ~addr:false ~ctrl:false in
let zone = get_zones data (ki, kf) in
- Slicing.Api.Select.select_stmt_zone_internal kf ki ~before:true zone mark
+ Slicing.Api.Select.select_stmt_zone_internal kf ki ~before:true zone mark
(* with Logic_interp.Error (_, str) -> raise (Unknown_data data) *)
with _ -> raise (Unknown_data data)
;;
(** build the selection ONLY for the control dependencies of the statement
-* [numstmt]*)
+ * [numstmt]*)
let select_ctrl numstmt kf =
try
let s = get_stmt numstmt in
@@ -130,17 +130,17 @@ let prop_to_callers (kf, ff) =
let callers = !Db.Value.callers kf in
let process_caller (kf_caller,_) =
let ff_caller = Slicing.Api.Slice.create kf_caller in
- Slicing.Api.Request.add_call_slice ~caller:ff_caller ~to_call:ff;
- prop kf_caller ff_caller
+ Slicing.Api.Request.add_call_slice ~caller:ff_caller ~to_call:ff;
+ prop kf_caller ff_caller
in
- List.iter process_caller callers
+ List.iter process_caller callers
in prop kf ff
(** compute and print a slice of [fname] where the selection is given by
-* [select_fct] (which could be [select_retres] or [(select_data str_data)].
-* If [do_prop_to_callers] if also recursively computes new functions for
-* [fname] callers in order to call the new slices. *)
+ * [select_fct] (which could be [select_retres] or [(select_data str_data)].
+ * If [do_prop_to_callers] if also recursively computes new functions for
+ * [fname] callers in order to call the new slices. *)
let test ?(keep_project=false) fname ?(do_prop_to_callers=false) select_fct =
if not keep_project then Slicing.Api.Project.reset_slicing ();
try
@@ -160,11 +160,11 @@ let test ?(keep_project=false) fname ?(do_prop_to_callers=false) select_fct =
extract_and_print ()
with
| No_return ->
- Format.printf
- "Impossible to select 'retres' for a void function (%s)\n" fname
+ Format.printf
+ "Impossible to select 'retres' for a void function (%s)\n" fname
| Unknown_data str ->
- Format.printf
- "Impossible to select this data : %s in %s\n" str fname
+ Format.printf
+ "Impossible to select this data : %s in %s\n" str fname
;;
let test_select_retres ?(do_prop_to_callers=false) fname =
diff --git a/tests/slicing/mark_all_slices.ml b/tests/slicing/mark_all_slices.ml
index 0f0ca762df66af1c6f065329b1d14fb81aca0cb7..368ca32111e0e6c146a934c0a1ad3c7f3bf02b98 100644
--- a/tests/slicing/mark_all_slices.ml
+++ b/tests/slicing/mark_all_slices.ml
@@ -1,7 +1,7 @@
(* ledit bin/toplevel.top -deps tests/slicing/mark_all_slices.c
- #use "tests/slicing/select.ml";;
-ou
- #use "tests/slicing/mark_all_slices.ml";;
+ #use "tests/slicing/select.ml";;
+ ou
+ #use "tests/slicing/mark_all_slices.ml";;
*)
@@ -38,7 +38,7 @@ let main _ =
(* select B2 in main_1 : this should create a second slice all_2
* and its result should be computed even if it is not needed by this request
- *)
+ *)
let select = select_data "B2" kf_main in
Slicing.Api.Request.add_slice_selection_internal ff_main select;
Slicing.Api.Request.apply_next_internal ();
diff --git a/tests/slicing/merge.ml b/tests/slicing/merge.ml
index 3b12cf6728f01660e87da29ada7c4c7a0e434f1f..779736380bbeacedb289bdd76ba997d4da072c04 100644
--- a/tests/slicing/merge.ml
+++ b/tests/slicing/merge.ml
@@ -1,4 +1,4 @@
-(*
+(*
* Small example to test function merge_slices.
* To try it, use the following commands :
diff --git a/tests/slicing/min_call.ml b/tests/slicing/min_call.ml
index de1b11726f2ce2c0f84dcaa1a34a626845603e33..ebb0e3e8983bf0c210980e6700575ac75ff6f5ab 100644
--- a/tests/slicing/min_call.ml
+++ b/tests/slicing/min_call.ml
@@ -50,7 +50,7 @@ let main _ =
(* Project2 :
* same than project1, except that we use [select_min_call_internal].
* But as [send_bis] is an undefined function, this makes no difference.
- *)
+ *)
Slicing.Api.Project.reset_slicing ();
(*let pdg_k = !Db.Pdg.get kf_k;;*)
let calls = !Db.Pdg.find_call_stmts (*pdg_k*)~caller:kf_k kf_send_bis in
@@ -69,7 +69,7 @@ let main _ =
* Select the calls to [k] to be visible in a minimal version.
* This builds an empty slice [k_1] for [k] and call it in [f] and [g].
* [f_1] is also called in [g_1] because it calls [k_1].
- *)
+ *)
Slicing.Api.Project.reset_slicing ();
add_select_fun_calls kf_k;
@@ -84,10 +84,10 @@ let main _ =
(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
(* Project4 is CAS_1 from Patrick's 19th April 2007 mail.
-* step 1 - select calls to send and apply : OK
-* step 2 - (automatically done in step1)
-* step 3 - select calls to send_bis and apply : TODO
-* step 4 - (automatically done in step3)
+ * step 1 - select calls to send and apply : OK
+ * step 2 - (automatically done in step1)
+ * step 3 - select calls to send_bis and apply : TODO
+ * step 4 - (automatically done in step3)
*)
(*
@@ -113,8 +113,8 @@ extract_and_print project;;
(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
(* Project5 : same than the previous one,
-* except that we create the two requests before applying.
-* *)
+ * except that we create the two requests before applying.
+ * *)
(*
let project = mk_project();;
diff --git a/tests/slicing/select_by_annot.ml b/tests/slicing/select_by_annot.ml
index 907f258bc0d565ba2f3570e5067d55a05534dd1e..c3dec000e6239395812460cca35e5dd40299bcda 100644
--- a/tests/slicing/select_by_annot.ml
+++ b/tests/slicing/select_by_annot.ml
@@ -12,11 +12,11 @@ let main _ =
let mark = Slicing.Api.Mark.make ~data:true ~addr:false ~ctrl:false in
let select = Slicing.Api.Select.empty_selects in
let select = Slicing.Api.Select.select_func_annots select mark
- ~spare:true ~threat:false ~user_assert:false ~slicing_pragma:true
- ~loop_inv:true ~loop_var:true kf
+ ~spare:true ~threat:false ~user_assert:false ~slicing_pragma:true
+ ~loop_inv:true ~loop_var:true kf
in
Slicing.Api.Request.add_persistent_selection select
- (*Slicing.Api.Request.read_annotations project kf_main ;;*)
+ (*Slicing.Api.Request.read_annotations project kf_main ;;*)
in
let kf_main = Globals.Functions.find_def_by_name "main" in
add_annot kf_main;
diff --git a/tests/slicing/select_simple.ml b/tests/slicing/select_simple.ml
index 3aa0403891373879e2f3a05719f72ac00fd4c239..3f4f91a882baf5854948d5ae40233726b28d64ec 100644
--- a/tests/slicing/select_simple.ml
+++ b/tests/slicing/select_simple.ml
@@ -1,5 +1,5 @@
(* ledit bin/toplevel.top -deps tests/slicing/simple_intra_slice.c
-* *)
+ * *)
include LibSelect ;;
diff --git a/tests/slicing/simple_intra_slice.ml b/tests/slicing/simple_intra_slice.ml
index 3746bbdf37d28c52eab3315d0c74485117b40a63..f9e17c3b87c76683424ec6fc3679609606e3beac 100644
--- a/tests/slicing/simple_intra_slice.ml
+++ b/tests/slicing/simple_intra_slice.ml
@@ -1,5 +1,5 @@
(* ledit bin/toplevel.top -deps tests/slicing/simple_intra_slice.c \
- < tests/slicing/simple_intra_slice.ml
+ < tests/slicing/simple_intra_slice.ml
*)
@@ -79,32 +79,32 @@ let main _ =
print_fct_stmts kf;
select_out0_and_print kf;
select_ctrl_and_print kf 40;
-(* G++. VP 2008-02-04: Was ki 113, and corresponded to
- if(c<Unknown) { goto L2; }, not to G++
- Fixed ki number to the test instead of the incrementation.
- As of this date, ki for G++ is 31.
- VP 2008-06-25 ki for G++ is 32
- VP 2008-07-17 ki for G++ is 37
- BY 2011-04-14 sid for G++ is 38
- VP 2012-04-09 sid for G++ is 44
- VP 2017-02-16 sid for G++ is 43
- *)
+ (* G++. VP 2008-02-04: Was ki 113, and corresponded to
+ if(c<Unknown) { goto L2; }, not to G++
+ Fixed ki number to the test instead of the incrementation.
+ As of this date, ki for G++ is 31.
+ VP 2008-06-25 ki for G++ is 32
+ VP 2008-07-17 ki for G++ is 37
+ BY 2011-04-14 sid for G++ is 38
+ VP 2012-04-09 sid for G++ is 44
+ VP 2017-02-16 sid for G++ is 43
+ *)
let kf = get_fct "f6" in
Format.printf "@[%a@]@\n" pretty_pdg kf;
print_fct_stmts kf;
select_ctrl_and_print kf 68;
-(* return_label
-VP 2008-02-04: Was ki 135, corresponding to first stmt in the else
-branch of if (i) { __retres = 0; goto return_label; }
- else { /* here*/__retres = 10*n; goto return_label; }
-Fixed ki number for this particular ki.
-As of this date, ki for return_label is 92
-VP 2008-06-25: ki for return_label is 96
-VP 2008-07-17: ki for return_label is 112
-BY 2011-04-14 sid for return_label is 128
-VP 2012-04-09: sid for return_label is 134
-*)
+ (* return_label
+ VP 2008-02-04: Was ki 135, corresponding to first stmt in the else
+ branch of if (i) { __retres = 0; goto return_label; }
+ else { /* here*/__retres = 10*n; goto return_label; }
+ Fixed ki number for this particular ki.
+ As of this date, ki for return_label is 92
+ VP 2008-06-25: ki for return_label is 96
+ VP 2008-07-17: ki for return_label is 112
+ BY 2011-04-14 sid for return_label is 128
+ VP 2012-04-09: sid for return_label is 134
+ *)
Slicing.Api.Project.pretty Format.std_formatter
diff --git a/tests/slicing/slice_no_body.ml b/tests/slicing/slice_no_body.ml
index 8bbcde8573d6d3d4821df039f2bfcfc92795c5a7..b27b4c9f33ac88b6f6b4170590d5f73a0b3152f7 100644
--- a/tests/slicing/slice_no_body.ml
+++ b/tests/slicing/slice_no_body.ml
@@ -1,5 +1,5 @@
(* ledit bin/toplevel.top -deps tests/slicing/slice_no_body.c
- #use "tests/slicing/select.ml";;
+ #use "tests/slicing/select.ml";;
*)
include LibSelect;;
@@ -7,10 +7,10 @@ include LibSelect;;
let callers kf = !Db.Value.callers kf
(** simple implementation to select every calls to [kf] source function.
-* The problem of this implementation is that it can generate several slice
-* for one function during propagation to the callers.
-* See [Slicing.Api.Request.select_fun_calls] for a better implementation.
-* *)
+ * The problem of this implementation is that it can generate several slice
+ * for one function during propagation to the callers.
+ * See [Slicing.Api.Request.select_fun_calls] for a better implementation.
+ * *)
let call_f kf =
let callers = callers kf in
let process_caller (kf_caller,_) =
@@ -18,7 +18,7 @@ let call_f kf =
Slicing.Api.Request.add_call_fun ~caller:ff_caller ~to_call:kf;
prop_to_callers (kf_caller, ff_caller);
in
- List.iter process_caller callers
+ List.iter process_caller callers
let slice_on_fun_calls kf =
let table = Cil_datatype.Varinfo.Hashtbl.create 17 in
@@ -27,13 +27,13 @@ let slice_on_fun_calls kf =
try Cil_datatype.Varinfo.Hashtbl.find table vf
with Not_found ->
let ff = Slicing.Api.Slice.create kf in
- Cil_datatype.Varinfo.Hashtbl.add table vf ff;
- ff
+ Cil_datatype.Varinfo.Hashtbl.add table vf ff;
+ ff
in
let rec process_ff_caller ff (kf_caller,_) =
let ff_caller = get_slice kf_caller in
- Slicing.Api.Request.add_call_slice ~caller:ff_caller ~to_call:ff;
- process_ff_callers (kf_caller, ff_caller)
+ Slicing.Api.Request.add_call_slice ~caller:ff_caller ~to_call:ff;
+ process_ff_callers (kf_caller, ff_caller)
and process_ff_callers (kf, ff) =
List.iter (process_ff_caller ff) (callers kf)
in
diff --git a/tests/slicing/switch.ml b/tests/slicing/switch.ml
index bff182f72adf37a9450c052fc63812e540b44896..3ca361344c91d376826f603ced718685d0c257ac 100644
--- a/tests/slicing/switch.ml
+++ b/tests/slicing/switch.ml
@@ -1,5 +1,5 @@
(* ledit bin/toplevel.top -deps tests/slicing/switch.c
-* *)
+ * *)
include LibSelect ;;
@@ -8,4 +8,3 @@ let main _ =
test_select_data "main" "y";
test_select_data "main" "z"
let () = Db.Main.extend main
-
diff --git a/tests/spec/Extend.ml b/tests/spec/Extend.ml
index af1f9f6510af20f330150938ce0703849e464a3c..db2b0600fb056e3493e2567ff559ebaf3b460813 100644
--- a/tests/spec/Extend.ml
+++ b/tests/spec/Extend.ml
@@ -18,10 +18,10 @@ module Bar_table =
(Datatype.Int.Hashtbl)
(Datatype.List(Cil_datatype.Predicate))
(struct
- let name = "Bar_table"
- let dependencies = [ Count.self ]
- let size = 3
- end)
+ let name = "Bar_table"
+ let dependencies = [ Count.self ]
+ let size = 3
+ end)
let type_bar typing_context _loc l =
let i = Count.next() in
@@ -57,7 +57,7 @@ let visit_bar vis ext =
Cil.SkipChildren
end
| Ext_terms _ | Ext_preds _ | Ext_annot _ ->
- Kernel.fatal "bar extension should have ids as arguments"
+ Kernel.fatal "bar extension should have ids as arguments"
let type_baz typing_context _loc l =
let t =
diff --git a/tests/spec/Extend_preprocess.ml b/tests/spec/Extend_preprocess.ml
index 51e60d554404dca8e533abfada8cadc183efc44c..d33a4be1a1a3d31609c3a0bf1da7b370688da188 100644
--- a/tests/spec/Extend_preprocess.ml
+++ b/tests/spec/Extend_preprocess.ml
@@ -7,8 +7,8 @@ open Logic_const
- code annotation: ca
- next statement: ns
- global: gl
- replaces node "must_replace(x)" with "<kind>_ok(x)". The typing phase
- validates that we find the right "<kind>_ok" for each kind of extension:
+ replaces node "must_replace(x)" with "<kind>_ok(x)". The typing phase
+ validates that we find the right "<kind>_ok" for each kind of extension:
- if a must_replace is found, it fails,
- if the wrong kind is found, a "\false" is generated
- if everything is ok "\true" is generated
diff --git a/tests/spec/Extend_recursive_preprocess.ml b/tests/spec/Extend_recursive_preprocess.ml
index 51b53f09b821d9ff3544ab39ff265e6d30366235..49ebe8a4369d0367afcecc959f034e61381861d1 100644
--- a/tests/spec/Extend_recursive_preprocess.ml
+++ b/tests/spec/Extend_recursive_preprocess.ml
@@ -67,7 +67,7 @@ let () = Acsl_extension.register_global
~printer:ext_fooo_printer ~visitor:ext_fooo_visitor false ;
Acsl_extension.register_global_block
"gl_foo" ~preprocessor:preprocess_foo_ptree ext_typing_foo
- ~visitor:ext_foo_visitor false
+ ~visitor:ext_foo_visitor false
let run () =
let old = Project.current () in
diff --git a/tests/spec/Type_of_term.ml b/tests/spec/Type_of_term.ml
index 44a1b404faa7d3d80ec4c5613a6834ad31de15d9..30350f7bc83682ce293385dccfec0cbbb1015729 100644
--- a/tests/spec/Type_of_term.ml
+++ b/tests/spec/Type_of_term.ml
@@ -1,11 +1,11 @@
open Cil_types
include Plugin.Register
- (struct
+ (struct
let name = "type_of_term"
let shortname = "type_of_term"
let help = "checks typeOfTermLval over sets"
- end)
+ end)
class visitor =
object
diff --git a/tests/spec/add_global.ml b/tests/spec/add_global.ml
index ddb4d76221225860fa846fced0a6450a7d75f0e3..20497076ec3e57581978dddbee179f5355356a45 100644
--- a/tests/spec/add_global.ml
+++ b/tests/spec/add_global.ml
@@ -4,28 +4,28 @@ let emitter =
Emitter.create "Fancy" [ Emitter.Global_annot ] ~correctness:[] ~tuning:[]
class vis prj =
-object(self)
- inherit Visitor.frama_c_copy prj
+ object(self)
+ inherit Visitor.frama_c_copy prj
- method! vglob_aux g =
- match g with
- | GFun ({ svar = { vname = "main" }},_) ->
- let ax =
- Daxiomatic
- ("MyAxiomatic",
- [ Dlemma(
- "myaxiom", [], [],
- Logic_const.(toplevel_predicate ~kind:Admit ptrue),
- [], Cil_datatype.Location.unknown)],
- [], Cil_datatype.Location.unknown)
- in
- Queue.add (fun () -> Annotations.add_global emitter ax)
- self#get_filling_actions;
- Cil.ChangeDoChildrenPost
- ([ GAnnot(ax, Cil_datatype.Location.unknown); g ], fun x -> x)
- | _ -> Cil.DoChildren
+ method! vglob_aux g =
+ match g with
+ | GFun ({ svar = { vname = "main" }},_) ->
+ let ax =
+ Daxiomatic
+ ("MyAxiomatic",
+ [ Dlemma(
+ "myaxiom", [], [],
+ Logic_const.(toplevel_predicate ~kind:Admit ptrue),
+ [], Cil_datatype.Location.unknown)],
+ [], Cil_datatype.Location.unknown)
+ in
+ Queue.add (fun () -> Annotations.add_global emitter ax)
+ self#get_filling_actions;
+ Cil.ChangeDoChildrenPost
+ ([ GAnnot(ax, Cil_datatype.Location.unknown); g ], fun x -> x)
+ | _ -> Cil.DoChildren
-end
+ end
let transform () =
Ast.compute ();
diff --git a/tests/spec/assigns_from_kf.ml b/tests/spec/assigns_from_kf.ml
index 875006cd3a6d37b85f257a7acae2f2a9d36ca615..d0c1e3965c83412df495adc03bcd88a623f2a509 100644
--- a/tests/spec/assigns_from_kf.ml
+++ b/tests/spec/assigns_from_kf.ml
@@ -1,4 +1,4 @@
let run () =
- Globals.Functions.iter (fun kf -> ignore (Annotations.funspec kf))
+ Globals.Functions.iter (fun kf -> ignore (Annotations.funspec kf))
let () = Db.Main.extend run
diff --git a/tests/spec/bts0655.ml b/tests/spec/bts0655.ml
index 4394b5784d45492e3729ac99ceeb85f56761b993..6137de01c4f3443ed4e811608d4a18ca94de7a6f 100644
--- a/tests/spec/bts0655.ml
+++ b/tests/spec/bts0655.ml
@@ -1,4 +1,4 @@
-include
+include
Plugin.Register
(struct
let name = "bts0655"
@@ -8,13 +8,13 @@ include
class check_float =
-object
-inherit Visitor.frama_c_inplace
- method! vterm t =
- result "term %a has type %a"
- Printer.pp_term t Printer.pp_logic_type t.Cil_types.term_type;
- Cil.DoChildren
-end
+ object
+ inherit Visitor.frama_c_inplace
+ method! vterm t =
+ result "term %a has type %a"
+ Printer.pp_term t Printer.pp_logic_type t.Cil_types.term_type;
+ Cil.DoChildren
+ end
let run () =
let f = Ast.get () in
diff --git a/tests/spec/comparison.ml b/tests/spec/comparison.ml
index 6b01aee38fd307ade41855386117d59316cf462d..b04cbf629387bf88dfc337863dfbed17b492e2bb 100644
--- a/tests/spec/comparison.ml
+++ b/tests/spec/comparison.ml
@@ -7,22 +7,22 @@ let run () =
inherit Visitor.frama_c_inplace
method! vterm t =
match t.term_node with
- | TBinOp ((Lt | Gt | Le | Ge | Eq | Ne), t1, t2) ->
- Kernel.result
- "Term comparison between %a of type %a and %a of type %a"
- Printer.pp_term t1 Printer.pp_logic_type t1.term_type
- Printer.pp_term t2 Printer.pp_logic_type t2.term_type;
- DoChildren
- | _ -> DoChildren
+ | TBinOp ((Lt | Gt | Le | Ge | Eq | Ne), t1, t2) ->
+ Kernel.result
+ "Term comparison between %a of type %a and %a of type %a"
+ Printer.pp_term t1 Printer.pp_logic_type t1.term_type
+ Printer.pp_term t2 Printer.pp_logic_type t2.term_type;
+ DoChildren
+ | _ -> DoChildren
method! vpredicate p =
match p.pred_content with
- | Prel ((Rlt | Rgt | Rle | Rge | Req | Rneq), t1, t2) ->
- Kernel.result
- "Predicate comparison between %a of type %a and %a of type %a"
- Printer.pp_term t1 Printer.pp_logic_type t1.term_type
- Printer.pp_term t2 Printer.pp_logic_type t2.term_type;
- DoChildren
- | _ -> DoChildren
+ | Prel ((Rlt | Rgt | Rle | Rge | Req | Rneq), t1, t2) ->
+ Kernel.result
+ "Predicate comparison between %a of type %a and %a of type %a"
+ Printer.pp_term t1 Printer.pp_logic_type t1.term_type
+ Printer.pp_term t2 Printer.pp_logic_type t2.term_type;
+ DoChildren
+ | _ -> DoChildren
end
in
Visitor.visitFramacFileSameGlobals vis (Ast.get())
diff --git a/tests/spec/expr_to_term.ml b/tests/spec/expr_to_term.ml
index 0e05b84eb593d2bf9a9c3c061a469d8096ae6054..41b49eb9e3ed3eff4355af91ab4201f08011548e 100644
--- a/tests/spec/expr_to_term.ml
+++ b/tests/spec/expr_to_term.ml
@@ -5,14 +5,14 @@ let emitter = Emitter.(create "Test" [Funspec] ~correctness:[] ~tuning:[])
let check_expr_term check fct s post =
let exp =
match s.skind with
- | Instr (Set (lv,_,loc)) -> Cil.new_exp ~loc (Lval lv)
- | If (c,_,_,_) -> c
- | _ -> Kernel.fatal "Unexpected statement %a" Printer.pp_stmt s
+ | Instr (Set (lv,_,loc)) -> Cil.new_exp ~loc (Lval lv)
+ | If (c,_,_,_) -> c
+ | _ -> Kernel.fatal "Unexpected statement %a" Printer.pp_stmt s
in
let term =
match post with
- | (_,{ip_content={tp_statement={pred_content = Papp(_,_,[l;_])}}}) -> l
- | _ -> Kernel.fatal "Unexpected ensures %a" Printer.pp_post_cond post
+ | (_,{ip_content={tp_statement={pred_content = Papp(_,_,[l;_])}}}) -> l
+ | _ -> Kernel.fatal "Unexpected ensures %a" Printer.pp_post_cond post
in
let term' = Logic_utils.expr_to_term ~coerce:false exp in
if check && not (Cil_datatype.Term.equal term term') then
@@ -44,7 +44,7 @@ let treat_fct check fct =
let stmts =
List.filter
(function
- { skind = Instr (Set (lv,_,_)) } ->
+ { skind = Instr (Set (lv,_,_)) } ->
(match lv with (Var v,_) -> v.vglob | _ -> true)
| { skind = If _ } -> true
| _ -> false)
diff --git a/tests/spec/extend_extern.ml b/tests/spec/extend_extern.ml
index 50dc6941ce3f3691e515f2d9bc04f59f1db844c9..e5c2f208daa0da69b050079e2917b19e417fc40d 100644
--- a/tests/spec/extend_extern.ml
+++ b/tests/spec/extend_extern.ml
@@ -25,9 +25,9 @@ let main () =
"Checking handler of exception occurring in extension typing";
Ast.compute (); assert false
with
- | Log.AbortFatal _ -> Kernel.feedback "Extension typing failed as expected"
- | Not_found -> Kernel.fatal "kernel did not capture our exception"
- | Assert_failure _ -> Kernel.fatal "kernel silently captured our exception"
+ | Log.AbortFatal _ -> Kernel.feedback "Extension typing failed as expected"
+ | Not_found -> Kernel.fatal "kernel did not capture our exception"
+ | Assert_failure _ -> Kernel.fatal "kernel silently captured our exception"
let () = Kernel.TypeCheck.set false
diff --git a/tests/spec/location_char.ml b/tests/spec/location_char.ml
index 335700d2f5108e080ce20cdfef723dc76ed0d324..59768fd96d6e2f7a79f844c3eb7514e5b84a7b57 100644
--- a/tests/spec/location_char.ml
+++ b/tests/spec/location_char.ml
@@ -15,23 +15,23 @@ class print_term = object(self)
method! vterm v =
if not self#should_print then Cil.SkipChildren
else begin
- Kernel.feedback
- "Term %a:@\nstart %a@\nend %a"
- Printer.pp_term v
- print_pos (fst v.term_loc)
- print_pos (snd v.term_loc);
- Cil.DoChildren
- end
+ Kernel.feedback
+ "Term %a:@\nstart %a@\nend %a"
+ Printer.pp_term v
+ print_pos (fst v.term_loc)
+ print_pos (snd v.term_loc);
+ Cil.DoChildren
+ end
method! vpredicate p =
if not self#should_print then Cil.SkipChildren
else begin
- Kernel.feedback
- "Predicate %a:@\nstart %a@\nend %a"
- Printer.pp_predicate p
- print_pos (fst p.pred_loc)
- print_pos (snd p.pred_loc);
- Cil.DoChildren
- end
+ Kernel.feedback
+ "Predicate %a:@\nstart %a@\nend %a"
+ Printer.pp_predicate p
+ print_pos (fst p.pred_loc)
+ print_pos (snd p.pred_loc);
+ Cil.DoChildren
+ end
end
let main () =
diff --git a/tests/spec/model.ml b/tests/spec/model.ml
index fba3cca209a56078e72acc82411c988a1b1b2cc7..0199a1377741054724df687749950ae71605b6dd 100644
--- a/tests/spec/model.ml
+++ b/tests/spec/model.ml
@@ -1,12 +1,12 @@
open Cil_types
-let find () =
+let find () =
let module M = struct exception Found of typeinfo end in
try
List.iter
(function
| GType (ty,_) ->
- if ty.tname = "T" then raise (M.Found ty)
+ if ty.tname = "T" then raise (M.Found ty)
| _ -> ())
(Ast.get ()).globals;
Kernel.fatal "No typedef for T: test is broken"
@@ -21,7 +21,7 @@ let print_models typ =
let e = Emitter.create "test" [Emitter.Global_annot] ~correctness:[] ~tuning:[]
let add_model ty =
- let m =
+ let m =
{ mi_name = "test_field";
mi_attr = [];
mi_field_type = Linteger;
diff --git a/tests/spec/pp_empty_spec.ml b/tests/spec/pp_empty_spec.ml
index 6a8482f2a27516a60c871d6c6b5961ace329e1aa..44d43d49c608c905cabfd37e5b05f25ceb60bf7d 100644
--- a/tests/spec/pp_empty_spec.ml
+++ b/tests/spec/pp_empty_spec.ml
@@ -16,7 +16,7 @@ let run () =
Annotations.add_ensures e main [];
File.pretty_ast();
(try
- Annotations.add_complete e main ["foo"; "bar"];
+ Annotations.add_complete e main ["foo"; "bar"];
with
Log.AbortFatal s -> Kernel.warning "Caught fatal error: %s" s);
(try
diff --git a/tests/spec/property_test.ml b/tests/spec/property_test.ml
index 9be9b8114bedc86a765e346bb25cafc41490f591..00407c161ac46f53abe7aa0ccd0f38fc3d5a203d 100644
--- a/tests/spec/property_test.ml
+++ b/tests/spec/property_test.ml
@@ -1,7 +1,7 @@
open Cil
open Cil_types
-let emitter =
+let emitter =
Emitter.create "Property_test" [ Emitter.Funspec ] ~correctness:[] ~tuning:[]
class visit prj =
@@ -14,19 +14,19 @@ class visit prj =
let x = Cil.cvar_to_lvar x in
let c = Globals.Vars.find_from_astinfo "c" (VFormal kf) in
let c = Cil.cvar_to_lvar c in
- b.b_assigns <-
- Writes
- [ Logic_const.new_identified_term (Logic_const.tvar x),
- From [ Logic_const.new_identified_term (Logic_const.tvar x);
- Logic_const.new_identified_term (Logic_const.tvar c)]
- ];
+ b.b_assigns <-
+ Writes
+ [ Logic_const.new_identified_term (Logic_const.tvar x),
+ From [ Logic_const.new_identified_term (Logic_const.tvar x);
+ Logic_const.new_identified_term (Logic_const.tvar c)]
+ ];
let nkf = Visitor_behavior.Get.kernel_function self#behavior kf in
let keep_empty = true in
let post b =
Queue.add
(fun () ->
Annotations.add_assigns ~keep_empty emitter nkf b.b_assigns)
- self#get_filling_actions;
+ self#get_filling_actions;
b
in
ChangeDoChildrenPost(b, post)
@@ -60,7 +60,7 @@ let show_properties () =
Property_status.fold
(fun p acc ->
let s = Format.asprintf "Status of %a: %a@."
- Property.pretty p Property_status.pretty (Property_status.get p)
+ Property.pretty p Property_status.pretty (Property_status.get p)
in
Datatype.String.Set.add s acc
) Datatype.String.Set.empty
@@ -68,7 +68,7 @@ let show_properties () =
Datatype.String.Set.iter (Format.pp_print_string Format.std_formatter) strs
let run () =
- let prj =
+ let prj =
File.create_project_from_visitor "property_test" (fun p -> new visit p)
in
show_properties ();
diff --git a/tests/spec/type_constructors_in_env.ml b/tests/spec/type_constructors_in_env.ml
index 5d64434081c91a1fb7c2c49b61b33b447331e6ed..91848fca46bde9e68c9fa474f0419c94aa6d9ddf 100644
--- a/tests/spec/type_constructors_in_env.ml
+++ b/tests/spec/type_constructors_in_env.ml
@@ -1,8 +1,8 @@
let run () =
Ast.compute ();
(match Logic_env.find_all_logic_functions "f" with
- | [] -> Kernel.fatal "f should be in the environment"
- | _ -> ());
+ | [] -> Kernel.fatal "f should be in the environment"
+ | _ -> ());
(try
ignore (Logic_env.find_logic_ctor "A")
with Not_found -> Kernel.fatal "A should be in the environment");
diff --git a/tests/syntax/Enum_repr.ml b/tests/syntax/Enum_repr.ml
index 8c0d7d7b512ae19305c6ad1389e21adea26ddd1a..907d611a59531e83826bbde6cf7e45831311cc4d 100644
--- a/tests/syntax/Enum_repr.ml
+++ b/tests/syntax/Enum_repr.ml
@@ -6,16 +6,16 @@ let warn_cast =
Kernel.feedback ~source:(fst e.eloc) "Inserted implicit cast from %a to %a"
Printer.pp_typ t1 Printer.pp_typ t2;
typeForInsertedCast e t1 t2
-
+
let () = Cabs2cil.typeForInsertedCast := warn_cast
let run () =
let f = Ast.get () in
let output = function
| GEnumTag(e,_) ->
- Kernel.feedback "Enum %s is represented by %a@."
- e.ename Printer.pp_ikind e.ekind
+ Kernel.feedback "Enum %s is represented by %a@."
+ e.ename Printer.pp_ikind e.ekind
| _ -> ()
- in
+ in
List.iter output f.globals
let () = Db.Main.extend run
diff --git a/tests/syntax/Refresh_visitor.ml b/tests/syntax/Refresh_visitor.ml
index d4075698d6899674174c5738c32b5e3eb3a02685..b5473e4babc253445b1cdc78594f3b683f93830d 100644
--- a/tests/syntax/Refresh_visitor.ml
+++ b/tests/syntax/Refresh_visitor.ml
@@ -5,14 +5,14 @@ let category = Kernel.register_category "refresh-test"
module Check(M: Datatype.S_with_collections) =
struct
- let check cat fold bhv =
- let f o c (orig, copy) = M.Set.add o orig, M.Set.add c copy in
- let (orig,copy) = fold bhv f (M.Set.empty, M.Set.empty) in
- let common = M.Set.inter orig copy in
- if not (M.Set.is_empty common) then begin
- Format.printf "ids for %s are not properly refreshed.@." cat;
- end;
- orig, copy, common
+ let check cat fold bhv =
+ let f o c (orig, copy) = M.Set.add o orig, M.Set.add c copy in
+ let (orig,copy) = fold bhv f (M.Set.empty, M.Set.empty) in
+ let common = M.Set.inter orig copy in
+ if not (M.Set.is_empty common) then begin
+ Format.printf "ids for %s are not properly refreshed.@." cat;
+ end;
+ orig, copy, common
end
module CheckVarinfo = Check(Cil_datatype.Varinfo)
@@ -36,37 +36,37 @@ let main () =
if Kernel.is_debug_key_enabled category then begin
Varinfo.Set.iter
(fun x ->
- Format.printf "variable id %d (%s) is in orig@." x.vid x.vname)
+ Format.printf "variable id %d (%s) is in orig@." x.vid x.vname)
orig_id;
Varinfo.Set.iter
(fun x ->
- Format.printf "variable id %d (%s) is in copy@." x.vid x.vname)
+ Format.printf "variable id %d (%s) is in copy@." x.vid x.vname)
copy_id;
Varinfo.Set.iter
(fun x -> Format.printf "variable id %d (%s) is reused@." x.vid x.vname)
shared_id;
- end;
+ end;
let _ =
CheckCompinfo.check "compinfo" Fold.compinfo vis#behavior
in
let _ =
CheckStmt.check "stmt" Fold.stmt vis#behavior;
in
- let orig_id, copy_id, shared_id =
+ let orig_id, copy_id, shared_id =
CheckLogic_var.check "logic var" Fold.logic_var vis#behavior
in
if Kernel.is_debug_key_enabled category then begin
Logic_var.Set.iter
(fun x -> Format.printf "logic variable id %d (%s) is in orig@."
- x.lv_id x.lv_name)
+ x.lv_id x.lv_name)
orig_id;
Logic_var.Set.iter
(fun x -> Format.printf "logic variable id %d (%s) is in copy@."
- x.lv_id x.lv_name)
+ x.lv_id x.lv_name)
copy_id;
Logic_var.Set.iter
(fun x -> Format.printf "logic variable id %d (%s) is reused@."
- x.lv_id x.lv_name)
+ x.lv_id x.lv_name)
shared_id;
end
);
diff --git a/tests/syntax/ast_diff_1.ml b/tests/syntax/ast_diff_1.ml
index fd43df597f6eb2b8a04e96c5db8600afcd28a6f1..9cf6b01c5d5a3c04b1e180846e05ad48883ebc5b 100644
--- a/tests/syntax/ast_diff_1.ml
+++ b/tests/syntax/ast_diff_1.ml
@@ -1,9 +1,9 @@
include Plugin.Register(
- struct
- let name = "AST diff test"
- let shortname = "AST diff test"
- let help = "Show results of AST diff computation"
- end)
+ struct
+ let name = "AST diff test"
+ let shortname = "AST diff test"
+ let help = "Show results of AST diff computation"
+ end)
let show_var vi c =
result "Variable %a: %a"
diff --git a/tests/syntax/copy_visitor_bts_1073.ml b/tests/syntax/copy_visitor_bts_1073.ml
index d057ae1f8327c8b9dc043b61cc4fe3feb1133837..65cfeb144d9e11ed0dff43387c254d8ff4088af3 100644
--- a/tests/syntax/copy_visitor_bts_1073.ml
+++ b/tests/syntax/copy_visitor_bts_1073.ml
@@ -1,11 +1,11 @@
open Cil_types
open Cil
-class vis prj =
-object(self)
- inherit Visitor.frama_c_refresh prj
- method! vglob_aux g =
- match g with
+class vis prj =
+ object(self)
+ inherit Visitor.frama_c_refresh prj
+ method! vglob_aux g =
+ match g with
| GFun (f,loc) ->
let my_kf = Option.get self#current_kf in
let f1 = Visitor.visitFramacFunction (self:>Visitor.frama_c_visitor) f
@@ -22,7 +22,7 @@ object(self)
self#set_current_kf my_kf;
ChangeTo ([GFun(f1,loc); GFun(f2,loc)])
| _ -> DoChildren
-end
+ end
let run () =
let prj =
diff --git a/tests/syntax/copy_visitor_bts_1073_bis.ml b/tests/syntax/copy_visitor_bts_1073_bis.ml
index aa25c7d63531add1fe1f9c55cbbb7c08b55ef05c..a7565bab3bef2d100eb43771ad5e758bbf2b48df 100644
--- a/tests/syntax/copy_visitor_bts_1073_bis.ml
+++ b/tests/syntax/copy_visitor_bts_1073_bis.ml
@@ -1,23 +1,23 @@
(*============================================================================*)
module P = Plugin.Register
- (struct
- let name = "Testing plugin"
- let shortname = "test"
- let help = "Just to test Filter..."
- end)
+ (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)
+ (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
-
+
let fct_name vf _fi = vf.Cil_types.vname
let fct_info () _ = [ () ]
let param_visible _ _ = true
@@ -43,14 +43,14 @@ let main () =
if Opt.get () then
begin
let _ast = Ast.get () in
- P.feedback "start compute";
+ 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
+ Project.on new_prj Opt.clear ();
+ P.feedback "exported in new project : %s" new_proj_name
end
-
+
let () = Db.Main.extend main
(*============================================================================*)
-
+
diff --git a/tests/syntax/forloophook.ml b/tests/syntax/forloophook.ml
index a34f4fd68c85e6a8582933a2a934e4e2eda4ba0b..bd548e055b61ae42b0a521b83f21e4b394241fdc 100644
--- a/tests/syntax/forloophook.ml
+++ b/tests/syntax/forloophook.ml
@@ -7,27 +7,27 @@ let () =
let () =
Cabs2cil.register_for_loop_init_hook
(fun fc ->
- match fc with
- | FC_EXP _ -> Format.printf "No declaration@."
- | FC_DECL _ -> Format.printf "Local declaration@.")
+ match fc with
+ | FC_EXP _ -> Format.printf "No declaration@."
+ | FC_DECL _ -> Format.printf "Local declaration@.")
let () =
Cabs2cil.register_for_loop_test_hook
(fun e ->
- match e.expr_node with
- | NOTHING -> Format.printf "No test@."
- | _ -> Format.printf "Has a test@.")
+ match e.expr_node with
+ | NOTHING -> Format.printf "No test@."
+ | _ -> Format.printf "Has a test@.")
let () =
Cabs2cil.register_for_loop_incr_hook
(fun e ->
- match e.expr_node with
- | NOTHING -> Format.printf "No increment@."
- | _ -> Format.printf "Has an increment@.")
-
+ match e.expr_node with
+ | NOTHING -> Format.printf "No increment@."
+ | _ -> Format.printf "Has an increment@.")
+
let () =
Cabs2cil.register_for_loop_body_hook
(fun s ->
- match s.stmt_node with
- | NOP _ -> Format.printf "No body@."
- | _ -> Format.printf "Has a body@.")
+ match s.stmt_node with
+ | NOP _ -> Format.printf "No body@."
+ | _ -> Format.printf "Has a body@.")
diff --git a/tests/syntax/formals_decl_leak.ml b/tests/syntax/formals_decl_leak.ml
index 7db245eddd75bc99f3f41030ca04cbbcacbab234..ad61b6e9d03a365784d31010f6c2f3aae5a09eec 100644
--- a/tests/syntax/formals_decl_leak.ml
+++ b/tests/syntax/formals_decl_leak.ml
@@ -4,7 +4,7 @@ let check_vi_exists vi _ =
try
ignore (Globals.Functions.get vi)
with Not_found ->
- Kernel.fatal
+ Kernel.fatal
"%s(%d) has an entry in FormalsDecl, but does not exist in AST"
vi.vname vi.vid
diff --git a/tests/syntax/get_astinfo_bts1136.ml b/tests/syntax/get_astinfo_bts1136.ml
index 2df239b29f310eb6669576a42cb50d323b644eea..98c338bf7c935b57c284e2392d2380a4460982b8 100644
--- a/tests/syntax/get_astinfo_bts1136.ml
+++ b/tests/syntax/get_astinfo_bts1136.ml
@@ -1,7 +1,7 @@
let get_formal_variables name =
let add_kf_vars kf vars =
- try
+ try
let v = Globals.Vars.find_from_astinfo name (Cil_types.VFormal kf) in
Format.printf "found variable vid:%d formal in %a@."
v.Cil_types.vid Cil_datatype.Kf.pretty kf;
@@ -9,11 +9,11 @@ let get_formal_variables name =
with Not_found -> vars
in
let vars = Globals.Functions.fold add_kf_vars [] in
- vars
+ vars
let get_local_variables name =
let add_kf_vars kf vars =
- try
+ try
let v = Globals.Vars.find_from_astinfo name (Cil_types.VLocal kf) in
Format.printf "found variable vid:%d formal in %a@."
v.Cil_types.vid Cil_datatype.Kf.pretty kf;
@@ -21,7 +21,7 @@ let get_local_variables name =
with Not_found -> vars
in
let vars = Globals.Functions.fold add_kf_vars [] in
- vars
+ vars
@@ -32,14 +32,14 @@ let main () =
let do_v v =
let pp_kind fmt kind = match kind with
| Cil_types.VGlobal -> Format.fprintf fmt "global"
- | Cil_types.VFormal kf ->
- Format.fprintf fmt "formal in %a" Cil_datatype.Kf.pretty kf
- | Cil_types.VLocal kf ->
- Format.fprintf fmt "local in %a" Cil_datatype.Kf.pretty kf
+ | Cil_types.VFormal kf ->
+ Format.fprintf fmt "formal in %a" Cil_datatype.Kf.pretty kf
+ | Cil_types.VLocal kf ->
+ Format.fprintf fmt "local in %a" Cil_datatype.Kf.pretty kf
in
let _, kind = Globals.Vars.get_astinfo v in
- Format.printf "[do_v] vid:%d %a@." v.Cil_types.vid
- (* Cil_datatype.Localisation.pretty *) pp_kind kind
+ Format.printf "[do_v] vid:%d %a@." v.Cil_types.vid
+ (* Cil_datatype.Localisation.pretty *) pp_kind kind
in List.iter do_v vars; List.iter do_v vars'
let () = Db.Main.extend main
diff --git a/tests/syntax/ghost_parameters_formals_status.ml b/tests/syntax/ghost_parameters_formals_status.ml
index 9181658f40760e61e3572a727260aca3c141cc17..792d21a8f44538b02c681ebff028fc22208362c8 100644
--- a/tests/syntax/ghost_parameters_formals_status.ml
+++ b/tests/syntax/ghost_parameters_formals_status.ml
@@ -17,12 +17,12 @@ let run () =
(Pretty_utils.pp_flowlist ~left:"" ~sep:"" ~right:"" pretty_formal) l
in
let vi = Kernel_function.get_vi kf in
- let formals = Cil.getFormalsDecl vi in
+ let formals = Cil.getFormalsDecl vi in
Kernel.feedback "Type of %s is %a.@ %a"
vi.vname
Cil_datatype.Typ.pretty vi.vtype
pretty_formal_list formals
in
Globals.Functions.iter print_info
-
+
let () = Db.Main.extend run
diff --git a/tests/syntax/inserted_casts.ml b/tests/syntax/inserted_casts.ml
index 1dd28c61752acc83dbd75dffe8c9e5ca17ca3edc..ebd466c230473c94bf6623deb3dffb01e1017fea 100644
--- a/tests/syntax/inserted_casts.ml
+++ b/tests/syntax/inserted_casts.ml
@@ -1,9 +1,9 @@
include Plugin.Register
- (struct
- let name = "test"
- let shortname = "test"
- let help = "unitary test of inserted cast hook"
- end)
+ (struct
+ let name = "test"
+ let shortname = "test"
+ let help = "unitary test of inserted cast hook"
+ end)
let print_warning e ot nt =
result "Inserting cast for expression %a of type %a to type %a@."
diff --git a/tests/syntax/logic_env_script.ml b/tests/syntax/logic_env_script.ml
index 4cfd75c4fcc7971adc8995f9423f1e0877493a74..6598804b5dabf33d46bd35e748643f5f99661364 100644
--- a/tests/syntax/logic_env_script.ml
+++ b/tests/syntax/logic_env_script.ml
@@ -1,6 +1,6 @@
open Cil_types
-let emitter =
+let emitter =
Emitter.create "test" [ Emitter.Global_annot ] ~correctness:[] ~tuning:[]
let add () =
@@ -10,7 +10,7 @@ let add () =
Logic_utils.add_logic_function li;
Annotations.add_global emitter glob
-let check () =
+let check () =
assert (Logic_env.find_all_logic_functions "foo" <> []);
assert (Logic_env.find_all_logic_functions "bar" <> []);
assert (Logic_env.find_all_logic_functions "bla" <> []);
@@ -24,7 +24,7 @@ let run () =
add ();
check ();
let prj = File.create_project_from_visitor "foo"
- (fun p -> new Visitor.frama_c_copy p)
+ (fun p -> new Visitor.frama_c_copy p)
in
Project.on prj check ()
diff --git a/tests/syntax/machdep_char_unsigned.ml b/tests/syntax/machdep_char_unsigned.ml
index 296683fbd7b36ade780bc74482aff8e5d99758f9..2e0a28c35f4145122f84813999c726cd0315ffb3 100644
--- a/tests/syntax/machdep_char_unsigned.ml
+++ b/tests/syntax/machdep_char_unsigned.ml
@@ -2,39 +2,39 @@
open Cil_types
let md = {
- version = "";
- compiler = "gcc";
- cpp_arch_flags = ["-m32"];
- sizeof_short = 2;
- sizeof_int = 2;
- sizeof_long = 4;
- sizeof_longlong = 8;
- sizeof_ptr = 4;
- sizeof_float = 4;
- sizeof_double = 8;
- sizeof_longdouble = 8;
- sizeof_void = -1;
- sizeof_fun = 0;
- alignof_short = 2;
- alignof_int = 2;
- alignof_long = 2;
- alignof_longlong = 2;
- alignof_ptr = 2;
- alignof_float = 2;
- alignof_double = 2;
- alignof_longdouble = 2;
- alignof_str = 0;
- alignof_fun = 0;
- alignof_aligned= 0;
- char_is_unsigned = true;
- const_string_literals = true;
- little_endian = true;
- underscore_name = true ;
- size_t = "unsigned int";
- wchar_t = "int";
- ptrdiff_t = "int";
- has__builtin_va_list = true;
- }
+ version = "";
+ compiler = "gcc";
+ cpp_arch_flags = ["-m32"];
+ sizeof_short = 2;
+ sizeof_int = 2;
+ sizeof_long = 4;
+ sizeof_longlong = 8;
+ sizeof_ptr = 4;
+ sizeof_float = 4;
+ sizeof_double = 8;
+ sizeof_longdouble = 8;
+ sizeof_void = -1;
+ sizeof_fun = 0;
+ alignof_short = 2;
+ alignof_int = 2;
+ alignof_long = 2;
+ alignof_longlong = 2;
+ alignof_ptr = 2;
+ alignof_float = 2;
+ alignof_double = 2;
+ alignof_longdouble = 2;
+ alignof_str = 0;
+ alignof_fun = 0;
+ alignof_aligned= 0;
+ char_is_unsigned = true;
+ const_string_literals = true;
+ little_endian = true;
+ underscore_name = true ;
+ size_t = "unsigned int";
+ wchar_t = "int";
+ ptrdiff_t = "int";
+ has__builtin_va_list = true;
+}
let () =
File.new_machdep "unsigned_char" md
diff --git a/tests/syntax/reorder.ml b/tests/syntax/reorder.ml
index ee7fe008f268672f3bcbf7c52da030b0ea517567..9a527c7a9a2d98e168b6a14ec29b3d449ff65dcc 100644
--- a/tests/syntax/reorder.ml
+++ b/tests/syntax/reorder.ml
@@ -17,19 +17,19 @@ let run () =
ll.l_type <- Some Linteger;
li.l_body <-
LBterm
- (Logic_const.term
- (TBinOp
- (PlusA,
- Logic_const.term (Tapp(lj,[],[])) Linteger,
- Logic_const.term (Tapp(lk,[],[])) Linteger))
- Linteger);
+ (Logic_const.term
+ (TBinOp
+ (PlusA,
+ Logic_const.term (Tapp(lj,[],[])) Linteger,
+ Logic_const.term (Tapp(lk,[],[])) Linteger))
+ Linteger);
lj.l_body <- LBterm (Logic_const.term (Tapp(ll,[],[])) Linteger);
lk.l_body <- LBterm (Logic_const.term (Tapp(ll,[],[])) Linteger);
ll.l_body <- LBterm (Logic_const.tinteger 1);
let post_cond =
[Normal,
- Logic_const.new_predicate
- (Logic_const.prel
+ Logic_const.new_predicate
+ (Logic_const.prel
(Req,
Logic_const.term (Tapp(li,[],[])) Linteger,
Logic_const.term (Tapp(li,[],[])) Linteger))]
diff --git a/tests/syntax/temporary_location.ml b/tests/syntax/temporary_location.ml
index c6792bd916b11be0921473018addb73a3b3e714e..0f09f3308a6ece20e90940de47f88beb9e0c89a0 100644
--- a/tests/syntax/temporary_location.ml
+++ b/tests/syntax/temporary_location.ml
@@ -6,13 +6,12 @@ class vis = object(_)
method! vvrbl vi =
Kernel.result "%s -> %a" vi.vname Printer.pp_location vi.vdecl;
Cil.DoChildren
-
+
end
let main () =
Ast.compute ();
Cil.visitCilFile (new vis :> Cil.cilVisitor) (Ast.get ())
-
+
let () =
Db.Main.extend main
-
diff --git a/tests/syntax/typedef_multi.ml b/tests/syntax/typedef_multi.ml
index ef964131f958caed146a0afed8f6fb873fae911e..2401972bb518c95055702f302615bf86e0814697 100644
--- a/tests/syntax/typedef_multi.ml
+++ b/tests/syntax/typedef_multi.ml
@@ -1,4 +1,4 @@
-let run () =
+let run () =
File.reorder_ast ();
File.pretty_ast ()
diff --git a/tests/syntax/visit_create_local.ml b/tests/syntax/visit_create_local.ml
index 1ae5cabb9a4890af488d4f583f8d4f40639b4dbf..8a82d9d421339f8c89731d786fd60bc2d32dd017 100644
--- a/tests/syntax/visit_create_local.ml
+++ b/tests/syntax/visit_create_local.ml
@@ -3,21 +3,21 @@ open Cil
class cF = object(self) inherit Visitor.frama_c_inplace
-method! vstmt s =
-let fd = (Option.get self#current_func) in
-match s.skind with
-| Instr (Set (lv,e,loc)) ->
- let vi = makeLocalVar fd "varbidon" (typeOf e) in
- let sk = Instr (Set (var vi,new_exp ~loc (Lval lv),loc)) in
- let s0 = mkStmt ~valid_sid:true sk in
- ChangeTo (Cil.mkStmtCfgBlock [s0; s])
-| _ -> SkipChildren
+ method! vstmt s =
+ let fd = (Option.get self#current_func) in
+ match s.skind with
+ | Instr (Set (lv,e,loc)) ->
+ let vi = makeLocalVar fd "varbidon" (typeOf e) in
+ let sk = Instr (Set (var vi,new_exp ~loc (Lval lv),loc)) in
+ let s0 = mkStmt ~valid_sid:true sk in
+ ChangeTo (Cil.mkStmtCfgBlock [s0; s])
+ | _ -> SkipChildren
end
let run () =
-Visitor.visitFramacFileSameGlobals (new cF) (Ast.get());
-Cfg.clearFileCFG ~clear_id:false (Ast.get());
-Cfg.computeFileCFG (Ast.get())
+ Visitor.visitFramacFileSameGlobals (new cF) (Ast.get());
+ Cfg.clearFileCFG ~clear_id:false (Ast.get());
+ Cfg.computeFileCFG (Ast.get())
module Computed =
State_builder.False_ref
@@ -27,11 +27,11 @@ let main () =
if not (Computed.get ()) then begin
Computed.set true;
if not (Ast.is_computed()) then Ast.compute();
- let prj =
- File.create_project_from_visitor
- "bidon" (fun prj -> new Visitor.frama_c_copy prj)
- in
- Project.on prj run ();
+ let prj =
+ File.create_project_from_visitor
+ "bidon" (fun prj -> new Visitor.frama_c_copy prj)
+ in
+ Project.on prj run ();
end
let () = Db.Main.extend main