Merge branch 'master' into ppc64

Resolved conflicts in:configure	powerpc/Asmexpand.ml

13 files changed, 585 insertions, 228 deletions

diff --git a/cparser/Bitfields.ml b/cparser/Bitfields.ml
index 6569bb4c..d064f4b1 100644
--- a/cparser/Bitfields.ml
+++ b/cparser/Bitfields.ml
@@ -111,16 +111,16 @@ let pack_bitfields env sid ml =
           end
   in pack [] 0 ml
 
-let rec transf_members env id count = function
+let rec transf_struct_members env id count = function
   | [] -> []
   | m :: ms as ml ->
       if m.fld_bitfield = None then
-        m :: transf_members env id count ms
+        m :: transf_struct_members env id count ms
       else begin
         let (nbits, bitfields, ml') = pack_bitfields env id ml in
         if nbits = 0 then
           (* Lone zero-size bitfield: just ignore *)
-          transf_members env id count ml'
+          transf_struct_members env id count ml'
         else begin
           (* Create integer field of sufficient size for this bitfield group *)
           let carrier = sprintf "__bf%d" count in
@@ -134,6 +134,7 @@ let rec transf_members env id count = function
                   if !config.bitfields_msb_first
                   then sizeof_ikind carrier_ikind * 8 - pos - sz
                   else pos in
+                Debug.set_bitfield_offset id name pos carrier (sizeof_ikind carrier_ikind);
                 Hashtbl.add bitfield_table
                   (id, name)
                   {bf_carrier = carrier; bf_carrier_typ = carrier_typ;
@@ -143,14 +144,49 @@ let rec transf_members env id count = function
               end)
             bitfields;
           { fld_name = carrier; fld_typ = carrier_typ; fld_bitfield = None}
-          :: transf_members env id (count + 1) ml'
+          :: transf_struct_members env id (count + 1) ml'
         end
       end
 
+let rec transf_union_members env id count = function
+    [] -> []
+  | m :: ms ->
+      (match m.fld_bitfield with
+      | None ->  m::transf_union_members env id count ms
+      | Some nbits ->
+          let carrier = sprintf "__bf%d" count in
+          let carrier_ikind = unsigned_ikind_for_carrier nbits in
+          let carrier_typ = TInt(carrier_ikind, []) in
+          let signed =
+            match unroll env m.fld_typ with
+            | TInt(ik, _) -> is_signed_ikind ik
+            | TEnum(eid, _) -> is_signed_enum_bitfield env id m.fld_name eid nbits
+            | _ -> assert false (* should never happen, checked in Elab *) in
+          let signed2 =
+            match unroll env (type_of_member env m) with
+            | TInt(ik, _) -> is_signed_ikind ik
+            | _ -> assert false (* should never happen, checked in Elab *) in
+          let pos' =
+            if !config.bitfields_msb_first
+            then sizeof_ikind carrier_ikind * 8 - nbits
+            else 0 in
+          let is_bool =
+            match unroll env m.fld_typ with
+            | TInt(IBool, _) -> true
+            | _ -> false in
+          Hashtbl.add bitfield_table
+            (id, m.fld_name)
+            {bf_carrier = carrier; bf_carrier_typ = carrier_typ;
+             bf_pos = pos'; bf_size = nbits;
+             bf_signed = signed; bf_signed_res = signed2;
+             bf_bool = is_bool};
+          { fld_name = carrier; fld_typ = carrier_typ; fld_bitfield = None}
+          :: transf_struct_members env id (count + 1) ms)
+
 let transf_composite env su id attr ml =
   match su with
-  | Struct -> (attr, transf_members env id 1 ml)
-  | Union  -> (attr, ml)
+  | Struct -> (attr, transf_struct_members env id 1 ml)
+  | Union  -> (attr, transf_union_members env id 1 ml)
 
 (* Bitfield manipulation expressions *)
 
@@ -317,6 +353,7 @@ let rec is_bitfield_access env e =
   match e.edesc with
   | EUnop(Odot fieldname, e1) ->
       begin match unroll env e1.etyp with
+      | TUnion (id,_)
       | TStruct(id, _) ->
           (try Some(e1, Hashtbl.find bitfield_table (id, fieldname))
            with Not_found -> None)
diff --git a/cparser/Cleanup.ml b/cparser/Cleanup.ml
index 254f6fed..c81fd498 100644
--- a/cparser/Cleanup.ml
+++ b/cparser/Cleanup.ml
@@ -184,6 +184,11 @@ let saturate p =
 
 (* Remove unreferenced definitions *)
 
+let remove_unused_debug =  function
+  | Gdecl (_,id,_,_) ->  Debug.remove_unused id
+  | Gfundef f -> Debug.remove_unused f.fd_name
+  | _ -> ()    
+
 let rec simpl_globdecls accu = function
   | [] -> accu
   | g :: rem ->
@@ -199,7 +204,7 @@ let rec simpl_globdecls accu = function
         | Gpragma s -> true in
       if need
       then simpl_globdecls (g :: accu) rem
-      else simpl_globdecls accu rem
+      else begin remove_unused_debug g.gdesc; simpl_globdecls accu rem end
 
 let program p =
   referenced := IdentSet.empty;
diff --git a/cparser/Cprint.ml b/cparser/Cprint.ml
index 4ceaa016..1af5af1e 100644
--- a/cparser/Cprint.ml
+++ b/cparser/Cprint.ml
@@ -20,6 +20,8 @@ open C
 
 let print_idents_in_full = ref false
 
+let print_debug_idents = ref false
+
 let print_line_numbers = ref false
 
 let location pp (file, lineno) =
@@ -27,7 +29,9 @@ let location pp (file, lineno) =
     fprintf pp "# %d \"%s\"@ " lineno file
 
 let ident pp i =
-  if !print_idents_in_full
+  if !print_debug_idents
+  then fprintf pp "$%d" i.stamp
+  else if !print_idents_in_full
   then fprintf pp "%s$%d" i.name i.stamp
   else fprintf pp "%s" i.name
 
diff --git a/cparser/Cprint.mli b/cparser/Cprint.mli
index d63e341c..349b5f9a 100644
--- a/cparser/Cprint.mli
+++ b/cparser/Cprint.mli
@@ -15,6 +15,7 @@
 
 val print_idents_in_full : bool ref
 val print_line_numbers : bool ref
+val print_debug_idents : bool ref
 
 val location : Format.formatter -> C.location -> unit
 val attributes : Format.formatter -> C.attributes -> unit
diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml
index a3c05c34..0def347f 100644
--- a/cparser/Cutil.ml
+++ b/cparser/Cutil.ml
@@ -273,6 +273,42 @@ let combine_types mode env t1 t2 =
 
   in try Some(comp mode t1 t2) with Incompat -> None
 
+let rec equal_types env t1 t2 =
+  match t1, t2 with
+  | TVoid a1, TVoid a2 ->
+     a1=a2
+  | TInt(ik1, a1), TInt(ik2, a2) ->
+      ik1 = ik2 && a1 = a2
+  | TFloat(fk1, a1), TFloat(fk2, a2) ->
+     fk1 = fk2 && a1 = a2
+  | TPtr(ty1, a1), TPtr(ty2, a2) ->
+      a1 = a2 && equal_types env ty1 ty2
+  | TArray(ty1, sz1, a1), TArray(ty2, sz2, a2) ->
+      let size = begin match sz1,sz2 with
+      | None, None -> true
+      | Some s1, Some s2 -> s1 = s2
+      | _ -> false end in
+      size && a1 = a2 && equal_types env t1 t2
+  | TFun(ty1, params1, vararg1, a1), TFun(ty2, params2, vararg2, a2) ->
+      let params =
+        match params1, params2 with
+        | None, None -> true
+        | None, Some _
+        | Some _, None -> false
+        | Some l1, Some l2 ->
+            try
+              List.for_all2 (fun (_,t1) (_,t2) -> equal_types env t1 t2) l1 l2
+            with _ -> false
+      in params && a1 = a2 && vararg1 = vararg2 && equal_types env ty1 ty2
+  | TNamed _, _ -> equal_types env (unroll env t1) t2
+  | _, TNamed _ -> equal_types env t1 (unroll env t2)
+  | TStruct(s1, a1), TStruct(s2, a2)
+  | TUnion(s1, a1), TUnion(s2, a2)
+  | TEnum(s1, a1), TEnum(s2, a2) ->
+      s1 = s2 && a1 = a2
+  | _, _ ->
+      false
+
 (** Check whether two types are compatible. *)
 
 let compatible_types mode env t1 t2 =
@@ -427,7 +463,6 @@ let sizeof_union env members =
    We lay out fields consecutively, inserting padding to preserve
    their alignment.
    Not done here but in composite_info_decl: rounding size to alignment. *)
