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/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/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/code/docgen.ml b/doc/code/docgen.ml
index a3a013b7955a45e805145625a56701b96d554155..de75c3583974c1f2edd9f985024e2ac7c1086682 100644
--- a/doc/code/docgen.ml
+++ b/doc/code/docgen.ml
@@ -63,55 +63,55 @@ let merge3
if c <> 0 then c else
let c = s2 y' y in
if c <> 0 then c else
- s3 z' z
+ s3 z' z
in
let rec merge3_rev acc triplets =
match triplets , acc with
| [] , _ -> acc
| (a,b,c)::tail , (dir_a,all_a)::a_merged when a = dir_a ->
- begin
- match all_a with
- | (dir_b,all_b)::b_merged when b = dir_b ->
- merge3_rev ((dir_a,(dir_b,c::all_b)::b_merged)::a_merged) tail
- | _ ->
- merge3_rev ((dir_a,(b,[c])::all_a)::a_merged) tail
- end
+ begin
+ match all_a with
+ | (dir_b,all_b)::b_merged when b = dir_b ->
+ merge3_rev ((dir_a,(dir_b,c::all_b)::b_merged)::a_merged) tail
+ | _ ->
+ merge3_rev ((dir_a,(b,[c])::all_a)::a_merged) tail
+ end
| (a,b,c)::tail , merged ->
- merge3_rev (( a , [b,[c]] )::merged) tail
+ merge3_rev (( a , [b,[c]] )::merged) tail
in
merge3_rev [] (List.sort (sort3_rev s1 s2 s3) triplets)
module Generator (G:Odoc_html.Html_generator) =
struct
class html = object (self)
-
+
inherit G.html as super
val mutable memo = []
-
+
method private loaded_modules =
match memo with
| [] ->
- let l = List.flatten
- (List.map
- (fun f ->
- Odoc_info.verbose (Odoc_messages.loading f);
- try
- let l = Odoc_analyse.load_modules f in
- Odoc_info.verbose Odoc_messages.ok;
- l
- with Failure s ->
- prerr_endline s ;
- incr Odoc_global.errors ;
- []
- )
- !Odoc_global.load
- )
- in
- memo <- l;
- l
+ let l = List.flatten
+ (List.map
+ (fun f ->
+ Odoc_info.verbose (Odoc_messages.loading f);
+ try
+ let l = Odoc_analyse.load_modules f in
+ Odoc_info.verbose Odoc_messages.ok;
+ l
+ with Failure s ->
+ prerr_endline s ;
+ incr Odoc_global.errors ;
+ []
+ )
+ !Odoc_global.load
+ )
+ in
+ memo <- l;
+ l
| (_ :: _) as l -> l
-
+
method private path s =
let name = root_name s in
if List.exists (fun m -> m = name) !lib_files then
@@ -126,18 +126,18 @@ struct
let match_s = Str.matched_string str_t in
let rel = Odoc_info.Name.get_relative m_name match_s in
let s_final = Odoc_info.apply_if_equal
- Odoc_info.use_hidden_modules
- match_s
- rel
+ Odoc_info.use_hidden_modules
+ match_s
+ rel
in
if String.Set.mem match_s known_types_names then
- "<a href=\"" ^ self#path match_s ^ Naming.complete_target Naming.mark_type
- match_s ^"\">" ^ s_final ^ "</a>"
+ "<a href=\"" ^ self#path match_s ^ Naming.complete_target Naming.mark_type
+ match_s ^"\">" ^ s_final ^ "</a>"
else
- if String.Set.mem match_s known_classes_names then
+ if String.Set.mem match_s known_classes_names then
let (html_file, _) = Naming.html_files match_s in
"<a href=\""^ self#path html_file ^ html_file^"\">"^s_final^"</a>"
- else
+ else
s_final
in
let s2 = Str.global_substitute
@@ -154,15 +154,15 @@ struct
let match_s = Str.matched_string str_t in
let rel = Odoc_info.Name.get_relative m_name match_s in
let s_final = Odoc_info.apply_if_equal
- Odoc_info.use_hidden_modules
- match_s
- rel
+ Odoc_info.use_hidden_modules
+ match_s
+ rel
in
if String.Set.mem match_s known_modules_names then
- let (html_file, _) = Naming.html_files match_s in
- "<a href=\"" ^ self#path match_s ^ html_file^"\">"^s_final^"</a>"
+ let (html_file, _) = Naming.html_files match_s in
+ "<a href=\"" ^ self#path match_s ^ html_file^"\">"^s_final^"</a>"
else
- s_final
+ s_final
in
let s2 = Str.global_substitute
(Str.regexp "\\([A-Z]\\([a-zA-Z_'0-9]\\)*\\.\\)+\\([A-Z][a-zA-Z_'0-9]*\\)")
@@ -175,10 +175,10 @@ struct
method html_of_Module_list b l =
let dir f = (* <dir> , <name> *)
let chop dir f =
- let n = Str.search_forward (Str.regexp dir) f 0 in
- let f = String.sub f n (String.length f - n) in
- let d = Filename.dirname f in
- String.capitalize_ascii (Filename.basename d)
+ let n = Str.search_forward (Str.regexp dir) f 0 in
+ let f = String.sub f n (String.length f - n) in
+ let d = Filename.dirname f in
+ String.capitalize_ascii (Filename.basename d)
in
try
Chapter(1,"Kernel Services","src/kernel_services"),
@@ -207,34 +207,34 @@ struct
in
List.iter
(fun (chapter, subdirs) ->
- let dir =
- ( match chapter with
- | Chapter (n,a,d) ->
- bp b "<h1 class=\"chapter\">Chapter %d. %s</h1>" n a ; d
- | Directory d ->
- bp b "<h1>Directory %s</h1>" d ; d)
- in
- List.iter
- (fun (subdir,modules) ->
- bp b "<h2 class=\"section\">Section %s <span class=\"directory\">(in %s/%s)</span></h2>\n"
- subdir dir (String.lowercase_ascii subdir) ;
- bs b "<br>\n<table class=\"indextable\">\n";
- List.iter
- (fun m ->
- bs b "<tr><td>";
- (try
- let (html, _) = Naming.html_files m.m_name in
- bp b "<a href=\"%s\">%s</a></td>" html m.m_name;
- bs b "<td>";
- self#html_of_info_first_sentence b m.m_info;
- with Not_found ->
- Odoc_global.pwarning
- (Odoc_messages.cross_module_not_found m.m_name);
- bp b "%s</td><td>" m.m_name);
- bs b "</td></tr>\n")
- modules;
- bs b "</table>\n")
- subdirs)
+ let dir =
+ ( match chapter with
+ | Chapter (n,a,d) ->
+ bp b "<h1 class=\"chapter\">Chapter %d. %s</h1>" n a ; d
+ | Directory d ->
+ bp b "<h1>Directory %s</h1>" d ; d)
+ in
+ List.iter
+ (fun (subdir,modules) ->
+ bp b "<h2 class=\"section\">Section %s <span class=\"directory\">(in %s/%s)</span></h2>\n"
+ subdir dir (String.lowercase_ascii subdir) ;
+ bs b "<br>\n<table class=\"indextable\">\n";
+ List.iter
+ (fun m ->
+ bs b "<tr><td>";
+ (try
+ let (html, _) = Naming.html_files m.m_name in
+ bp b "<a href=\"%s\">%s</a></td>" html m.m_name;
+ bs b "<td>";
+ self#html_of_info_first_sentence b m.m_info;
+ with Not_found ->
+ Odoc_global.pwarning
+ (Odoc_messages.cross_module_not_found m.m_name);
+ bp b "%s</td><td>" m.m_name);
+ bs b "</td></tr>\n")
+ modules;
+ bs b "</table>\n")
+ subdirs)
toc_modules
(** Print html code for an included module. *)
@@ -253,8 +253,8 @@ struct
(html_file, m.m_name)
| Modtype mt ->
let (html_file, _) =
- Naming.html_files mt.mt_name
- in
+ Naming.html_files mt.mt_name
+ in
(html_file, mt.mt_name)
in
bp b "<a href=\"%s%s\">%s</a>" (self#path name) file name
@@ -322,8 +322,8 @@ struct
(* generate html for each module *)
let keep_list =
let keep m =
- not (List.exists (equal_module m) self#loaded_modules) &&
- not (List.exists (equal_module_name m) !lib_files)
+ not (List.exists (equal_module m) self#loaded_modules) &&
+ not (List.exists (equal_module_name m) !lib_files)
in
List.filter keep module_list
in
@@ -363,20 +363,20 @@ struct
method private html_of_ignore _t = ""
method private html_of_modify t = match t with
- | [] ->
- Odoc_info.warning "Found an empty @modify tag";
+ | [] ->
+ Odoc_info.warning "Found an empty @modify tag";
""
| Raw s :: l ->
let time, explanation =
- try
- let idx = String.index s ' ' in
- String.sub s 0 idx,
- ":" ^ String.sub s idx (String.length s - idx)
- with Not_found ->
- s, ""
+ try
+ let idx = String.index s ' ' in
+ String.sub s 0 idx,
+ ":" ^ String.sub s idx (String.length s - idx)
+ with Not_found ->
+ s, ""
in
let text =
- Bold [ Raw "Change in "; Raw time ] :: Raw explanation :: l
+ Bold [ Raw "Change in "; Raw time ] :: Raw explanation :: l
in
let buf = Buffer.create 7 in
self#html_of_text buf text;
@@ -386,8 +386,8 @@ struct
assert false
method private html_of_call t = match t with
- | [] ->
- Odoc_info.warning "Found an empty @call tag";
+ | [] ->
+ Odoc_info.warning "Found an empty @call tag";
""
| l ->
let buf = Buffer.create 97 in
@@ -405,7 +405,7 @@ struct
tag_functions <-
("modify", self#html_of_modify) ::
("ignore", self#html_of_ignore) ::
- ("call", self#html_of_call) ::
+ ("call", self#html_of_call) ::
("plugin", self#html_of_plugin_developer_guide) :: tag_functions
end
diff --git a/doc/developer/check_api/check_and_compare.ml b/doc/developer/check_api/check_and_compare.ml
index e767939d391a8f5760b5239aa1627a82f05f6718..82c77a8173949385b1629f06bca60afa81586a29 100644
--- a/doc/developer/check_api/check_and_compare.ml
+++ b/doc/developer/check_api/check_and_compare.ml
@@ -13,96 +13,96 @@
let replace_space_by_dot s = Str.global_replace (Str.regexp " ") "." s
-let repair_word s =
- let rec repair_word_aux st =
+let repair_word s =
+ let rec repair_word_aux st =
try let d1 = String.index st '$'
- in
- try let d2 = String.index_from st d1 '$'
- in (Str.string_before st d1)^
- (repair_word_aux (Str.string_after st (d2+1)))
- with Not_found -> st
+ in
+ try let d2 = String.index_from st d1 '$'
+ in (Str.string_before st d1)^
+ (repair_word_aux (Str.string_after st (d2+1)))
+ with Not_found -> st
with Not_found -> st
in
Str.global_replace (Str.regexp "\\") "" (repair_word_aux s)
-
-(** [fill_tbl] takes a file containing data which is
+
+(** [fill_tbl] takes a file containing data which is
as "element_name/type/comment/" or "element_name".
It fills the hashtable [tbl]
- with all the element [type;comment] or [] recorded
+ with all the element [type;comment] or [] recorded
with the key "element_name". *)
let fill_tbl tbl file_name =
try
let c = open_in file_name in
- try
- while true do
- let s = input_line c
- in
- if not (Str.string_match (Str.regexp "Command.Line") s 0)
- && not ( Hashtbl.mem tbl s)
- then match (Str.split (Str.regexp "/") s) with
- | [] -> ()
- | h::[] -> Hashtbl.add tbl h []
- | h::q -> Hashtbl.add tbl h q
+ try
+ while true do
+ let s = input_line c
+ in
+ if not (Str.string_match (Str.regexp "Command.Line") s 0)
+ && not ( Hashtbl.mem tbl s)
+ then match (Str.split (Str.regexp "/") s) with
+ | [] -> ()
+ | h::[] -> Hashtbl.add tbl h []
+ | h::q -> Hashtbl.add tbl h q
done
with End_of_file -> close_in c
with Sys_error _ as exn ->
- Format.eprintf "cannot handle file %s: %s" file_name
+ Format.eprintf "cannot handle file %s: %s" file_name
(Printexc.to_string exn)
-(** [fill_list] takes a file containing data which is
+(** [fill_list] takes a file containing data which is
as "element_name/type/comment/" if (has_type=true) or
"element_name" if (has_type=false). It fills the list [li]
with all the element names and alphabetically sorts them. *)
-let fill_list li name ~has_type =
+let fill_list li name ~has_type =
let fill_list_no_sorting l file_name =
try let c = open_in file_name in
- try
- while true do
- let s = input_line c in
- if not (Str.string_match
- (Str.regexp "Command.Line") s 0)&& not ( List.mem s !l)
- then begin
- if has_type then
- try let t =(Str.string_before s
- (String.index_from s 0 '/' )) in
- match t with
- |"" -> ()
- | _ -> if not( List.mem t !l)
- then l := t::!l
- with Not_found ->()
- else l := s::!l
- end
- done
- with End_of_file -> close_in c
+ try
+ while true do
+ let s = input_line c in
+ if not (Str.string_match
+ (Str.regexp "Command.Line") s 0)&& not ( List.mem s !l)
+ then begin
+ if has_type then
+ try let t =(Str.string_before s
+ (String.index_from s 0 '/' )) in
+ match t with
+ |"" -> ()
+ | _ -> if not( List.mem t !l)
+ then l := t::!l
+ with Not_found ->()
+ else l := s::!l
+ end
+ done
+ with End_of_file -> close_in c
with Sys_error _ as exn ->
- Format.eprintf "cannot handle file %s: %s" file_name
- (Printexc.to_string exn) in
- fill_list_no_sorting li name ;
+ Format.eprintf "cannot handle file %s: %s" file_name
+ (Printexc.to_string exn) in
+ fill_list_no_sorting li name ;
li := List.sort String.compare !li
(** [run_oracle] takes two hashtables [t1] and [t2] when called.
It first tests if the file "run.oracle" is already existing.
If this file exists, it uses the function [w_tbl] and creates
[tbl] a hashtable that contains the information found in "run.oracle".
- It first looks for all the elements in common in [t1] and [t2] and then
+ It first looks for all the elements in common in [t1] and [t2] and then
compares the corresponding pieces of information of [t1] and [tbl]
If the pieces of information are different, it writes this difference.
It eventually overwrites the "run.oracle" file with
- the pieces of information of the common elements of [t1] and [t2].
- If the file "run.oracle" does not exit, it only fills this file with
+ the pieces of information of the common elements of [t1] and [t2].
+ If the file "run.oracle" does not exit, it only fills this file with
the pieces of information in common using the function [wo_tbl]. *)
let run_oracle t1 t2 =
- let to_fill = ref ""
+ let to_fill = ref ""
in
let fill_oracle s =
try let chan_out = open_out "run.oracle"
- in
- output_string chan_out s;
- close_out chan_out
+ in
+ output_string chan_out s;
+ close_out chan_out
with Sys_error _ as exn ->
- Format.eprintf "cannot handle file %s: %s" "run.oracle"
- (Printexc.to_string exn)
+ Format.eprintf "cannot handle file %s: %s" "run.oracle"
+ (Printexc.to_string exn)
in
let rec string_of_list l = match l with
| [] -> ""
@@ -117,31 +117,31 @@ let run_oracle t1 t2 =
then h ^ "\n" ^ (string_of_info_list q)
else (string_of_info_list q)
in
- let wo_tbl t k d =
+ let wo_tbl t k d =
try let element_info = Hashtbl.find t k
- in
- to_fill :=
- !to_fill ^ "\n" ^ k ^ "/" ^ (string_of_list element_info)
+ in
+ to_fill :=
+ !to_fill ^ "\n" ^ k ^ "/" ^ (string_of_list element_info)
with Not_found -> ()
in
- let w_tbl t k d =
+ let w_tbl t k d =
let tbl: (string,string list) Hashtbl.t = Hashtbl.create 197
in
fill_tbl tbl "run.oracle";
- try
+ try
let element_info = Hashtbl.find t k
in
- to_fill :=
- !to_fill ^ "\n" ^ k ^ "/"^ string_of_list element_info;
- let previous_element_info = Hashtbl.find tbl k
+ to_fill :=
+ !to_fill ^ "\n" ^ k ^ "/"^ string_of_list element_info;
+ let previous_element_info = Hashtbl.find tbl k
in
if not (element_info = previous_element_info) then
- Format.printf " \n \n ----%s---- \n\n ** Information \
+ Format.printf " \n \n ----%s---- \n\n ** Information \
previously registered in 'run.oracle' :\n %s \n\n ** Information in \
the current API :\n %s \n "
- k (string_of_info_list previous_element_info)
- (string_of_info_list element_info)
- with Not_found ->
+ k (string_of_info_list previous_element_info)
+ (string_of_info_list element_info)
+ with Not_found ->
(* element not previously registered *)
()
in
@@ -150,18 +150,18 @@ let run_oracle t1 t2 =
\nELEMENTS OF THE INDEX OF THE DEVELOPER GUIDE EXISTING \
IN THE CODE: \n*****************************************\
*************************\n\n";
- if (Sys.file_exists "run.oracle")
- then (Hashtbl.iter (w_tbl t2) t1;
- fill_oracle !to_fill)
+ if (Sys.file_exists "run.oracle")
+ then (Hashtbl.iter (w_tbl t2) t1;
+ fill_oracle !to_fill)
else (Hashtbl.iter (wo_tbl t2) t1 ;
- fill_oracle !to_fill)
-
-
-(** [compare] takes two lists and returns the elements
+ fill_oracle !to_fill)
+
+
+(** [compare] takes two lists and returns the elements
of the first list not in the second list and then the elements
of the second list not in the first list.
The two names are corresponding (same order) to the two tables
- and are used in the introduction sentences. *)
+ and are used in the introduction sentences. *)
let compare t1 t2 name1 name2 =
let compare_aux t k =
if not(List.mem k t) then Format.printf "%s" (k ^ "\n") in
@@ -169,7 +169,7 @@ let compare t1 t2 name1 name2 =
*******************\
\nELEMENTS OF %s NOT IN %s: \n***********************************\
*************************\
-\n\n"
+\n\n"
name1 name2;
List.iter (compare_aux t2) t1;
Format.printf " \n \n*******************************************\
@@ -177,12 +177,12 @@ let compare t1 t2 name1 name2 =
\nELEMENTS OF %s NOT IN %s: \n************************************\
************************\
\n\n"
- name2 name1;
+ name2 name1;
List.iter (compare_aux t1) t2
(** here are used the lexer and parser "check_index_lexer" and
- "check_index_grammar" to create the file "index_file".
+ "check_index_grammar" to create the file "index_file".
The files "main.idx" and "code_file" must already exist. *)
let () =
let index_hstbl: (string,string list) Hashtbl.t = Hashtbl.create 197 in
@@ -212,7 +212,7 @@ OF THE DEVELOPER GUIDE" "THE CODE";
run_oracle index_hstbl code_hstbl ;
with Sys_error _ as exn ->
Format.eprintf "cannot handle file %s: %s" "index_file"
- (Printexc.to_string exn)
+ (Printexc.to_string exn)
with Sys_error _ as exn ->
- Format.eprintf "cannot handle file %s: %s" "main.idx"
+ Format.eprintf "cannot handle file %s: %s" "main.idx"
(Printexc.to_string exn)
diff --git a/doc/developer/check_api/check_code.ml b/doc/developer/check_api/check_code.ml
index 72539005fc293e584338f9333afe0a5eb4b47072..b50e8d70e92df029595f64ff0c1245bdd80684ec 100644
--- a/doc/developer/check_api/check_code.ml
+++ b/doc/developer/check_api/check_code.ml
@@ -17,7 +17,7 @@ open Odoc_html
open Odoc_module
open Odoc_info
-let remove_nl s = Str.global_replace (Str.regexp "\n") "" s
+let remove_nl s = Str.global_replace (Str.regexp "\n") "" s
let remove_useless_space s = Str.global_replace (Str.regexp " ") " " s
let doc_dev_path = ref "."
@@ -28,14 +28,14 @@ let print_in_file l =
| h :: q -> h ^ "\n" ^ string_of_list q
in
let file_path = !doc_dev_path ^ "/code_file" in
- try
+ try
let chan_out = open_out file_path in
output_string chan_out (string_of_list l) ;
flush chan_out ;
- close_out chan_out
+ close_out chan_out
with Sys_error _ as exn ->
Format.eprintf
- "cannot handle file %s: %s"
+ "cannot handle file %s: %s"
file_path
(Printexc.to_string exn)
@@ -43,7 +43,7 @@ module Generator (G : Odoc_html.Html_generator) = struct
class html = object (self)
- inherit G.html as super
+ inherit G.html as super
val mutable last_name = ""
val mutable last_type = ""
val mutable last_info = ""
@@ -55,19 +55,19 @@ module Generator (G : Odoc_html.Html_generator) = struct
| (s, t) :: [] ->
self#html_of_text b t;
let temp =
- last_info ^ " raised exception: "
- ^ Odoc_info.string_of_text [Raw s] ^ "."
+ last_info ^ " raised exception: "
+ ^ Odoc_info.string_of_text [Raw s] ^ "."
in
last_info <- temp
- | _ ->
+ | _ ->
let temp = last_info ^ " raised exceptions: " in
last_info <- temp;
List.iter
- (fun (ex, desc) ->
+ (fun (ex, desc) ->
self#html_of_text b desc;
- let temp = last_info ^ ", " ^ Odoc_info.string_of_text desc in
- last_info <- temp)
- l
+ let temp = last_info ^ ", " ^ Odoc_info.string_of_text desc in
+ last_info <- temp)
+ l
method html_of_info ?(cls="") ?(indent=true) b = function
| None ->
@@ -75,21 +75,21 @@ module Generator (G : Odoc_html.Html_generator) = struct
| Some info ->
(match info.Odoc_info.i_deprecated with
| None -> ()
- | Some d ->
- self#html_of_text b d;
- last_info <- string_of_text d);
+ | Some d ->
+ self#html_of_text b d;
+ last_info <- string_of_text d);
(match info.Odoc_info.i_desc with
| None -> ()
| Some d when d = [Odoc_info.Raw ""] -> ()
- | Some d ->
- self#html_of_text b d;
- last_info <- string_of_text d);
+ | Some d ->
+ self#html_of_text b d;
+ last_info <- string_of_text d);
self#html_of_raised_exceptions b info.Odoc_info.i_raised_exceptions;
self#html_of_return_opt b info.Odoc_info.i_return_value;
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 ->
@@ -97,11 +97,11 @@ module Generator (G : Odoc_html.Html_generator) = struct
| None -> ()
| Some d when d = [Odoc_info.Raw ""] -> ()
| Some d ->
- self#html_of_text b
+ self#html_of_text b
(Odoc_info.text_no_title_no_list
(Odoc_info.first_sentence_of_text d));
- last_info <- string_of_text
- (Odoc_info.text_no_title_no_list
+ last_info <- string_of_text
+ (Odoc_info.text_no_title_no_list
(Odoc_info.first_sentence_of_text d));
method generate module_list =
@@ -110,12 +110,12 @@ module Generator (G : Odoc_html.Html_generator) = struct
method private html_of_type_expr_param_list_1 b m_name t =
if string_of_type_param_list t <> "" then
- last_type <-
- last_type ^ "parameters: "^ string_of_type_param_list t
- ^ ", constructors: "
+ last_type <-
+ last_type ^ "parameters: "^ string_of_type_param_list t
+ ^ ", constructors: "
method private html_of_type_expr_list_2 ?par b m_name sep l =
- last_type <- last_type ^ " of " ^ string_of_type_list ?par sep l
+ last_type <- last_type ^ " of " ^ string_of_type_list ?par sep l
method private html_of_type_expr_3 b m_name t =
last_type <- last_type ^ ": " ^ string_of_type_expr t
@@ -124,20 +124,20 @@ module Generator (G : Odoc_html.Html_generator) = struct
last_type <- string_of_type_expr t
method html_of_class_type_param_expr_list b m_name l =
- last_type <- string_of_class_type_param_list l
+ last_type <- string_of_class_type_param_list l
method html_of_class_parameter_list b father c =
- last_type <- string_of_class_params c
+ last_type <- string_of_class_params c
method html_of_type_expr_param_list b m_name t =
- last_type <- string_of_type_param_list t
+ last_type <- string_of_type_param_list t
method html_of_module_type b ?code m_name t =
- last_type <- string_of_module_type ?code t
+ last_type <- string_of_module_type ?code t
method html_of_module_parameter b father p =
let s_functor, s_arrow =
- if !Odoc_html.html_short_functors then "", "" else "functor ", "-> "
+ if !Odoc_html.html_short_functors then "", "" else "functor ", "-> "
in
last_type <- last_type ^ s_functor ^ "(" ^ p.mp_name ^ " : ";
self#html_of_module_type_kind b father p.mp_kind;
@@ -148,17 +148,17 @@ module Generator (G : Odoc_html.Html_generator) = struct
| Module_type_struct eles ->
(match mt with
| None ->
- (match modu with
- | None ->
- last_type <- last_type ^ "sig ";
+ (match modu with
+ | None ->
+ last_type <- last_type ^ "sig ";
List.iter (self#html_of_module_element b father) eles;
- last_type <- last_type ^ " end "
- | Some m ->
- last_type <- last_type ^ "sig ";
+ last_type <- last_type ^ " end "
+ | Some m ->
+ last_type <- last_type ^ "sig ";
List.iter (self#html_of_module_element b father) eles;
- last_type <- last_type ^ " end ")
+ last_type <- last_type ^ " end ")
| Some mt ->
- last_type <- last_type ^ mt.mt_name)
+ last_type <- last_type ^ mt.mt_name)
| Module_type_functor (p, k) ->
self#html_of_module_parameter b father p;
self#html_of_module_type_kind b father ?modu ?mt k
@@ -174,13 +174,13 @@ module Generator (G : Odoc_html.Html_generator) = struct
| Module_struct eles ->
(match modu with
| None ->
- last_type <- last_type ^ "sig " ;
- List.iter (self#html_of_module_element b father) eles;
- last_type <- last_type ^ "end "
+ last_type <- last_type ^ "sig " ;
+ List.iter (self#html_of_module_element b father) eles;
+ last_type <- last_type ^ "end "
| Some m ->
- last_type <- last_type ^ "sig " ;
- List.iter (self#html_of_module_element b father) eles;
- last_type <- last_type ^ "end ");
+ last_type <- last_type ^ "sig " ;
+ List.iter (self#html_of_module_element b father) eles;
+ last_type <- last_type ^ "end ");
| Module_alias a ->
last_type <- last_type ^ (a.Module.ma_name)
| Module_functor (p, k) ->
@@ -188,7 +188,7 @@ module Generator (G : Odoc_html.Html_generator) = struct
(match k with
| Module_functor _ -> ()
| _ when !Odoc_html.html_short_functors ->
- last_type <- last_type ^ " : "
+ last_type <- last_type ^ " : "
| _ -> ());
self#html_of_module_kind b father ?modu k;
| Module_apply (k1, k2) ->
@@ -197,7 +197,7 @@ module Generator (G : Odoc_html.Html_generator) = struct
last_type <- last_type ^ " ( " ;
self#html_of_module_kind b father k2;
self#html_of_text b [Code ")"];
- last_type <- last_type ^ " ) "
+ last_type <- last_type ^ " ) "
| Module_with (k, s) ->
self#html_of_module_type_kind b father ?modu k;
last_type <- last_type ^ s
@@ -217,7 +217,7 @@ module Generator (G : Odoc_html.Html_generator) = struct
method html_of_exception b e =
last_name <- e.Exception.ex_name;
- last_type <-
+ last_type <-
(match e.Exception.ex_args with
| Odoc_type.Cstr_tuple t -> Odoc_info.string_of_type_list " " t
| Odoc_type.Cstr_record r -> Odoc_info.string_of_record r
@@ -273,9 +273,9 @@ module Generator (G : Odoc_html.Html_generator) = struct
super#html_of_attribute b a
method html_of_method b m =
- last_name <- m.Value.met_value.Value.val_name;
+ last_name <- m.Value.met_value.Value.val_name;
last_type <- "";
- super#html_of_method b m
+ super#html_of_method b m
method html_of_module b ?(info=true) ?(complete=true) ?(with_link=true) m =
last_name <- m.Module.m_name;
@@ -313,13 +313,13 @@ module Generator (G : Odoc_html.Html_generator) = struct
method html_of_class_type b ?(complete=true) ?(with_link=true) ct =
last_name <- ct.Class.clt_name;
last_type <- "" ;
- super#html_of_class_type b ~complete:complete ~with_link:with_link ct
+ super#html_of_class_type b ~complete:complete ~with_link:with_link ct
method private html_of_plugin_developer_guide _t =
- let temp =
- last_name ^ "/"
- ^ remove_useless_space
- (remove_useless_space (remove_nl (last_type ^ "/" ^ last_info ^ "/")))
+ let temp =
+ last_name ^ "/"
+ ^ remove_useless_space
+ (remove_useless_space (remove_nl (last_type ^ "/" ^ last_info ^ "/")))
in
to_print <- temp :: to_print;
last_name <- "" ;
@@ -329,7 +329,7 @@ module Generator (G : Odoc_html.Html_generator) = struct
initializer
tag_functions <-
- ("plugin", self#html_of_plugin_developer_guide) :: tag_functions
+ ("plugin", self#html_of_plugin_developer_guide) :: tag_functions
end
end
diff --git a/doc/developer/examples/acsl_extension_ext_types.ml b/doc/developer/examples/acsl_extension_ext_types.ml
index a387bad3fef54bfc18dd31db4121cc76feb6251f..bd8efcd6e7672dbd4835a5baad3ecef8759e85d7 100644
--- a/doc/developer/examples/acsl_extension_ext_types.ml
+++ b/doc/developer/examples/acsl_extension_ext_types.ml
@@ -39,4 +39,4 @@ let short_printer = gen_printer true
let () =
Acsl_extension.register_global
- "ext_type" ~preprocessor typer ~visitor ~printer ~short_printer false
\ No newline at end of file
+ "ext_type" ~preprocessor typer ~visitor ~printer ~short_printer false
diff --git a/doc/developer/examples/syntactic_check.ml b/doc/developer/examples/syntactic_check.ml
index 5c157d4e18bddb63f133e9f69f04dead891eb564..88d5765315bfe5c71a33b66cda7370d822485375 100644
--- a/doc/developer/examples/syntactic_check.ml
+++ b/doc/developer/examples/syntactic_check.ml
@@ -67,7 +67,7 @@ end
(* This function creates a new project initialized with the current file plus
the annotations related to division. *)
let create_syntactic_check_project () =
- ignore
+ ignore
(File.create_project_from_visitor "syntactic check" (new non_zero_divisor))
let () = Db.Main.extend create_syntactic_check_project
diff --git a/doc/developer/examples/use_callstack.ml b/doc/developer/examples/use_callstack.ml
index 0b4c456d06570894c1097f4c20515276ffcef286..956b27d41cf24e51414223d6dfdd5076d327c5a6 100644
--- a/doc/developer/examples/use_callstack.ml
+++ b/doc/developer/examples/use_callstack.ml
@@ -25,17 +25,17 @@ let callstack_ref = ref (get "empty" C.ty)
(* operations over this mutable callstack *)
-let push_callstack =
+let push_callstack =
(* getting the function outside the closure is more efficient *)
let push = get "push" (Datatype.func3 kf_ty stmt_ty C.ty C.ty) in
fun kf stmt -> callstack_ref := push kf stmt !callstack_ref
-let pop_callstack =
+let pop_callstack =
(* getting the function outside the closure is more efficient *)
let pop = get "pop" (Datatype.func C.ty C.ty) in
fun () -> callstack_ref := pop !callstack_ref
-let print_callstack =
+let print_callstack =
(* getting the function outside the closure is more efficient *)
let print = get "print" (Datatype.func C.ty Datatype.unit) in
fun () -> print !callstack_ref
diff --git a/doc/developer/tutorial/hello/src/hello_test.c b/doc/developer/tutorial/hello/src/hello_test.c
index 6ee10eeafa3bf084d6bb579ed00d4b31076b3a4b..d2f4ef3e1bfd30db301c62a3108511e6f6289e55 100644
--- a/doc/developer/tutorial/hello/src/hello_test.c
+++ b/doc/developer/tutorial/hello/src/hello_test.c
@@ -1,3 +1,3 @@
/* run.config
OPT: -hello
- */
\ No newline at end of file
+ */
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/developer/tutorial/viewcfg/src/dump_function.ml b/doc/developer/tutorial/viewcfg/src/dump_function.ml
index 29afbf838412d7d31316ca33b19a3f88daa7a74b..3be7ef642dc7e0fcc38a0c520255e192fbe39256 100644
--- a/doc/developer/tutorial/viewcfg/src/dump_function.ml
+++ b/doc/developer/tutorial/viewcfg/src/dump_function.ml
@@ -1,4 +1,4 @@
-let dump_function fundec fmt =
+let dump_function fundec fmt =
Format.fprintf fmt "@[<hov 2>digraph cfg {@ ";
ignore(Visitor.visitFramacFunction (new print_cfg fmt) fundec);
Format.fprintf fmt "}@]@\n"
diff --git a/doc/developer/tutorial/viewcfg/src/dump_function_memo_clear_cache.ml b/doc/developer/tutorial/viewcfg/src/dump_function_memo_clear_cache.ml
index 36eb30f11660c19bc89f3524067d71382e014733..224843d7deff9473e4fac1f421819ec907cc961f 100644
--- a/doc/developer/tutorial/viewcfg/src/dump_function_memo_clear_cache.ml
+++ b/doc/developer/tutorial/viewcfg/src/dump_function_memo_clear_cache.ml
@@ -1,5 +1,5 @@
let dump_function fundec fmt =
- if not (Value_is_computed.get ()) && Eva.Analysis.is_computed () then begin
+ if not (Value_is_computed.get ()) && Eva.Analysis.is_computed () then begin
Value_is_computed.set true;
let selection = State_selection.with_dependencies Cfg_graph_state.self in
Project.clear ~selection ();
diff --git a/doc/developer/tutorial/viewcfg/src/dump_function_memo_no_clear_cache.ml b/doc/developer/tutorial/viewcfg/src/dump_function_memo_no_clear_cache.ml
index 4db72d2e9b3ef05ae8fa34d64ee6edd6fec06e34..4352e8ddbf4e5f9a68f0ad75a53d331d1a2c2670 100644
--- a/doc/developer/tutorial/viewcfg/src/dump_function_memo_no_clear_cache.ml
+++ b/doc/developer/tutorial/viewcfg/src/dump_function_memo_no_clear_cache.ml
@@ -1,3 +1,3 @@
let dump_function fundec fmt =
- Format.fprintf fmt "@[digraph cfg {%s}@]@\n"
+ Format.fprintf fmt "@[digraph cfg {%s}@]@\n"
(dump_to_string_memoized fundec)
diff --git a/doc/developer/tutorial/viewcfg/src/dump_to_string_memoized.ml b/doc/developer/tutorial/viewcfg/src/dump_to_string_memoized.ml
index fee1b811f6565eed18e2586024ba6e2f6a40af76..360e8be2922529204500bd1df2ebe160d65bf035 100644
--- a/doc/developer/tutorial/viewcfg/src/dump_to_string_memoized.ml
+++ b/doc/developer/tutorial/viewcfg/src/dump_to_string_memoized.ml
@@ -1,6 +1,6 @@
-let dump_to_string fundec =
+let dump_to_string fundec =
Self.feedback "Computing CFG for function %s" (fundec.svar.vorig_name);
- ignore
+ ignore
(Visitor.visitFramacFunction (new print_cfg Format.str_formatter) fundec);
Format.flush_str_formatter ()
diff --git a/doc/developer/tutorial/viewcfg/src/extend_with_run_with_options.ml b/doc/developer/tutorial/viewcfg/src/extend_with_run_with_options.ml
index c5f060af17ef1ba883a9a571249ac80d699be807..b498fdb3da4511bc0a74c731c6e0c88046886d00 100644
--- a/doc/developer/tutorial/viewcfg/src/extend_with_run_with_options.ml
+++ b/doc/developer/tutorial/viewcfg/src/extend_with_run_with_options.ml
@@ -1,5 +1,5 @@
let run () =
- if Enabled.get() then
+ if Enabled.get() then
let filename = OutputFile.get () in
let chan = open_out filename in
let fmt = Format.formatter_of_out_channel chan in
diff --git a/doc/developer/tutorial/viewcfg/src/gui.ml b/doc/developer/tutorial/viewcfg/src/gui.ml
index bbb2874292e86b5c87fa4fc71f4d300d304ebd64..20ecefc84d6a9e1fe6274c41cdbe788b6318ba73 100644
--- a/doc/developer/tutorial/viewcfg/src/gui.ml
+++ b/doc/developer/tutorial/viewcfg/src/gui.ml
@@ -1,14 +1,14 @@
let cfg_selector
- (popup_factory:GMenu.menu GMenu.factory) main_ui ~button:_ localizable =
+ (popup_factory:GMenu.menu GMenu.factory) main_ui ~button:_ localizable =
match localizable with
(* Matches global declarations that are functions. *)
- | Pretty_source.PVDecl(_, _, ({vtype = TFun(_,_,_,_)} as vi)) ->
- let callback () =
+ | Pretty_source.PVDecl(_, _, ({vtype = TFun(_,_,_,_)} as vi)) ->
+ let callback () =
let kf = Globals.Functions.get vi in
let fundec = Kernel_function.get_definition kf in
let window:GWindow.window = main_ui#main_window in
Dgraph_helper.graph_window_through_dot
- ~parent:window ~title:"Control flow graph"
+ ~parent:window ~title:"Control flow graph"
(dump_function fundec)
in
ignore (popup_factory#add_item "Show _CFG" ~callback)
diff --git a/doc/developer/tutorial/viewcfg/src/print_cfg_vglob.ml b/doc/developer/tutorial/viewcfg/src/print_cfg_vglob.ml
index 8be1a7120afce6efd934c41b57c03402c7c0917c..2a01d5a038179a17fab9a088ed0608e1c3363d38 100644
--- a/doc/developer/tutorial/viewcfg/src/print_cfg_vglob.ml
+++ b/doc/developer/tutorial/viewcfg/src/print_cfg_vglob.ml
@@ -2,7 +2,7 @@
match g with
| GFun(f,_) ->
Format.fprintf out "@[<hov 2>subgraph cluster_%a {@ \
- @[<hv 2>graph@ [label=\"%a\"];@]@ "
+ @[<hv 2>graph@ [label=\"%a\"];@]@ "
Printer.pp_varinfo f.svar
Printer.pp_varinfo f.svar;
Cil.DoChildrenPost(fun g -> Format.fprintf out "}@]@ "; g)
diff --git a/doc/developer/tutorial/viewcfg/src/print_cfg_vstmt_aux_novalue.ml b/doc/developer/tutorial/viewcfg/src/print_cfg_vstmt_aux_novalue.ml
index fc8510119d4a427784413b53237b6c52f9a46587..2cf7028f64212143671a6c922b22fc57db934708 100644
--- a/doc/developer/tutorial/viewcfg/src/print_cfg_vstmt_aux_novalue.ml
+++ b/doc/developer/tutorial/viewcfg/src/print_cfg_vstmt_aux_novalue.ml
@@ -1,7 +1,7 @@
method! vstmt_aux s =
Format.fprintf out "@[<hov 2>s%d@ [label=%S]@];@ "
s.sid (Pretty_utils.to_string print_stmt s.skind);
- List.iter
+ List.iter
(fun succ -> Format.fprintf out "@[s%d -> s%d;@]@ " s.sid succ.sid)
s.succs;
Format.fprintf out "@]";
diff --git a/doc/developer/tutorial/viewcfg/src/print_cfg_vstmt_aux_value.ml b/doc/developer/tutorial/viewcfg/src/print_cfg_vstmt_aux_value.ml
index 67038d53098490e5c6d7b14991dac834b5b9e9a9..0f18131313641361fadc7e622679ffd508c06da0 100644
--- a/doc/developer/tutorial/viewcfg/src/print_cfg_vstmt_aux_value.ml
+++ b/doc/developer/tutorial/viewcfg/src/print_cfg_vstmt_aux_value.ml
@@ -1,15 +1,15 @@
method! vstmt_aux s =
- let color =
+ let color =
if Eva.Analysis.is_computed () then
- let state = Db.Value.get_stmt_state s in
- let reachable = Db.Value.is_reachable state in
- if reachable then "fillcolor=\"#ccffcc\" style=filled"
- else "fillcolor=pink style=filled"
- else ""
+ let state = Db.Value.get_stmt_state s in
+ let reachable = Db.Value.is_reachable state in
+ if reachable then "fillcolor=\"#ccffcc\" style=filled"
+ else "fillcolor=pink style=filled"
+ else ""
in
Format.fprintf out "@[s%d@ [label=%S %s]@];@ "
s.sid (Pretty_utils.to_string print_stmt s.skind) color;
- List.iter
+ List.iter
(fun succ -> Format.fprintf out "@[s%d -> s%d;@]@ " s.sid succ.sid)
s.succs;
Cil.DoChildren
diff --git a/doc/developer/tutorial/viewcfg/src/print_stmt.ml b/doc/developer/tutorial/viewcfg/src/print_stmt.ml
index 7b3d97a77a688ebf3ee4e92839647df1e9021537..20fd996d6dc335739b054091dc0228e8dc468dea 100644
--- a/doc/developer/tutorial/viewcfg/src/print_stmt.ml
+++ b/doc/developer/tutorial/viewcfg/src/print_stmt.ml
@@ -13,4 +13,3 @@ let print_stmt out = function
| UnspecifiedSequence _ -> Format.fprintf out "<unspecified sequence>"
| TryFinally _ | TryExcept _ | TryCatch _ -> Format.fprintf out "<try>"
| Throw _ -> Format.fprintf out "<throw>"
-
diff --git a/doc/slicing/algo.ml b/doc/slicing/algo.ml
index 35755d65866f27523d34355ed7ebcfb7cb07225a..43af54ff6a00057b2abe5251783aa22b7b929952 100644
--- a/doc/slicing/algo.ml
+++ b/doc/slicing/algo.ml
@@ -11,7 +11,7 @@ let rec mark_rec_pdg_elem pdg stmt_elems m e ff =
and
(* [add_elem_mark] ajoute la marque [m] Ã l'instruction correspondant Ã
l'élément [e] et marque les autres éléments éventuels comme superflus. *)
- add_elem_mark pdg stmt_elems m e ff =
+ add_elem_mark pdg stmt_elems m e ff =
let stmt = H.get_stmt e stmt_elems in
let old_m = H.get_stmt_mark stmt ff in
let new_m = H.combine_mark old_m m in
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/training/developer/sources/basic_script.ml b/doc/training/developer/sources/basic_script.ml
index fd83c661bb190de5faf19f44fb978f59641aa548..bf59c5b89e8c26ef7a0d73c51b05a9e2973943e2 100644
--- a/doc/training/developer/sources/basic_script.ml
+++ b/doc/training/developer/sources/basic_script.ml
@@ -15,7 +15,7 @@ let run f () =
(*# Main driver function*)
let all_entry_points () =
(*## Setting options. *)
- let files = [ "huffman.c"; "rice.c"; "shannonfano.c"; "lz.c"; "rle.c";
+ let files = [ "huffman.c"; "rice.c"; "shannonfano.c"; "lz.c"; "rle.c";
"systimer.c" ]
in
let files = List.map (Filename.concat "bcl") files in
@@ -27,7 +27,7 @@ let all_entry_points () =
(*## Find entry points *)
Globals.Functions.iter
(fun kf ->
- if Kernel_function.is_definition kf &&
+ if Kernel_function.is_definition kf &&
(Kernel_function.find_syntactic_callsites kf = [])
then
run (Kernel_function.get_name kf) ());
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.