[Lexer] do some refactoring

src/kernel_internals/parsing/clexer.mll

@@ -53,6 +53,9 @@ module E = Errorloc
 
 let currentLoc () = E.currentLoc ()
 
+(* Convert char into Int64 *)
+let int64_of_char c = Int64.of_int (Char.code c)
+
 let one_line_ghost = ref false
 let is_oneline_ghost () = !one_line_ghost
 let enter_oneline_ghost () = one_line_ghost := true
@@ -68,274 +71,222 @@ let is_ghost_annot () = !ghost_annot
 let enter_ghost_annot () = ghost_annot := true
 let exit_ghost_annot () = ghost_annot := false
 
-let addComment c = Cabshelper.Comments.add (currentLoc()) c
-
-(* Some debugging support for line numbers *)
-let dbgToken (t: token) =
-  if false then begin
-    let dprintf fmt = Kernel.debug fmt in
-    (match t with
-         IDENT n -> dprintf "IDENT(%s)\n" n
-       | LBRACE l -> dprintf "LBRACE(%d)\n" (fst l).Filepath.pos_lnum
-       | RBRACE l -> dprintf "RBRACE(%d)\n" (fst l).Filepath.pos_lnum
-       | IF l -> dprintf "IF(%d)\n" (fst l).Filepath.pos_lnum
-       | SWITCH l -> dprintf "SWITCH(%d)\n" (fst l).Filepath.pos_lnum
-       | RETURN l -> dprintf "RETURN(%d)\n" (fst l).Filepath.pos_lnum
-       | _ -> ()) ;
-    t
-  end else
-    t
+let add_comment c = Cabshelper.Comments.add (currentLoc()) c
+
+
+
 
 (*
 ** Keyword hashtable
 *)
+
 let lexicon = H.create 211
-let init_lexicon _ =
+let add key builder = H.add lexicon key builder
+let remove key = H.remove lexicon key
+let is_c_keyword s = Hashtbl.mem lexicon s
+
+(* Search for a keyword, default to variable name, as opposed to type *)
+let scan_ident id =
+  let here = currentLoc () in
+  try (H.find lexicon id) here
+  with Not_found -> IDENT id
+
+let valid key builder =
+  add key builder
+
+let unsupported key =
+  let msg f k = Format.fprintf f "%s is currently unsupported by Frama-C." k in
+  add key (fun loc -> Kernel.abort ~source:(fst loc) "%a" msg key)
+
+let warning_C11 key builder =
+  let warning () = Kernel.(warning ~wkey:wkey_c11 "%s is a C11 keyword" key) in
+  add key (fun loc -> warning () ; builder loc)
+
+let thread_keyword () =
+  let wkey = Kernel.wkey_conditional_feature in
+  let s = "__thread is a GCC extension, use a GCC-based machdep to enable it" in
+  let warning () = Kernel.warning ~wkey "%s" s ; IDENT "__thread" in
+  add "__thread" (fun loc -> if Cil.gccMode () then THREAD loc else warning ())
+
+let filename_keyword () =
+  let convert acc c = int64_of_char c :: acc in
+  let path (loc : Cil_types.location) = (fst loc).pos_path in
+  let filename loc = Filepath.Normalized.to_pretty_string (path loc) in
+  let ints loc = List.rev (String.fold_left convert [] (filename loc)) in
+  add "__FC_FILENAME__" (fun loc -> CST_STRING (ints loc, loc))
+
+let init_lexicon () =
   H.clear lexicon ;
   Logic_env.reset_typenames () ;
   Logic_env.builtin_types_as_typenames () ;