-
 let sizeof_struct env members =
   let rec sizeof_rec ofs = function
   | [] ->
@@ -449,6 +484,26 @@ let sizeof_struct env members =
       end
   in sizeof_rec 0 members
 
+(* Simplified version to compute offsets on structs without bitfields *)
+let struct_layout env members =
+  let rec struct_layout_rec mem ofs = function
+    | [] ->
+        mem
+    | [ { fld_typ = TArray(_, None, _) } as m ] ->
+      (* C99: ty[] allowed as last field *)
+      begin match alignof env m.fld_typ with
+      | Some a -> ( m.fld_name,align ofs a)::mem
+      | None -> []
+      end
+    | m :: rem ->
+        match alignof env m.fld_typ, sizeof env m.fld_typ with
+        | Some a, Some s -> 
+            let offset = align ofs a in
+            struct_layout_rec ((m.fld_name,offset)::mem) (offset + s) rem
+        | _, _ -> []
+  in struct_layout_rec [] 0 members
+
+
 (* Determine whether a type is incomplete *)
 
 let incomplete_type env t =
diff --git a/cparser/Cutil.mli b/cparser/Cutil.mli
index b1f77944..a322bfb1 100644
--- a/cparser/Cutil.mli
+++ b/cparser/Cutil.mli
@@ -80,6 +80,8 @@ val combine_types : attr_handling -> Env.t -> typ -> typ -> typ option
      with the same meaning as for [compatible_types].
      When two sets of attributes are compatible, the result of
      [combine_types] carries the union of these two sets of attributes. *)
+val equal_types : Env.t -> typ -> typ -> bool
+   (* Check that the two given types are equal up to typedef use *)
 
 (* Size and alignment *)
 
@@ -105,6 +107,8 @@ val composite_info_decl:
   Env.t -> struct_or_union -> attributes -> Env.composite_info
 val composite_info_def:
   Env.t -> struct_or_union -> attributes -> field list -> Env.composite_info
+val struct_layout:
+  Env.t -> field list -> (string * int) list
 
 (* Type classification functions *)
 
diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index 820f90f5..4d3d1d02 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -56,9 +56,11 @@ let elab_loc l = (l.filename, l.lineno)
 
 let top_declarations = ref ([] : globdecl list)
 
-let emit_elab loc td =
+let emit_elab ?(enter:bool=true) env loc td =
   let loc = elab_loc loc in
-  top_declarations := { gdesc = td; gloc = loc } :: !top_declarations
+  let dec ={ gdesc = td; gloc = loc } in
+  if enter then  Debug.insert_global_declaration env dec;
+  top_declarations := dec :: !top_declarations
 
 let reset() = top_declarations := []
 
@@ -556,9 +558,9 @@ and elab_parameters env params =
   | _ ->
       (* Prototype introduces a new scope *)
       let (vars, _) = mmap elab_parameter (Env.new_scope env) params in
-      (* Catch special case f(void) *)
+      (* Catch special case f(t) where t is void or a typedef to void *)
       match vars with
-        | [ ( {name=""}, TVoid _) ] -> Some []
+        | [ ( {name=""}, t) ] when is_void_type env t -> Some []
         | _ -> Some vars
 
 (* Elaboration of a function parameter *)
@@ -730,7 +732,7 @@ and elab_struct_or_union only kind loc tag optmembers attrs env =
       (* finishing the definition of an incomplete struct or union *)
       let (ci', env') = elab_struct_or_union_info kind loc env members attrs in
       (* Emit a global definition for it *)
