check.ml

(* 
 *
 * Copyright (c) 2001-2002, 
 *  George C. Necula    <necula@cs.berkeley.edu>
 *  Scott McPeak        <smcpeak@cs.berkeley.edu>
 *  Wes Weimer          <weimer@cs.berkeley.edu>
 * All rights reserved.
 * 
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are
 * met:
 *
 * 1. Redistributions of source code must retain the above copyright
 * notice, this list of conditions and the following disclaimer.
 *
 * 2. Redistributions in binary form must reproduce the above copyright
 * notice, this list of conditions and the following disclaimer in the
 * documentation and/or other materials provided with the distribution.
 *
 * 3. The names of the contributors may not be used to endorse or promote
 * products derived from this software without specific prior written
 * permission.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS
 * IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED
 * TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
 * PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER
 * OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
 * EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
 * PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
 * PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
 * LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
 * NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
 * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 *
 *)

(* A consistency checker for CIL *)
open Cil
module E = Errormsg
module H = Hashtbl
open Pretty


(* A few parameters to customize the checking *)
type checkFlags = 
    NoCheckGlobalIds   (* Do not check that the global ids have the proper 
                        * hash value *)
    | IgnoreInstructions of (instr -> bool) (* Ignore the specified instructions *)
        
let checkGlobalIds = ref true
let ignoreInstr = ref (fun i -> false)

  (* Attributes must be sorted *)
type ctxAttr = 
    CALocal                             (* Attribute of a local variable *)
  | CAGlobal                            (* Attribute of a global variable *)
  | CAType                              (* Attribute of a type *)

let valid = ref true

let warn fmt =
  valid := false;
  Cil.warn ("CIL invariant broken: "^^fmt)

let warnContext fmt =
  valid := false;
  Cil.warnContext fmt

let checkAttributes (attrs: attribute list) : unit = 
  let rec loop lastname = function
      [] -> ()
    | Attr(an, _) :: resta -> 
        if an < lastname then
          ignore (warn "Attributes not sorted");
        loop an resta
  in
  loop "" attrs


  (* Keep track of defined types *)
let typeDefs : (string, typ) H.t = H.create 117


  (* Keep track of all variables names, enum tags and type names *)
let varNamesEnv : (string, unit) H.t = H.create 117

  (* We also keep a map of variables indexed by id, to ensure that only one 
   * varinfo has a given id *)
let varIdsEnv: (int, varinfo) H.t = H.create 117

  (* And keep track of all varinfo's to check the uniqueness of the 
   * identifiers *)
let allVarIds: (int, varinfo) H.t = H.create 117

 (* Also keep a list of environments. We place an empty string in the list to 
  * mark the start of a local environment (i.e. a function) *)
let varNamesList : (string * int) list ref = ref []
let defineName s = 
  if s = "" then
    E.s (bug "Empty name\n"); 
  if H.mem varNamesEnv s then
    ignore (warn "Multiple definitions for %s" s);
  H.add varNamesEnv s ()

let defineVariable vi = 
  (* E.log "saw %s: %d\n" vi.vname vi.vid; *)
  defineName vi.vname;
  varNamesList := (vi.vname, vi.vid) :: !varNamesList;
  (* Check the id *)
  if H.mem allVarIds vi.vid then
    ignore (warn "Id %d is already defined (%s)" vi.vid vi.vname);
  H.add allVarIds vi.vid vi;
  (* And register it in the current scope also *)
  H.add varIdsEnv vi.vid vi

(* Check that a varinfo has already been registered *)
let checkVariable vi = 
  try
    (* Check in the current scope only *)
    let old = H.find varIdsEnv vi.vid in
    if vi != old then begin
      if vi.vname = old.vname then
        ignore (warnContext "varinfos for %s not shared" vi.vname)
      else
        ignore (warnContext "variables %s and %s share id %d"
                  vi.vname old.vname vi.vid )
    end
  with Not_found -> 
    ignore (warn "Unknown id (%d) for %s" vi.vid vi.vname)


let startEnv () = 
  varNamesList := ("", -1) :: !varNamesList

let endEnv () = 
  let rec loop = function
      [] -> E.s (bug "Cannot find start of env")
    | ("", _) :: rest -> varNamesList := rest
    | (s, id) :: rest -> begin
        H.remove varNamesEnv s;
        H.remove varIdsEnv id;
        loop rest
    end
  in
  loop !varNamesList
    

    
(* The current function being checked *)
let currentReturnType : typ ref = ref voidType

(* A map of labels in the current function *)
let labels: (string, unit) H.t = H.create 17

(* A list of statements seen in the current function *)
let statements: stmt list ref = ref []

(* A list of the targets of Gotos *)
let gotoTargets: (string * stmt) list ref = ref []