-  List.iter
-    (fun (key, builder) -> H.add lexicon key builder)
-    [ ("auto", fun loc -> AUTO loc);
-      ("const", fun loc -> CONST loc);
-      ("__const", fun loc -> CONST loc);
-      ("__const__", fun loc -> CONST loc);
-      ("static", fun loc -> STATIC loc);
-      ("extern", fun loc -> EXTERN loc);
-      ("long", fun loc -> LONG loc);
-      ("short", fun loc -> SHORT loc);
-      ("register", fun loc -> REGISTER loc);
-      ("signed", fun loc -> SIGNED loc);
-      ("__signed", fun loc -> SIGNED loc);
-      ("unsigned", fun loc -> UNSIGNED loc);
-      ("volatile", fun loc -> VOLATILE loc);
-      ("__volatile", fun loc -> VOLATILE loc);
+  valid "auto" (fun loc -> AUTO loc) ;
+  valid "const" (fun loc -> CONST loc) ;
+  valid "__const" (fun loc -> CONST loc) ;
+  valid "__const__" (fun loc -> CONST loc) ;
+  valid "static" (fun loc -> STATIC loc) ;
+  valid "extern" (fun loc -> EXTERN loc) ;
+  valid "long" (fun loc -> LONG loc) ;
+  valid "short" (fun loc -> SHORT loc) ;
+  valid "register" (fun loc -> REGISTER loc) ;
+  valid "signed" (fun loc -> SIGNED loc) ;
+  valid "__signed" (fun loc -> SIGNED loc) ;
+  valid "unsigned" (fun loc -> UNSIGNED loc) ;
+  valid "volatile" (fun loc -> VOLATILE loc) ;
+  valid "__volatile" (fun loc -> VOLATILE loc) ;
   (* WW: see /usr/include/sys/cdefs.h for why __signed and __volatile
    * are accepted GCC-isms *)
-      ("char", fun loc -> CHAR loc);
-      ("_Bool", fun loc -> BOOL loc);
-      ("int", fun loc -> INT loc);
-      ("float", fun loc -> FLOAT loc);
-      ("double", fun loc -> DOUBLE loc);
-      ("void", fun loc -> VOID loc);
-      ("enum", fun loc -> ENUM loc);
-      ("struct", fun loc -> STRUCT loc);
-      ("typedef", fun loc -> TYPEDEF loc);
-      ("union", fun loc -> UNION loc);
-      ("break", fun loc -> BREAK loc);
-      ("continue", fun loc -> CONTINUE loc);
-      ("goto", fun loc -> GOTO loc);
-      ("return", fun loc -> dbgToken (RETURN loc));
-      ("switch", fun loc -> dbgToken (SWITCH loc));
-      ("case", fun loc -> CASE loc);
-      ("default", fun loc -> DEFAULT loc);
-      ("while", fun loc -> WHILE loc);
-      ("do", fun loc -> DO loc);
-      ("for", fun loc -> FOR loc);
-      ("if", fun loc -> dbgToken (IF loc));
-      ("else", fun _ -> ELSE);
+  valid "char" (fun loc -> CHAR loc) ;
+  valid "_Bool" (fun loc -> BOOL loc) ;
+  valid "int" (fun loc -> INT loc) ;
+  valid "float" (fun loc -> FLOAT loc) ;
+  valid "double" (fun loc -> DOUBLE loc) ;
+  valid "void" (fun loc -> VOID loc) ;
+  valid "enum" (fun loc -> ENUM loc) ;
+  valid "struct" (fun loc -> STRUCT loc) ;
+  valid "typedef" (fun loc -> TYPEDEF loc) ;
+  valid "union" (fun loc -> UNION loc) ;
+  valid "break" (fun loc -> BREAK loc) ;
+  valid "continue" (fun loc -> CONTINUE loc) ;
+  valid "goto" (fun loc -> GOTO loc) ;
+  valid "return" (fun loc -> RETURN loc) ;
+  valid "switch" (fun loc -> SWITCH loc) ;
+  valid "case" (fun loc -> CASE loc) ;
+  valid "default" (fun loc -> DEFAULT loc) ;
+  valid "while" (fun loc -> WHILE loc) ;
+  valid "do" (fun loc -> DO loc) ;
+  valid "for" (fun loc -> FOR loc) ;
+  valid "if" (fun loc -> IF loc) ;
+  valid "else" (fun _ -> ELSE) ;
   (*** Implementation specific keywords ***)
-      ("__signed__", fun loc -> SIGNED loc);
-      ("__inline__", fun loc -> INLINE loc);
-      ("inline", fun loc -> INLINE loc);
-      ("__inline", fun loc -> INLINE loc);
-      ("_Noreturn",
-       fun loc ->
-         Kernel.(warning ~wkey:wkey_c11 "_Noreturn is a C11 keyword");
-         NORETURN loc);
-      ("_Static_assert",
-       fun loc ->
-         Kernel.(warning ~wkey:wkey_c11 "_Static_assert is a C11 keyword");
-         STATIC_ASSERT loc);
-      ("__attribute__", fun loc -> ATTRIBUTE loc);
-      ("__attribute", fun loc -> ATTRIBUTE loc);
-      ("_Nullable", fun loc -> NOP_ATTRIBUTE loc);
-      ("__blockattribute__", fun _ -> BLOCKATTRIBUTE);
-      ("__blockattribute", fun _ -> BLOCKATTRIBUTE);
-      ("__asm__", fun loc -> ASM loc);
-      ("asm", fun loc -> ASM loc);
-      ("__typeof__", fun loc -> TYPEOF loc);
-      ("__typeof", fun loc -> TYPEOF loc);
-      ("typeof", fun loc -> TYPEOF loc);
-      ("__alignof", fun loc -> ALIGNOF loc);
-      ("__alignof__", fun loc -> ALIGNOF loc);
-      ("__volatile__", fun loc -> VOLATILE loc);
-      ("__volatile", fun loc -> VOLATILE loc);
-
-      ("__FUNCTION__", fun loc -> FUNCTION__ loc);
-      ("__func__", fun loc -> FUNCTION__ loc); (* ISO 6.4.2.2 *)
-      ("__PRETTY_FUNCTION__", fun loc -> PRETTY_FUNCTION__ loc);
-      ("__label__", fun _ -> LABEL__);
+  valid "__signed__" (fun loc -> SIGNED loc) ;
+  valid "__inline__" (fun loc -> INLINE loc) ;
+  valid "inline" (fun loc -> INLINE loc) ;
+  valid "__inline" (fun loc -> INLINE loc) ;
+  warning_C11 "_Noreturn" (fun loc -> NORETURN loc) ;
+  warning_C11 "_Static_assert" (fun loc -> STATIC_ASSERT loc) ;
+  valid "__attribute__" (fun loc -> ATTRIBUTE loc) ;
+  valid "__attribute" (fun loc -> ATTRIBUTE loc) ;
+  valid "_Nullable" (fun loc -> NOP_ATTRIBUTE loc) ;
+  valid "__blockattribute__" (fun _ -> BLOCKATTRIBUTE) ;
+  valid "__blockattribute" (fun _ -> BLOCKATTRIBUTE) ;
+  valid "__asm__" (fun loc -> ASM loc) ;
+  valid "asm" (fun loc -> ASM loc) ;
+  valid "__typeof__" (fun loc -> TYPEOF loc) ;
+  valid "__typeof" (fun loc -> TYPEOF loc) ;
+  valid "typeof" (fun loc -> TYPEOF loc) ;
+  valid "__alignof" (fun loc -> ALIGNOF loc) ;
+  valid "__alignof__" (fun loc -> ALIGNOF loc) ;
+  valid "__volatile__" (fun loc -> VOLATILE loc) ;
+  valid "__volatile" (fun loc -> VOLATILE loc) ;
+  valid "__FUNCTION__" (fun loc -> FUNCTION__ loc) ;
+  valid "__func__" (fun loc -> FUNCTION__ loc) ; (* ISO 6.4.2.2 *)
+  valid "__PRETTY_FUNCTION__" (fun loc -> PRETTY_FUNCTION__ loc) ;
+  valid "__label__" (fun _ -> LABEL__) ;
   (*** weimer: GCC arcana ***)
-      ("__restrict", fun loc -> RESTRICT loc);
-      ("restrict", fun loc -> RESTRICT loc);
-(*      ("__extension__", EXTENSION); *)
+  valid "__restrict" (fun loc -> RESTRICT loc) ;
+  valid "restrict" (fun loc -> RESTRICT loc) ;
   (**** MS VC ***)
-      ("__int64", fun _ -> INT64 (currentLoc ()));
-      ("__int32", fun loc -> INT loc);
-      ("_cdecl",  fun _ -> MSATTR ("_cdecl", currentLoc ()));
-      ("__cdecl", fun _ -> MSATTR ("__cdecl", currentLoc ()));
-      ("_stdcall", fun _ -> MSATTR ("_stdcall", currentLoc ()));
-      ("__stdcall", fun _ -> MSATTR ("__stdcall", currentLoc ()));
-      ("_fastcall", fun _ -> MSATTR ("_fastcall", currentLoc ()));
-      ("__fastcall", fun _ -> MSATTR ("__fastcall", currentLoc ()));
-      ("__w64", fun _ -> MSATTR("__w64", currentLoc ()));
-      ("__declspec", fun loc -> DECLSPEC loc);
-      ("__forceinline", fun loc -> INLINE loc); (* !! we turn forceinline
-                                                 * into inline *)
-      (* weimer: some files produced by 'GCC -E' expect this type to be
-       * defined *)
-      ("__builtin_va_list",
-       fun _ -> NAMED_TYPE "__builtin_va_list");
-      ("__builtin_va_arg", fun loc -> BUILTIN_VA_ARG loc);
-      ("__builtin_types_compatible_p", fun loc -> BUILTIN_TYPES_COMPAT loc);
-      ("__builtin_offsetof", fun loc -> BUILTIN_OFFSETOF loc);
-      ("_Thread_local",
-       fun loc ->
-         Kernel.(warning ~wkey:wkey_c11 "_Thread_local is a C11 keyword");
-         THREAD_LOCAL loc);
+  valid "__int64" (fun _ -> INT64 (currentLoc ())) ;
+  valid "__int32" (fun loc -> INT loc) ;
+  valid "_cdecl" ( fun _ -> MSATTR ("_cdecl", currentLoc ())) ;
+  valid "__cdecl" (fun _ -> MSATTR ("__cdecl", currentLoc ())) ;
+  valid "_stdcall" (fun _ -> MSATTR ("_stdcall", currentLoc ())) ;
+  valid "__stdcall" (fun _ -> MSATTR ("__stdcall", currentLoc ())) ;
+  valid "_fastcall" (fun _ -> MSATTR ("_fastcall", currentLoc ())) ;
+  valid "__fastcall" (fun _ -> MSATTR ("__fastcall", currentLoc ())) ;
+  valid "__w64" (fun _ -> MSATTR("__w64", currentLoc ())) ;
+  valid "__declspec" (fun loc -> DECLSPEC loc) ;
+  (* !! we turn forceinline into inline *)
+  valid "__forceinline" (fun loc -> INLINE loc) ;
+  (* Some files produced by 'GCC -E' expect this type to be defined *)
+  valid "__builtin_va_list" (fun _ -> NAMED_TYPE "__builtin_va_list") ;
+  valid "__builtin_va_arg" (fun loc -> BUILTIN_VA_ARG loc) ;
+  valid "__builtin_types_compatible_p" (fun loc -> BUILTIN_TYPES_COMPAT loc) ;
+  valid "__builtin_offsetof" (fun loc -> BUILTIN_OFFSETOF loc) ;
+  warning_C11 "_Thread_local" (fun loc -> THREAD_LOCAL loc) ;
   (* We recognize __thread for GCC machdeps *)
-      ("__thread",
-       fun loc ->
-         if Cil.gccMode () then
-           THREAD loc
-         else begin
-           Kernel.(
-             warning
-               ~wkey:wkey_conditional_feature
-               "__thread is a GCC extension, use a GCC-based machdep to enable it");
-           IDENT "__thread"
-         end);
-      ("__FC_FILENAME__",
-       (fun loc ->
-          let filename =
-            Filepath.Normalized.to_pretty_string (fst loc).pos_path
-          in
-          let seq = String.to_seq filename in
-          let convert_char c = Int64.of_int (Char.code c) in
-          let l =
-            Seq.fold_left (fun acc c -> convert_char c :: acc) [] seq
-          in
-          CST_STRING (List.rev l,loc)));
+  thread_keyword () ;
+  filename_keyword () ;
   (* The following C11 tokens are not yet supported, so we provide some
      helpful error messages. Usage of 'fatal' instead of 'error' below
      prevents duplicate error messages due to parsing errors. *)
-      ("_Alignas",
-       fun loc ->
-         Kernel.abort ~source:(fst loc)
-           "_Alignas is currently unsupported by Frama-C.");
-      ("_Alignof",
-       fun loc ->
-         Kernel.abort ~source:(fst loc)
-           "_Alignof is currently unsupported by Frama-C.");
-      ("_Complex",
-       fun loc ->
-         Kernel.abort ~source:(fst loc)
-           "_Complex is currently unsupported by Frama-C.");
-      ("_Generic",
-       fun loc ->
-         Kernel.(warning ~wkey:wkey_c11 "_Generic is a C11 keyword");
-         GENERIC loc);
-      ("_Imaginary",
-       fun loc ->
-         Kernel.abort ~source:(fst loc)
-           "_Imaginary is currently unsupported by Frama-C.");
-     ]
+  unsupported "_Alignas" ;
+  unsupported "_Alignof" ;
+  unsupported "_Complex" ;
+  warning_C11 "_Generic" (fun loc -> GENERIC loc) ;
+  unsupported "_Imaginary"
+
 
