diff --git a/.git-blame-ignore-revs b/.git-blame-ignore-revs
index b860e46d138a48d687d1fe164a54c20ef200f740..eb5ae4704b269753011df720e74d521d6a0b352d 100644
--- a/.git-blame-ignore-revs
+++ b/.git-blame-ignore-revs
@@ -34,3 +34,5 @@ a767fdcb7adda81a5ef192733ef7c62fd56b30e2
6cc1a6f2036b75c6b2451518ffbfbe025eb1a1f8
aef808e15e4dcc02dcee7004add8530083d33474
220072cecdcc0b0b8292c40d93e793b3219b506f
+6ead6d862f1960e6baca64d335b811c954cf8430
+7955ef2039b2010cc30b88da7a47d4f07e298042
diff --git a/.mailmap b/.mailmap
index 5f500d8a33dca5d2728508c275e2c98f58b78199..799ba7668ebfc76496349755a0252e891cc32269 100644
--- a/.mailmap
+++ b/.mailmap
@@ -13,4 +13,4 @@ Muriel Roger <muriel.roger@cea.fr>
<loic.correnson@cea.fr> <lcorrenson@gmail.com>
<loic.correnson@cea.fr> <loïc.correnson@cea.fr>
Géraud Canet <geraud.canet@cea.fr>
-<mounir.assaf@cea.fr> <mounir.assaf@cea.Fr>
\ No newline at end of file
+<mounir.assaf@cea.fr> <mounir.assaf@cea.Fr>
diff --git a/devel_tools/size.ml b/devel_tools/size.ml
index bd24feec4f33c718189a759be496d3abe39047f6..116006f2bb7c8b8c84a70987bfadb898573c2cd1 100644
--- a/devel_tools/size.ml
+++ b/devel_tools/size.ml
@@ -53,19 +53,19 @@ let rec traverse t =
let n = size t in
let tag = tag t in
if tag < no_scan_tag then begin
- count := !count + 1 + n;
- for i = 0 to n - 1 do
- let f = field t i in
- if is_block f then traverse f
- done
+ count := !count + 1 + n;
+ for i = 0 to n - 1 do
+ let f = field t i in
+ if is_block f then traverse f
+ done
end else if tag = string_tag then
- count := !count + 1 + n
+ count := !count + 1 + n
else if tag = double_tag then
- count := !count + size_of_double
+ count := !count + size_of_double
else if tag = double_array_tag then
- count := !count + 1 + size_of_double * n
+ count := !count + 1 + size_of_double * n
else
- incr count
+ incr count
end
end
@@ -80,8 +80,8 @@ let res () =
let size_w ?except o =
reset_table ();
(match except with
- | None -> ()
- | Some except -> traverse (repr except)
+ | None -> ()
+ | Some except -> traverse (repr except)
);
count := 0;
traverse (repr o);
diff --git a/devel_tools/size_states.ml b/devel_tools/size_states.ml
index 2cdec788b99c6ab76f53c26f12003c31c5e116ed..ad62726e2b8427127497eea54cc0526c00ae650b 100644
--- a/devel_tools/size_states.ml
+++ b/devel_tools/size_states.ml
@@ -57,19 +57,19 @@ let rec traverse t =
let n = size t in
let tag = tag t in
if tag < no_scan_tag then begin
- count := !count + 1 + n;
- for i = 0 to n - 1 do
- let f = field t i in
- if is_block f then traverse f
- done
+ count := !count + 1 + n;
+ for i = 0 to n - 1 do
+ let f = field t i in
+ if is_block f then traverse f
+ done
end else if tag = string_tag then
- count := !count + 1 + n
+ count := !count + 1 + n
else if tag = double_tag then
- count := !count + size_of_double
+ count := !count + size_of_double
else if tag = double_array_tag then
- count := !count + 1 + size_of_double * n
+ count := !count + 1 + size_of_double * n
else
- incr count
+ incr count
end
end
diff --git a/doc/CHANGES.obfuscator b/doc/CHANGES.obfuscator
index 6e2057626df2d41ffd666604db0844ca9caf6a6d..70a697bdac5588ce3d20e108167ffe07b3ea0559 100644
--- a/doc/CHANGES.obfuscator
+++ b/doc/CHANGES.obfuscator
@@ -5,4 +5,4 @@ V3
V2
New dictionary output using #define
V1
- Initial release
\ No newline at end of file
+ Initial release
diff --git a/doc/acsl_tutorial_slides/1max.sh b/doc/acsl_tutorial_slides/1max.sh
index 82944e95f97a00bad8ab70e6ad8b19d772197666..99851981e56ffa61b5b0200a90d99c23b9dc2a82 100755
--- a/doc/acsl_tutorial_slides/1max.sh
+++ b/doc/acsl_tutorial_slides/1max.sh
@@ -1,2 +1,2 @@
#!/bin/sh
-emacs 1max.c
\ No newline at end of file
+emacs 1max.c
diff --git a/doc/acsl_tutorial_slides/script b/doc/acsl_tutorial_slides/script
index 9ae7ac14fc9a221bdd569e7ab72818de6fcb03ee..cdc4a4df21dc4e088a7a06f8887812c150d8d51d 100644
--- a/doc/acsl_tutorial_slides/script
+++ b/doc/acsl_tutorial_slides/script
@@ -1,18 +1,18 @@
-* Faire un slide 0 avec le nom de celui qui présente et
+* Faire un slide 0 avec le nom de celui qui présente et
l'URL pour Frama-C. Faire le discours sur ACSL qui est la
-glue faisant marcher plusieurs plug-ins complémentaires.
+glue faisant marcher plusieurs plug-ins complémentaires.
* slide 1max.c
-montrer que l'on peut déjà vérifier la syntaxe des annotation
+montrer que l'on peut déjà vérifier la syntaxe des annotation
en introduisant une erreur de syntaxe et en compilant depuis Emacs.
Localiser l'erreur avec Emacs.
-Alors que l'idée des prés et posts est de prouver que la post tient
-en n'utilisant que le code de la fonction en supposant que la pré
-était satisfaite en entrée, la deuxième page montre l'utilisation
-de l'analyse de valeurs pour vérifier ces propriétés avec une
-exécution symbolique.
+Alors que l'idée des prés et posts est de prouver que la post tient
+en n'utilisant que le code de la fonction en supposant que la pré
+était satisfaite en entrée, la deuxième page montre l'utilisation
+de l'analyse de valeurs pour vérifier ces propriétés avec une
+exécution symbolique.
* slide 2maxp.c
@@ -23,29 +23,29 @@ C'est pour montrer que ACSL supporte les pointeurs.
Avertissements sur le fait que le langage logique est
un langage pur.
Le && est commutatif. Parler de (*p) n'a pas de sens en
-général mais des propriétés telles que *p==*p sont
-vraies même si p n'est pas valide. Mieux vaut
-toujours écrire "\valid(p) && *p == ..."
+général mais des propriétés telles que *p==*p sont
+vraies même si p n'est pas valide. Mieux vaut
+toujours écrire "\valid(p) && *p == ..."
* slide 4comp_part.c
-Attirer l'attention sur ce que c'est une spécification
-complète. Insister sur le fait que c'est très difficile
-d'en écrire en pratique (formelles ou non formelles) mais
-que les spécifications partielles sont utiles aussi
+Attirer l'attention sur ce que c'est une spécification
+complète. Insister sur le fait que c'est très difficile
+d'en écrire en pratique (formelles ou non formelles) mais
+que les spécifications partielles sont utiles aussi
(et qu'on peut se servir d'ACSL pour en faire).
* slide 5assigns_term.c
-A propos de spécifications complètes, c'est le bon moment
+A propos de spécifications complètes, c'est le bon moment
pour parler des assigns et de la terminaison.
* slide 6pred.c
-Les spécifications peuvent devenir plus élaborée en
-commençant par définir des prédicats utilisateurs.
-Ici, défini comme une fonction
+Les spécifications peuvent devenir plus élaborée en
+commençant par définir des prédicats utilisateurs.
+Ici, défini comme une fonction
* slide 7pred.c
-Définition dans le style prolog du même prédicat.
+Définition dans le style prolog du même prédicat.
diff --git a/doc/aorai/.gitignore b/doc/aorai/.gitignore
index 7af91cd419db82b54ead3e68b22a67a87ef72b18..0682bf3d785b90f19aeba9598ca8f66b38edfa39 100644
--- a/doc/aorai/.gitignore
+++ b/doc/aorai/.gitignore
@@ -1 +1 @@
-/transf
\ No newline at end of file
+/transf
diff --git a/doc/aorai/example/example.ltl b/doc/aorai/example/example.ltl
index 0c0910e3e9073e1e1e8f42dcbdb85194b05429ea..6df141a147552c23c9cb3e2e219ec04c2a0d6169 100644
--- a/doc/aorai/example/example.ltl
+++ b/doc/aorai/example/example.ltl
@@ -3,4 +3,4 @@ CALL(main)
&& _X_ (!RETURN(opb)
&& _X_ (!CALL(opa)
&& _X_ (RETURN(opb)
- && _X_ (RETURN(main))))))
\ No newline at end of file
+ && _X_ (RETURN(main))))))
diff --git a/doc/developer/check_api/check_code.ml b/doc/developer/check_api/check_code.ml
index 2fcb3fc4aa525d9e60d043b5843cc4a0eacf66fe..9592cbf22bc5f79165742745640a8fcc0e70a69e 100644
--- a/doc/developer/check_api/check_code.ml
+++ b/doc/developer/check_api/check_code.ml
@@ -87,7 +87,7 @@ module Generator (G : Odoc_html.Html_generator) = struct
self#html_of_custom b info.Odoc_info.i_custom
(** Print html code for the first sentence of a description.
- The titles and lists in this first sentence has been removed.*)
+ The titles and lists in this first sentence has been removed.*)
method html_of_info_first_sentence b = function
| None -> ()
| Some info ->
diff --git a/doc/developer/tutorial/hello/src/run_log.ml b/doc/developer/tutorial/hello/src/run_log.ml
index fb5256b08281abe6a33ab76a423977ba7022c7e3..b76d5462a2c3d9ddab64a803a68410ec7c9c688c 100644
--- a/doc/developer/tutorial/hello/src/run_log.ml
+++ b/doc/developer/tutorial/hello/src/run_log.ml
@@ -1,7 +1,7 @@
let run () =
Self.result "Hello, world!";
- let product =
- Self.feedback ~level:2 "Computing the product of 11 and 5...";
+ let product =
+ Self.feedback ~level:2 "Computing the product of 11 and 5...";
11 * 5
in
Self.result "11 * 5 = %d" product
diff --git a/doc/index.html b/doc/index.html
index 961f99ad1f9635f02b6a19a1fc852f072d334592..67520447c419c95d4faca4fc20d469b793d83318 100644
--- a/doc/index.html
+++ b/doc/index.html
@@ -4,7 +4,7 @@ PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
<html>
<head>
-<meta http-equiv="Content-Type" content="text/xhtml; charset=ISO-8859-1"/>
+<meta http-equiv="Content-Type" content="text/xhtml; charset=utf-8"/>
<link rel="stylesheet" href="style.css" type="text/css"/>
<title>Frama-C</title>
</head>
@@ -125,7 +125,7 @@ PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
(<a href="wp/Spec/index.html">spec</a> : <tt>cd wp/Spec; make</tt>)
(<a href="wp/Notes/index.html">informal notes</a> : <tt>cd wp/Notes; make</tt>)
(<a href="wp/Implem/index.html">implementation</a> : <tt>cd wp/Implem; make</tt>)
- (<a href="wp/Coq/doc/toc.html">modélisation COQ</a>)
+ (<a href="wp/Coq/doc/toc.html">modélisation COQ</a>)
(<a href="code/wp/metrics.html">metrics</a> : <tt>make Wp_metrics)</tt>)
</li><li>
<a href="code/cxx_elsa/index.html">cxx</a>
diff --git a/doc/slicing/algoH.mli b/doc/slicing/algoH.mli
index a514d3fedd1df4b77162a9b5d10ae67d66f29c14..fc75ef1b7cc04ea2b5a51ffbd21abd9579cb302f 100644
--- a/doc/slicing/algoH.mli
+++ b/doc/slicing/algoH.mli
@@ -38,7 +38,7 @@ val get_stmts : t_elem list -> t_stmt_elems -> t_stmt list ;;
(* retrouver les éléments correspondant à une instruction *)
val get_elems : t_stmt -> t_stmt_elems -> t_elem list ;;
-type t_state
+type t_state
type t_data
diff --git a/doc/training/developer/beamerfontthemeframa-c.sty b/doc/training/developer/beamerfontthemeframa-c.sty
index 214ff73b722ae526ad38259bf1e9a6ddc3e778f7..8769c1f3904f82b25f85815a62f72a3783db1dfc 100644
--- a/doc/training/developer/beamerfontthemeframa-c.sty
+++ b/doc/training/developer/beamerfontthemeframa-c.sty
@@ -1 +1 @@
-\setbeamerfont{section in head}{size=\scriptsize}
\ No newline at end of file
+\setbeamerfont{section in head}{size=\scriptsize}
diff --git a/doc/training/developer/kernel.tex b/doc/training/developer/kernel.tex
index 65ebfbe2bbafc2a22b47c8f6f43d97db60e19844..3f0fa7ef7acd6dd5a9ddd7f24b065b6f789212f2 100644
--- a/doc/training/developer/kernel.tex
+++ b/doc/training/developer/kernel.tex
@@ -26,4 +26,4 @@
% Local Variables:
% ispell-local-dictionary: "english"
% TeX-master: "slides.tex"
-% End:
\ No newline at end of file
+% End:
diff --git a/doc/training/developer/script.tex b/doc/training/developer/script.tex
index acf0e67fbe5fd95c654aae543762c4c8a74b0261..16362b096a35c0a40012592044a022f5fd71eb2a 100644
--- a/doc/training/developer/script.tex
+++ b/doc/training/developer/script.tex
@@ -89,4 +89,4 @@
% Local Variables:
% TeX-master: "slides.tex"
% ispell-local-dictionary: "english"
-% End:
\ No newline at end of file
+% End:
diff --git a/doc/value/README b/doc/value/README
index 8e8ce00b65d7748875ee88c28cb23996f5418b26..cf8e721bb34ecc977620a5554f410251bfe47912 100644
--- a/doc/value/README
+++ b/doc/value/README
@@ -1,13 +1,13 @@
-Si vous n'êtes pas un développeur de Value, vous avez
-reçu ce document par erreur, et vous pouvez l'ignorer.
+Si vous n'êtes pas un développeur de Value, vous avez
+reçu ce document par erreur, et vous pouvez l'ignorer.
Conventions s'appliquant dans la documentation de Value :
* Le "plug-in d'analyse de valeur" s'appelle "the value analysis plug-in",
"the plug-in", "the value analysis" ou "the analysis".
- Les deux derniers sont à utiliser quand le sujet de l'action
- peut être une analyse particulière d'un code particulier.
+ Les deux derniers sont à utiliser quand le sujet de l'action
+ peut être une analyse particulière d'un code particulier.
Utiliser "Frama-C" si et seulement si Frama-C est
l'interface visible pour l'action dont il est question, par exemple :
@@ -20,19 +20,19 @@ synthetic information on the behavior of analyzed functions:
inputs, outputs, and alarms.
* La personne qui utilise Value s'appelle "l'utilisateur" ;
-la personne qui a écrit l'application s'appelle "programmeur",
+la personne qui a écrit l'application s'appelle "programmeur",
mais on n'a pas souvent de raison de parler d'elle.
-* Sauf cas particulier, si un exemple contient le point d'entrée,
-alors ce point d'entrée s'appelle \verb|main|. Un exemple peut
+* Sauf cas particulier, si un exemple contient le point d'entrée,
+alors ce point d'entrée s'appelle \verb|main|. Un exemple peut
aussi ne pas contenir de fonction \verb|main|, ce qui indique
qu'il ne s'agit que d'une partie d'un projet plus grand.
-* Le shell n'est pas csh. Le shell peut être bash, zsh, le prompt
-peut avoir été customisé par l'utilisateur, ou l'utilisateur peut
-être sous Windows et avoir un prompt de la forme "C:\>". Donc,
-on n'écrit pas de prompt précédant les commandes à taper au
-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
+* Le shell n'est pas csh. Le shell peut être bash, zsh, le prompt
+peut avoir été customisé par l'utilisateur, ou l'utilisateur peut
+être sous Windows et avoir un prompt de la forme "C:\>". Donc,
+on n'écrit pas de prompt précédant les commandes à taper au
+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.
diff --git a/doc/value/examples/parametrizing/loop-unroll-insuf.c b/doc/value/examples/parametrizing/loop-unroll-insuf.c
index f977bfe31f574efdb9f5a13ca0b3b2f9f14f06c2..a16c8b457d692c3baf50469a92c477bd3bc8be3d 100644
--- a/doc/value/examples/parametrizing/loop-unroll-insuf.c
+++ b/doc/value/examples/parametrizing/loop-unroll-insuf.c
@@ -3,4 +3,4 @@ void main()
//@ loop unroll 20; // should be 21
for (int i = 0 ; i <= 20 ; i ++) {
}
-}
\ No newline at end of file
+}
diff --git a/doc/value/examples/parametrizing/pragma-widen-hints.c b/doc/value/examples/parametrizing/pragma-widen-hints.c
index af0263b686172e036af93205f2cfa9cacb2f31d7..1e829bf9757fb58a22d79318d5dbec16e7e3c4f3 100644
--- a/doc/value/examples/parametrizing/pragma-widen-hints.c
+++ b/doc/value/examples/parametrizing/pragma-widen-hints.c
@@ -6,4 +6,4 @@ void main(void)
/*@ loop pragma WIDEN_HINTS i, 12, 13; */
for (i=0; i<n; i++)
j = 4 * i + 7;
-}
\ No newline at end of file
+}
diff --git a/doc/value/tutorial/README b/doc/value/tutorial/README
index e9d633c09797c58605cf875de0627360cbc1c296..087e9349ecbf5f889b6a1c626d9e41c5eb0f787d 100644
--- a/doc/value/tutorial/README
+++ b/doc/value/tutorial/README
@@ -1 +1 @@
-Reference_implementation is extracted from http://www.schneier.com/code/skein.zip
\ No newline at end of file
+Reference_implementation is extracted from http://www.schneier.com/code/skein.zip
diff --git a/doc/value/watchpoints b/doc/value/watchpoints
index 5c3009130a66b061986e39bea29ccf12ad99a59d..6ea47f519d6390aca812faa20b9a5d9b7bd5486f 100644
--- a/doc/value/watchpoints
+++ b/doc/value/watchpoints
@@ -54,4 +54,4 @@ Frama_C_watch_cardinal() allows to set a maximum number of elements
associated to lvalue in the abstract memory state. This is useful
in order to watch variables that should remain precise during
the entire execution (e.g. should remain a singleton) but which can
-take different values at different points.
\ No newline at end of file
+take different values at different points.
diff --git a/headers/hdrck.ml b/headers/hdrck.ml
index 692c80226819e5a076d40b4f454249e4134b7ee1..14c04d2568bbc7eed18638f0ef670f64e5965b82 100755
--- a/headers/hdrck.ml
+++ b/headers/hdrck.ml
@@ -105,7 +105,7 @@ let has_no_warning_nor_error = ref true
let warn fmt =
pp_job_first_line ();
if !exit_on_warning then
- has_no_warning_nor_error := false ;
+ has_no_warning_nor_error := false ;
Format.printf "- [warning] ";
Format.printf fmt
@@ -164,7 +164,7 @@ let get_string_null (ic:in_channel) =
*
* Defaults to reading the file entirely since any integer will ever be greater
* or equal than [max_int].
- *)
+*)
let read_lines ?nlines:(nlines=max_int) get_line filename =
let lines = ref [] in
let ic = if filename = "--stdin" then stdin else open_in filename in
@@ -355,7 +355,7 @@ let get_header_files ?directories:(dirs=(get_header_dirs ())) () :
warn "%s: duplicated license name (same contents as file: %s)@." filepath previous_entry
else
error ~exit_value:7
- "%s: duplicated license name (contents differs to file: %s)@." filepath previous_entry
+ "%s: duplicated license name (contents differs to file: %s)@." filepath previous_entry
with Not_found -> ());
Hashtbl.add license_path_tbl license_name filepath;
)
@@ -408,7 +408,7 @@ let extract_header filename template_hdr =
* @param headers a license header -> template header file hashtable
* @requires all files in specs exist
* @requires all header specifications have a corresponding existing template
- *)
+*)
let check_spec_discrepancies
(specs: (string, string) Hashtbl.t)
(headers: (string, string) Hashtbl.t) : unit =
@@ -433,18 +433,18 @@ let check_spec_discrepancies
let hdr_file_spec = Hashtbl.find headers hdr_type in
(* Guaranteed to exists after check_declared_headers *)
if not (eq_header file hdr_file_spec) then begin
- discrepancies := (file, hdr_type) :: !discrepancies;
- incr n;
+ discrepancies := (file, hdr_type) :: !discrepancies;
+ incr n;
end;
end
- ) specs ;
+ ) specs ;
if !n > 0 then begin
error ~exit_value:4 "@[<v 2>%a%d / %d files with bad headers@]@."
(fun _ppf l ->
List.iter
(fun (file, hdr_type) ->
error_fmt "%s : header differs from spec %s@."
- file hdr_type
+ file hdr_type
) l) !discrepancies
!n
(Hashtbl.length specs) ;
@@ -473,8 +473,8 @@ let check_forbidden_headers (forbidden_headers:StringSet.t) header_specification
error_fmt "%s : forbidden header %s@."
file hdr_type
) l) !forbidden
- !n
- (StringSet.cardinal distributed_files);
+ !n
+ (StringSet.cardinal distributed_files);
job_done ()
end
@@ -543,7 +543,7 @@ let check files_ignored header_specifications distributed_files exceptions =
*
* @param header_specifications file -> license header name hashtable
* @requires: files and licenses appearing in [header_specifications] exists
- *)
+*)
let update_headers header_specifications =
let headers = get_header_files () in
check_declared_headers header_specifications headers;
@@ -640,7 +640,7 @@ let rec argspec = [
| "3-lines" -> spec_format := Line3
| "3-zeros" -> spec_format := Zero3
| s -> Format.printf "invalid spec format: %s@." s ; print_usage ()),
- "<format>\t \"2-fields-by-line\"|\"3-fields-by-line\"|\"3-lines\"|\"3-zeros\"";
+ "<format>\t \"2-fields-by-line\"|\"3-fields-by-line\"|\"3-lines\"|\"3-zeros\"";
"-z", Arg.Set zero_stdin,
" force to use the spec format \"3-zeros\" when reading from stdin";
]
@@ -693,6 +693,6 @@ let _ =
if !exit_on_warning && not !has_no_warning_nor_error then
exit 8 ;
-(* Local Variables: *)
-(* compile-command: "ocamlc -o hdrck unix.cma str.cma hdrck.ml" *)
-(* End: *)
+ (* Local Variables: *)
+ (* compile-command: "ocamlc -o hdrck unix.cma str.cma hdrck.ml" *)
+ (* End: *)
diff --git a/ivette/src/frama-c/api_generator.ml b/ivette/src/frama-c/api_generator.ml
index b72055204a8002d9e3778a336fd422f14d2f6e69..5e29fab1eb556a5c6925f9f7eaafc9369d33c2bd 100644
--- a/ivette/src/frama-c/api_generator.ml
+++ b/ivette/src/frama-c/api_generator.ml
@@ -25,11 +25,11 @@
(* -------------------------------------------------------------------------- *)
module Self = Plugin.Register
- (struct
- let name = "Server TypeScript API"
- let shortname = "server-tsc"
- let help = "Generate TypeScript API for Server"
- end)
+ (struct
+ let name = "Server TypeScript API"
+ let shortname = "server-tsc"
+ let help = "Generate TypeScript API for Server"
+ end)
module TSC = Self.Action
(struct
@@ -353,7 +353,7 @@ let makeDeclaration fmt names d =
(Pretty_utils.pp_list
~empty:"[]" ~pre:"@[<hov 2>[ " ~sep:",@ " ~suf:"@ ]@]"
(fun fmt s -> Format.fprintf fmt "{ name: '%s' }" s))
- rq.rq_signals;
+ rq.rq_signals;
Format.fprintf fmt "};@\n" ;
makeDescr fmt d.d_descr ;
Format.fprintf fmt
diff --git a/src/plugins/aorai/.gitignore b/src/plugins/aorai/.gitignore
index 6e2440c7d5053e68723ce0ec0a462d751551dda1..1b77fb8deb8db509c14ac4bd15afc70dca627d69 100644
--- a/src/plugins/aorai/.gitignore
+++ b/src/plugins/aorai/.gitignore
@@ -18,4 +18,4 @@
/tests/*/result
/tests/test_config_prove
/tests/*/result_prove
-/top
\ No newline at end of file
+/top
diff --git a/src/plugins/instantiate/tests/plugin/needs_global.ml b/src/plugins/instantiate/tests/plugin/needs_global.ml
index 506da455fdb5b23a60a0d994dc2fcfb0e268c021..652b66a9cdeb303453c7b32774f0be742820ef6c 100644
--- a/src/plugins/instantiate/tests/plugin/needs_global.ml
+++ b/src/plugins/instantiate/tests/plugin/needs_global.ml
@@ -39,14 +39,14 @@ let generate_spec needed _ _ _ =
Cil_types.Writes [ Logic_const.new_identified_term t, From [] ]
in {
spec_behavior = [ {
- b_name = Cil.default_behavior_name ;
- b_requires = [] ;
- b_assumes = [] ;
- b_post_cond = [] ;
- b_assigns = assigns ;
- b_allocation = FreeAllocAny ;
- b_extended = []
- } ] ;
+ b_name = Cil.default_behavior_name ;
+ b_requires = [] ;
+ b_assumes = [] ;
+ b_post_cond = [] ;
+ b_assigns = assigns ;
+ b_allocation = FreeAllocAny ;
+ b_extended = []
+ } ] ;
spec_variant = None ;
spec_terminates = None ;
spec_complete_behaviors = [] ;
diff --git a/src/plugins/variadic/tests/declared/called_in_ghost.ml b/src/plugins/variadic/tests/declared/called_in_ghost.ml
index 5f7f6383d20b8aadc71520d60afb92e081300b74..4aa4ac68015e0d5c4aa32f616f850e0f41f3456a 100755
--- a/src/plugins/variadic/tests/declared/called_in_ghost.ml
+++ b/src/plugins/variadic/tests/declared/called_in_ghost.ml
@@ -6,15 +6,15 @@ class print =
method! vglob_aux g =
begin match g with
- | GFun(fd, _) ->
- Kernel.feedback "%a is%s ghost"
- Cil_datatype.Varinfo.pretty fd.svar
- (if fd.svar.vghost then "" else " not")
- | GFunDecl(_, vi, _) ->
- Kernel.feedback "%a is%s ghost"
- Cil_datatype.Varinfo.pretty vi
- (if vi.vghost then "" else " not")
- | _ -> ()
+ | GFun(fd, _) ->
+ Kernel.feedback "%a is%s ghost"
+ Cil_datatype.Varinfo.pretty fd.svar
+ (if fd.svar.vghost then "" else " not")
+ | GFunDecl(_, vi, _) ->
+ Kernel.feedback "%a is%s ghost"
+ Cil_datatype.Varinfo.pretty vi
+ (if vi.vghost then "" else " not")
+ | _ -> ()
end ;
Cil.DoChildren
diff --git a/src/plugins/wp/tests/wp/stmtcompiler_test_rela.ml b/src/plugins/wp/tests/wp/stmtcompiler_test_rela.ml
index 12849805c20ad3d7c7d73393dae7914bde04163e..1172d4ab1a585418b1629c950c86759a53aaa72b 100644
--- a/src/plugins/wp/tests/wp/stmtcompiler_test_rela.ml
+++ b/src/plugins/wp/tests/wp/stmtcompiler_test_rela.ml
@@ -70,15 +70,15 @@ let run () =
Property_status.iter (fun x ->
match Wpo.goals_of_property x with
| h :: _ ->
- inter_po := Wpo.{
- po_gid = "";
- po_sid = "";
- po_name = "";
- po_idx = Function(kf, None);
- po_model = model;
- po_pid = h.po_pid;
- po_formula = Wpo.GoalAnnot vc_annot;
- }
+ inter_po := Wpo.{
+ po_gid = "";
+ po_sid = "";
+ po_name = "";
+ po_idx = Function(kf, None);
+ po_model = model;
+ po_pid = h.po_pid;
+ po_formula = Wpo.GoalAnnot vc_annot;
+ }
| _ -> ()
);
spawn !inter_po;
diff --git a/src/plugins/wp/tests/wp_tip/TacNOP.ml b/src/plugins/wp/tests/wp_tip/TacNOP.ml
index a398efe3ac597d6d3b7dec5ff98f1d206c299f59..21faecfe4c3252cb9781aba7b120117c574129b1 100644
--- a/src/plugins/wp/tests/wp_tip/TacNOP.ml
+++ b/src/plugins/wp/tests/wp_tip/TacNOP.ml
@@ -19,9 +19,9 @@ class nop =
| Multi _
| Inside _
| Clause _ ->
- feedback#set_title "NOP" ;
- feedback#set_descr "Does nothing; just for testing." ;
- Applicable (fun s -> ["Nop", s])
+ feedback#set_title "NOP" ;
+ feedback#set_descr "Does nothing; just for testing." ;
+ Applicable (fun s -> ["Nop", s])
end
diff --git a/tests/syntax/copy_visitor_bts_1073_bis.ml b/tests/syntax/copy_visitor_bts_1073_bis.ml
index a7565bab3bef2d100eb43771ad5e758bbf2b48df..d26b1010abf5ca0abdc6ed8c1f089c43bc39291c 100644
--- a/tests/syntax/copy_visitor_bts_1073_bis.ml
+++ b/tests/syntax/copy_visitor_bts_1073_bis.ml
@@ -53,4 +53,3 @@ let main () =
let () = Db.Main.extend main
(*============================================================================*)
-