(*** TYPES ***)
(* Cetain types can only occur in some contexts, so keep a list of context *)
type ctxType = 
    CTStruct                            (* In a composite type *)
  | CTUnion
  | CTFArg                              (* In a function argument type *)
  | CTFRes                              (* In a function result type *)
  | CTArray                             (* In an array type *)
  | CTPtr                               (* In a pointer type *)
  | CTExp                               (* In an expression, as the type of 
                                         * the result of binary operators, or 
                                         * in a cast *)
  | CTSizeof                            (* In a sizeof *)
  | CTDecl                              (* In a typedef, or a declaration *)

let d_context () = function
    CTStruct -> text "CTStruct"
  | CTUnion -> text "CTUnion"
  | CTFArg -> text "CTFArg"
  | CTFRes -> text "CTFRes"
  | CTArray -> text "CTArray"
  | CTPtr -> text "CTPtr"
  | CTExp -> text "CTExp"
  | CTSizeof -> text "CTSizeof"
  | CTDecl -> text "CTDecl"


(* Keep track of all tags that we use. For each tag remember also the info 
 * structure and a flag whether it was actually defined or just used. A 
 * forward declaration acts as a definition. *)
type defuse = 
    Defined (* We actually have seen a definition of this tag *)
  | Forward (* We have seen a forward declaration for it. This is done using 
             * a GType with an empty type name *)
  | Used    (* Only uses *)
let compUsed : (int, compinfo * defuse ref) H.t = H.create 117
let enumUsed : (string, enuminfo * defuse ref) H.t = H.create 117
let typUsed  : (string, typeinfo * defuse ref) H.t = H.create 117
 
(* For composite types we also check that the names are unique *)
let compNames : (string, unit) H.t = H.create 17
    

let typeSigIgnoreConst (t : typ) : typsig =
  let attrFilter (attr : attribute) : bool =
    match attr with
      | Attr ("const", []) -> false
      | _ -> true
  in
  typeSigWithAttrs (List.filter attrFilter) t


  (* Check a type *)
let rec checkType (t: typ) (ctx: ctxType) = 
  (* Check that it appears in the right context *)
  let rec checkContext = function
      TVoid _ -> ctx = CTPtr || ctx = CTFRes || ctx = CTDecl || ctx = CTSizeof
    | TNamed (ti, a) -> checkContext ti.ttype
    | TArray _ -> 
        (ctx = CTStruct || ctx = CTUnion 
         || ctx = CTSizeof || ctx = CTDecl || ctx = CTArray || ctx = CTPtr)
    | TFun _ -> 
        if ctx = CTSizeof && !msvcMode then
          (ignore(warn "sizeof(function) is not defined in MSVC."); false)
        else
          ctx = CTPtr || ctx = CTDecl || ctx = CTSizeof
    | _ -> true
  in
  if not (checkContext t) then 
    ignore (warn "Type (%a) used in wrong context. Expected context: %a"
              d_plaintype t d_context ctx);
  match t with
    (TVoid a | TBuiltin_va_list a) -> checkAttributes a
  | TInt (ik, a) -> checkAttributes a
  | TFloat (_, a) -> checkAttributes a
  | TPtr (t, a) -> checkAttributes a;  checkType t CTPtr

  | TNamed (ti, a) ->
      checkAttributes a;
      if ti.tname = "" then 
        ignore (warnContext "Using a typeinfo for an empty-named type");
      checkTypeInfo Used ti

  | TComp (comp, a) ->
      checkAttributes a;
      (* Mark it as a forward. We'll check it later. If we try to check it 
       * now we might encounter undefined types *)
      checkCompInfo Used comp


  | TEnum (enum, a) -> begin
      checkAttributes a;
      checkEnumInfo Used enum
  end

  | TArray(bt, len, a) -> 
      checkAttributes a;
      checkType bt CTArray;
      (match len with
        None -> ()
      | Some l -> begin
          let t = checkExp true l in
          if not (isIntegralType t) then
            E.s (bug "Type of array length is not integer")
      end)

  | TFun (rt, targs, isva, a) -> 
      checkAttributes a;
      checkType rt CTFRes;
      List.iter 
        (fun (an, at, aa) -> 
          checkType at CTFArg;
          checkAttributes aa) (argsToList targs)

(* Check that a type is a promoted integral type *)
and checkIntegralType (t: typ) = 
  checkType t CTExp;
  if not (isIntegralType t) then
    ignore (warn "Non-integral type")

(* Check that a type is a promoted arithmetic type *)
and checkArithmeticType (t: typ) = 
  checkType t CTExp;
  if not (isArithmeticType t) then
    ignore (warn "Non-arithmetic type")