-let is_c_keyword s = Hashtbl.mem lexicon s
 
 (* Mark an identifier as a type name. The old mapping is preserved and will
  * be reinstated when we exit this context *)
 let add_type name =
-   (* ignore (print_string ("adding type name " ^ name ^ "\n"));  *)
-  H.add lexicon name (fun _ -> NAMED_TYPE name);
+  add name (fun _ -> NAMED_TYPE name) ;
   Logic_env.add_typename name
 
-let context : string list list ref = ref [ [] ]
-
-let typedef_decl = ref false
+let remove_type name =
+  remove name ; Logic_env.remove_typename name
 
-let is_typedef () = !typedef_decl
 
-let set_typedef () = typedef_decl := true
 
-let reset_typedef () = typedef_decl := false
+let context : string list list ref = ref [ [] ]
 
 let push_context _ = context := [] :: !context
 
 let pop_context _ =
   match !context with
-    [] -> Kernel.fatal "Empty context stack"
-  | con::sub ->
-		(context := sub;
-		List.iter (fun name ->
-                            (* Format.eprintf
-                              "removing lexicon for %s@." name; *)
-                             H.remove lexicon name;
-                             Logic_env.remove_typename name
-                          ) con)
+  | [] -> Kernel.fatal "Empty context stack"
+  | con :: sub -> context := sub ; List.iter remove_type con
 
 (* Mark an identifier as a variable name. The old mapping is preserved and
  * will be reinstated when we exit this context  *)
 let add_identifier name =
   match !context with
-    [] -> Kernel.fatal "Empty context stack"
+  | [] -> Kernel.fatal "Empty context stack"
   | con :: sub ->
-      (context := (name::con)::sub;
-       (*Format.eprintf "adding IDENT for %s@." name;*)
-       H.add lexicon name (fun _ -> dbgToken (IDENT name));
+    context := (name :: con) :: sub ;
+    add name (fun _ -> IDENT name) ;
     Logic_env.hide_typename name
-      )
 
 
-(*
-** Useful primitives
-*)
-let scan_ident id =
-  let here = currentLoc () in
-  try (H.find lexicon id) here
-  (* default to variable name, as opposed to type *)
-  with Not_found -> dbgToken (IDENT id)
+
+let typedef_decl = ref false
+let is_typedef () = !typedef_decl
+let set_typedef () = typedef_decl := true
+let reset_typedef () = typedef_decl := false
+
 
 
 (*
 ** Buffer processor
 *)
 
