diff --git a/doc/code/docgen.ml b/doc/code/docgen.ml
index a3a013b7955a45e805145625a56701b96d554155..86d4520c3707db5a9aa0b4fd710afec47a1d9147 100644
--- a/doc/code/docgen.ml
+++ b/doc/code/docgen.ml
@@ -31,7 +31,7 @@ let add_libfiles analyse s =
let f = Odoc_global.Intf_file s in
lib_files :=
(String.capitalize_ascii (Filename.chop_extension (Filename.basename s))) ::
- !lib_files;
+ !lib_files;
if analyse then Odoc_global.files := f :: !Odoc_global.files
let rec root_name s =
@@ -47,103 +47,103 @@ let equal_module m1 m2 = equal_module_name m1 m2.m_name
type chapter = Chapter of int * string * string | Directory of string
let compare_chapter c1 c2 = match c1 , c2 with
- | Chapter(a,_,_) , Chapter(b,_,_) -> a-b
- | Directory a , Directory b -> compare a b
- | Chapter _ , Directory _ -> (-1)
- | Directory _ , Chapter _ -> 1
+ | Chapter(a,_,_) , Chapter(b,_,_) -> a-b
+ | Directory a , Directory b -> compare a b
+ | Chapter _ , Directory _ -> (-1)
+ | Directory _ , Chapter _ -> 1
let merge3
(s1 : 'a -> 'a -> int)
(s2 : 'b -> 'b -> int)
(s3 : 'c -> 'c -> int)
(triplets : ('a * 'b * 'c) list)
- : ('a * ('b * 'c list) list) list =
+ : ('a * ('b * 'c list) list) list =
let sort3_rev s1 s2 s3 (x,y,z) (x',y',z') =
let c = s1 x' x in
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
- | (a,b,c)::tail , merged ->
- merge3_rev (( a , [b,[c]] )::merged) tail
+ | [] , _ -> 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
+ | (a,b,c)::tail , merged ->
+ 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
"http://caml.inria.fr/pub/docs/manual-ocaml/libref/"
else
- if List.exists (fun m -> m.m_name = name) self#loaded_modules
- then !doc_path ^ "/"
- else "./"
+ if List.exists (fun m -> m.m_name = name) self#loaded_modules
+ then !doc_path ^ "/"
+ else "./"
method create_fully_qualified_idents_links m_name s =
let f str_t =
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
- let (html_file, _) = Naming.html_files match_s in
- "<a href=\""^ self#path html_file ^ html_file^"\">"^s_final^"</a>"
- else
- s_final
+ 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
+ s_final
in
let s2 = Str.global_substitute
- (Str.regexp "\\([A-Z]\\([a-zA-Z_'0-9]\\)*\\.\\)+\\([a-z][a-zA-Z_'0-9]*\\)")
- f
- s
+ (Str.regexp "\\([A-Z]\\([a-zA-Z_'0-9]\\)*\\.\\)+\\([a-z][a-zA-Z_'0-9]*\\)")
+ f
+ s
in
s2
@@ -154,20 +154,20 @@ 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]*\\)")
- f
- s
+ (Str.regexp "\\([A-Z]\\([a-zA-Z_'0-9]\\)*\\.\\)+\\([A-Z][a-zA-Z_'0-9]*\\)")
+ f
+ s
in
s2
@@ -175,31 +175,31 @@ 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"),
chop "kernel_services/" f
with Not_found ->
- try Chapter(2,"Libraries","src/libraries"), chop "libraries/" f
- with Not_found ->
- try
- Chapter(3,"Kernel Internals","src/kernel_internals"),
- chop "kernel_internals/" f
- with Not_found ->
- let d = Filename.dirname f in
- Directory (Filename.basename (Filename.dirname d)) ,
- String.capitalize_ascii (Filename.basename d)
+ try Chapter(2,"Libraries","src/libraries"), chop "libraries/" f
+ with Not_found ->
+ try
+ Chapter(3,"Kernel Internals","src/kernel_internals"),
+ chop "kernel_internals/" f
+ with Not_found ->
+ let d = Filename.dirname f in
+ Directory (Filename.basename (Filename.dirname d)) ,
+ String.capitalize_ascii (Filename.basename d)
in
let structured_modules (* chapter, section, module *) =
(List.map
(fun name ->
- let m = List.find (fun m -> m.m_name = name) self#list_modules in
- let dir,name = dir m.m_file in
- dir,name,m)
+ let m = List.find (fun m -> m.m_name = name) self#list_modules in
+ let dir,name = dir m.m_file in
+ dir,name,m)
l)
in
let toc_modules (* chapter/section/modules *) =
@@ -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. *)
@@ -244,17 +244,17 @@ struct
(
match im.im_module with
None ->
- bs b im.im_name
+ bs b im.im_name
| Some mmt ->
let (file, name) =
match mmt with
Mod m ->
- let (html_file, _) = Naming.html_files m.m_name in
- (html_file, m.m_name)
+ let (html_file, _) = Naming.html_files m.m_name in
+ (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
@@ -287,43 +287,43 @@ struct
let types = Odoc_info.Search.types module_list in
known_types_names <-
List.fold_left
- (fun acc t -> String.Set.add t.Odoc_type.ty_name acc)
- known_types_names
- types ;
+ (fun acc t -> String.Set.add t.Odoc_type.ty_name acc)
+ known_types_names
+ types ;
(* Get the names of all class and class types. *)
let classes = Odoc_info.Search.classes module_list in
let class_types = Odoc_info.Search.class_types module_list in
known_classes_names <-
List.fold_left
- (fun acc c -> String.Set.add c.Odoc_class.cl_name acc)
- known_classes_names
- classes ;
+ (fun acc c -> String.Set.add c.Odoc_class.cl_name acc)
+ known_classes_names
+ classes ;
known_classes_names <-
List.fold_left
- (fun acc ct -> String.Set.add ct.Odoc_class.clt_name acc)
- known_classes_names
- class_types ;
+ (fun acc ct -> String.Set.add ct.Odoc_class.clt_name acc)
+ known_classes_names
+ class_types ;
(* Get the names of all known modules and module types. *)
let module_types = Odoc_info.Search.module_types module_list in
let modules = Odoc_info.Search.modules module_list in
known_modules_names <-
List.fold_left
- (fun acc m -> String.Set.add m.m_name acc)
- known_modules_names
- modules ;
+ (fun acc m -> String.Set.add m.m_name acc)
+ known_modules_names
+ modules ;
known_modules_names <-
List.fold_left
- (fun acc mt -> String.Set.add mt.mt_name acc)
- known_modules_names
- module_types ;
+ (fun acc mt -> String.Set.add mt.mt_name acc)
+ known_modules_names
+ module_types ;
(* 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,38 +363,38 @@ struct
method private html_of_ignore _t = ""
method private html_of_modify t = match t with
- | [] ->
- 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, ""
- in
- let text =
- Bold [ Raw "Change in "; Raw time ] :: Raw explanation :: l
- in
- let buf = Buffer.create 7 in
- self#html_of_text buf text;
- Buffer.add_string buf "<br>\n";
- Buffer.contents buf
- | _ :: _ ->
- assert false
+ | [] ->
+ 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, ""
+ in
+ let text =
+ Bold [ Raw "Change in "; Raw time ] :: Raw explanation :: l
+ in
+ let buf = Buffer.create 7 in
+ self#html_of_text buf text;
+ Buffer.add_string buf "<br>\n";
+ Buffer.contents buf
+ | _ :: _ ->
+ assert false
method private html_of_call t = match t with
- | [] ->
- Odoc_info.warning "Found an empty @call tag";
- ""
- | l ->
- let buf = Buffer.create 97 in
- Buffer.add_string buf "<b>Access it by</b> <code class=\"code\">";
- self#html_of_text buf l;
- Buffer.add_string buf "</code>\n";
- Buffer.contents buf
+ | [] ->
+ Odoc_info.warning "Found an empty @call tag";
+ ""
+ | l ->
+ let buf = Buffer.create 97 in
+ Buffer.add_string buf "<b>Access it by</b> <code class=\"code\">";
+ self#html_of_text buf l;
+ Buffer.add_string buf "</code>\n";
+ Buffer.contents buf
(* Write the subtitle (eg. "Frama-C Kernel" after the main title
instead of before, for users that use many tabs in their browser *)
@@ -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 155c3001dc99172829058c1fd1637d6fcc38a596..e7005ca2585843d3f9c87a291a825fd10771480e 100644
--- a/doc/developer/check_api/check_and_compare.ml
+++ b/doc/developer/check_api/check_and_compare.ml
@@ -102,12 +102,12 @@ let run_oracle t1 t2 =
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)
+ (Printexc.to_string exn)
in
let rec string_of_list l = match l with
| [] -> ""
@@ -124,9 +124,9 @@ let run_oracle t1 t2 =
in
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 =
@@ -137,31 +137,31 @@ let run_oracle t1 t2 =
let element_info = Hashtbl.find t k
in
to_fill :=
- !to_fill ^ "\n" ^ k ^ "/"^ string_of_list element_info;
+ !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 \
- 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)
+ 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 ->
(* element not previously registered *)
()
in
Format.printf "%s" " \n \n*****************************\
-*************************************\
-\nELEMENTS OF THE INDEX OF THE DEVELOPER GUIDE EXISTING \
-IN THE CODE: \n*****************************************\
-*************************\n\n";
+ *************************************\
+ \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)
+ fill_oracle !to_fill)
else (Hashtbl.iter (wo_tbl t2) t1 ;
- fill_oracle !to_fill)
-
-
+ 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.
@@ -171,17 +171,17 @@ let compare t1 t2 name1 name2 =
let compare_aux t k =
if not(List.mem k t) then Format.printf "%s" (k ^ "\n") in
Format.printf " \n \n*****************************************\
-*******************\
-\nELEMENTS OF %s NOT IN %s: \n***********************************\
-*************************\
-\n\n"
+ *******************\
+ \nELEMENTS OF %s NOT IN %s: \n***********************************\
+ *************************\
+ \n\n"
name1 name2;
List.iter (compare_aux t2) t1;
Format.printf " \n \n*******************************************\
-*****************\
-\nELEMENTS OF %s NOT IN %s: \n************************************\
-************************\
-\n\n"
+ *****************\
+ \nELEMENTS OF %s NOT IN %s: \n************************************\
+ ************************\
+ \n\n"
name2 name1;
List.iter (compare_aux t1) t2
@@ -206,17 +206,17 @@ let () =
output_string chan_out res;
done
with End_of_file -> ();
- close_out chan_out ; close_in chan_in;
- fill_tbl code_hstbl "code_file";
- fill_tbl index_hstbl "index_file";
- let code_list = sort_keys code_hstbl in
- let index_list = sort_keys index_hstbl in
- compare index_list code_list "THE INDEX \
-OF THE DEVELOPER GUIDE" "THE CODE";
- run_oracle index_hstbl code_hstbl ;
+ close_out chan_out ; close_in chan_in;
+ fill_tbl code_hstbl "code_file";
+ fill_tbl index_hstbl "index_file";
+ let code_list = sort_keys code_hstbl in
+ let index_list = sort_keys index_hstbl in
+ compare index_list code_list "THE INDEX \
+ 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"
(Printexc.to_string exn)
diff --git a/doc/developer/check_api/check_code.ml b/doc/developer/check_api/check_code.ml
index 6f312d6779f257b9333206e744a5799d8595818c..9a2cab0b2c11858584073dd1fbc5b1deed2e7060 100644
--- a/doc/developer/check_api/check_code.ml
+++ b/doc/developer/check_api/check_code.ml
@@ -49,58 +49,58 @@ module Generator (G : Odoc_html.Html_generator) = struct
(** Print html code for the given list of raised exceptions.*)
method html_of_raised_exceptions b l = match l with
- | [] -> ()
- | (s, t) :: [] ->
- self#html_of_text b t;
- let temp =
- 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) ->
- self#html_of_text b desc;
- let temp = last_info ^ ", " ^ Odoc_info.string_of_text desc in
- last_info <- temp)
- l
+ | [] -> ()
+ | (s, t) :: [] ->
+ self#html_of_text b t;
+ let temp =
+ 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) ->
+ self#html_of_text b desc;
+ 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 ->
- ()
- | Some info ->
- (match info.Odoc_info.i_deprecated with
- | None -> ()
- | 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);
- 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
+ | None ->
+ ()
+ | Some info ->
+ (match info.Odoc_info.i_deprecated with
+ | None -> ()
+ | 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);
+ 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 ->
- match info.Odoc_info.i_desc with
| None -> ()
- | Some d when d = [Odoc_info.Raw ""] -> ()
- | Some d ->
- 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
- (Odoc_info.first_sentence_of_text d));
+ | Some info ->
+ match info.Odoc_info.i_desc with
+ | None -> ()
+ | Some d when d = [Odoc_info.Raw ""] -> ()
+ | Some d ->
+ 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
+ (Odoc_info.first_sentence_of_text d));
method generate module_list =
super#generate module_list;
@@ -108,9 +108,9 @@ 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
@@ -135,7 +135,7 @@ module Generator (G : Odoc_html.Html_generator) = struct
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;
@@ -143,70 +143,70 @@ module Generator (G : Odoc_html.Html_generator) = struct
(** Print html code to display the given module type kind. *)
method html_of_module_type_kind b father ?modu ?mt = function
- | Module_type_struct eles ->
- (match mt with
- | None ->
- (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 ";
- List.iter (self#html_of_module_element b father) eles;
- last_type <- last_type ^ " end ")
- | Some mt ->
- 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
- | Module_type_alias a ->
- last_type <- last_type ^ a.Module.mta_name
- | Module_type_with (k, s) ->
- self#html_of_module_type_kind b father ?modu ?mt k;
- last_type <- last_type ^ s
- | Module_type_typeof s ->
- last_type <- last_type ^ " module type of " ^ s
+ | Module_type_struct eles ->
+ (match mt with
+ | None ->
+ (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 ";
+ List.iter (self#html_of_module_element b father) eles;
+ last_type <- last_type ^ " end ")
+ | Some mt ->
+ 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
+ | Module_type_alias a ->
+ last_type <- last_type ^ a.Module.mta_name
+ | Module_type_with (k, s) ->
+ self#html_of_module_type_kind b father ?modu ?mt k;
+ last_type <- last_type ^ s
+ | Module_type_typeof s ->
+ last_type <- last_type ^ " module type of " ^ s
method html_of_module_kind b father ?modu = function
- | 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 "
- | Some m ->
- 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) ->
- self#html_of_module_parameter b father p;
- (match k with
- | Module_functor _ -> ()
- | _ when !Odoc_html.html_short_functors ->
- last_type <- last_type ^ " : "
- | _ -> ());
- self#html_of_module_kind b father ?modu k;
- | Module_apply (k1, k2) ->
- self#html_of_module_kind b father k1;
- self#html_of_text b [Code "("];
- last_type <- last_type ^ " ( " ;
- self#html_of_module_kind b father k2;
- self#html_of_text b [Code ")"];
- last_type <- last_type ^ " ) "
- | Module_with (k, s) ->
- self#html_of_module_type_kind b father ?modu k;
- last_type <- last_type ^ s
- | Module_constraint (k, tk) ->
- self#html_of_module_kind b father ?modu k
- | Module_typeof s ->
- last_type <- last_type ^ " module type of " ^ s
- | Module_unpack (code, mta) ->
- (match mta.mta_module with
- | None -> last_type <- last_type ^ self#escape code
- | Some mt -> last_type <- last_type ^ mt.Module.mt_name ^ self#escape code)
+ | 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 "
+ | Some m ->
+ 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) ->
+ self#html_of_module_parameter b father p;
+ (match k with
+ | Module_functor _ -> ()
+ | _ when !Odoc_html.html_short_functors ->
+ last_type <- last_type ^ " : "
+ | _ -> ());
+ self#html_of_module_kind b father ?modu k;
+ | Module_apply (k1, k2) ->
+ self#html_of_module_kind b father k1;
+ self#html_of_text b [Code "("];
+ last_type <- last_type ^ " ( " ;
+ self#html_of_module_kind b father k2;
+ self#html_of_text b [Code ")"];
+ last_type <- last_type ^ " ) "
+ | Module_with (k, s) ->
+ self#html_of_module_type_kind b father ?modu k;
+ last_type <- last_type ^ s
+ | Module_constraint (k, tk) ->
+ self#html_of_module_kind b father ?modu k
+ | Module_typeof s ->
+ last_type <- last_type ^ " module type of " ^ s
+ | Module_unpack (code, mta) ->
+ (match mta.mta_module with
+ | None -> last_type <- last_type ^ self#escape code
+ | Some mt -> last_type <- last_type ^ mt.Module.mt_name ^ self#escape code)
method html_of_value b v =
last_name <- v.Value.val_name;
@@ -217,41 +217,41 @@ module Generator (G : Odoc_html.Html_generator) = struct
last_name <- e.Exception.ex_name;
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
+ | Odoc_type.Cstr_tuple t -> Odoc_info.string_of_type_list " " t
+ | Odoc_type.Cstr_record r -> Odoc_info.string_of_record r
);
super#html_of_exception b e
method private print_record b father l =
- let print_one r =
- last_name <- father ^ "." ^ r.Type.rf_name;
- last_type <- father ^ " -> " ^ Odoc_info.string_of_type_expr r.Type.rf_type;
- self#html_of_info b r.Type.rf_text
- in
- print_concat b "\n" print_one l;
+ let print_one r =
+ last_name <- father ^ "." ^ r.Type.rf_name;
+ last_type <- father ^ " -> " ^ Odoc_info.string_of_type_expr r.Type.rf_type;
+ self#html_of_info b r.Type.rf_text
+ in
+ print_concat b "\n" print_one l;
method html_of_type b t =
Odoc_info.reset_type_names ();
let father = Name.father t.Type.ty_name in
self#html_of_type_expr_param_list_1 b father t;
(match t.Type.ty_kind with
- | Type.Type_abstract -> ()
- | Type.Type_variant l ->
- let print_one constr =
- last_type <- "";
- last_name <- t.Type.ty_name ^ "." ^ constr.Type.vc_name;
- (match constr.Type.vc_args with
- | Odoc_type.Cstr_tuple [] -> ()
- | Odoc_type.Cstr_tuple l ->
+ | Type.Type_abstract -> ()
+ | Type.Type_variant l ->
+ let print_one constr =
+ last_type <- "";
+ last_name <- t.Type.ty_name ^ "." ^ constr.Type.vc_name;
+ (match constr.Type.vc_args with
+ | Odoc_type.Cstr_tuple [] -> ()
+ | Odoc_type.Cstr_tuple l ->
self#html_of_type_expr_list_2 ~par: false b father " * " l
- | Odoc_type.Cstr_record r ->
+ | Odoc_type.Cstr_record r ->
self#print_record b father r
- );
- self#html_of_info b constr.Type.vc_text
- in
- print_concat b "\n" print_one l;
- | Type.Type_record l -> self#print_record b father l
- | _ -> ());
+ );
+ self#html_of_info b constr.Type.vc_text
+ in
+ print_concat b "\n" print_one l;
+ | Type.Type_record l -> self#print_record b father l
+ | _ -> ());
last_name <- t.Type.ty_name;
last_type <- "";
self#html_of_info b t.Type.ty_info;
@@ -281,8 +281,8 @@ module Generator (G : Odoc_html.Html_generator) = struct
last_type <- "" ;
let father = Name.father mt.mt_name in
(match mt.mt_kind with
- | None -> ()
- | Some k -> self#html_of_module_type_kind b father ~mt k);
+ | None -> ()
+ | Some k -> self#html_of_module_type_kind b father ~mt k);
last_name <- mt.Module.mt_name;
if info then
if complete then self#html_of_info ~indent: false b mt.mt_info
@@ -306,9 +306,9 @@ module Generator (G : Odoc_html.Html_generator) = struct
method private html_of_plugin_developer_guide _t =
let temp =
- last_name ^ "/"
- ^ remove_useless_space
- (remove_useless_space (remove_nl (last_type ^ "/" ^ last_info ^ "/")))
+ last_name ^ "/"
+ ^ remove_useless_space
+ (remove_useless_space (remove_nl (last_type ^ "/" ^ last_info ^ "/")))
in
to_print <- temp :: to_print;
last_name <- "" ;
@@ -318,7 +318,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_foo.ml b/doc/developer/examples/acsl_extension_foo.ml
index 239ccd00b7ab944e00e02acc3d086207b22fc296..a30fbbe5625e5c72ad7918d11e79012f53b7bc5b 100644
--- a/doc/developer/examples/acsl_extension_foo.ml
+++ b/doc/developer/examples/acsl_extension_foo.ml
@@ -5,8 +5,8 @@ open Logic_typing
let type_foo typing_context _loc l =
let type_term ctxt env expr =
match expr.lexpr_node with
- | PLvar "\\foo" -> Logic_const.tinteger ~loc:expr.lexpr_loc 42
- | _ -> typing_context.type_term ctxt env expr
+ | PLvar "\\foo" -> Logic_const.tinteger ~loc:expr.lexpr_loc 42
+ | _ -> typing_context.type_term ctxt env expr
in
let typing_context = { typing_context with type_term } in
let res =
diff --git a/doc/developer/examples/callstack.ml b/doc/developer/examples/callstack.ml
index e5b5380a728743447d19e0a4a823b685b52712f8..8edfe1cfd863bbcaa7698c9e6830523a2e1d7ae2 100644
--- a/doc/developer/examples/callstack.ml
+++ b/doc/developer/examples/callstack.ml
@@ -17,7 +17,7 @@ module P =
let name = "Callstack"
let shortname = "Callstack"
let help = "callstack library"
- end)
+ end)
(* A callstack is a list of a pair (kf * stmt) where [kf] is the kernel
function called at statement [stmt]. Building the datatype also creates the
@@ -47,7 +47,7 @@ module D =
let name = "Callstack.t"
let reprs = [ empty; [ Kernel_function.dummy (), Cil.dummyStmt ] ]
include Datatype.Serializable_undefined
- end)
+ end)
(* Dynamic API registration *)
let register name ty =
diff --git a/doc/developer/examples/syntactic_check.ml b/doc/developer/examples/syntactic_check.ml
index 5c157d4e18bddb63f133e9f69f04dead891eb564..6049b37e8d824b6a4b2dd741e4ad20623531c4eb 100644
--- a/doc/developer/examples/syntactic_check.ml
+++ b/doc/developer/examples/syntactic_check.ml
@@ -30,38 +30,38 @@ class non_zero_divisor prj = object (self)
(* A division is an expression: we override the vexpr method *)
method! vexpr e = match e.enode with
- | BinOp((Div|Mod), _, denom, _) ->
- let logic_denom = Logic_utils.expr_to_term ~coerce:false denom in
- let assertion = Logic_const.prel (Rneq, logic_denom, Cil.lzero ()) in
- (* At this point, we have built the assertion we want to insert. It remains
- to attach it to the correct statement. The cil visitor maintains the
- information of which statement and function are currently visited in
- the [current_stmt] and [current_kf] methods, which return None when
- outside of a statement or a function , e.g. when visiting a global
- declaration. Here, it necessarily returns [Some]. *)
- let stmt = match self#current_kinstr with
- | Kglobal -> assert false
- | Kstmt s -> s
- in
- let kf = Option.get self#current_kf in
- (* The above statement and function are related to the original project. We
- need to attach the new assertion to the corresponding statement and
- function of the new project. Cil provides functions to convert a
- statement (function) of the original project to the corresponding
- one of the new project. *)
- let new_stmt = Visitor_behavior.Get.stmt self#behavior stmt in
- let new_kf = Visitor_behavior.Get.kernel_function self#behavior kf in
- (* Since we are copying the file in a new project, we cannot insert
- the annotation into the current table, but in the table of the new
- project. To avoid the cost of switching projects back and forth,
- all operations on the new project are queued until the end of the
- visit, as mentioned above. This is done in the following statement. *)
- Queue.add
- (fun () ->
- Annotations.add_assert syntax_alarm ~kf:new_kf new_stmt assertion)
- self#get_filling_actions;
- DoChildren
- | _ -> DoChildren
+ | BinOp((Div|Mod), _, denom, _) ->
+ let logic_denom = Logic_utils.expr_to_term ~coerce:false denom in
+ let assertion = Logic_const.prel (Rneq, logic_denom, Cil.lzero ()) in
+ (* At this point, we have built the assertion we want to insert. It remains
+ to attach it to the correct statement. The cil visitor maintains the
+ information of which statement and function are currently visited in
+ the [current_stmt] and [current_kf] methods, which return None when
+ outside of a statement or a function , e.g. when visiting a global
+ declaration. Here, it necessarily returns [Some]. *)
+ let stmt = match self#current_kinstr with
+ | Kglobal -> assert false
+ | Kstmt s -> s
+ in
+ let kf = Option.get self#current_kf in
+ (* The above statement and function are related to the original project. We
+ need to attach the new assertion to the corresponding statement and
+ function of the new project. Cil provides functions to convert a
+ statement (function) of the original project to the corresponding
+ one of the new project. *)
+ let new_stmt = Visitor_behavior.Get.stmt self#behavior stmt in
+ let new_kf = Visitor_behavior.Get.kernel_function self#behavior kf in
+ (* Since we are copying the file in a new project, we cannot insert
+ the annotation into the current table, but in the table of the new
+ project. To avoid the cost of switching projects back and forth,
+ all operations on the new project are queued until the end of the
+ visit, as mentioned above. This is done in the following statement. *)
+ Queue.add
+ (fun () ->
+ Annotations.add_assert syntax_alarm ~kf:new_kf new_stmt assertion)
+ self#get_filling_actions;
+ DoChildren
+ | _ -> DoChildren
end
(* This function creates a new project initialized with the current file plus
diff --git a/doc/developer/hello_world/hello_world.ml b/doc/developer/hello_world/hello_world.ml
index 8fb440417ed1112b2367dfb47252b70e249cbf8f..bc6c4f1c095c906e9c15ea7b859074955c98b083 100644
--- a/doc/developer/hello_world/hello_world.ml
+++ b/doc/developer/hello_world/hello_world.ml
@@ -22,18 +22,18 @@
module Self =
Plugin.Register
(struct
- let name = "Hello world"
- let shortname = "hello"
- let help = "The famous 'Hello world' plugin"
- end)
+ let name = "Hello world"
+ let shortname = "hello"
+ let help = "The famous 'Hello world' plugin"
+ end)
(** Register the new Frama-C option "-hello". *)
module Enabled =
Self.False
(struct
- let option_name = "-hello"
- let help = "pretty print \"Hello world!\""
- end)
+ let option_name = "-hello"
+ let help = "pretty print \"Hello world!\""
+ end)
let print () = Self.result "Hello world!"
@@ -45,7 +45,7 @@ let print () = Self.result "Hello world!"
let print =
Dynamic.register
~comment:"[Dynamic.get \"Hello.run\" (Datatype.func Datatype.unit \
-Datatype.unit)] calls [run] and pretty prints \"Hello world!\""
+ Datatype.unit)] calls [run] and pretty prints \"Hello world!\""
~plugin:"Hello"
"run"
(Datatype.func Datatype.unit Datatype.unit)
diff --git a/doc/developer/tutorial/hello/src/options_enabled.ml b/doc/developer/tutorial/hello/src/options_enabled.ml
index 7f4fae2e394eb73f0397dab72a0e17ff58c348a5..dfd1f36753e8e46e2dbf42101d8375323509ce21 100644
--- a/doc/developer/tutorial/hello/src/options_enabled.ml
+++ b/doc/developer/tutorial/hello/src/options_enabled.ml
@@ -1,5 +1,5 @@
module Enabled = Self.False
- (struct
- let option_name = "-hello"
- let help = "when on (off by default), " ^ help_msg
- end)
+ (struct
+ let option_name = "-hello"
+ let help = "when on (off by default), " ^ help_msg
+ end)
diff --git a/doc/developer/tutorial/hello/src/options_output_file.ml b/doc/developer/tutorial/hello/src/options_output_file.ml
index 10df52fa46d2415c55b0b36716ad56e5401cf60a..160d20a7790cca6848e7f737405c4f16d9141f58 100644
--- a/doc/developer/tutorial/hello/src/options_output_file.ml
+++ b/doc/developer/tutorial/hello/src/options_output_file.ml
@@ -1,8 +1,8 @@
module Output_file = Self.String
- (struct
- let option_name = "-hello-output"
- let default = "-"
- let arg_name = "output-file"
- let help =
- "file where the message is output (default: output to the console)"
- end)
+ (struct
+ let option_name = "-hello-output"
+ let default = "-"
+ let arg_name = "output-file"
+ let help =
+ "file where the message is output (default: output to the console)"
+ end)
diff --git a/doc/developer/tutorial/hello/src/register.ml b/doc/developer/tutorial/hello/src/register.ml
index 196b0ad93091ebef14d11d5efda32f1122fd99b3..e339ccbd73eb4d505a4565a7be71eb72efb62b83 100644
--- a/doc/developer/tutorial/hello/src/register.ml
+++ b/doc/developer/tutorial/hello/src/register.ml
@@ -1,6 +1,6 @@
module Self = Plugin.Register
- (struct
- let name = "hello world"
- let shortname = "hello"
- let help = help_msg
- end)
+ (struct
+ let name = "hello world"
+ let shortname = "hello"
+ let help = help_msg
+ end)
diff --git a/doc/developer/tutorial/hello/src/run_with_options.ml b/doc/developer/tutorial/hello/src/run_with_options.ml
index 639bd76c27ce46217ca5947e0d5b5af4792f5c49..724d3e6d3bfdfc115c22d46aa485db1dd2ef954d 100644
--- a/doc/developer/tutorial/hello/src/run_with_options.ml
+++ b/doc/developer/tutorial/hello/src/run_with_options.ml
@@ -1,17 +1,17 @@
let run () =
try
- if Enabled.get() then
- let filename = Output_file.get () in
- let output msg =
- if Output_file.is_default() then
- Self.result "%s" msg
- else
- let chan = open_out filename in
- Printf.fprintf chan "%s\n" msg;
- flush chan;
- close_out chan;
- in
- output "Hello, world!"
+ if Enabled.get() then
+ let filename = Output_file.get () in
+ let output msg =
+ if Output_file.is_default() then
+ Self.result "%s" msg
+ else
+ let chan = open_out filename in
+ Printf.fprintf chan "%s\n" msg;
+ flush chan;
+ close_out chan;
+ in
+ output "Hello, world!"
with Sys_error _ as exc ->
let msg = Printexc.to_string exc in
Printf.eprintf "There was an error: %s\n" msg
diff --git a/doc/developer/tutorial/viewcfg/src/gui.ml b/doc/developer/tutorial/viewcfg/src/gui.ml
index bbb2874292e86b5c87fa4fc71f4d300d304ebd64..81ba16c1478969486829ae4c6e9b6557c3233f2a 100644
--- a/doc/developer/tutorial/viewcfg/src/gui.ml
+++ b/doc/developer/tutorial/viewcfg/src/gui.ml
@@ -8,7 +8,7 @@ let cfg_selector
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_vfile.ml b/doc/developer/tutorial/viewcfg/src/print_cfg_vfile.ml
index 737c6a63e44f3aae64ad564fa285c9df6a776699..387f3611c95b4a8c4ea00e612acf35d71c7fad27 100644
--- a/doc/developer/tutorial/viewcfg/src/print_cfg_vfile.ml
+++ b/doc/developer/tutorial/viewcfg/src/print_cfg_vfile.ml
@@ -1,3 +1,3 @@
- method! vfile _ =
- Format.fprintf out "@[<hov 2>digraph cfg {@ ";
- Cil.DoChildrenPost (fun f -> Format.fprintf out "}@]@."; f)
+method! vfile _ =
+ Format.fprintf out "@[<hov 2>digraph cfg {@ ";
+ Cil.DoChildrenPost (fun f -> Format.fprintf out "}@]@."; f)
diff --git a/doc/developer/tutorial/viewcfg/src/print_cfg_vglob.ml b/doc/developer/tutorial/viewcfg/src/print_cfg_vglob.ml
index 8be1a7120afce6efd934c41b57c03402c7c0917c..999f7c3de637f6e6e5e9c3925a499f9b9bc4627a 100644
--- a/doc/developer/tutorial/viewcfg/src/print_cfg_vglob.ml
+++ b/doc/developer/tutorial/viewcfg/src/print_cfg_vglob.ml
@@ -1,9 +1,9 @@
- method! vglob_aux g =
- match g with
- | GFun(f,_) ->
- Format.fprintf out "@[<hov 2>subgraph cluster_%a {@ \
- @[<hv 2>graph@ [label=\"%a\"];@]@ "
- Printer.pp_varinfo f.svar
- Printer.pp_varinfo f.svar;
- Cil.DoChildrenPost(fun g -> Format.fprintf out "}@]@ "; g)
- | _ -> Cil.SkipChildren
+method! vglob_aux g =
+ match g with
+ | GFun(f,_) ->
+ Format.fprintf out "@[<hov 2>subgraph cluster_%a {@ \
+ @[<hv 2>graph@ [label=\"%a\"];@]@ "
+ Printer.pp_varinfo f.svar
+ Printer.pp_varinfo f.svar;
+ Cil.DoChildrenPost(fun g -> Format.fprintf out "}@]@ "; g)
+ | _ -> Cil.SkipChildren
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..cadcb03391ba237bfd4c50975d38b1628f41fc29 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,8 +1,8 @@
- 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
- (fun succ -> Format.fprintf out "@[s%d -> s%d;@]@ " s.sid succ.sid)
- s.succs;
- Format.fprintf out "@]";
- Cil.DoChildren
+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
+ (fun succ -> Format.fprintf out "@[s%d -> s%d;@]@ " s.sid succ.sid)
+ s.succs;
+ Format.fprintf out "@]";
+ Cil.DoChildren
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..585fc9e6948fc475ab5c01d8ecab685acdb8b607 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 =
- 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 ""
- in
- Format.fprintf out "@[s%d@ [label=%S %s]@];@ "
- s.sid (Pretty_utils.to_string print_stmt s.skind) color;
- List.iter
- (fun succ -> Format.fprintf out "@[s%d -> s%d;@]@ " s.sid succ.sid)
- s.succs;
- Cil.DoChildren
+method! vstmt_aux s =
+ 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 ""
+ in
+ Format.fprintf out "@[s%d@ [label=%S %s]@];@ "
+ s.sid (Pretty_utils.to_string print_stmt s.skind) color;
+ 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/register_and_options.ml b/doc/developer/tutorial/viewcfg/src/register_and_options.ml
index 37a9e8b8335edcea3ca0ffd28b3f3fe6fb4b69b7..ee7a8678bd823d7f93b84fd76bea7458204b2d23 100644
--- a/doc/developer/tutorial/viewcfg/src/register_and_options.ml
+++ b/doc/developer/tutorial/viewcfg/src/register_and_options.ml
@@ -1,18 +1,18 @@
module Self = Plugin.Register(struct
- let name = "control flow graph"
- let shortname = "viewcfg"
- let help = "control flow graph computation and display"
-end)
+ let name = "control flow graph"
+ let shortname = "viewcfg"
+ let help = "control flow graph computation and display"
+ end)
module Enabled = Self.False(struct
- let option_name = "-cfg"
- let help =
- "when on (off by default), computes the CFG of all functions."
-end)
+ let option_name = "-cfg"
+ let help =
+ "when on (off by default), computes the CFG of all functions."
+ end)
module OutputFile = Self.String(struct
- let option_name = "-cfg-output"
- let default = "cfg.dot"
- let arg_name = "output-file"
- let help = "file where the graph is output, in dot format."
-end)
+ let option_name = "-cfg-output"
+ let default = "cfg.dot"
+ let arg_name = "output-file"
+ let help = "file where the graph is output, in dot format."
+ end)
diff --git a/doc/developer/tutorial/viewcfg/src/register_cfg_graph_state.ml b/doc/developer/tutorial/viewcfg/src/register_cfg_graph_state.ml
index 474ed1f2a4407a71179cdc6b7d42136b14cd04d0..93fa563539a71ddf353a23de59c08d7d300585c4 100644
--- a/doc/developer/tutorial/viewcfg/src/register_cfg_graph_state.ml
+++ b/doc/developer/tutorial/viewcfg/src/register_cfg_graph_state.ml
@@ -1,8 +1,8 @@
module Cfg_graph_state = State_builder.Hashtbl
- (Cil_datatype.Fundec.Hashtbl)
- (Datatype.String)
- (struct
- let name = "Data_for_cfg.Cfg_graph_state"
- let dependencies = [ Ast.self; Db.Value.self ]
- let size = 17
- end);;
+ (Cil_datatype.Fundec.Hashtbl)
+ (Datatype.String)
+ (struct
+ let name = "Data_for_cfg.Cfg_graph_state"
+ let dependencies = [ Ast.self; Db.Value.self ]
+ let size = 17
+ end);;
diff --git a/doc/developer/tutorial/viewcfg/src/register_value_computed_state.ml b/doc/developer/tutorial/viewcfg/src/register_value_computed_state.ml
index 8457e84fbde20d578cda2bdd0807d7c7005a07d5..504a670f491736d6178767ba89994f8a4902a669 100644
--- a/doc/developer/tutorial/viewcfg/src/register_value_computed_state.ml
+++ b/doc/developer/tutorial/viewcfg/src/register_value_computed_state.ml
@@ -1,7 +1,7 @@
module Value_is_computed = State_builder.Ref
- (Datatype.Bool)
- (struct
- let name = "Data_for_cfg.Value_computed"
- let dependencies = []
- let default () = false
- end);;
+ (Datatype.Bool)
+ (struct
+ let name = "Data_for_cfg.Value_computed"
+ let dependencies = []
+ let default () = false
+ end);;
diff --git a/doc/scope/M.v b/doc/scope/M.v
index f9758e8a131b33ca06f9d75c757a8a3a0da352d3..f57ee83e7a37cf88dfeffbd9e2a7b290900979a4 100644
--- a/doc/scope/M.v
+++ b/doc/scope/M.v
@@ -175,7 +175,7 @@ Parameter ma : inst -> inst -> mark.
Axiom maStart : forall L I, ma L I = Start -> L = I.
Axiom maL : forall L, ma L L = Start.
-(** propriété du marquage après stabilité *)
+(** propriété du marquage après stabilité *)
Axiom Pma : forall L i',
ma L i' = lmerge (List.map (fun i => trans i (ma L i)) (pred i')).
diff --git a/doc/scope/Makefile b/doc/scope/Makefile
index ac55e30f1991ffdb38612fdfcb1ee248d6e01ce8..5f47605deb544a3fe1371695312c2207b21d11f3 100644
--- a/doc/scope/Makefile
+++ b/doc/scope/Makefile
@@ -20,7 +20,7 @@
# #
##########################################################################
-#vide : pour ne pas utiliser de règles implicites
+#vide : pour ne pas utiliser de règles implicites
.SUFFIXE:
.PHONY: clean all debug
diff --git a/doc/slicing/algo.ml b/doc/slicing/algo.ml
index 35755d65866f27523d34355ed7ebcfb7cb07225a..86e953be8da1aab27617211512fd5aa389aa4c04 100644
--- a/doc/slicing/algo.ml
+++ b/doc/slicing/algo.ml
@@ -6,12 +6,12 @@ module H = AlgoH ;;
let rec mark_rec_pdg_elem pdg stmt_elems m e ff =
let new_ff = add_elem_mark pdg stmt_elems m e ff in
let dpds = H.get_dpds e pdg in
- List.fold_right (mark_rec_pdg_elem pdg stmt_elems m) dpds new_ff
- (* ;; *)
+ List.fold_right (mark_rec_pdg_elem pdg stmt_elems m) dpds new_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] 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 =
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
@@ -19,4 +19,4 @@ and
let elems = H.get_elems stmt stmt_elems in
let (_, other_elems) = List.partition (fun elem -> elem = e) elems in
let mark_spare_elem e ff = mark_rec_pdg_elem pdg stmt_elems H.spare_mark e ff in
- List.fold_right mark_spare_elem other_elems new_ff
+ List.fold_right mark_spare_elem other_elems new_ff
diff --git a/doc/training/developer/sources/basic_script.ml b/doc/training/developer/sources/basic_script.ml
index fd83c661bb190de5faf19f44fb978f59641aa548..e3f7ddfe0de26c896b153c05e2bace0034b8a690 100644
--- a/doc/training/developer/sources/basic_script.ml
+++ b/doc/training/developer/sources/basic_script.ml
@@ -27,10 +27,10 @@ let all_entry_points () =
(*## Find entry points *)
Globals.Functions.iter
(fun kf ->
- if Kernel_function.is_definition kf &&
- (Kernel_function.find_syntactic_callsites kf = [])
- then
- run (Kernel_function.get_name kf) ());
+ if Kernel_function.is_definition kf &&
+ (Kernel_function.find_syntactic_callsites kf = [])
+ then
+ run (Kernel_function.get_name kf) ());
Kernel.feedback "Analyzed %d potential entry points" !nb_entry_points
(*# Basic script *)
diff --git a/doc/training/developer/sources/const_violation.ml b/doc/training/developer/sources/const_violation.ml
index 2eadb5524debd6e35c3ca20913df90252636c07a..80a4484e8d71d165a1dc4910c8880ee26410e443 100644
--- a/doc/training/developer/sources/const_violation.ml
+++ b/doc/training/developer/sources/const_violation.ml
@@ -14,8 +14,8 @@ let run () =
let end_val = Cvalue.V.project_ival end_binding in
if Ival.is_singleton_int init_val && Ival.is_singleton_int end_val then begin
if not
- (Abstract_interp.Int.equal
- (Ival.project_int init_val) (Ival.project_int end_val))
+ (Abstract_interp.Int.equal
+ (Ival.project_int init_val) (Ival.project_int end_val))
then
Kernel.error "Glob has been assigned"
end else begin
diff --git a/doc/training/developer/sources/object.ml b/doc/training/developer/sources/object.ml
index 07c71a188c084b42ce23a9b8fd9677431d15d60c..4138e6f892940e808439b6ab2009233ccdf54632 100644
--- a/doc/training/developer/sources/object.ml
+++ b/doc/training/developer/sources/object.ml
@@ -1,26 +1,26 @@
class a =
let x = 1 in
-object(self)
- method get_x_a = x
- val y = 2
- method get_y_a = y
- val z = 3
- method private t = 4
- method get_t_a = self#t
-end
+ object(self)
+ method get_x_a = x
+ val y = 2
+ method get_y_a = y
+ val z = 3
+ method private t = 4
+ method get_t_a = self#t
+ end
class b =
-object(self)
- inherit a as super
- (* method get_x_b = x (* ill-typed: no x in env *) *)
- val y = 4
- method get_y_b = y
- method get_z_b = z
- method t = 5
- method get_t_b = super#t
-end
+ object(self)
+ inherit a as super
+ (* method get_x_b = x (* ill-typed: no x in env *) *)
+ val y = 4
+ method get_y_b = y
+ method get_z_b = z
+ method t = 5
+ method get_t_b = super#t
+ end
let bobj = new b;;
Printf.printf "get_x_a:%d\nget_y_a:%d\nget_y_b:%d\nget_z_b:%d\nget_t_a:%d\nget_t_b:%d\n" bobj#get_x_a bobj#get_y_a bobj#get_y_b bobj#get_z_b bobj#get_t_a
-bobj#get_t_b
+ bobj#get_t_b
diff --git a/src/plugins/e-acsl/examples/ensuresec/.gitignore b/src/plugins/e-acsl/examples/ensuresec/.gitignore
index 624a0d90452b7edfc6a43b3a7409e123d5dd0ac3..48f917578b41ed6b873e778abb6c5869fd01af2f 100644
--- a/src/plugins/e-acsl/examples/ensuresec/.gitignore
+++ b/src/plugins/e-acsl/examples/ensuresec/.gitignore
@@ -1,3 +1,3 @@
build/
__pycache__/
-.env
\ No newline at end of file
+.env
diff --git a/src/plugins/instantiate/README.md b/src/plugins/instantiate/README.md
index bf55ae2cf31a74fe80eb1d587adaa83803c8a03e..f54df561537931255c333ad87e782322275b535c 100644
--- a/src/plugins/instantiate/README.md
+++ b/src/plugins/instantiate/README.md
@@ -127,4 +127,4 @@ let () = Transform.register (module struct
end)
```
-The role and types of each function is documented in `Instantiator_builder.mli`.
\ No newline at end of file
+The role and types of each function is documented in `Instantiator_builder.mli`.
diff --git a/src/plugins/server/tests/batch/wrong.json b/src/plugins/server/tests/batch/wrong.json
index 0178e8af2950cbc6b6a49d98367265e2bf993989..3c5f5262d12e7719a49df8d8fca4607f8db4b1b0 100644
--- a/src/plugins/server/tests/batch/wrong.json
+++ b/src/plugins/server/tests/batch/wrong.json
@@ -1,4 +1,4 @@
[
{ id:"unknown request", request:"kernel.unknown", data:null, comment:"the request doesn't exist" },
{ id:"wrong data", request:"kernel.ast.printFunction", data:{f1:1, f2:{x:1, y:2}, f3:null}, comment:"ident is expected, object is given" }
-]
\ No newline at end of file
+]
diff --git a/src/plugins/value/legacy/TOREMOVE b/src/plugins/value/legacy/TOREMOVE
index ffa44b40808f3595a318a93d84a20e6dd73f20ad..a45847d25ad5d534973f2563e1c31130ecacab8f 100644
--- a/src/plugins/value/legacy/TOREMOVE
+++ b/src/plugins/value/legacy/TOREMOVE
@@ -8,4 +8,4 @@
To be moved elsewhere, probably in domains/cvalue or in engine:
- eval_annots, eval_terms
\ No newline at end of file
+ eval_annots, eval_terms