diff --git a/.mailmap b/.mailmap
index 5f500d8a33dca5d2728508c275e2c98f58b78199..799ba7668ebfc76496349755a0252e891cc32269 100644
--- a/.mailmap
+++ b/.mailmap
@@ -13,4 +13,4 @@ Muriel Roger <muriel.roger@cea.fr>
<loic.correnson@cea.fr> <lcorrenson@gmail.com>
<loic.correnson@cea.fr> <loïc.correnson@cea.fr>
Géraud Canet <geraud.canet@cea.fr>
-<mounir.assaf@cea.fr> <mounir.assaf@cea.Fr>
\ No newline at end of file
+<mounir.assaf@cea.fr> <mounir.assaf@cea.Fr>
diff --git a/devel_tools/size.ml b/devel_tools/size.ml
index bd24feec4f33c718189a759be496d3abe39047f6..116006f2bb7c8b8c84a70987bfadb898573c2cd1 100644
--- a/devel_tools/size.ml
+++ b/devel_tools/size.ml
@@ -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
@@ -80,8 +80,8 @@ let res () =
let size_w ?except o =
reset_table ();
(match except with
- | None -> ()
- | Some except -> traverse (repr except)
+ | None -> ()
+ | Some except -> traverse (repr except)
);
count := 0;
traverse (repr o);
diff --git a/devel_tools/size_states.ml b/devel_tools/size_states.ml
index 2cdec788b99c6ab76f53c26f12003c31c5e116ed..ad62726e2b8427127497eea54cc0526c00ae650b 100644
--- a/devel_tools/size_states.ml
+++ b/devel_tools/size_states.ml
@@ -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
diff --git a/doc/CHANGES.obfuscator b/doc/CHANGES.obfuscator
index 6e2057626df2d41ffd666604db0844ca9caf6a6d..70a697bdac5588ce3d20e108167ffe07b3ea0559 100644
--- a/doc/CHANGES.obfuscator
+++ b/doc/CHANGES.obfuscator
@@ -5,4 +5,4 @@ V3
V2
New dictionary output using #define
V1
- Initial release
\ No newline at end of file
+ Initial release
diff --git a/doc/acsl_tutorial_slides/1max.sh b/doc/acsl_tutorial_slides/1max.sh
index 82944e95f97a00bad8ab70e6ad8b19d772197666..99851981e56ffa61b5b0200a90d99c23b9dc2a82 100755
--- a/doc/acsl_tutorial_slides/1max.sh
+++ b/doc/acsl_tutorial_slides/1max.sh
@@ -1,2 +1,2 @@
#!/bin/sh
-emacs 1max.c
\ No newline at end of file
+emacs 1max.c
diff --git a/doc/aorai/.gitignore b/doc/aorai/.gitignore
index 7af91cd419db82b54ead3e68b22a67a87ef72b18..0682bf3d785b90f19aeba9598ca8f66b38edfa39 100644
--- a/doc/aorai/.gitignore
+++ b/doc/aorai/.gitignore
@@ -1 +1 @@
-/transf
\ No newline at end of file
+/transf
diff --git a/doc/aorai/example/example.ltl b/doc/aorai/example/example.ltl
index 0c0910e3e9073e1e1e8f42dcbdb85194b05429ea..6df141a147552c23c9cb3e2e219ec04c2a0d6169 100644
--- a/doc/aorai/example/example.ltl
+++ b/doc/aorai/example/example.ltl
@@ -3,4 +3,4 @@ CALL(main)
&& _X_ (!RETURN(opb)
&& _X_ (!CALL(opa)
&& _X_ (RETURN(opb)
- && _X_ (RETURN(main))))))
\ No newline at end of file
+ && _X_ (RETURN(main))))))
diff --git a/doc/developer/check_api/check_code.ml b/doc/developer/check_api/check_code.ml
index 2fcb3fc4aa525d9e60d043b5843cc4a0eacf66fe..9592cbf22bc5f79165742745640a8fcc0e70a69e 100644
--- a/doc/developer/check_api/check_code.ml
+++ b/doc/developer/check_api/check_code.ml
@@ -87,7 +87,7 @@ module Generator (G : Odoc_html.Html_generator) = struct
self#html_of_custom b info.Odoc_info.i_custom
(** Print html code for the first sentence of a description.
- The titles and lists in this first sentence has been removed.*)
+ The titles and lists in this first sentence has been removed.*)
method html_of_info_first_sentence b = function
| None -> ()
| Some info ->
diff --git a/doc/developer/tutorial/hello/src/run_log.ml b/doc/developer/tutorial/hello/src/run_log.ml
index fb5256b08281abe6a33ab76a423977ba7022c7e3..b76d5462a2c3d9ddab64a803a68410ec7c9c688c 100644
--- a/doc/developer/tutorial/hello/src/run_log.ml
+++ b/doc/developer/tutorial/hello/src/run_log.ml
@@ -1,7 +1,7 @@
let run () =
Self.result "Hello, world!";
- let product =
- Self.feedback ~level:2 "Computing the product of 11 and 5...";
+ let product =
+ Self.feedback ~level:2 "Computing the product of 11 and 5...";
11 * 5
in
Self.result "11 * 5 = %d" product
diff --git a/doc/slicing/algoH.mli b/doc/slicing/algoH.mli
index a514d3fedd1df4b77162a9b5d10ae67d66f29c14..fc75ef1b7cc04ea2b5a51ffbd21abd9579cb302f 100644
--- a/doc/slicing/algoH.mli
+++ b/doc/slicing/algoH.mli
@@ -38,7 +38,7 @@ val get_stmts : t_elem list -> t_stmt_elems -> t_stmt list ;;
(* retrouver les éléments correspondant à une instruction *)
val get_elems : t_stmt -> t_stmt_elems -> t_elem list ;;
-type t_state
+type t_state
type t_data
diff --git a/doc/training/developer/beamerfontthemeframa-c.sty b/doc/training/developer/beamerfontthemeframa-c.sty
index 214ff73b722ae526ad38259bf1e9a6ddc3e778f7..8769c1f3904f82b25f85815a62f72a3783db1dfc 100644
--- a/doc/training/developer/beamerfontthemeframa-c.sty
+++ b/doc/training/developer/beamerfontthemeframa-c.sty
@@ -1 +1 @@
-\setbeamerfont{section in head}{size=\scriptsize}
\ No newline at end of file
+\setbeamerfont{section in head}{size=\scriptsize}
diff --git a/doc/training/developer/kernel.tex b/doc/training/developer/kernel.tex
index 65ebfbe2bbafc2a22b47c8f6f43d97db60e19844..3f0fa7ef7acd6dd5a9ddd7f24b065b6f789212f2 100644
--- a/doc/training/developer/kernel.tex
+++ b/doc/training/developer/kernel.tex
@@ -26,4 +26,4 @@
% Local Variables:
% ispell-local-dictionary: "english"
% TeX-master: "slides.tex"
-% End:
\ No newline at end of file
+% End:
diff --git a/doc/training/developer/script.tex b/doc/training/developer/script.tex
index acf0e67fbe5fd95c654aae543762c4c8a74b0261..16362b096a35c0a40012592044a022f5fd71eb2a 100644
--- a/doc/training/developer/script.tex
+++ b/doc/training/developer/script.tex
@@ -89,4 +89,4 @@
% Local Variables:
% TeX-master: "slides.tex"
% ispell-local-dictionary: "english"
-% End:
\ No newline at end of file
+% End:
diff --git a/doc/value/README b/doc/value/README
index 8e8ce00b65d7748875ee88c28cb23996f5418b26..8c0abd89e17425eda471574f518ff91775e453d0 100644
--- a/doc/value/README
+++ b/doc/value/README
@@ -35,4 +35,4 @@ on n'
prompt, sinon l'utilisateur il croit que ça fait partie de la commande.
Le style "verbatim" fait partie des éléments qui aident à reconnaître
les commandes qui peuvent être tappées, et puis on peut/pourra aussi
-tout faire dans l'interface graphique.
\ No newline at end of file
+tout faire dans l'interface graphique.
diff --git a/doc/value/examples/parametrizing/loop-unroll-insuf.c b/doc/value/examples/parametrizing/loop-unroll-insuf.c
index f977bfe31f574efdb9f5a13ca0b3b2f9f14f06c2..a16c8b457d692c3baf50469a92c477bd3bc8be3d 100644
--- a/doc/value/examples/parametrizing/loop-unroll-insuf.c
+++ b/doc/value/examples/parametrizing/loop-unroll-insuf.c
@@ -3,4 +3,4 @@ void main()
//@ loop unroll 20; // should be 21
for (int i = 0 ; i <= 20 ; i ++) {
}
-}
\ No newline at end of file
+}
diff --git a/doc/value/examples/parametrizing/pragma-widen-hints.c b/doc/value/examples/parametrizing/pragma-widen-hints.c
index af0263b686172e036af93205f2cfa9cacb2f31d7..1e829bf9757fb58a22d79318d5dbec16e7e3c4f3 100644
--- a/doc/value/examples/parametrizing/pragma-widen-hints.c
+++ b/doc/value/examples/parametrizing/pragma-widen-hints.c
@@ -6,4 +6,4 @@ void main(void)
/*@ loop pragma WIDEN_HINTS i, 12, 13; */
for (i=0; i<n; i++)
j = 4 * i + 7;
-}
\ No newline at end of file
+}
diff --git a/doc/value/tutorial/README b/doc/value/tutorial/README
index e9d633c09797c58605cf875de0627360cbc1c296..087e9349ecbf5f889b6a1c626d9e41c5eb0f787d 100644
--- a/doc/value/tutorial/README
+++ b/doc/value/tutorial/README
@@ -1 +1 @@
-Reference_implementation is extracted from http://www.schneier.com/code/skein.zip
\ No newline at end of file
+Reference_implementation is extracted from http://www.schneier.com/code/skein.zip
diff --git a/doc/value/watchpoints b/doc/value/watchpoints
index 5c3009130a66b061986e39bea29ccf12ad99a59d..6ea47f519d6390aca812faa20b9a5d9b7bd5486f 100644
--- a/doc/value/watchpoints
+++ b/doc/value/watchpoints
@@ -54,4 +54,4 @@ Frama_C_watch_cardinal() allows to set a maximum number of elements
associated to lvalue in the abstract memory state. This is useful
in order to watch variables that should remain precise during
the entire execution (e.g. should remain a singleton) but which can
-take different values at different points.
\ No newline at end of file
+take different values at different points.
diff --git a/headers/hdrck.ml b/headers/hdrck.ml
index 692c80226819e5a076d40b4f454249e4134b7ee1..14c04d2568bbc7eed18638f0ef670f64e5965b82 100755
--- a/headers/hdrck.ml
+++ b/headers/hdrck.ml
@@ -105,7 +105,7 @@ let has_no_warning_nor_error = ref true
let warn fmt =
pp_job_first_line ();
if !exit_on_warning then
- has_no_warning_nor_error := false ;
+ has_no_warning_nor_error := false ;
Format.printf "- [warning] ";
Format.printf fmt
@@ -164,7 +164,7 @@ let get_string_null (ic:in_channel) =
*
* Defaults to reading the file entirely since any integer will ever be greater
* or equal than [max_int].
- *)
+*)
let read_lines ?nlines:(nlines=max_int) get_line filename =
let lines = ref [] in
let ic = if filename = "--stdin" then stdin else open_in filename in
@@ -355,7 +355,7 @@ let get_header_files ?directories:(dirs=(get_header_dirs ())) () :
warn "%s: duplicated license name (same contents as file: %s)@." filepath previous_entry
else
error ~exit_value:7
- "%s: duplicated license name (contents differs to file: %s)@." filepath previous_entry
+ "%s: duplicated license name (contents differs to file: %s)@." filepath previous_entry
with Not_found -> ());
Hashtbl.add license_path_tbl license_name filepath;
)
@@ -408,7 +408,7 @@ let extract_header filename template_hdr =
* @param headers a license header -> template header file hashtable
* @requires all files in specs exist
* @requires all header specifications have a corresponding existing template
- *)
+*)
let check_spec_discrepancies
(specs: (string, string) Hashtbl.t)
(headers: (string, string) Hashtbl.t) : unit =
@@ -433,18 +433,18 @@ let check_spec_discrepancies
let hdr_file_spec = Hashtbl.find headers hdr_type in
(* Guaranteed to exists after check_declared_headers *)
if not (eq_header file hdr_file_spec) then begin
- discrepancies := (file, hdr_type) :: !discrepancies;
- incr n;
+ discrepancies := (file, hdr_type) :: !discrepancies;
+ incr n;
end;
end
- ) specs ;
+ ) specs ;
if !n > 0 then begin
error ~exit_value:4 "@[<v 2>%a%d / %d files with bad headers@]@."
(fun _ppf l ->
List.iter
(fun (file, hdr_type) ->
error_fmt "%s : header differs from spec %s@."
- file hdr_type
+ file hdr_type
) l) !discrepancies
!n
(Hashtbl.length specs) ;
@@ -473,8 +473,8 @@ let check_forbidden_headers (forbidden_headers:StringSet.t) header_specification
error_fmt "%s : forbidden header %s@."
file hdr_type
) l) !forbidden
- !n
- (StringSet.cardinal distributed_files);
+ !n
+ (StringSet.cardinal distributed_files);
job_done ()
end
@@ -543,7 +543,7 @@ let check files_ignored header_specifications distributed_files exceptions =
*
* @param header_specifications file -> license header name hashtable
* @requires: files and licenses appearing in [header_specifications] exists
- *)
+*)
let update_headers header_specifications =
let headers = get_header_files () in
check_declared_headers header_specifications headers;
@@ -640,7 +640,7 @@ let rec argspec = [
| "3-lines" -> spec_format := Line3
| "3-zeros" -> spec_format := Zero3
| s -> Format.printf "invalid spec format: %s@." s ; print_usage ()),
- "<format>\t \"2-fields-by-line\"|\"3-fields-by-line\"|\"3-lines\"|\"3-zeros\"";
+ "<format>\t \"2-fields-by-line\"|\"3-fields-by-line\"|\"3-lines\"|\"3-zeros\"";
"-z", Arg.Set zero_stdin,
" force to use the spec format \"3-zeros\" when reading from stdin";
]
@@ -693,6 +693,6 @@ let _ =
if !exit_on_warning && not !has_no_warning_nor_error then
exit 8 ;
-(* Local Variables: *)
-(* compile-command: "ocamlc -o hdrck unix.cma str.cma hdrck.ml" *)
-(* End: *)
+ (* Local Variables: *)
+ (* compile-command: "ocamlc -o hdrck unix.cma str.cma hdrck.ml" *)
+ (* End: *)
diff --git a/ivette/src/frama-c/api_generator.ml b/ivette/src/frama-c/api_generator.ml
index b72055204a8002d9e3778a336fd422f14d2f6e69..5e29fab1eb556a5c6925f9f7eaafc9369d33c2bd 100644
--- a/ivette/src/frama-c/api_generator.ml
+++ b/ivette/src/frama-c/api_generator.ml
@@ -25,11 +25,11 @@
(* -------------------------------------------------------------------------- *)
module Self = Plugin.Register
- (struct
- let name = "Server TypeScript API"
- let shortname = "server-tsc"
- let help = "Generate TypeScript API for Server"
- end)
+ (struct
+ let name = "Server TypeScript API"
+ let shortname = "server-tsc"
+ let help = "Generate TypeScript API for Server"
+ end)
module TSC = Self.Action
(struct
@@ -353,7 +353,7 @@ let makeDeclaration fmt names d =
(Pretty_utils.pp_list
~empty:"[]" ~pre:"@[<hov 2>[ " ~sep:",@ " ~suf:"@ ]@]"
(fun fmt s -> Format.fprintf fmt "{ name: '%s' }" s))
- rq.rq_signals;
+ rq.rq_signals;
Format.fprintf fmt "};@\n" ;
makeDescr fmt d.d_descr ;
Format.fprintf fmt
diff --git a/src/plugins/aorai/.gitignore b/src/plugins/aorai/.gitignore
index 6e2440c7d5053e68723ce0ec0a462d751551dda1..1b77fb8deb8db509c14ac4bd15afc70dca627d69 100644
--- a/src/plugins/aorai/.gitignore
+++ b/src/plugins/aorai/.gitignore
@@ -18,4 +18,4 @@
/tests/*/result
/tests/test_config_prove
/tests/*/result_prove
-/top
\ No newline at end of file
+/top
diff --git a/src/plugins/instantiate/tests/plugin/needs_global.ml b/src/plugins/instantiate/tests/plugin/needs_global.ml
index 506da455fdb5b23a60a0d994dc2fcfb0e268c021..652b66a9cdeb303453c7b32774f0be742820ef6c 100644
--- a/src/plugins/instantiate/tests/plugin/needs_global.ml
+++ b/src/plugins/instantiate/tests/plugin/needs_global.ml
@@ -39,14 +39,14 @@ let generate_spec needed _ _ _ =
Cil_types.Writes [ Logic_const.new_identified_term t, From [] ]
in {
spec_behavior = [ {
- b_name = Cil.default_behavior_name ;
- b_requires = [] ;
- b_assumes = [] ;
- b_post_cond = [] ;
- b_assigns = assigns ;
- b_allocation = FreeAllocAny ;
- b_extended = []
- } ] ;
+ b_name = Cil.default_behavior_name ;
+ b_requires = [] ;
+ b_assumes = [] ;
+ b_post_cond = [] ;
+ b_assigns = assigns ;
+ b_allocation = FreeAllocAny ;
+ b_extended = []
+ } ] ;
spec_variant = None ;
spec_terminates = None ;
spec_complete_behaviors = [] ;
diff --git a/src/plugins/variadic/tests/declared/called_in_ghost.ml b/src/plugins/variadic/tests/declared/called_in_ghost.ml
index 5f7f6383d20b8aadc71520d60afb92e081300b74..4aa4ac68015e0d5c4aa32f616f850e0f41f3456a 100755
--- a/src/plugins/variadic/tests/declared/called_in_ghost.ml
+++ b/src/plugins/variadic/tests/declared/called_in_ghost.ml
@@ -6,15 +6,15 @@ class print =
method! vglob_aux g =
begin match g with
- | GFun(fd, _) ->
- Kernel.feedback "%a is%s ghost"
- Cil_datatype.Varinfo.pretty fd.svar
- (if fd.svar.vghost then "" else " not")
- | GFunDecl(_, vi, _) ->
- Kernel.feedback "%a is%s ghost"
- Cil_datatype.Varinfo.pretty vi
- (if vi.vghost then "" else " not")
- | _ -> ()
+ | GFun(fd, _) ->
+ Kernel.feedback "%a is%s ghost"
+ Cil_datatype.Varinfo.pretty fd.svar
+ (if fd.svar.vghost then "" else " not")
+ | GFunDecl(_, vi, _) ->
+ Kernel.feedback "%a is%s ghost"
+ Cil_datatype.Varinfo.pretty vi
+ (if vi.vghost then "" else " not")
+ | _ -> ()
end ;
Cil.DoChildren
diff --git a/src/plugins/wp/tests/wp/stmtcompiler_test_rela.ml b/src/plugins/wp/tests/wp/stmtcompiler_test_rela.ml
index 12849805c20ad3d7c7d73393dae7914bde04163e..1172d4ab1a585418b1629c950c86759a53aaa72b 100644
--- a/src/plugins/wp/tests/wp/stmtcompiler_test_rela.ml
+++ b/src/plugins/wp/tests/wp/stmtcompiler_test_rela.ml
@@ -70,15 +70,15 @@ let run () =
Property_status.iter (fun x ->
match Wpo.goals_of_property x with
| h :: _ ->
- inter_po := Wpo.{
- po_gid = "";
- po_sid = "";
- po_name = "";
- po_idx = Function(kf, None);
- po_model = model;
- po_pid = h.po_pid;
- po_formula = Wpo.GoalAnnot vc_annot;
- }
+ inter_po := Wpo.{
+ po_gid = "";
+ po_sid = "";
+ po_name = "";
+ po_idx = Function(kf, None);
+ po_model = model;
+ po_pid = h.po_pid;
+ po_formula = Wpo.GoalAnnot vc_annot;
+ }
| _ -> ()
);
spawn !inter_po;
diff --git a/src/plugins/wp/tests/wp_tip/TacNOP.ml b/src/plugins/wp/tests/wp_tip/TacNOP.ml
index a398efe3ac597d6d3b7dec5ff98f1d206c299f59..21faecfe4c3252cb9781aba7b120117c574129b1 100644
--- a/src/plugins/wp/tests/wp_tip/TacNOP.ml
+++ b/src/plugins/wp/tests/wp_tip/TacNOP.ml
@@ -19,9 +19,9 @@ class nop =
| Multi _
| Inside _
| Clause _ ->
- feedback#set_title "NOP" ;
- feedback#set_descr "Does nothing; just for testing." ;
- Applicable (fun s -> ["Nop", s])
+ feedback#set_title "NOP" ;
+ feedback#set_descr "Does nothing; just for testing." ;
+ Applicable (fun s -> ["Nop", s])
end
diff --git a/tests/syntax/copy_visitor_bts_1073_bis.ml b/tests/syntax/copy_visitor_bts_1073_bis.ml
index a7565bab3bef2d100eb43771ad5e758bbf2b48df..d26b1010abf5ca0abdc6ed8c1f089c43bc39291c 100644
--- a/tests/syntax/copy_visitor_bts_1073_bis.ml
+++ b/tests/syntax/copy_visitor_bts_1073_bis.ml
@@ -53,4 +53,3 @@ let main () =
let () = Db.Main.extend main
(*============================================================================*)
-