(* Check that a type is a pointer type *)
and checkPointerType (t: typ) = 
  checkType t CTExp;
  if not (isPointerType t) then
    ignore (warn "Non-pointer type")

(* Check that a type is a scalar type *)
and checkScalarType (t: typ) = 
  checkType t CTExp;
  if not (isScalarType t) then
    ignore (warn "Non-scalar type")


and typeMatch (t1: typ) (t2: typ) = 
  if !Cil.insertImplicitCasts then begin
    (* Allow mismatches in const-ness, so that string literals can be used
       as char*s *)
    if typeSigIgnoreConst t1 <> typeSigIgnoreConst t2 then
      match unrollType t1, unrollType t2 with
        (* Allow free interchange of TInt and TEnum *)
        TInt (ik, _), TEnum (ei, _) when ik = ei.ekind -> ()
      | TEnum (ei, _), TInt (ik, _) when ik = ei.ekind -> ()
          
      (* Allow unspecified array lengths - this happens with
       * flexible array members *)
      | TArray (t, None, _), TArray (t', _, _)
      | TArray (t, _, _), TArray (t', None, _) -> typeMatch t t'
      | _, _ -> ignore (warn "Type mismatch:@!    %a@!and %a@!"
                           d_type t1 d_type t2)
  end else begin
    (* Many casts are missing.  For now, just skip this check. *)
  end

and checkCompInfo (isadef: defuse) comp = 
  let fullname = compFullName comp in
  try
    let oldci, olddef = H.find compUsed comp.ckey in
    (* Check that it is the same *)
    if oldci != comp then 
      ignore (warnContext "compinfo for %s not shared" fullname);
    (match !olddef, isadef with 
    | Defined, Defined -> 
        ignore (warnContext "Multiple definition of %s" fullname)
    | _, Defined -> olddef := Defined
    | Defined, _ -> ()
    | _, Forward -> olddef := Forward
    | _, _ -> ())
  with Not_found -> begin (* This is the first time we see it *)
    (* Check that the name is not empty *)
    if comp.cname = "" then 
      E.s (bug "Compinfo with empty name");
    (* Check that the name is unique *)
    if H.mem compNames fullname then
      ignore (warn "Duplicate name %s" fullname);
    (* Add it to the map before we go on *)
    H.add compUsed comp.ckey (comp, ref isadef);
    H.add compNames fullname ();
    (* Do not check the compinfo unless this is a definition. Otherwise you 
     * might run into undefined types. *)
    if isadef = Defined then begin
      checkAttributes comp.cattr;
      let fctx = if comp.cstruct then CTStruct else CTUnion in
      let rec checkField f =
        if not 
            (f.fcomp == comp &&  (* Each field must share the self cell of 
             * the host *)
             f.fname <> "") then
          ignore (warn "Self pointer not set in field %s of %s" 
                    f.fname fullname);
        checkType f.ftype fctx;
        (* Check the bitfields *)
        (match unrollType f.ftype, f.fbitfield with
        | TInt (ik, a), Some w -> 
            checkAttributes a;
            if w < 0 || w > bitsSizeOf (TInt(ik, a)) then
              ignore (warn "Wrong width (%d) in bitfield" w)
        | _, Some w -> 
            ignore (E.error "Bitfield on a non integer type")
        | _ -> ());
        checkAttributes f.fattr
      in
      List.iter checkField comp.cfields
    end
  end


and checkEnumInfo (isadef: defuse) enum = 
  if enum.ename = "" then 
    E.s (bug "Enuminfo with empty name");
  try
    let oldei, olddef = H.find enumUsed enum.ename in
    (* Check that it is the same *)
    if oldei != enum then 
      ignore (warnContext "enuminfo for %s not shared" enum.ename);
    (match !olddef, isadef with 
      Defined, Defined -> 
        ignore (warnContext "Multiple definition of enum %s" enum.ename)
    | _, Defined -> olddef := Defined
    | Defined, _ -> ()
    | _, Forward -> olddef := Forward
    | _, _ -> ())
  with Not_found -> begin (* This is the first time we see it *)
    (* Add it to the map before we go on *)
    H.add enumUsed enum.ename (enum, ref isadef);
    checkAttributes enum.eattr;
    List.iter (fun (tn, _, _) -> defineName tn) enum.eitems;
  end

and checkTypeInfo (isadef: defuse) ti = 
  try
    let oldti, olddef = H.find typUsed ti.tname in
    (* Check that it is the same *)
    if oldti != ti then 
      ignore (warnContext "typeinfo for %s not shared" ti.tname);
    (match !olddef, isadef with 
      Defined, Defined -> 
        ignore (warnContext "Multiple definition of type %s" ti.tname)
    | Defined, Used -> ()
    | Used, Defined -> 
        ignore (warnContext "Use of type %s before its definition" ti.tname)
    | _, _ -> 
        ignore (warnContext "Bug in checkTypeInfo for %s" ti.tname))
  with Not_found -> begin (* This is the first time we see it *)
    if ti.tname = "" then
      ignore (warnContext "typeinfo with empty name");
    checkType ti.ttype CTDecl;
    (* Add it to the map before we go on *)
    H.add typUsed ti.tname (ti, ref isadef);
  end

(* Check an lvalue. If isconst then the lvalue appears in a context where 
 * only a compile-time constant can appear. Return the type of the lvalue. 
 * See the typing rule from cil.mli *)
and checkLval (isconst: bool) (forAddrof: bool) (lv: lval) : typ = 
  match lv with
    Var vi, off -> 
      checkVariable vi; 
      checkOffset vi.vtype off

  | Mem addr, off -> begin
      if isconst && not forAddrof then
        ignore (warn "Memory operation in constant");
      let ta = checkExp false addr in
      match unrollType ta with
        TPtr (t, _) -> checkOffset t off
      | _ -> E.s (bug "Mem on a non-pointer")
  end

(* Check an offset. The basetype is the type of the object referenced by the 
 * base. Return the type of the lvalue constructed from a base value of right 
 * type and the offset. See the typing rules from cil.mli *)
and checkOffset basetyp : offset -> typ = function
    NoOffset -> basetyp
  | Index (ei, o) -> 
      checkIntegralType (checkExp false ei);
      begin
        match unrollType basetyp with
          TArray (t, _, _) -> checkOffset t o
        | t -> E.s (bug "typeOffset: Index on a non-array: %a" d_plaintype t)
      end

  | Field (fi, o) -> 
      (* Now check that the host is shared propertly *)
      checkCompInfo Used fi.fcomp;
      (* Check that this exact field is part of the host *)
      if not (List.exists (fun f -> f == fi) fi.fcomp.cfields) then
        ignore (warn "Field %s not part of %s" 
                  fi.fname (compFullName fi.fcomp));
      checkOffset fi.ftype o
        
and checkExpType (isconst: bool) (e: exp) (t: typ) =
  let t' = checkExp isconst e in (* compute the type *)
  (* ignore(E.log "checkType %a %a\n" d_plainexp e d_plaintype t); *)
  typeMatch t' t

(* Check an expression. isconst specifies if the expression occurs in a 
 * context where only a compile-time constant can occur. Return the computed 
 * type of the expression *)
and checkExp (isconst: bool) (e: exp) : typ = 
  E.withContext 
    (fun _ -> dprintf "check%s: %a" 
        (if isconst then "Const" else "Exp") d_exp e)
    (fun _ ->
      match e with
      | Const(_) -> typeOf e
      | Lval(lv) -> 
          if isconst then
            ignore (warn "Lval in constant");
          checkLval isconst false lv

      | SizeOf(t) -> begin
          (* Sizeof cannot be applied to certain types *)
          checkType t CTSizeof;
          (match unrollType t with
            (TFun _ ) -> 
              ignore (warn "Invalid operand for sizeof")
          | _ ->());
          typeOf e
      end
      | SizeOfE(e') ->
          (* The expression in a sizeof can be anything *)
          let te = checkExp false e' in
          checkType te CTSizeof;
          typeOf e

      | SizeOfStr s ->  typeOf e

      | AlignOf(t) -> begin
          (* Sizeof cannot be applied to certain types *)
          checkType t CTSizeof;
          typeOf e
      end
      | AlignOfE(e') ->
          (* The expression in an AlignOfE can be anything *)
          let te = checkExp false e' in
          checkType te CTSizeof;
          typeOf e

      | UnOp (Neg, e, tres) -> 
          checkArithmeticType tres; checkExpType isconst e tres; tres

      | UnOp (BNot, e, tres) -> 
          checkIntegralType tres; checkExpType isconst e tres; tres

      | UnOp (LNot, e, tres) -> 
          let te = checkExp isconst e in
          checkScalarType te;
          checkIntegralType tres; (* Must check that t is well-formed *)
          typeMatch tres intType;
          tres

      | BinOp (bop, e1, e2, tres) -> begin
          let t1 = checkExp isconst e1 in
          let t2 = checkExp isconst e2 in
          match bop with
            (Mult | Div) -> 
              typeMatch t1 t2; checkArithmeticType tres; 
              typeMatch t1 tres; tres
          | (Eq|Ne|Lt|Le|Ge|Gt) -> 
              typeMatch t1 t2; checkArithmeticType t1; 
              typeMatch tres intType; tres
          | Mod|BAnd|BOr|BXor -> 
              typeMatch t1 t2; checkIntegralType tres;
              typeMatch t1 tres; tres
          | LAnd | LOr -> 
              checkScalarType t1; checkScalarType t2;
              typeMatch tres intType; tres
          | Shiftlt | Shiftrt -> 
              typeMatch t1 tres; checkIntegralType t1; 
              checkIntegralType t2; tres
          | (PlusA | MinusA) -> 
                typeMatch t1 t2; typeMatch t1 tres;
                checkArithmeticType tres; tres
          | (PlusPI | MinusPI | IndexPI) -> 
              checkPointerType tres;
              typeMatch t1 tres;
              checkIntegralType t2;
              tres
          | MinusPP  -> 
              checkPointerType t1; checkPointerType t2;
              typeMatch t1 t2;
              typeMatch tres !ptrdiffType;
              tres
      end

      | Question (e1, e2, e3, tres) -> begin
          let t1 = checkExp isconst e1 in
          let t2 = checkExp isconst e2 in
          let t3 = checkExp isconst e3 in
          checkScalarType t1;
          typeMatch t2 t3;
          typeMatch t2 tres;
          tres
      end

      | AddrOf (lv) -> begin
          let tlv = checkLval isconst true lv in
          (* Only certain types can be in AddrOf *)
          match unrollType tlv with
          | TVoid _ -> 
              E.s (bug "AddrOf on improper type");
              
          | (TInt _ | TFloat _ | TPtr _ | TComp _ | TFun _ | TArray _ ) -> 
              TPtr(tlv, [])

          | TEnum (ei, _) -> TPtr(TInt(ei.ekind, []), [])
          | _ -> E.s (bug "AddrOf on unknown type")
      end

      | AddrOfLabel (gref) -> begin
          (* Find a label *)
          let lab =
            match List.filter (function Label _ -> true | _ -> false)
                  !gref.labels with
              Label (lab, _, _) :: _ -> lab
            | _ ->
                ignore (warn "Address of label to block without a label");
                "<missing label>"
          in
          (* Remember it as a target *)
          gotoTargets := (lab, !gref) :: !gotoTargets;
          voidPtrType
      end
      | StartOf lv -> begin
          let tlv = checkLval isconst true lv in
          match unrollType tlv with
            TArray (t,_, _) -> TPtr(t, [])
          | _ -> E.s (bug "StartOf on a non-array")
      end
            
      | CastE (tres, e) -> begin
          let et = checkExp isconst e in
          checkType tres CTExp;
          (* Not all types can be cast *)
          match unrollType et with
            TArray _ -> E.s (bug "Cast of an array type")
          | TFun _ -> E.s (bug "Cast of a function type")
          (* A TComp cast that changes the attributes is okay. *)
          (* | TComp _ -> E.s (bug "Cast of a composite type") *)
          | TVoid _ -> E.s (bug "Cast of a void type")
          | _ -> tres
      end)
    () (* The argument of withContext *)

and checkInit  (i: init) : typ = 
  E.withContext 
    (fun _ -> dprintf "checkInit: %a" d_init i)
    (fun _ ->
      match i with
        SingleInit e -> checkExp true e
(*
      | ArrayInit (bt, len, initl) -> begin
          checkType bt CTSizeof;
          if List.length initl > len then 
            ignore (warn "Too many initializers in array");
          List.iter (fun i -> checkInitType i bt) initl;
          TArray(bt, Some (integer len), [])
      end
*)
      | CompoundInit (ct, initl) -> begin
          checkType ct CTSizeof;
          (match unrollType ct with
            TArray(bt, elen, _) -> 
              let len =
                match elen with
                | None -> 0L
                | Some e -> (ignore (checkExp true e);
                match isInteger (constFold true e) with
                  Some len -> len
                | None -> 
                    ignore (warn "Array length is not a constant");
                    0L)
              in
              let rec loopIndex i = function
                  [] -> 
                    if i > len then 
                      ignore (warn "Wrong number of initializers in array")

                | (Index(Const(CInt64(i', _, _)), NoOffset), ei) :: rest -> 
                    if i' <> i then 
                      ignore (warn "Initializer for index %s when %s was expected"
                                (Int64.format "%d" i') (Int64.format "%d" i));
                    checkInitType ei bt;
                    loopIndex (Int64.succ i) rest
                | _ :: rest -> 
                    ignore (warn "Malformed initializer for array element")
              in
              loopIndex Int64.zero initl
          | TComp (comp, _) -> 
              if comp.cstruct then
                let rec loopFields 
                    (nextflds: fieldinfo list) 
                    (initl: (offset * init) list) : unit = 
                  match nextflds, initl with 
                    [], [] -> ()   (* We are done *)
                  | f :: restf, (Field(f', NoOffset), i) :: resti -> 
                      if f.fname <> f'.fname then 
                        ignore (warn "Expected initializer for field %s and found one for %s" f.fname f'.fname);
                      checkInitType i f.ftype;
                      loopFields restf resti
                  | [], _ :: _ -> 
                      ignore (warn "Too many initializers for struct")
                  | _ :: _, [] -> 
                      ignore (warn "Too few initializers for struct")
                  | _, _ -> 
                      ignore (warn "Malformed initializer for struct")
                in
                loopFields
                  (List.filter (fun f -> f.fname <> missingFieldName) 
                     comp.cfields) 
                  initl

              else (* UNION *)
                if comp.cfields == [] then begin
                  if initl != [] then 
                    ignore (warn "Initializer for empty union not empty");
                end else begin
                  match initl with 
                    [(Field(f, NoOffset), ei)] -> 
                      if f.fcomp != comp then 
                        ignore (bug "Wrong designator for union initializer");
                      if !msvcMode && f != List.hd comp.cfields then
                        ignore (warn "On MSVC you can only initialize the first field of a union");
                      checkInitType ei f.ftype
                      
                  | _ -> 
                      ignore (warn "Malformed initializer for union")
                end
          | _ -> 
              E.s (warn "Type of Compound is not array or struct or union"));
          ct
      end)
    () (* The arguments of withContext *)


and checkInitType (i: init) (t: typ) : unit = 
  let it = checkInit i in
  typeMatch it t
  
and checkStmt (s: stmt) = 
  E.withContext 
    (fun _ -> 
      (* Print context only for certain small statements *)
      match s.skind with 
        Loop _ | If _ | Switch _  -> nil
      | _ -> dprintf "checkStmt: %a" d_stmt s)
    (fun _ -> 
      (* Check the labels *)
      let checkLabel = function
          Label (ln, l, _) -> 
            if H.mem labels ln then
              ignore (warn "Multiply defined label %s" ln);
            H.add labels ln ()
        | Case (e, _) -> 
           let t = checkExp true e in
           if not (isIntegralType t) then
               E.s (bug "Type of case expression is not integer");
        | CaseRange (e1, e2, _) ->
           let t1 = checkExp true e1 in
           if not (isIntegralType t1) then
               E.s (bug "Type of case expression is not integer");
           let t2 = checkExp true e2 in
           if not (isIntegralType t2) then
               E.s (bug "Type of case expression is not integer");
        | _ -> () (* Not yet implemented *)
      in
      List.iter checkLabel s.labels;
      (* See if we have seen this statement before *)
      if List.memq s !statements then 
        ignore (warn "Statement is shared");
      (* Remember that we have seen this one *)
      statements := s :: !statements;
      match s.skind with
        Break _ | Continue _ -> ()
      | Goto (gref, l) -> 
          currentLoc := l;
          (* Find a label *)
          let lab = 
            match List.filter (function Label _ -> true | _ -> false) 
                  !gref.labels with
              Label (lab, _, _) :: _ -> lab
            | _ -> 
                ignore (warn "Goto to block without a label");
                "<missing label>"
          in
          (* Remember it as a target *)
          gotoTargets := (lab, !gref) :: !gotoTargets
      | ComputedGoto (e, l) ->
          currentLoc := l;
          let te = checkExp false e in
          typeMatch te voidPtrType
      | Return (re,l) -> begin
          currentLoc := l;
          match re, !currentReturnType with
            None, TVoid _  -> ()
          | _, TVoid _ -> ignore (warn "Invalid return value")
          | None, _ -> ignore (warn "Invalid return value")
          | Some re', rt' -> checkExpType false re' rt'
        end
      | Loop (b, l, _, _) -> checkBlock b
      | Block b -> checkBlock b
      | If (e, bt, bf, l) -> 
          currentLoc := l;
          let te = checkExp false e in
          checkScalarType te;
          checkBlock bt;
          checkBlock bf
      | Switch (e, b, cases, l) -> 
          currentLoc := l;
          let t = checkExp false e in
          if not (isIntegralType t) then
              E.s (bug "Type of switch expression is not integer");
          (* Remember the statements so far *)
          let prevStatements = !statements in
          checkBlock b;
          (* Now make sure that all the cases do occur in that block,
             and that no case is listed twice. *)
          let casesVisited : stmt list ref = ref [] in
          List.iter
            (fun c -> 
               (if List.memq c !casesVisited then
                  ignore (warnContext 
                            "Duplicate stmt in \"cases\" list of Switch.")
                else
                  casesVisited := c::!casesVisited);
              (* Make sure it is in there *)
              let rec findCase = function
                | l when l == prevStatements -> (* Not found *)
                    ignore (warnContext 
                              "Cannot find target of switch statement")
                | [] -> E.s (E.bug "Check: findCase")
                | c' :: rest when c == c' -> () (* Found *)
                | _ :: rest -> findCase rest
              in
              findCase !statements)
            cases;
      | TryFinally (b, h, l) -> 
          currentLoc := l;
          checkBlock b;
          checkBlock h

      | TryExcept (b, (il, e), h, l) -> 
          currentLoc := l;
          checkBlock b;
          List.iter checkInstr il;
          checkExpType false e intType;
          checkBlock h

      | Instr il -> List.iter checkInstr il)
    () (* argument of withContext *)

and checkBlock (b: block) : unit = 
  List.iter checkStmt b.bstmts


and checkInstr (i: instr) = 
  if !ignoreInstr i then ()
  else
  match i with 
  | Set (dest, e, l) -> 
      currentLoc := l;
      let t = checkLval false false dest in
      (* Not all types can be assigned to *)
      (match unrollType t with
        TFun _ -> ignore (warn "Assignment to a function type")
      | TArray _ -> ignore (warn "Assignment to an array type")
      | TVoid _ -> ignore (warn "Assignment to a void type")
      | _ -> ());
      checkExpType false e t
            
  | Call(dest, what, args, l) -> 
      currentLoc := l;
      let (rt, formals, isva, fnAttrs) = 
        match unrollType (checkExp false what) with
          TFun(rt, formals, isva, fnAttrs) -> rt, formals, isva, fnAttrs
        | _ -> E.s (bug "Call to a non-function")
      in
          (* Now check the return value*)
      (match dest, unrollType rt with
        None, TVoid _ -> ()
      (* Avoid spurious warnings for atomic builtins *)
      | Some _, TVoid [Attr ("overloaded", [])] -> ()
      | Some _, TVoid _ -> ignore (warn "void value is assigned")
      | None, _ -> () (* "Call of function is not assigned" *)
      | Some destlv, rt' -> 
          let desttyp = checkLval false false destlv in
          if typeSig desttyp <> typeSig rt then begin
            if not !Cabs2cil.doCollapseCallCast then
              ignore (warn
                        "Destination of Call does not match the return type.");
            (* Not all types can be assigned to *)
            (match unrollType desttyp with
              TFun _ -> ignore (warn "Assignment to a function type")
            | TArray _ -> ignore (warn "Assignment to an array type")
            | TVoid _ -> ignore (warn "Assignment to a void type")
            | _ -> ());
            (* Not all types can be cast *)
            (match unrollType rt' with
              TArray _ -> ignore (warn "Cast of an array type")
            | TFun _ -> ignore (warn "Cast of a function type")
            | TComp _ -> ignore (warn "Cast of a composite type")
            | TVoid _ -> ignore (warn "Cast of a void type")
                  
            | _ -> ())
          end);
          (* Now check the arguments *)
      let rec loopArgs formals args = 
        match formals, args with
          [], _ when (isva || args = []) -> ()
        | (fn,ft,_) :: formals, a :: args -> 
            checkExpType false a ft;
            loopArgs formals args
        | _, _ -> ignore (warn "Not enough arguments")
      in
      if formals <> None then
        loopArgs (argsToList formals) args
        
  | Asm _ -> ()  (* Not yet implemented *)
  
let rec checkGlobal = function
    GAsm _ -> ()
  | GPragma _ -> ()
  | GText _ -> ()
  | GType (ti, l) -> 
      currentLoc := l;
      E.withContext (fun _ -> dprintf "GType(%s)" ti.tname)
        (fun _ ->
          checkTypeInfo Defined ti;
          if ti.tname <> "" then defineName ti.tname)
        ()

  | GCompTag (comp, l) -> 
      currentLoc := l;
      checkCompInfo Defined comp;

  | GCompTagDecl (comp, l) -> 
      currentLoc := l;
      checkCompInfo Forward comp;

  | GEnumTag (enum, l) -> 
      currentLoc := l;
      checkEnumInfo Defined enum

  | GEnumTagDecl (enum, l) -> 
      currentLoc := l;
      checkEnumInfo Forward enum

  | GVarDecl (vi, l) -> 
      currentLoc := l;
      (* We might have seen it already *)
      E.withContext (fun _ -> dprintf "GVarDecl(%s)" vi.vname)
        (fun _ -> 
          (* If we have seen this vid already then it must be for the exact 
           * same varinfo *)
          if H.mem varIdsEnv vi.vid then
            checkVariable vi
          else begin
            defineVariable vi; 
            checkAttributes vi.vattr;
            checkType vi.vtype CTDecl;
            if not (vi.vglob &&
                    vi.vstorage <> Register) then
              E.s (bug "Invalid declaration of %s" vi.vname)
          end)
        ()
        
  | GVar (vi, init, l) -> 
      currentLoc := l;
      (* Maybe this is the first occurrence *)
      E.withContext (fun _ -> dprintf "GVar(%s)" vi.vname)
        (fun _ -> 
          checkGlobal (GVarDecl (vi, l));
          (* Check the initializer *)
          if vi.vinit != init then
              E.s (bug "GVar initializer doesn't match vinit (%s)" vi.vname);
          begin match init.init with
            None -> ()
          | Some i -> ignore (checkInitType i vi.vtype)
          end;
          (* Cannot be a function *)
          if isFunctionType vi.vtype then
            E.s (bug "GVar for a function (%s)\n" vi.vname);
          )
        ()
        

  | GFun (fd, l) -> begin
      currentLoc := l;
      (* Check if this is the first occurrence *)
      let vi = fd.svar in
      let fname = vi.vname in
      E.withContext (fun _ -> dprintf "GFun(%s)" fname)
        (fun _ -> 
          checkGlobal (GVarDecl (vi, l));
          (* Check that the argument types in the type are identical to the 
           * formals *)
          let rec loopArgs targs formals = 
            match targs, formals with
              [], [] -> ()
            | (fn, ft, fa) :: targs, fo :: formals -> 
                if fn <> fo.vname then 
                  ignore (warnContext 
                            "Formal %s not shared (expecting name %s) in %s" 
                            fo.vname fn fname);
                E.withContext (fun () -> text "formal "++ text fo.vname)
                  (fun () -> typeMatch ft fo.vtype)
                  ();
                if fa != fo.vattr then 
                  ignore (warnContext 
                            "Formal %s not shared (different attrs) in %s" 
                            fo.vname fname);
                loopArgs targs formals

            | _ -> 
                E.s (bug "Type has different number of formals for %s" 
                       fname)
          in
          begin match unrollType vi.vtype with
            TFun (rt, args, isva, a) -> begin
              currentReturnType := rt;
              loopArgs (argsToList args) fd.sformals
            end
          | _ -> E.s (bug "Function %s does not have a function type" 
                        fname)
          end;
          ignore (fd.smaxid >= 0 || E.s (bug "smaxid < 0 for %s" fname));
          (* Now start a new environment, in a finally clause *)
          begin try
            startEnv ();
            (* Do the locals *)
            let doLocal tctx v = 
              if v.vglob then
                ignore (warnContext
                          "Local %s has the vglob flag set" v.vname);
              if v.vstorage <> NoStorage && v.vstorage <> Register && v.vstorage <> Static then
                ignore (warnContext
                          "Local %s has storage %a\n" v.vname
                          d_storage v.vstorage);
              checkType v.vtype tctx;
              checkAttributes v.vattr;
              defineVariable v
            in
            List.iter (doLocal CTFArg) fd.sformals;
            List.iter (doLocal CTDecl) fd.slocals;
            statements := [];
            gotoTargets := [];
            checkBlock fd.sbody;
            H.clear labels;
            (* Now verify that we have scanned all targets *)
            List.iter 
              (fun (lab, t) -> if not (List.memq t !statements) then 
                ignore (warnContext
                          "Target of \"goto %s\" statement does not appear in function body" lab))
              !gotoTargets;
            statements := [];
            gotoTargets := [];
            (* Done *)
            endEnv ()
          with e -> 
            endEnv ();
            raise e
          end;
          ())
        () (* final argument of withContext *)
  end


let checkFile flags fl = 
  if !E.verboseFlag then ignore (E.log "Checking file %s\n" fl.fileName);
  valid := true;
  List.iter 
    (function
        NoCheckGlobalIds -> checkGlobalIds := false
      | IgnoreInstructions f -> ignoreInstr := f
    )
    flags;
  iterGlobals fl (fun g -> try checkGlobal g with _ -> ());
  (* Check that for all struct/union tags there is a definition *)
  H.iter 
    (fun k (comp, isadef) -> 
      if !isadef = Used then 
	begin
	  valid := false;
          ignore (E.warn "Compinfo %s is referenced but not defined" 
                    (compFullName comp))
	end)
    compUsed;
  (* Check that for all enum tags there is a definition *)
  H.iter 
    (fun k (enum, isadef) -> 
      if !isadef = Used then 
	begin
	  valid := false;
          ignore (E.warn "Enuminfo %s is referenced but not defined" 
                    enum.ename)
	end)
    enumUsed;
  (* Clean the hashes to let the GC do its job *)
  H.clear typeDefs;
  H.clear varNamesEnv;
  H.clear varIdsEnv;
  H.clear allVarIds;
  H.clear compNames;
  H.clear compUsed;
  H.clear enumUsed;
  H.clear typUsed;
  varNamesList := [];
  if !E.verboseFlag then 
    ignore (E.log "Finished checking file %s\n" fl.fileName);
  !valid