Merge branch 'feature/patrick/lint-some-files' into 'master'

lint some files

See merge request frama-c/frama-c!3809

.git-blame-ignore-revs

@@ -34,3 +34,5 @@ a767fdcb7adda81a5ef192733ef7c62fd56b30e2
 6cc1a6f2036b75c6b2451518ffbfbe025eb1a1f8
 aef808e15e4dcc02dcee7004add8530083d33474
 220072cecdcc0b0b8292c40d93e793b3219b506f
+6ead6d862f1960e6baca64d335b811c954cf8430
+7955ef2039b2010cc30b88da7a47d4f07e298042

.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>

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);

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
 

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

doc/acsl_tutorial_slides/1max.sh

 #!/bin/sh
-emacs 1max.c
\ No newline at end of file
+emacs 1max.c

doc/acsl_tutorial_slides/script

-* 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.

doc/aorai/.gitignore

-/transf
\ No newline at end of file
+/transf

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))))))

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 ->

doc/developer/tutorial/hello/src/run_log.ml

 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

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">modlisation 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>

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
 

doc/training/developer/beamerfontthemeframa-c.sty

-\setbeamerfont{section in head}{size=\scriptsize}
\ No newline at end of file
+\setbeamerfont{section in head}{size=\scriptsize}

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:

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:

doc/value/README

 
-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.

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
+}

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
+}

doc/value/tutorial/README

-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