-      emit_elab loc (Gcompositedef(kind, tag', attrs, ci'.ci_members));
+      emit_elab env' loc (Gcompositedef(kind, tag', attrs, ci'.ci_members));
       (* Replace infos but keep same ident *)
       (tag', Env.add_composite env' tag' ci')
   | Some(tag', {ci_sizeof = Some _}), Some _
@@ -745,7 +747,7 @@ and elab_struct_or_union only kind loc tag optmembers attrs env =
       (* enter it with a new name *)
       let (tag', env') = Env.enter_composite env tag ci in
       (* emit it *)
-      emit_elab loc (Gcompositedecl(kind, tag', attrs));
+      emit_elab env' loc (Gcompositedecl(kind, tag', attrs));
       (tag', env')
   | _, Some members ->
       (* definition of a complete struct or union *)
@@ -753,12 +755,12 @@ and elab_struct_or_union only kind loc tag optmembers attrs env =
       (* enter it, incomplete, with a new name *)
       let (tag', env') = Env.enter_composite env tag ci1 in
       (* emit a declaration so that inner structs and unions can refer to it *)
-      emit_elab loc (Gcompositedecl(kind, tag', attrs));
+      emit_elab env' loc (Gcompositedecl(kind, tag', attrs));
       (* elaborate the members *)
       let (ci2, env'') =
         elab_struct_or_union_info kind loc env' members attrs in
       (* emit a definition *)
-      emit_elab loc (Gcompositedef(kind, tag', attrs, ci2.ci_members));
+      emit_elab env'' loc (Gcompositedef(kind, tag', attrs, ci2.ci_members));
       (* Replace infos but keep same ident *)
       (tag', Env.add_composite env'' tag' ci2)
 
@@ -809,7 +811,7 @@ and elab_enum only loc tag optmembers attrs env =
       let (dcls, env') = elab_members env 0L members in
       let info = { ei_members = dcls; ei_attr = attrs } in
       let (tag', env'') = Env.enter_enum env' tag info in
-      emit_elab loc (Genumdef(tag', attrs, dcls));
+      emit_elab env' loc (Genumdef(tag', attrs, dcls));
       (tag', env'')
 
 (* Elaboration of a naked type, e.g. in a cast *)
@@ -1312,7 +1314,7 @@ let elab_expr loc env a =
             let ty = TFun(TInt(IInt, []), None, false, []) in
             (* Emit an extern declaration for it *)
             let id = Env.fresh_ident n in
-            emit_elab loc (Gdecl(Storage_extern, id, ty, None));
+            emit_elab env loc (Gdecl(Storage_extern, id, ty, None));
             { edesc = EVar id; etyp = ty }
         | _ -> elab a1 in
       let bl = List.map elab al in
@@ -1784,13 +1786,21 @@ let enter_typedefs loc env sto dl =
   List.fold_left (fun env (s, ty, init) ->
     if init <> NO_INIT then
       error loc "initializer in typedef";
-    if redef Env.lookup_typedef env s then
-      error loc "redefinition of typedef '%s'" s;
-    if redef Env.lookup_ident env s then
-      error loc "redefinition of identifier '%s' as different kind of symbol" s;
-    let (id, env') = Env.enter_typedef env s ty in
-    emit_elab loc (Gtypedef(id, ty));
-    env') env dl
+    match previous_def Env.lookup_typedef env s with
+    | Some (s',ty') ->
+        if equal_types env ty ty' then begin
+          warning loc "redefinition of typedef '%s'" s;
+          env
+        end else begin
+          error loc "redefinition of typedef '%s' with different type" s;
+          env
+        end
+    | None ->
+        if redef Env.lookup_ident env s then
+          error loc "redefinition of identifier '%s' as different kind of symbol" s;
+        let (id, env') = Env.enter_typedef env s ty in
+        emit_elab env loc (Gtypedef(id, ty));
+        env') env dl
 
 let enter_or_refine_ident local loc env s sto ty =
   if redef Env.lookup_typedef env s then
@@ -1865,7 +1875,7 @@ let enter_decdefs local loc env sto dl =
       ((sto', id, ty', init') :: decls, env2)
     else begin
       (* Global definition *)
-      emit_elab loc (Gdecl(sto', id, ty', init'));
+      emit_elab env2 loc (Gdecl(sto', id, ty', init'));
       (decls, env2)
     end in
   let (decls, env') = List.fold_left enter_decdef ([], env) dl in
@@ -1899,7 +1909,7 @@ let elab_fundef env spec name body loc =
   let (func_ty, func_init) = __func__type_and_init s in
   let (func_id, _, env3,func_ty) =
     enter_or_refine_ident true loc env2 "__func__" Storage_static func_ty in
-  emit_elab loc (Gdecl(Storage_static, func_id, func_ty, Some func_init));
+  emit_elab ~enter:false env3 loc (Gdecl(Storage_static, func_id, func_ty, Some func_init));
   (* Elaborate function body *)
   let body' = !elab_funbody_f ty_ret env3 body in
   (* Special treatment of the "main" function *)
@@ -1925,7 +1935,7 @@ let elab_fundef env spec name body loc =
       fd_vararg = vararg;
       fd_locals = [];
       fd_body = body'' } in
-  emit_elab loc (Gfundef fn);
+  emit_elab env1 loc (Gfundef fn);
   env1
 
 let elab_kr_fundef env spec name params defs body loc =
@@ -1997,7 +2007,7 @@ let rec elab_definition (local: bool) (env: Env.t) (def: Cabs.definition)
 
   (* pragma *)
   | PRAGMA(s, loc) ->
-      emit_elab loc (Gpragma s);
+      emit_elab env loc (Gpragma s);
       ([], env)
 
 and elab_definitions local env = function
@@ -2224,7 +2234,9 @@ and elab_block_body env ctx sl =
   | DEFINITION def :: sl1 ->
       let (dcl, env') = elab_definition true env def in
       let loc = elab_loc (get_definitionloc def) in
-      List.map (fun d -> {sdesc = Sdecl d; sloc = loc}) dcl
+      List.map (fun ((sto,id,ty,_) as d) ->
+        Debug.insert_local_declaration sto id ty loc;
+        {sdesc = Sdecl d; sloc = loc}) dcl
       @ elab_block_body env' ctx sl1
   | s :: sl1 ->
       let s' = elab_stmt env ctx s in
@@ -2250,20 +2262,3 @@ let elab_file prog =
   reset();
   ignore (elab_definitions false (Builtins.environment()) prog);
   elaborated_program()
-(*
-  let rec inf = Datatypes.S inf in
-  let ast:Cabs.definition list =
-    Obj.magic
-      (match Parser.translation_unit_file inf (Lexer.tokens_stream lb) with
-         | Parser.Parser.Inter.Fail_pr ->
-             (* Theoretically impossible : implies inconsistencies
-                between grammars. *)
-             Cerrors.fatal_error "Internal error while parsing"
-         | Parser.Parser.Inter.Timeout_pr -> assert false
-         | Parser.Parser.Inter.Parsed_pr (ast, _ ) -> ast)
-  in
-  reset();
-  ignore (elab_definitions false (Builtins.environment()) ast);
-  elaborated_program()
-*)
-
diff --git a/cparser/Lexer.mll b/cparser/Lexer.mll
index 82e6589c..5cfe74fd 100644
--- a/cparser/Lexer.mll
+++ b/cparser/Lexer.mll
@@ -20,16 +20,14 @@ open Pre_parser_aux
 open Cabshelper
 open Camlcoq
 
-let contexts : string list list ref = ref []
-let lexicon : (string, Cabs.cabsloc -> token) Hashtbl.t = Hashtbl.create 0
+module SMap = Map.Make(String)
 
-let init filename channel : Lexing.lexbuf =
-  assert (!contexts = []);
-  Hashtbl.clear lexicon;
-  List.iter
-    (fun (key, builder) -> Hashtbl.add lexicon key builder)
-    [ 
-      ("_Alignas", fun loc -> ALIGNAS loc);
+let contexts_stk : (Cabs.cabsloc -> token) SMap.t list ref = ref []
+
+let init_ctx =
+  List.fold_left (fun ctx (key, builder) -> SMap.add key builder ctx)
+    SMap.empty
+    [ ("_Alignas", fun loc -> ALIGNAS loc);
       ("_Alignof", fun loc -> ALIGNOF loc);
       ("_Bool", fun loc -> UNDERSCORE_BOOL loc);
       ("__alignof", fun loc -> ALIGNOF loc);
@@ -85,37 +83,42 @@ let init filename channel : Lexing.lexbuf =
       ("void", fun loc -> VOID loc);
       ("volatile", fun loc -> VOLATILE loc);
       ("while", fun loc -> WHILE loc);
-    ];
-
-  push_context := begin fun () -> contexts := []::!contexts end;
-  pop_context := begin fun () ->
-    match !contexts with
-      | [] -> assert false
-      | t::q -> List.iter (Hashtbl.remove lexicon) t;
-                contexts := q
+      (let id = "__builtin_va_list" in
+       id, fun loc -> TYPEDEF_NAME (id, ref TypedefId, loc))]
+
+let _ =
+  (* See comments in pre_parser_aux.ml *)
+  open_context := begin fun () ->
+    contexts_stk := List.hd !contexts_stk::!contexts_stk
   end;
 
- declare_varname := begin fun id ->
-   if Hashtbl.mem lexicon id then begin
-     Hashtbl.add lexicon id (fun loc -> VAR_NAME (id, ref VarId, loc));
-     match !contexts with
-       | [] -> ()
-       | t::q -> contexts := (id::t)::q
-     end
+  close_context := begin fun () ->
+    contexts_stk := List.tl !contexts_stk
   end;
 
-  declare_typename := begin fun id ->
-    Hashtbl.add lexicon id (fun loc -> TYPEDEF_NAME (id, ref TypedefId, loc));
-    match !contexts with
-      | [] -> ()
-      | t::q -> contexts := (id::t)::q
+  save_contexts_stk := begin fun () ->
+    let save = !contexts_stk in
+    fun () -> contexts_stk := save
   end;
 
-  !declare_typename "__builtin_va_list";
+  declare_varname := begin fun id ->
+    match !contexts_stk with
+    (* This is the default, so there is no need to have an entry in this case. *)
+    | ctx::stk -> contexts_stk := SMap.remove id ctx::stk
+    | [] -> assert false
+  end;
+
+  declare_typename := begin fun id ->
+    match !contexts_stk with
+    | ctx::stk ->
+      contexts_stk :=
+        SMap.add id (fun loc -> TYPEDEF_NAME (id, ref TypedefId, loc)) ctx::stk
+    | [] -> assert false
+  end
 
+let init filename channel : Lexing.lexbuf =
   let lb = Lexing.from_channel channel in
-  lb.lex_curr_p <-
-    {lb.lex_curr_p with pos_fname = filename; pos_lnum = 1};
+  lb.lex_curr_p <- {lb.lex_curr_p with pos_fname = filename; pos_lnum = 1};
   lb
 
 let currentLoc =
@@ -337,8 +340,8 @@ rule initial = parse
   | ","                           { COMMA(currentLoc lexbuf) }
   | "."                           { DOT(currentLoc lexbuf) }
   | identifier as id              {
-        try Hashtbl.find lexicon id (currentLoc lexbuf)
-        with Not_found -> VAR_NAME (id, ref VarId, currentLoc lexbuf) }
+      try SMap.find id (List.hd !contexts_stk) (currentLoc lexbuf)
+      with Not_found -> VAR_NAME (id, ref VarId, currentLoc lexbuf) }
   | eof                           { EOF }
   | _ as c                        { fatal_error lexbuf "invalid symbol %C" c }
 
@@ -435,7 +438,7 @@ and singleline_comment = parse
   open Parser
   open Aut.GramDefs
 
-  let tokens_stream lexbuf : token coq_Stream =
+  let tokens_stream filename channel : token coq_Stream =
     let tokens = Queue.create () in
     let lexer_wraper lexbuf : Pre_parser.token =
       let res =
@@ -447,8 +450,11 @@ and singleline_comment = parse
       Queue.push res tokens;
       res
     in
+    let lexbuf = Lexing.from_channel channel in
+    lexbuf.lex_curr_p <- {lexbuf.lex_curr_p with pos_fname = filename; pos_lnum = 1};
+    contexts_stk := [init_ctx];
     Pre_parser.translation_unit_file lexer_wraper lexbuf;
-    assert (!contexts = []);
+    assert (List.length !contexts_stk = 1);
     let rec compute_token_stream () =
       let loop t v =
         Cons (Coq_existT (t, Obj.magic v), Lazy.from_fun compute_token_stream)
diff --git a/cparser/Parse.ml b/cparser/Parse.ml
index c9564c08..cfa95688 100644
--- a/cparser/Parse.ml
+++ b/cparser/Parse.ml
@@ -24,12 +24,7 @@ let transform_program t p name =
   (run_pass Unblock.program 'b'
   (run_pass Bitfields.program 'f'
   p)))) in
-  let debug = 
-    if !Clflags.option_g && Configuration.advanced_debug then
-      Some (CtoDwarf.program_to_dwarf p p1 name)
-    else
-      None in
-  (Rename.program p1 (Filename.chop_suffix name ".c")),debug
+  (Rename.program p1 (Filename.chop_suffix name ".c"))
 
 let parse_transformations s =
   let t = ref CharSet.empty in
@@ -46,15 +41,19 @@ let parse_transformations s =
 let preprocessed_file transfs name sourcefile =
   Cerrors.reset();
   let ic = open_in sourcefile in
-  let p,d =
+  let p =
     try
       let t = parse_transformations transfs in
-      let lb = Lexer.init name ic in
       let rec inf = Datatypes.S inf in
       let ast : Cabs.definition list =
         Obj.magic
-          (match Timing.time2 "Parsing"
-                 Parser.translation_unit_file inf (Lexer.tokens_stream lb) with
+          (match Timing.time "Parsing"
+              (* The call to Lexer.tokens_stream results in the pre
+                 parsing of the entire file. This is non-negligeabe,
+                 so we cannot use Timing.time2 *)
+              (fun () ->
+                Parser.translation_unit_file inf (Lexer.tokens_stream name ic)) ()
+           with
              | Parser.Parser.Inter.Fail_pr ->
                  (* Theoretically impossible : implies inconsistencies
                     between grammars. *)
@@ -65,6 +64,6 @@ let preprocessed_file transfs name sourcefile =
       Timing.time2 "Emulations" transform_program t p1 name
     with
     | Cerrors.Abort ->
-        [],None in
+        [] in
   close_in ic;
-  if Cerrors.check_errors() then None,None else Some p,d
+  if Cerrors.check_errors() then None else Some p
diff --git a/cparser/Parse.mli b/cparser/Parse.mli
index ac8feb70..58c3cfb9 100644
--- a/cparser/Parse.mli
+++ b/cparser/Parse.mli
@@ -15,7 +15,7 @@
 
 (* Entry point for the library: parse, elaborate, and transform *)
 
-val preprocessed_file: string -> string -> string -> C.program option * DwarfTypes.dw_entry option
+val preprocessed_file: string -> string -> string -> C.program option
 
 (* first arg: desired transformations
    second arg: source file name before preprocessing
diff --git a/cparser/Unblock.ml b/cparser/Unblock.ml
index 91f50552..c6646b5c 100644
--- a/cparser/Unblock.ml
+++ b/cparser/Unblock.ml
@@ -177,16 +177,89 @@ and expand_init islocal env i =
   in
     expand i
 
+(* Insertion of debug annotation, for -g mode *)
+
+let debug_id = Env.fresh_ident "__builtin_debug"
+let debug_ty =
+  TFun(TVoid [], Some [Env.fresh_ident "kind", TInt(IInt, [])], true, [])
+
+let debug_annot kind args =
+  { sloc = no_loc;
+    sdesc = Sdo { 
+      etyp = TVoid [];
+      edesc = ECall({edesc = EVar debug_id; etyp = debug_ty},
+                    intconst kind IInt :: args)
+    }
+  }
+
+let string_const str =
+  let c = CStr str in { edesc = EConst c; etyp = type_of_constant c }
+
+let integer_const n =
+  intconst (Int64.of_int n) IInt
+
+(* Line number annotation:
+      __builtin_debug(1, "#line:filename:lineno") *)
+(* TODO: consider
+      __builtin_debug(1, "filename", lineno)
+   instead. *)
+
+let debug_lineno (filename, lineno) =
+  debug_annot 1L
+    [string_const (Printf.sprintf "#line:%s:%d" filename lineno)]
+
+(* Scope annotation:
+      __builtin_debug(6, "", scope1, scope2, ..., scopeN)
+*)
+
+let empty_string = string_const ""
+
+let curr_fun_id = ref 0
+
+let debug_var_decl ctx id =
+  Debug.add_lvar_scope !curr_fun_id id (List.hd ctx)
+
+let debug_scope ctx =
+  debug_annot 6L (empty_string :: List.rev_map integer_const ctx)
+
+(* Add line number debug annotation if the line number changes.
+   Add scope debug annotation regardless. *)
+
+
+let add_lineno ctx prev_loc this_loc s =
+  if !Clflags.option_g then
+    sseq no_loc (debug_scope ctx)
+      (if this_loc <> prev_loc && this_loc <> no_loc
+       then sseq no_loc (debug_lineno this_loc) s
+       else s)
+  else s
+
+(* Generate fresh scope identifiers, for blocks that contain at least
+   one declaration *)
+
+let block_contains_decl sl =
+  List.exists
+    (function {sdesc = Sdecl _} -> true | _ -> false)
+    sl
+
+let next_scope_id = ref 0
+
+let new_scope_id () =
+  incr next_scope_id; !next_scope_id
+
 (* Process a block-scoped variable declaration.
    The variable is entered in [local_variables].
    The initializer, if any, is converted into assignments and
    prepended to [k]. *)
 
-let process_decl loc env (sto, id, ty, optinit) k =
+let process_decl loc env ctx (sto, id, ty, optinit) k =
   let ty' = remove_const env ty in
   local_variables := (sto, id, ty', None) :: !local_variables;
+  debug_var_decl ctx id;
+  (* TODO: register the fact that id is declared in scope ctx *)
   match optinit with
-  | None -> k
+  | None ->
+      k
   | Some init ->
       let init' = expand_init true env init in
       let l = local_initializer env { edesc = EVar id; etyp = ty' } init' [] in
@@ -194,57 +267,90 @@ let process_decl loc env (sto, id, ty, optinit) k =
 
 (* Simplification of blocks within a statement *)
 
-let rec unblock_stmt env s =
+let rec unblock_stmt env ctx ploc s =
   match s.sdesc with
   | Sskip -> s
   | Sdo e ->
-      {s with sdesc = Sdo(expand_expr true env e)}
+      add_lineno ctx ploc s.sloc
+        {s with sdesc = Sdo(expand_expr true env e)}
   | Sseq(s1, s2) ->
-      {s with sdesc = Sseq(unblock_stmt env s1, unblock_stmt env s2)}
+      {s with sdesc = Sseq(unblock_stmt env ctx ploc s1,
+                           unblock_stmt env ctx s1.sloc s2)}
   | Sif(e, s1, s2) -> 
-      {s with sdesc = Sif(expand_expr true env e,
-                          unblock_stmt env s1, unblock_stmt env s2)}
+      add_lineno ctx ploc s.sloc
+        {s with sdesc = Sif(expand_expr true env e,
+                            unblock_stmt env ctx s.sloc s1,
+                            unblock_stmt env ctx s.sloc s2)}
   | Swhile(e, s1) -> 
-      {s with sdesc = Swhile(expand_expr true env e, unblock_stmt env s1)}
+      add_lineno ctx ploc s.sloc
+        {s with sdesc = Swhile(expand_expr true env e,
+                               unblock_stmt env ctx s.sloc s1)}
   | Sdowhile(s1, e) ->
-      {s with sdesc = Sdowhile(unblock_stmt env s1, expand_expr true env e)}
+      add_lineno ctx ploc s.sloc
+        {s with sdesc = Sdowhile(unblock_stmt env ctx s.sloc s1,
+                                 expand_expr true env e)}
   | Sfor(s1, e, s2, s3) ->
-      {s with sdesc = Sfor(unblock_stmt env s1,
-                           expand_expr true env e,
-                           unblock_stmt env s2,
-                           unblock_stmt env s3)}
+      add_lineno ctx ploc s.sloc
+        {s with sdesc = Sfor(unblock_stmt env ctx s.sloc s1,
+                             expand_expr true env e,
+                             unblock_stmt env ctx s.sloc s2,
+                             unblock_stmt env ctx s.sloc s3)}
   | Sbreak -> s
   | Scontinue -> s
   | Sswitch(e, s1) ->
-      {s with sdesc = Sswitch(expand_expr true env e, unblock_stmt env s1)}
+      add_lineno ctx ploc s.sloc
+        {s with sdesc = Sswitch(expand_expr true env e,
+                                unblock_stmt env ctx s.sloc s1)}
   | Slabeled(lbl, s1) -> 
-      {s with sdesc = Slabeled(lbl, unblock_stmt env s1)}
-  | Sgoto lbl -> s
-  | Sreturn None -> s
+      add_lineno ctx ploc s.sloc
+        {s with sdesc = Slabeled(lbl, unblock_stmt env ctx s.sloc s1)}
+  | Sgoto lbl ->
+      add_lineno ctx ploc s.sloc s
+  | Sreturn None ->
+      add_lineno ctx ploc s.sloc s
   | Sreturn (Some e) ->
-      {s with sdesc = Sreturn(Some (expand_expr true env e))}
-  | Sblock sl -> unblock_block env sl
-  | Sdecl d -> assert false
+      add_lineno ctx ploc s.sloc 
+        {s with sdesc = Sreturn(Some (expand_expr true env e))}
+  | Sblock sl ->
+      let ctx' =
+        if block_contains_decl sl
+        then
+          let id = new_scope_id () in
+          (match ctx with
+          | [] -> Debug.enter_function_scope !curr_fun_id id
+          | a::_ -> Debug.enter_scope !curr_fun_id a id);
+          id:: ctx
+        else ctx in
+      unblock_block env ctx' ploc sl
+  | Sdecl d ->
+      assert false
   | Sasm(attr, template, outputs, inputs, clob) ->
       let expand_asm_operand (lbl, cstr, e) =
         (lbl, cstr, expand_expr true env e) in
-      {s with sdesc = Sasm(attr, template,
-                           List.map expand_asm_operand outputs,
-                           List.map expand_asm_operand inputs, clob)}
+      add_lineno ctx ploc s.sloc 
+        {s with sdesc = Sasm(attr, template,
+                             List.map expand_asm_operand outputs,
+                             List.map expand_asm_operand inputs, clob)}
 
 
-and unblock_block env = function
+and unblock_block env ctx ploc = function
   | [] -> sskip
   | {sdesc = Sdecl d; sloc = loc} :: sl ->
-      process_decl loc env d (unblock_block env sl)
+      add_lineno ctx ploc loc
+        (process_decl loc env ctx d
+           (unblock_block env ctx loc sl))
   | s :: sl ->
-      sseq s.sloc (unblock_stmt env s) (unblock_block env sl)
+      sseq s.sloc (unblock_stmt env ctx ploc s)
+                  (unblock_block env ctx s.sloc sl)
 
 (* Simplification of blocks and compound literals within a function *)
 
 let unblock_fundef env f =
   local_variables := [];
-  let body = unblock_stmt env f.fd_body in
+  next_scope_id := 0;
+  curr_fun_id:= f.fd_name.stamp;
+  (* TODO: register the parameters as being declared in function scope *)
+  let body = unblock_stmt env [] no_loc f.fd_body in
   let decls = !local_variables in
   local_variables := [];
   { f with fd_locals = f.fd_locals @ decls; fd_body = body }
@@ -299,4 +405,5 @@ let rec unblock_glob env accu = function
 (* Entry point *)
 
 let program p =
+  {gloc = no_loc; gdesc = Gdecl(Storage_extern, debug_id, debug_ty, None)} ::
   unblock_glob (Builtins.environment()) [] p
diff --git a/cparser/pre_parser.mly b/cparser/pre_parser.mly
index 44a06f8a..e73cc22a 100644
--- a/cparser/pre_parser.mly
+++ b/cparser/pre_parser.mly
@@ -57,9 +57,14 @@
 
 (* These precedences declarations solve the conflict in the following declaration :
 
-int f(int (a));
+   int f(int (a));
 
-when a is a TYPEDEF_NAME. It is specified by 6.7.5.3 11.
+   when a is a TYPEDEF_NAME. It is specified by 6.7.5.3 11.
+
+   WARNING: These precedence declarations tend to silently solve other
+   conflicts. So, if you change the grammar (especially or
+   statements), you should check that without these declarations, it
+   has ONLY ONE CONFLICT.
 *)
 %nonassoc TYPEDEF_NAME
 %nonassoc highPrec
@@ -89,25 +94,30 @@ string_literals_list:
 | string_literals_list STRING_LITERAL
     {}
 
-(* WARNING : because of the lookahead token, the context might
-   be pushed or popped one token after the position of this
-   non-terminal !
+(* WARNING : because of the lookahead token, the context might be
+   opened or closed one token after the position of this non-terminal !
 
-   Pushing too late is not dangerous for us, because this does not
+   Opening too late is not dangerous for us, because this does not
    change the token stream. However, we have to make sure the
-   lookahead token present just after popping is not an identifier.
- *)
+   lookahead token present just after closing/declaring/restoring is
+   not an identifier. An easy way to check that is to look at the
+   follow set of the non-terminal in question. The follow sets are
+   given by menhir with option -lg 3. *)
+
+%inline nop: (* empty *) { }
 
-push_context:
-  (* empty *)%prec highPrec { !push_context () }
-pop_context:
-  (* empty *) { !pop_context () }
+open_context:
+  (* empty *)%prec highPrec { !open_context () }
+close_context:
+  (* empty *) { !close_context () }
 in_context(nt):
-  push_context x = nt pop_context { x }
+  open_context x = nt close_context { x }
+
+save_contexts_stk:
+  (* empty *) { !save_contexts_stk () }
 
 declare_varname(nt):
   i = nt { declare_varname i; i }
-
 declare_typename(nt):
   i = nt { declare_typename i; i }
 
@@ -267,39 +277,20 @@ constant_expression:
 | conditional_expression
     {}
 
+(* We separate two kinds of declarations: the typedef declaration and
+   the normal declarations. This makes possible to distinguish /in the
+   grammar/ whether a declaration should add a typename or a varname
+   in the context.  There is an other difference between
+   [init_declarator_list] and [typedef_declarator_list]: the later
+   cannot contain an initialization (this is an error to initialize a
+   typedef). *)
+
 declaration:
 | declaration_specifiers init_declarator_list? SEMICOLON
     {}
 | declaration_specifiers_typedef typedef_declarator_list? SEMICOLON
     {}
 
-declaration_specifiers_no_type:
-| storage_class_specifier_no_typedef declaration_specifiers_no_type?
-| type_qualifier declaration_specifiers_no_type?
-| function_specifier declaration_specifiers_no_type?
-    {}
-
-declaration_specifiers_no_typedef_name:
-| storage_class_specifier_no_typedef declaration_specifiers_no_typedef_name?
-| type_qualifier declaration_specifiers_no_typedef_name?
-| function_specifier declaration_specifiers_no_typedef_name?
-| type_specifier_no_typedef_name declaration_specifiers_no_typedef_name?
-    {}
-
-declaration_specifiers:
-| declaration_specifiers_no_type? i = TYPEDEF_NAME declaration_specifiers_no_type?
-    { set_id_type i TypedefId }
-| declaration_specifiers_no_type? type_specifier_no_typedef_name declaration_specifiers_no_typedef_name?
-    {}
-
-declaration_specifiers_typedef:
-| declaration_specifiers_no_type? TYPEDEF declaration_specifiers_no_type? i = TYPEDEF_NAME declaration_specifiers_no_type?
-| declaration_specifiers_no_type? i = TYPEDEF_NAME declaration_specifiers_no_type? TYPEDEF declaration_specifiers_no_type?
-    { set_id_type i TypedefId }
-| declaration_specifiers_no_type? TYPEDEF declaration_specifiers_no_type? type_specifier_no_typedef_name declaration_specifiers_no_typedef_name?
-| declaration_specifiers_no_type? type_specifier_no_typedef_name declaration_specifiers_no_typedef_name? TYPEDEF declaration_specifiers_no_typedef_name?
-    {}
-
 init_declarator_list:
 | init_declarator
 | init_declarator_list COMMA init_declarator
@@ -326,6 +317,67 @@ storage_class_specifier_no_typedef:
 | REGISTER
     {}
 
+(* [declaration_specifiers_no_type] matches declaration specifiers
+   that do not contain either "typedef" nor type specifiers. *)
+declaration_specifiers_no_type:
+| storage_class_specifier_no_typedef declaration_specifiers_no_type?
+| type_qualifier declaration_specifiers_no_type?
+| function_specifier declaration_specifiers_no_type?
+    {}
+
+(* [declaration_specifiers_no_typedef_name] matches declaration
+   specifiers that contain neither "typedef" nor a typedef name
+   (i.e. type specifier declared using a previous "typedef
+   keyword"). *)
+declaration_specifiers_no_typedef_name:
+| storage_class_specifier_no_typedef declaration_specifiers_no_typedef_name?
+| type_qualifier declaration_specifiers_no_typedef_name?
+| function_specifier declaration_specifiers_no_typedef_name?
+| type_specifier_no_typedef_name declaration_specifiers_no_typedef_name?
+    {}
+
+(* [declaration_specifiers_no_type] matches declaration_specifiers
+   that do not contains "typedef". Moreover, it makes sure that it
+   contains either one typename and not other type specifier or no
+   typename.
+
+   This is a weaker condition than 6.7.2 2. It is necessary to enforce
+   this in the grammar to disambiguate the example in 6.7.7 6:
+
+   typedef signed int t;
+   struct tag {
+     unsigned t:4;
+     const t:5;
+   };
+
+   The first field is a named t, while the second is unnamed of type t.
+*)
+declaration_specifiers:
+| declaration_specifiers_no_type? i = TYPEDEF_NAME declaration_specifiers_no_type?
+    { set_id_type i TypedefId }
+| declaration_specifiers_no_type? type_specifier_no_typedef_name declaration_specifiers_no_typedef_name?
+    {}
+
+(* This matches declaration_specifiers that do contains once the
+   "typedef" keyword. To avoid conflicts, we also encode the
+   constraint described in the comment for [declaration_specifiers]. *)
+declaration_specifiers_typedef:
+| declaration_specifiers_no_type?
+  TYPEDEF declaration_specifiers_no_type?
+  i = TYPEDEF_NAME declaration_specifiers_no_type?
+| declaration_specifiers_no_type?
+  i = TYPEDEF_NAME declaration_specifiers_no_type?
+  TYPEDEF declaration_specifiers_no_type?
+    { set_id_type i TypedefId }
+| declaration_specifiers_no_type?
+  TYPEDEF declaration_specifiers_no_type?
+  type_specifier_no_typedef_name declaration_specifiers_no_typedef_name?
+| declaration_specifiers_no_type?
+  type_specifier_no_typedef_name declaration_specifiers_no_typedef_name?
+  TYPEDEF declaration_specifiers_no_typedef_name?
+    {}
+
+(* A type specifier which is not a typedef name. *)
 type_specifier_no_typedef_name:
 | VOID
 | CHAR
@@ -366,6 +418,8 @@ struct_declaration:
 | specifier_qualifier_list struct_declarator_list? SEMICOLON
     {}
 
+(* As in the standard, except it also encodes the constraint described
+   in the comment above [declaration_specifiers]. *)
 specifier_qualifier_list:
 | type_qualifier_list? i = TYPEDEF_NAME type_qualifier_list?
     { set_id_type i TypedefId }
@@ -460,6 +514,10 @@ function_specifier:
 | INLINE
     {}
 
+(* The semantic action returned by [declarator] is a pair of the
+   identifier being defined and an option of the context stack that
+   has to be restored if entering the body of the function being
+   defined, if so. *)
 declarator:
 | pointer? x = direct_declarator attribute_specifier_list
     { x }
@@ -470,9 +528,11 @@ direct_declarator:
 | LPAREN x = declarator RPAREN
 | x = direct_declarator LBRACK type_qualifier_list? assignment_expression? RBRACK
     { x }
-| x = direct_declarator LPAREN l=in_context(parameter_type_list?) RPAREN
+| x = direct_declarator LPAREN
+    open_context parameter_type_list? restore_fun = save_contexts_stk
+    close_context RPAREN
     { match snd x with
-      | None -> (fst x, Some (match l with None -> [] | Some l -> l))
+      | None -> (fst x, Some restore_fun)
       | Some _ -> x }
 
 pointer:
@@ -542,26 +602,51 @@ designator:
 | DOT i = general_identifier
     { set_id_type i OtherId }
 
-statement_finish:
-| labeled_statement(statement_finish)
-| compound_statement
-| expression_statement
-| selection_statement_finish
-| iteration_statement(statement_finish)
-| jump_statement
-| asm_statement
-    {}
+(* The grammar of statements is replicated three times.
 
-statement_intern:
-| labeled_statement(statement_intern)
-| compound_statement
-| expression_statement
-| selection_statement_intern
-| iteration_statement(statement_intern)
-| jump_statement
-| asm_statement
-    {}
+   [statement_finish_close] should close the current context just
+   before its last token.
 
+   [statement_finish_noclose] should not close the current context. It
+   should modify it only if this modification actually changes the
+   context of the current block.
+
+   [statement_intern_close] is like [statement_finish_close], except
+   it cannot reduce to a single-branch if statement.
+*)
+
+statement_finish_close:
+| labeled_statement(statement_finish_close)
+| compound_statement(nop)
+| expression_statement(close_context)
+| selection_statement_finish(nop)
+| iteration_statement(nop,statement_finish_close)
+| jump_statement(close_context)
+| asm_statement(close_context)
+    {}
+
+statement_finish_noclose:
+| labeled_statement(statement_finish_noclose)
+| compound_statement(open_context)
+| expression_statement(nop)
+| selection_statement_finish(open_context)
+| iteration_statement(open_context,statement_finish_close)
+| jump_statement(nop)
+| asm_statement(nop)
+    {}
+
+statement_intern_close:
+| labeled_statement(statement_intern_close)
+| compound_statement(nop)
+| expression_statement(close_context)
+| selection_statement_intern_close
+| iteration_statement(nop,statement_intern_close)
+| jump_statement(close_context)
+| asm_statement(close_context)
+    {}
+
+(* [labeled_statement(last_statement)] has the same effect on contexts
+   as [last_statement]. *)
 labeled_statement(last_statement):
 | i = general_identifier COLON last_statement
     { set_id_type i OtherId }
@@ -569,10 +654,14 @@ labeled_statement(last_statement):
 | DEFAULT COLON last_statement
     {}
 
-compound_statement:
-| LBRACE in_context(block_item_list?) RBRACE
+(* [compound_statement] uses a local context and closes it before its
+   last token. It uses [openc] to open this local context if needed.
+   That is, if a local context has already been opened, [openc] = [nop],
+   otherwise, [openc] = [open_context]. *)
+compound_statement(openc):
+| LBRACE openc block_item_list? close_context RBRACE
     {}
-| LBRACE in_context(block_item_list?) error
+| LBRACE openc block_item_list? close_context error
     { unclosed "{" "}" $startpos($1) $endpos }
 
 block_item_list:
@@ -581,47 +670,99 @@ block_item_list:
 
 block_item:
 | declaration
-| statement_finish
+| statement_finish_noclose
 | PRAGMA
     {}
 
-expression_statement:
-| expression? SEMICOLON
+(* [expression_statement], [jump_statement] and [asm_statement] close
+   the local context if needed, depending of the close parameter. If
+   there is no local context, [close] = [nop]. Otherwise,
+   [close] = [close_context]. *)
+expression_statement(close):
+| expression? close SEMICOLON
     {}
 
-selection_statement_finish:
-| IF LPAREN expression RPAREN statement_finish
-| IF LPAREN expression RPAREN statement_intern ELSE statement_finish
-| SWITCH LPAREN expression RPAREN statement_finish
+jump_statement(close):
+| GOTO i = general_identifier close SEMICOLON
+    { set_id_type i OtherId }
+| CONTINUE close SEMICOLON
+| BREAK close SEMICOLON
+| RETURN expression? close SEMICOLON
     {}
 
-selection_statement_intern:
-| IF LPAREN expression RPAREN statement_intern ELSE statement_intern
-| SWITCH LPAREN expression RPAREN statement_intern
+asm_statement(close):
+| ASM asm_attributes LPAREN string_literals_list asm_arguments RPAREN close SEMICOLON
     {}
 
-iteration_statement(stmt):
-| WHILE LPAREN expression RPAREN stmt
-| DO statement_finish WHILE LPAREN expression RPAREN SEMICOLON
-| FOR LPAREN expression? SEMICOLON expression? SEMICOLON expression? RPAREN stmt
-| FOR LPAREN push_context declaration expression? SEMICOLON expression? RPAREN stmt pop_context
+(* [selection_statement_finish] and [selection_statement_intern] use a
+   local context and close it before their last token.
+
+   [selection_statement_finish(openc)] uses [openc] to open this local
+   context if needed. That is, if a local context has already been
+   opened, [openc] = [nop], otherwise, [openc] = [open_context].
+
+   [selection_statement_intern_close] is always called with a local
+   context openned. It closes it before its last token.  *)
+
+(* It should be noted that the token [ELSE] should be lookaheaded
+   /outside/ of the local context because if the lookaheaded token is
+   not [ELSE], then this is the end of the statement.
+
+   This is especially important to parse correctly the following
+   example:
+
+     typedef int a;
+
+     int f() {
+       for(int a; ;)
+         if(1);
+       a * x;
+     }
+
+   However, if the lookahead token is [ELSE], we should parse the
+   second branch in the same context as the first branch, so we have
+   to reopen the previously closed context. This is the reason for the
+   save/restore system.
+*)
+
+if_else_statement_begin(openc):
+| IF openc LPAREN expression RPAREN restore_fun = save_contexts_stk
+  statement_intern_close
+    { restore_fun () }
+
+selection_statement_finish(openc):
+| IF openc LPAREN expression RPAREN save_contexts_stk statement_finish_close
+| if_else_statement_begin(openc) ELSE statement_finish_close
+| SWITCH openc LPAREN expression RPAREN statement_finish_close
     {}
 
-jump_statement:
-| GOTO i = general_identifier SEMICOLON
-    { set_id_type i OtherId }
-| CONTINUE SEMICOLON
-| BREAK SEMICOLON
-| RETURN expression? SEMICOLON
+selection_statement_intern_close:
+| if_else_statement_begin(nop) ELSE statement_intern_close
+| SWITCH LPAREN expression RPAREN statement_intern_close
     {}
 
-asm_statement:
-| ASM asm_attributes LPAREN string_literals_list asm_arguments RPAREN SEMICOLON
+(* [iteration_statement] uses a local context and closes it before
+   their last token.
+
+   [iteration_statement] uses [openc] to open this local context if
+   needed. That is, if a local context has already been opened,
+   [openc] = [nop], otherwise, [openc] = [open_context].
+
+   [last_statement] is either [statement_intern_close] or
+   [statement_finish_close]. That is, it should /always/ close the
+   local context. *)
+
+iteration_statement(openc,last_statement):
+| WHILE openc LPAREN expression RPAREN last_statement
+| DO open_context statement_finish_close WHILE
+    openc LPAREN expression RPAREN close_context SEMICOLON
+| FOR openc LPAREN expression? SEMICOLON expression? SEMICOLON expression? RPAREN last_statement
+| FOR openc LPAREN declaration expression? SEMICOLON expression? RPAREN last_statement
     {}
 
 asm_attributes:
 | /* empty */
-| CONST asm_attributes    
+| CONST asm_attributes
 | VOLATILE asm_attributes
     {}
 
@@ -679,22 +820,14 @@ function_definition_begin:
 | declaration_specifiers pointer? x=direct_declarator
     { match x with
       | (_, None) -> $syntaxerror
-      | (i, Some l) ->
-	declare_varname i;
-	!push_context ();
-	List.iter (fun x ->
-	  match x with
-	    | None -> ()
-	    | Some i -> declare_varname i
-	  ) l
+      | (i, Some restore_fun) -> restore_fun ()
     }
-| declaration_specifiers pointer? x=direct_declarator 
-  LPAREN params=identifier_list RPAREN in_context(declaration_list)
+| declaration_specifiers pointer? x=direct_declarator
+  LPAREN params=identifier_list RPAREN open_context declaration_list
     { match x with
       | (_, Some _) -> $syntaxerror
       | (i, None) ->
 	declare_varname i;
-	!push_context ();
 	List.iter declare_varname params
     }
 
@@ -711,8 +844,7 @@ declaration_list:
     { }
 
 function_definition:
-| function_definition_begin LBRACE block_item_list? pop_context RBRACE
+| function_definition_begin LBRACE block_item_list? close_context RBRACE
     { }
-| function_definition_begin LBRACE block_item_list? pop_context error
+| function_definition_begin LBRACE block_item_list? close_context error
     { unclosed "{" "}" $startpos($2) $endpos }
-
diff --git a/cparser/pre_parser_aux.ml b/cparser/pre_parser_aux.ml
index 55dfdfde..c6b48608 100644
--- a/cparser/pre_parser_aux.ml
+++ b/cparser/pre_parser_aux.ml
@@ -18,8 +18,20 @@ type identifier_type =
   | TypedefId
   | OtherId
 
-let push_context:(unit -> unit) ref= ref (fun () -> assert false)
-let pop_context:(unit -> unit) ref = ref (fun () -> assert false)
+(* These functions push and pop a context on the contexts stack. *)
+let open_context:(unit -> unit) ref = ref (fun () -> assert false)
+let close_context:(unit -> unit) ref = ref (fun () -> assert false)
 
+(* Applying once this functions saves the whole contexts stack, and
+   applying it the second time restores it.
+
+   This is mainly used to rollback the context stack to a previous
+   state. This is usefull for example when we pop too much contexts at
+   the end of the first branch of an if statement. See
+   pre_parser.mly. *)
+let save_contexts_stk:(unit -> (unit -> unit)) ref = ref (fun _ -> assert false)
+
+(* Change the context at the top of the top stack of context, by
+   changing an identifier to be a varname or a typename*)
 let declare_varname:(string -> unit) ref = ref (fun _ -> assert false)
 let declare_typename:(string -> unit) ref = ref (fun _ -> assert false)