-
 let init ~filename lexer =
-  init_lexicon ();
-  E.startParsing filename lexer
-
+  init_lexicon () ; E.startParsing filename lexer
 
 let finish () =
-  E.finishParsing ();
-  Logic_env.reset_typenames ()
+  E.finishParsing () ; Logic_env.reset_typenames ()
 
 
 (*** escape character management ***)
-let scan_escape (char: char) : int64 =
-  let result = match char with
-    'n' -> '\n'
-  | 'r' -> '\r'
-  | 't' -> '\t'
-  | 'b' -> '\b'
-  | 'f' -> '\012'  (* ASCII code 12 *)
-  | 'v' -> '\011'  (* ASCII code 11 *)
-  | 'a' -> '\007'  (* ASCII code 7 *)
-  | 'e' | 'E' -> '\027'  (* ASCII code 27. This is a GCC extension *)
-  | '\'' -> '\''
-  | '"'-> '"'     (* '"' *)
-  | '?' -> '?'
-  | '(' -> '('
-  | '{' -> '{'
-  | '[' -> '['
-  | '%' -> '%'
-  | '\\' -> '\\'
-  | other ->
-    E.parse_error "Unrecognized escape sequence: \\%c" other
-  in
-  Int64.of_int (Char.code result)
+let scan_escape = function
+  | 'n' -> int64_of_char '\n'
+  | 'r' -> int64_of_char '\r'
+  | 't' -> int64_of_char '\t'
+  | 'b' -> int64_of_char '\b'
+  | 'f' -> int64_of_char '\012'  (* ASCII code 12 *)
+  | 'v' -> int64_of_char '\011'  (* ASCII code 11 *)
+  | 'a' -> int64_of_char '\007'  (* ASCII code 7 *)
+  | 'e' | 'E' -> int64_of_char '\027'  (* ASCII code 27. This is a GCC extension *)
+  | '\'' -> int64_of_char '\''
+  | '"' -> int64_of_char '"'     (* '"' *)
+  | '?' -> int64_of_char '?'
+  | '(' -> int64_of_char '('
+  | '{' -> int64_of_char '{'
+  | '[' -> int64_of_char '['
+  | '%' -> int64_of_char '%'
+  | '\\' -> int64_of_char '\\'
+  | other -> E.parse_error "Unrecognized escape sequence: \\%c" other
 
 let scan_hex_escape str =
   let radix = Int64.of_int 16 in
@@ -373,77 +324,49 @@ let lex_simple_escape remainder lexbuf =
   prefix :: remainder lexbuf
 
 let lex_unescaped remainder lexbuf =
-  let prefix = Int64.of_int (Char.code (Lexing.lexeme_char lexbuf 0)) in
+  let prefix = int64_of_char (Lexing.lexeme_char lexbuf 0) in
   prefix :: remainder lexbuf
 
 let lex_comment remainder buffer lexbuf =
   let s = Lexing.lexeme lexbuf in
   if s = "\n" then E.newline() ;
-  (match buffer with None -> () | Some b -> Buffer.add_string b s) ;
+  Option.iter (fun b -> Buffer.add_string b s) buffer ;
   remainder buffer lexbuf
 
+(* We ignore the last line if it does not contain "\n" as it means that
+  it directly precedes the "else" and thus contains only whitespaces *)
+let rec iter_comments ends_with_n f = function
+  | [] -> ()
+  | [ _ ] when not ends_with_n -> ()
+  | x :: l -> f x ; iter_comments ends_with_n f l
+
 let do_ghost_else_comments register comments =
-  let ends_with_n =
   let last = String.length comments in
   (* note that comments contains at least a blank *)
-    '\n' = String.get comments (last - 1)
-  in
+  let ends_with_n = '\n' = String.get comments (last - 1) in
   let comments = String.split_on_char '\n' comments in
   let comments = List.map String.trim comments in
-  let process_line s =
-    E.newline () ;
-    if register
-    && Kernel.PrintComments.get ()
-    && not (String.equal "" s)
-    then
-      addComment s
-  in
-  let rec iter f = function
-    | [] -> ()
-    (* We ignore the last line if it does not contain "\n" as it means that
-      it directly precedes the "else" and thus contains only whitespaces *)
-    | [ _ ] when not ends_with_n -> ()
-    | x :: l -> f x ; iter f l
-  in
-  iter process_line comments
+  let print_comments = Kernel.PrintComments.get () in
+  let do_comment s = register && print_comments && not (String.equal "" s) in
+  let process_line s = E.newline () ; if do_comment s then add_comment s in
+  iter_comments ends_with_n process_line comments
 
 let do_lex_comment ?(first_string="") remainder lexbuf =
-  let buffer =
-    if Kernel.PrintComments.get () then begin
+  if Kernel.PrintComments.get () then
     let b = Buffer.create 80 in
-      Buffer.add_string b first_string;
-      Some b
-    end else None
-  in remainder buffer lexbuf ;
-  match buffer with
-    | Some b -> addComment (Buffer.contents b)
-    | None -> ()
-
-
-(* ISO standard locale-specific function to convert a wide character
- * into a sequence of normal characters. Here we work on strings.
- * We convert L"Hi" to "H\000i\000"
-  matth: this seems unused.
-let wbtowc wstr =
-  let len = String.length wstr in
-  let dest = String.make (len * 2) '\000' in
-  for i = 0 to len-1 do
-    dest.[i*2] <- wstr.[i] ;
-  done ;
-  dest
-*)
+    let () = Buffer.add_string b first_string in
+    let () = remainder (Some b) lexbuf in
+    add_comment (Buffer.contents b)
+  else remainder None lexbuf
+
+let do_oneline_ghost ~first_string comment lexbuf initial =
+  do_lex_comment ~first_string comment lexbuf ;
+  E.newline () ;
+  if is_oneline_ghost ()
+  then (exit_oneline_ghost () ; RGHOST)
+  else initial lexbuf
+
 
-(* This function converts the "Hi" in L"Hi" to { L'H', L'i', L'\0' }
-  matth: this seems unused.
-let wstr_to_warray wstr =
-  let len = String.length wstr in
-  let res = ref "{ " in
-  for i = 0 to len-1 do
-    res := !res ^ (Printf.sprintf "L'%c', " wstr.[i])
-  done ;
-  res := !res ^ "}" ;
-  !res
-*)
 
 (* Pragmas get explicit end-of-line tokens.
  * Elsewhere they are silently discarded as whitespace. *)
@@ -451,11 +374,9 @@ let pragmaLine = ref false
 
 let annot_char = ref '@'
 
-let () =
-  Kernel.ReadAnnot.add_set_hook
-    (fun _ x ->
 (* prevent the C lexer interpretation of comments *)
-      annot_char := if x then '@' else '\000')
+let prevent _ x = annot_char := if x then '@' else '\000'
+let () = Kernel.ReadAnnot.add_set_hook prevent
 
 let annot_start_pos = ref Cabshelper.cabslu
 let buf = Buffer.create 1024
@@ -464,40 +385,39 @@ let save_current_pos () =
   annot_start_pos := currentLoc ()
 
 let annot_lex initial rule lexbuf =
-  try
   save_current_pos () ;
   Buffer.clear buf ;
-    rule lexbuf
+  try rule lexbuf
   with Parsing.Parse_error ->
-    let source = Cil_datatype.Position.of_lexing_pos (Lexing.lexeme_start_p lexbuf) in
+    let start = Lexing.lexeme_start_p lexbuf in
+    let source = Cil_datatype.Position.of_lexing_pos start in
     Kernel.warning ~wkey:Kernel.wkey_annot_error ~source "skipping annotation" ;
     initial lexbuf
 
 let make_annot ~one_line default lexbuf s =
   let start = snd !annot_start_pos in
   match Logic_lexer.annot (start, s) with
+  (* error occured and annotation is discarded. Find a normal token. *)
+  | None -> default lexbuf
   | Some (stop, token) ->
     lexbuf.Lexing.lex_curr_p <- Cil_datatype.Position.to_lexing_pos stop ;
     if one_line then E.newline () ;
-    (match token with
+    match token with
     | Logic_ptree.Adecl d -> DECL d
     | Logic_ptree.Aspec -> SPEC (start, s)
     (* At this point, we only have identified a function spec. Complete
-           parsing of the annotation will only occur in the cparser.mly rule.
-     *)
+       parsing of the annotation will only occur in the cparser.mly rule. *)
     | Logic_ptree.Acode_annot (loc,a) -> CODE_ANNOT (a, loc)
     | Logic_ptree.Aloop_annot (loc,a) -> LOOP_ANNOT (a,loc)
-     | Logic_ptree.Aattribute_annot (loc,a) -> ATTRIBUTE_ANNOT (a, loc))
-  | None -> (* error occured and annotation is discarded. Find a normal token. *)
-    default lexbuf
+    | Logic_ptree.Aattribute_annot (loc,a) -> ATTRIBUTE_ANNOT (a, loc)
 
 let parse_error lexbuf msg =
   let loc = lexbuf.Lexing.lex_curr_p in
   let source = Cil_datatype.Position.of_lexing_pos loc in
   E.parse_error ~source msg
 
-let () =
 (* Initialize the pointer in Errormsg *)
+let () =
   Lexerhack.add_type := add_type ;
   Lexerhack.push_context := push_context ;
   Lexerhack.pop_context := pop_context ;
@@ -507,18 +427,18 @@ let () =
   Lexerhack.reset_typedef := reset_typedef
 }
 
+
+
 let decdigit = ['0'-'9']
 let octdigit = ['0'-'7']
 let hexdigit = ['0'-'9' 'a'-'f' 'A'-'F']
 let binarydigit = ['0' '1']
 let letter = ['a'- 'z' 'A'-'Z']
-
-
 let usuffix = ['u' 'U']
 let lsuffix = "l" | "L" | "ll" | "LL"
-let intsuffix = lsuffix | usuffix | usuffix lsuffix | lsuffix usuffix
-              | usuffix ? "i64"
 
+let intsuffix =
+  lsuffix | usuffix | usuffix lsuffix | lsuffix usuffix | usuffix ? "i64"
 
 let hexprefix = '0' ['x' 'X']
 let binaryprefix = '0' ['b' 'B']
@@ -530,144 +450,138 @@ let binarynum = binaryprefix binarydigit+ intsuffix?
 
 let exponent = ['e' 'E']['+' '-']? decdigit+
 let fraction  = '.' decdigit+
-let decfloat = (intnum? fraction)
+let decfloat =
+    (intnum? fraction)
   | (intnum exponent)
   | (intnum? fraction exponent)
   | (intnum '.')
   | (intnum '.' exponent)
 
-
 let hexfraction = hexdigit* '.' hexdigit+ | hexdigit+ '.'
 let binexponent = ['p' 'P'] ['+' '-']? decdigit+
-let hexfloat = hexprefix hexfraction binexponent
+let hexfloat =
+    hexprefix hexfraction binexponent
   | hexprefix hexdigit+   binexponent
 
 let floatsuffix = ['f' 'F' 'l' 'L']
 let floatnum = (decfloat | hexfloat) floatsuffix?
 
 let ident = (letter|'_')(letter|decdigit|'_'|'$')*
-let blank = [' ' '\t' '\012' '\r' '\026'(*this is the plain old DOS eof char*)]+
+(* \026 is the dos EOF character *)
+let blank = [' ' '\t' '\012' '\r' '\026']+
 let escape = '\\' _
 let hex_escape = '\\' ['x' 'X'] hexdigit+
 let oct_escape = '\\' octdigit octdigit? octdigit?
 
-(* Pragmas that are not parsed by CIL.  We lex them as PRAGMA_LINE tokens *)
-let no_parse_pragma =
-               "warning" | "GCC"
-             (* Solaris-style pragmas:  *)
-             | "ident" | "section" | "option" | "asm" | "use_section" | "weak"
-             | "redefine_extname"
-             | "TCS_align"
+(* Solaris-style pragmas *)
+let solaris_pragmas =
+    "ident" | "section" | "option" | "asm" | "use_section" | "weak"
+  | "redefine_extname" | "TCS_align"
+
 (* Embedded world *)
-             | "global_register" | "location"
+let embedded_pragmas = "global_register" | "location"
+
+(* Pragmas that are not parsed by CIL. We lex them as PRAGMA_LINE tokens *)
+let no_parse_pragma = "warning" | "GCC" | solaris_pragmas | embedded_pragmas
+
+let ghost_comments = "//\n" | ("//" [^'\n''@'] ([^'\n']*("\\\n")?)* '\n')
+
 
-let ghost_comments = "//\n"
-                   | ("//" [^'\n''@'] ([^'\n']*("\\\n")?)* '\n')
 
 rule initial = parse
-| "/*" ("" | "@{" | "@}" as suf) (* Skip special doxygen comments. Use of '@'
-                                    instead of '!annot_char' is intentional *)
+
+  (* Skip special doxygen comments. Use of '@' instead of '!annot_char' is
+     intentional *)
+  | "/*" ("" | "@{" | "@}" as suf)
     {
     do_lex_comment ~first_string:suf comment lexbuf ;
     initial lexbuf
     }
 
   | "/*" ([^ '*' '\n'] as c)
-    { if c = !annot_char then begin
-        annot_lex initial annot_first_token lexbuf
-      end else
-	begin
-	  do_lex_comment ~first_string:(String.make 1 c) comment lexbuf ;
-          initial lexbuf
-	end
+    {
+    let first_string = String.make 1 c in
+    if c = !annot_char
+    then annot_lex initial annot_first_token lexbuf
+    else (do_lex_comment ~first_string comment lexbuf ; initial lexbuf)
     }
 
-| "//" ("" | "@{" | "@}" as suf) (* See comment for "/*@{" above *)
+  (* See comment for "/*@{" above *)
+  | "//" ("" | "@{" | "@}" as suf)
     {
-      do_lex_comment ~first_string:suf onelinecomment lexbuf ;
-      E.newline();
-      if is_oneline_ghost () then begin
-        exit_oneline_ghost ();
-        RGHOST
-      end else begin
-        initial lexbuf
-      end
+    do_oneline_ghost ~first_string:suf onelinecomment lexbuf initial
     }
 
   | "//" ([^ '\n'] as c)
-    { if c = !annot_char then begin
-        annot_lex initial annot_one_line lexbuf
-      end else
-	begin
-	  do_lex_comment ~first_string:(String.make 1 c) onelinecomment lexbuf;
-	  E.newline();
-	  if is_oneline_ghost () then
-	    begin
-              exit_oneline_ghost ();
-              RGHOST
-	    end
-	  else
-	    begin
-              initial lexbuf
-	    end
-	end
+    {
+    let first_string = String.make 1 c in
+    if c = !annot_char
+    then annot_lex initial annot_one_line lexbuf
+    else do_oneline_ghost ~first_string onelinecomment lexbuf initial
     }
+
   | "\\ghost"
-    { if is_ghost_code () || is_oneline_ghost () then begin
-        GHOST (currentLoc())
-      end else begin
-        parse_error lexbuf "Use of \\ghost out of ghost code"
-      end
+    {
+    if is_ghost_code () || is_oneline_ghost ()
+    then GHOST (currentLoc())
+    else parse_error lexbuf "Use of \\ghost out of ghost code"
+    }
+
+  | blank {initial lexbuf} | '\n'
+    {
+    E.newline () ;
+    if !pragmaLine then (pragmaLine := false ; PRAGMA_EOL)
+    else if is_oneline_ghost () then (exit_oneline_ghost () ; RGHOST)
+    else initial lexbuf
     }
 
-|		blank			{initial lexbuf}
-|               '\n'                    { E.newline ();
-                                          if !pragmaLine then
-                                            begin
-                                              pragmaLine := false;
-                                              PRAGMA_EOL
-                                            end
-                                          else if is_oneline_ghost () then
-                                            begin
-                                              exit_oneline_ghost ();
-                                              RGHOST
-                                            end
-                                          else begin
-                                            initial lexbuf
-                                          end }
-|               '\\' '\r' * '\n'        { E.newline ();
+  | '\\' '\r' * '\n'
+    {
+    E.newline () ;
     initial lexbuf
     }
+
   | '#'  { hash lexbuf }
   | "%:" { hash lexbuf }
   | "_Pragma" { PRAGMA (currentLoc ()) }
-|		'\''			{
+
+  | '\''
+    {
     let start = Lexing.lexeme_start_p lexbuf in
     let content = chr lexbuf in
     let last = Lexing.lexeme_end_p lexbuf in
     CST_CHAR (content, Cil_datatype.Location.of_lexing_loc (start,last))
     }
-|		"L'"			{
+
+  | "L'"
+    {
     let start = Lexing.lexeme_start_p lexbuf in
     let content = chr lexbuf in
     let last = Lexing.lexeme_end_p lexbuf in
     CST_WCHAR (content, Cil_datatype.Location.of_lexing_loc (start,last))
     }
-|		'"'			{
+
+  | '"'
+    {
     let start = Lexing.lexeme_start_p lexbuf in
     let content = str lexbuf in
     let last = Lexing.lexeme_end_p lexbuf in
     CST_STRING (content, Cil_datatype.Location.of_lexing_loc (start,last))
     }
-|		"L\""			{
+
+  | "L\""
+    {
     let start = Lexing.lexeme_start_p lexbuf in
     let content = str lexbuf in
     let last = Lexing.lexeme_end_p lexbuf in
     CST_WSTRING(content, Cil_datatype.Location.of_lexing_loc (start,last))
     }
+
   | floatnum  { CST_FLOAT (Lexing.lexeme lexbuf, currentLoc ()) }
-|		binarynum               { (* GCC Extension for binary numbers *)
-                                          CST_INT (Lexing.lexeme lexbuf, currentLoc ())}
+
+  (* GCC Extension for binary numbers *)
+  | binarynum { CST_INT (Lexing.lexeme lexbuf, currentLoc ()) }
+
   | hexnum    { CST_INT (Lexing.lexeme lexbuf, currentLoc ()) }
   | octnum    { CST_INT (Lexing.lexeme lexbuf, currentLoc ()) }
   | intnum    { CST_INT (Lexing.lexeme lexbuf, currentLoc ()) }
@@ -697,21 +611,23 @@ rule initial = parse
   | "->"      { ARROW }
   | '+'       { PLUS (currentLoc ()) }
   | '-'       { MINUS (currentLoc ()) }
+
   | '*'
-                    { if is_ghost_code () then might_end_ghost lexbuf
-                      else
-                        STAR (currentLoc ())}
+    {
+    if is_ghost_code ()
+    then might_end_ghost lexbuf
+    else STAR (currentLoc ())
+    }
+
   | "/" ([^ '\n'] as c)
-   { if c = !annot_char then
-       if is_ghost_code () || is_oneline_ghost () then begin
-         enter_ghost_annot();
-         annot_lex initial annot_first_token lexbuf
-       end else
-         parse_error lexbuf "This kind of annotation is valid only inside ghost code"
-     else begin
-       lexbuf.Lexing.lex_curr_pos <- lexbuf.Lexing.lex_curr_pos - 1;
-       SLASH
-     end }
+    {
+    if c = !annot_char then
+      if is_ghost_code () || is_oneline_ghost ()
+      then (enter_ghost_annot () ; annot_lex initial annot_first_token lexbuf)
+      else parse_error lexbuf "This kind of annotation is valid only inside ghost code"
+    else (lexbuf.Lexing.lex_curr_pos <- lexbuf.Lexing.lex_curr_pos - 1 ; SLASH)
+    }
+
   | '/'   { SLASH }
   | '%'   { PERCENT }
   | '!'   { EXCLAM (currentLoc ()) }
@@ -721,152 +637,174 @@ rule initial = parse
   | '|'   { PIPE }
   | '^'   { CIRC }
   | '?'   { QUEST }
+
   | ':'
-  { if Cabshelper.is_attr_test () then begin
-        Cabshelper.pop_attr_test (); COLON2
-      end else COLON
+    {
+    if Cabshelper.is_attr_test ()
+    then (Cabshelper.pop_attr_test () ; COLON2)
+    else COLON
     }
-|		'~'		        {TILDE (currentLoc ())}
 
-|		'{'		       {dbgToken (LBRACE (currentLoc ()))}
-|		'}'		       {dbgToken (RBRACE (currentLoc ()))}
-|		"<%"		       {dbgToken (LBRACE (currentLoc ()))}
-|		"%>"		       {dbgToken (RBRACE (currentLoc ()))}
+  | '~'       { TILDE (currentLoc ()) }
+  | '{'       { LBRACE (currentLoc ()) }
+  | '}'       { RBRACE (currentLoc ()) }
+  | "<%"      { LBRACE (currentLoc ()) }
+  | "%>"      { RBRACE (currentLoc ()) }
   | '['       { LBRACKET }
   | ']'       { RBRACKET }
   | "<:"      { LBRACKET }
   | ":>"      { RBRACKET }
-|		'('		       {dbgToken (LPAREN (currentLoc ())) }
+  | '('       { LPAREN (currentLoc ()) }
   | ')'       { RPAREN }
-|		';'		       {dbgToken (SEMICOLON (currentLoc ())) }
+  | ';'       { SEMICOLON (currentLoc ()) }
   | ','       { COMMA }
   | '.'       { DOT }
   | "sizeof"  { SIZEOF (currentLoc ()) }
   | "__asm"   { ASM (currentLoc ()) }
 
-(* If we see __pragma we eat it and the matching parentheses as well *)
-|               "__pragma"              { let _ = matchingpars 0 lexbuf in
-                                          initial lexbuf
-                                        }
+  (* If we see __pragma we consume it and the matching parentheses as well *)
+  | "__pragma" { let _ = matchingpars 0 lexbuf in initial lexbuf }
 
   (* __extension__ is a black. The parser runs into some conflicts if we let it
- * pass *)
+     pass *)
   | "__extension__" { initial lexbuf }
+
   | ident { scan_ident (Lexing.lexeme lexbuf) }
+
   | eof
-  { if is_oneline_ghost() then begin
-      exit_oneline_ghost (); RGHOST
-    end
+    {
+    if is_oneline_ghost()
+    then (exit_oneline_ghost () ; RGHOST)
     else EOF
     }
+
   | _ as c
-  { if is_ghost_code() && c = '@' then initial lexbuf
+    {
+    if is_ghost_code() && c = '@' then initial lexbuf
     else parse_error lexbuf "Invalid symbol"
     }
+
+
 and might_end_ghost = parse
   | '/' { exit_ghost_code() ; RGHOST }
   | ""  { STAR (currentLoc()) }
 
+
 and comment buffer = parse
   | "*/" {  }
   | eof  { parse_error lexbuf "Unterminated C comment" }
   | _    { lex_comment comment buffer lexbuf }
 
+
 and onelinecomment buffer = parse
-  | "*/"        { if is_ghost_code () then
+  | "*/"
+    {
     (* end of multiline comment *)
-                      lexbuf.Lexing.lex_curr_pos <-
-                          lexbuf.Lexing.lex_curr_pos - 2
-                  else
-                      lex_comment onelinecomment buffer lexbuf
+    if is_ghost_code ()
+    then lexbuf.Lexing.lex_curr_pos <- lexbuf.Lexing.lex_curr_pos - 2
+    else lex_comment onelinecomment buffer lexbuf
     }
   | '\n' | eof {  }
   | _          { lex_comment onelinecomment buffer lexbuf }
 
+
 and matchingpars parsopen = parse
-  '\n'          { E.newline (); matchingpars parsopen lexbuf }
+  | '\n'  { E.newline (); matchingpars parsopen lexbuf }
   | blank { matchingpars parsopen lexbuf }
   | '('   { matchingpars (parsopen + 1) lexbuf }
-| ')'           { if parsopen > 1 then
-                    matchingpars (parsopen - 1) lexbuf
-                }
-|  "/*"		{ do_lex_comment comment lexbuf ;
-                  matchingpars parsopen lexbuf }
-|  '"'		{ let _ = str lexbuf in
-                  matchingpars parsopen lexbuf }
+  | ')'   { if parsopen > 1 then matchingpars (parsopen - 1) lexbuf }
+  | "/*"  { do_lex_comment comment lexbuf ; matchingpars parsopen lexbuf }
+  | '"'   { let _ = str lexbuf in matchingpars parsopen lexbuf }
   | _     { matchingpars parsopen lexbuf }
 
+
 (* # <line number> <file name> ... *)
 and hash = parse
-  '\n'		{ E.newline (); initial lexbuf}
+  | '\n' { E.newline (); initial lexbuf}
   | blank { hash lexbuf}
-| intnum	{ (* We are seeing a line number. This is the number for the
-                   * next line *)
+
+  (* We are seeing a line number. This is the number for the next line *)
+  | intnum
+    {
     let s = Lexing.lexeme lexbuf in
-                 let lineno = try
-                   int_of_string s
-                 with Failure _ ->
-                   (* the int is too big. *)
-                   Kernel.warning "Bad line number in preprocessed file: %s" s;
-                   (-1)
-                 in
+    let msg () = Kernel.warning "Bad line number in preprocessed file: %s" s in
+    let lineno = try int_of_string s with Failure _ -> msg () ; -1 in
     E.setCurrentLine (lineno - 1) ;
     (* A file name may follow *)
-		  file lexbuf }
-| "line"        { hash lexbuf } (* MSVC line number info *)
-                (* For pragmas with irregular syntax, like #pragma warning,
-                 * we parse them as a whole line. *)
+    file lexbuf
+    }
+
+  (* MSVC line number info *)
+  | "line" { hash lexbuf }
+
+  (* For pragmas with irregular syntax, like #pragma warning, we parse them as a
+     whole line. *)
   | "pragma" blank (no_parse_pragma as pragmaName)
-                { let here = currentLoc () in
+    {
+    let here = currentLoc () in
     PRAGMA_LINE (pragmaName ^ pragma lexbuf, here)
     }
+
   | "pragma"  { pragmaLine := true ; PRAGMA (currentLoc ()) }
   | _         { endline lexbuf }
 
+
 and file = parse
-        '\n'		        {E.newline (); initial lexbuf}
+  | '\n'  { E.newline () ; initial lexbuf }
   | blank { file lexbuf }
-(* The //-ending file directive is a GCC extension that provides the CWD of the
-   preprocessor when the file was preprocessed. *)
-|       '"' ([^ '\012' '\t' '"']* as d) "//\"" {
+
+  (* The //-ending file directive is a GCC extension that provides the CWD of
+     the preprocessor when the file was preprocessed. *)
+  | '"' ([^ '\012' '\t' '"']* as d) "//\""
+    {
     E.setCurrentWorkingDirectory d ;
-                                 endline lexbuf }
-|	'"' (([^ '\012' '\t' '"']|"\\\"")* as f) '"' {
+    endline lexbuf
+    }
+
+  | '"' (([^ '\012' '\t' '"']|"\\\"")* as f) '"'
+    {
     let unescape = Str.regexp_string "\\\"" in
     let f = Str.global_replace unescape "\"" f in
     E.setCurrentFile f ;
-				 endline lexbuf}
+    endline lexbuf
+    }
 
   | _ { endline lexbuf }
 
+
 and endline = parse
-        '\n' 			{ E.newline (); initial lexbuf}
+  | '\n'  { E.newline () ; initial lexbuf }
   | eof   { EOF }
   | _     { endline lexbuf }
 
+
 and pragma = parse
-   '\n'                 { E.newline (); "" }
-|   _                   { let cur = Lexing.lexeme lexbuf in
-                          cur ^ (pragma lexbuf) }
+  | '\n'  { E.newline () ; "" }
+  | _     { let cur = Lexing.lexeme lexbuf in cur ^ (pragma lexbuf) }
+
 
 and str = parse
-        '"'             {[]} (* no nul terminiation in CST_STRING '"' *)
+  (* no nul terminiation in CST_STRING '"' *)
+  | '"'         { [] }
   | hex_escape  { lex_hex_escape str lexbuf }
   | oct_escape  { lex_oct_escape str lexbuf }
   | escape      { lex_simple_escape str lexbuf }
   | eof         { parse_error lexbuf "unterminated string" }
   | _           { lex_unescaped str lexbuf }
 
+
 and chr =  parse
-	'\''	        {[]}
+  | '\''        { [] }
   | hex_escape  { lex_hex_escape chr lexbuf }
   | oct_escape  { lex_oct_escape chr lexbuf }
   | escape      { lex_simple_escape chr lexbuf }
   | eof         { parse_error lexbuf "unterminated char" }
   | _           { lex_unescaped chr lexbuf }
 
+
 and annot_first_token = parse
-  | "ghost" ((blank| '\\'?'\n' | ghost_comments)* as comments) "else" {
+  | "ghost" ((blank| '\\'?'\n' | ghost_comments)* as comments) "else"
+    {
     if is_oneline_ghost () then parse_error lexbuf "nested ghost code" ;
     Buffer.clear buf ;
     let loc = currentLoc () in
@@ -874,54 +812,78 @@ and annot_first_token = parse
     enter_ghost_code () ;
     LGHOST_ELSE (loc)
     }
-  | "ghost" {
+
+  | "ghost"
+    {
     if is_oneline_ghost () then parse_error lexbuf "nested ghost code" ;
     Buffer.clear buf ;
     enter_ghost_code () ;
     LGHOST
     }
+
   | ' '|'@'|'\t'|'\r' as c { Buffer.add_char buf c ; annot_first_token lexbuf }
   | '\n' { E.newline() ; Buffer.add_char buf '\n' ; annot_first_token lexbuf }
   | ""   { annot_token lexbuf }
+
+
 and annot_token = parse
-  | "*/" { if is_ghost_annot () then
-             parse_error lexbuf "Ghost multi-line annotation not terminated";
+  | "*/"
+    {
+    if is_ghost_annot ()
+    then parse_error lexbuf "Ghost multi-line annotation not terminated" ;
     let s = Buffer.contents buf in
-           make_annot ~one_line:false initial lexbuf s }
+    make_annot ~one_line:false initial lexbuf s
+    }
+
   | eof  { parse_error lexbuf "Unterminated annotation" }
   | '\n' { E.newline() ; Buffer.add_char buf '\n' ; annot_token lexbuf }
-  | _ as c { if is_ghost_annot () && c = !annot_char then
-               might_end_ghost_annot lexbuf
-             else (Buffer.add_char buf c; annot_token lexbuf) }
+  | _ as c
+    {
+    if is_ghost_annot () && c = !annot_char
+    then might_end_ghost_annot lexbuf
+    else (Buffer.add_char buf c ; annot_token lexbuf)
+    }
+
+
 and might_end_ghost_annot = parse
   | '/' { exit_ghost_annot ();
           let s = Buffer.contents buf in
           make_annot ~one_line:false initial lexbuf s }
   | "" { Buffer.add_char buf !annot_char; annot_token lexbuf }
+
+
 and annot_one_line = parse
-  | "ghost" ((blank|"\\\n")+ as comments) "else" {
+  | "ghost" ((blank|"\\\n")+ as comments) "else"
+    {
     do_ghost_else_comments false comments ;
     if is_oneline_ghost () then parse_error lexbuf "nested ghost code" ;
-      enter_oneline_ghost (); LGHOST_ELSE (currentLoc ())
+    enter_oneline_ghost () ;
+    LGHOST_ELSE (currentLoc ())
     }
-  | "ghost" {
+
+  | "ghost"
+    {
     if is_oneline_ghost () then parse_error lexbuf "nested ghost code" ;
-      enter_oneline_ghost (); LGHOST
+    enter_oneline_ghost () ;
+    LGHOST
     }
+
   | ' '|'@'|'\t'|'\r' as c { Buffer.add_char buf c ; annot_one_line lexbuf }
   | "" { annot_one_line_logic lexbuf }
+
+
 and annot_one_line_logic = parse
   | '\n'    { make_annot ~one_line:true initial lexbuf (Buffer.contents buf) }
   | eof     { parse_error lexbuf "Invalid C file: should end with a newline" }
   | _ as c  { Buffer.add_char buf c ; annot_one_line_logic lexbuf }
 
-{
 
+
+{
   (* Catch the exceptions raised by the lexer itself *)
   let initial lexbuf =
     try initial lexbuf
     with Failure _ -> raise Parsing.Parse_error
-
 }
 
 (*