1
(**************************************************************************)
3
(* Copyright (C) 2001-2003, *)
4
(* George C. Necula <necula@cs.berkeley.edu> *)
5
(* Scott McPeak <smcpeak@cs.berkeley.edu> *)
6
(* Wes Weimer <weimer@cs.berkeley.edu> *)
7
(* Ben Liblit <liblit@cs.berkeley.edu> *)
8
(* All rights reserved. *)
10
(* Redistribution and use in source and binary forms, with or without *)
11
(* modification, are permitted provided that the following conditions *)
14
(* 1. Redistributions of source code must retain the above copyright *)
15
(* notice, this list of conditions and the following disclaimer. *)
17
(* 2. Redistributions in binary form must reproduce the above copyright *)
18
(* notice, this list of conditions and the following disclaimer in the *)
19
(* documentation and/or other materials provided with the distribution. *)
21
(* 3. The names of the contributors may not be used to endorse or *)
22
(* promote products derived from this software without specific prior *)
23
(* written permission. *)
25
(* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS *)
26
(* "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT *)
27
(* LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS *)
28
(* FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE *)
29
(* COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, *)
30
(* INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, *)
31
(* BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; *)
32
(* LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER *)
33
(* CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT *)
34
(* LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN *)
35
(* ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE *)
36
(* POSSIBILITY OF SUCH DAMAGE. *)
38
(* File modified by CEA (Commissariat � l'�nergie Atomique). *)
39
(**************************************************************************)
41
(* A consistency checker for CIL *)
49
(* A few parameters to customize the checking *)
51
NoCheckGlobalIds (* Do not check that the global ids have the proper
54
let checkGlobalIds = ref true
56
(* Attributes must be sorted *)
58
CALocal (* Attribute of a local variable *)
59
| CAGlobal (* Attribute of a global variable *)
60
| CAType (* Attribute of a type *)
72
let checkAttributes (attrs: attribute list) : unit =
73
let rec loop lastname = function
75
| Attr(an, _) :: resta ->
77
ignore (warn "Attributes not sorted");
83
(* Keep track of defined types *)
84
let typeDefs : (string, typ) H.t = H.create 117
87
(* Keep track of all variables names, enum tags and type names *)
88
let varNamesEnv : (string, unit) H.t = H.create 117
90
(* We also keep a map of variables indexed by id, to ensure that only one
91
* varinfo has a given id *)
92
let varIdsEnv: (int, varinfo) H.t = H.create 117
94
(* And keep track of all varinfo's to check the uniqueness of the
96
let allBases: (int, varinfo) H.t = H.create 117
98
(* Also keep a list of environments. We place an empty string in the list to
99
* mark the start of a local environment (i.e. a function) *)
100
let varNamesList : (string * int) list ref = ref []
103
E.s (bug "Empty name\n");
104
if H.mem varNamesEnv s then
105
ignore (warn "Multiple definitions for %s\n" s);
106
H.add varNamesEnv s ()
108
let defineVariable vi =
110
varNamesList := (vi.vname, vi.vid) :: !varNamesList;
112
if H.mem allBases vi.vid then
113
ignore (warn "Id %d is already defined (%s)\n" vi.vid
114
(!Cil.output_ident vi.vname));
115
H.add allBases vi.vid vi;
116
(* And register it in the current scope also *)
117
H.add varIdsEnv vi.vid vi
119
(* Check that a varinfo has already been registered *)
120
let checkVariable vi =
122
(* Check in the current scope only *)
123
if vi != H.find varIdsEnv vi.vid then
124
ignore (warnContext "varinfos for %s not shared\n"
125
(!Cil.output_ident vi.vname));
127
ignore (warn "Unknown id (%d) for %s\n" vi.vid
128
(!Cil.output_ident vi.vname))
132
varNamesList := ("", -1) :: !varNamesList
135
let rec loop = function
136
[] -> E.s (bug "Cannot find start of env")
137
| ("", _) :: rest -> varNamesList := rest
138
| (s, id) :: rest -> begin
139
H.remove varNamesEnv s;
140
H.remove varIdsEnv id;
148
(* The current function being checked *)
149
let currentReturnType : typ ref = ref voidType
151
(* A map of labels in the current function *)
152
let labels: (string, unit) H.t = H.create 17
154
(* A list of statements seen in the current function *)
155
let statements: stmt list ref = ref []
157
(* A list of the targets of Gotos *)
158
let gotoTargets: (string * stmt) list ref = ref []
161
(* Cetain types can only occur in some contexts, so keep a list of context *)
163
CTStruct (* In a composite type *)
165
| CTFArg (* In a function argument type *)
166
| CTFRes (* In a function result type *)
167
| CTArray (* In an array type *)
168
| CTPtr (* In a pointer type *)
169
| CTExp (* In an expression, as the type of
170
* the result of binary operators, or
172
| CTSizeof (* In a sizeof *)
173
| CTDecl (* In a typedef, or a declaration *)
175
let d_context () = function
176
CTStruct -> text "CTStruct"
177
| CTUnion -> text "CTUnion"
178
| CTFArg -> text "CTFArg"
179
| CTFRes -> text "CTFRes"
180
| CTArray -> text "CTArray"
181
| CTPtr -> text "CTPtr"
182
| CTExp -> text "CTExp"
183
| CTSizeof -> text "CTSizeof"
184
| CTDecl -> text "CTDecl"
187
(* Keep track of all tags that we use. For each tag remember also the info
188
* structure and a flag whether it was actually defined or just used. A
189
* forward declaration acts as a definition. *)
191
Defined (* We actually have seen a definition of this tag *)
192
| Forward (* We have seen a forward declaration for it. This is done using
193
* a GType with an empty type name *)
194
| Used (* Only uses *)
195
let compUsed : (int, compinfo * defuse ref) H.t = H.create 117
196
let enumUsed : (string, enuminfo * defuse ref) H.t = H.create 117
197
let typUsed : (string, typeinfo * defuse ref) H.t = H.create 117
199
(* For composite types we also check that the names are unique *)
200
let compNames : (string, unit) H.t = H.create 17
204
let rec checkType (t: typ) (ctx: ctxType) =
205
(* Check that it appears in the right context *)
206
let rec checkContext = function
207
TVoid _ -> ctx = CTPtr || ctx = CTFRes || ctx = CTDecl
208
| TNamed (ti, a) -> checkContext ti.ttype
210
(ctx = CTStruct || ctx = CTUnion
211
|| ctx = CTSizeof || ctx = CTDecl || ctx = CTArray || ctx = CTPtr)
212
| TComp _ -> ctx <> CTExp
215
if not (checkContext t) then
216
ignore (warn "Type (%a) used in wrong context. Expected context: %a"
217
d_plaintype t d_context ctx);
219
(TVoid a | TBuiltin_va_list a) -> checkAttributes a
220
| TInt (ik, a) -> checkAttributes a
221
| TFloat (_, a) -> checkAttributes a
222
| TPtr (t, a) -> checkAttributes a; checkType t CTPtr
226
if ti.tname = "" then
227
ignore (warnContext "Using a typeinfo for an empty-named type\n");
228
checkTypeInfo Used ti
232
(* Mark it as a forward. We'll check it later. If we try to check it
233
* now we might encounter undefined types *)
234
checkCompInfo Used comp
237
| TEnum (enum, a) -> begin
239
checkEnumInfo Used enum
242
| TArray(bt, len, a) ->
244
checkType bt CTArray;
248
let t = checkExp true l in
250
TInt((IInt|IUInt), _) -> ()
251
| _ -> E.s (bug "Type of array length is not integer")
254
| TFun (rt, targs, isva, a) ->
260
checkAttributes aa) (argsToList targs)
262
(* Check that a type is a promoted integral type *)
263
and checkIntegralType (t: typ) =
265
match unrollType t with
267
| _ -> ignore (warn "Non-integral type")
269
(* Check that a type is a promoted arithmetic type *)
270
and checkArithmeticType (t: typ) =
272
match unrollType t with
273
TInt _ | TFloat _ -> ()
274
| _ -> ignore (warn "Non-arithmetic type")
276
(* Check that a type is a promoted boolean type *)
277
and checkBooleanType (t: typ) =
279
match unrollType t with
280
TInt _ | TFloat _ | TPtr _ -> ()
281
| _ -> ignore (warn "Non-boolean type")
284
(* Check that a type is a pointer type *)
285
and checkPointerType (t: typ) =
287
match unrollType t with
289
| _ -> ignore (warn "Non-pointer type")
292
and typeMatch (t1: typ) (t2: typ) =
293
if typeSig t1 <> typeSig t2 then
294
match unrollType t1, unrollType t2 with
295
(* Allow free interchange of TInt and TEnum *)
296
TInt (IInt, _), TEnum _ -> ()
297
| TEnum _, TInt (IInt, _) -> ()
299
| _, _ -> ignore (warn "Type mismatch:@\n %a@!and %a@\n"
302
and checkCompInfo (isadef: defuse) comp =
303
let fullname = compFullName comp in
305
let oldci, olddef = H.find compUsed comp.ckey in
306
(* Check that it is the same *)
307
if oldci != comp then
308
ignore (warnContext "compinfo for %s not shared\n" fullname);
309
(match !olddef, isadef with
310
| Defined, Defined ->
311
ignore (warnContext "Multiple definition of %s\n" fullname)
312
| _, Defined -> olddef := Defined
314
| _, Forward -> olddef := Forward
316
with Not_found -> begin (* This is the first time we see it *)
317
(* Check that the name is not empty *)
318
if comp.cname = "" then
319
E.s (bug "Compinfo with empty name");
320
(* Check that the name is unique *)
321
if H.mem compNames fullname then
322
ignore (warn "Duplicate name %s" fullname);
323
(* Add it to the map before we go on *)
324
H.add compUsed comp.ckey (comp, ref isadef);
325
H.add compNames fullname ();
326
(* Do not check the compinfo unless this is a definition. Otherwise you
327
* might run into undefined types. *)
328
if isadef = Defined then begin
329
checkAttributes comp.cattr;
330
let fctx = if comp.cstruct then CTStruct else CTUnion in
331
let rec checkField f =
333
(f.fcomp == comp && (* Each field must share the self cell of
336
ignore (warn "Self pointer not set in field %s of %s"
338
checkType f.ftype fctx;
339
(* Check the bitfields *)
340
(match unrollType f.ftype, f.fbitfield with
341
| TInt (ik, a), Some w ->
343
if w < 0 || w >= bitsSizeOf (TInt(ik, a)) then
344
ignore (warn "Wrong width (%d) in bitfield" w)
346
ignore (E.error "Bitfield on a non integer type\n")
348
checkAttributes f.fattr
350
List.iter checkField comp.cfields
355
and checkEnumInfo (isadef: defuse) enum =
356
if enum.ename = "" then
357
E.s (bug "Enuminfo with empty name");
359
let oldei, olddef = H.find enumUsed enum.ename in
360
(* Check that it is the same *)
361
if oldei != enum then
362
ignore (warnContext "enuminfo for %s not shared\n" enum.ename);
363
(match !olddef, isadef with
365
ignore (warnContext "Multiple definition of enum %s\n" enum.ename)
366
| _, Defined -> olddef := Defined
368
| _, Forward -> olddef := Forward
370
with Not_found -> begin (* This is the first time we see it *)
371
(* Add it to the map before we go on *)
372
H.add enumUsed enum.ename (enum, ref isadef);
373
checkAttributes enum.eattr;
374
List.iter (fun (tn, _, _) -> defineName tn) enum.eitems;
377
and checkTypeInfo (isadef: defuse) ti =
379
let oldti, olddef = H.find typUsed ti.tname in
380
(* Check that it is the same *)
382
ignore (warnContext "typeinfo for %s not shared\n" ti.tname);
383
(match !olddef, isadef with
385
ignore (warnContext "Multiple definition of type %s\n" ti.tname)
386
| Defined, Used -> ()
388
ignore (warnContext "Use of type %s before its definition\n" ti.tname)
390
ignore (warnContext "Bug in checkTypeInfo for %s\n" ti.tname))
391
with Not_found -> begin (* This is the first time we see it *)
392
if ti.tname = "" then
393
ignore (warnContext "typeinfo with empty name");
394
checkType ti.ttype CTDecl;
395
(* Add it to the map before we go on *)
396
H.add typUsed ti.tname (ti, ref isadef);
399
(* Check an lvalue. If isconst then the lvalue appears in a context where
400
* only a compile-time constant can appear. Return the type of the lvalue.
401
* See the typing rule from cil.mli *)
402
and checkLval (isconst: bool) (lv: lval) : typ =
406
checkOffset vi.vtype off
408
| Mem addr, off -> begin
410
ignore (warn "Memory operation in constant");
411
let ta = checkExp false addr in
412
match unrollType ta with
413
TPtr (t, _) -> checkOffset t off
414
| _ -> E.s (bug "Mem on a non-pointer")
417
(* Check an offset. The basetype is the type of the object referenced by the
418
* base. Return the type of the lvalue constructed from a base value of right
419
* type and the offset. See the typing rules from cil.mli *)
420
and checkOffset basetyp : offset -> typ = function
423
checkExpType false ei intType;
425
match unrollType basetyp with
426
TArray (t, _, _) -> checkOffset t o
427
| t -> E.s (bug "typeOffset: Index on a non-array: %a" d_plaintype t)
431
(* Now check that the host is shared propertly *)
432
checkCompInfo Used fi.fcomp;
433
(* Check that this exact field is part of the host *)
434
if not (List.exists (fun f -> f == fi) fi.fcomp.cfields) then
435
ignore (warn "Field %s not part of %s"
436
fi.fname (compFullName fi.fcomp));
437
checkOffset fi.ftype o
439
and checkExpType (isconst: bool) (e: exp) (t: typ) =
440
let t' = checkExp isconst e in (* compute the type *)
441
if isconst then begin (* For initializers allow a string to initialize an
442
* array of characters *)
443
if typeSig t' <> typeSig t then
445
| _ -> typeMatch t' t
449
(* Check an expression. isconst specifies if the expression occurs in a
450
* context where only a compile-time constant can occur. Return the computed
451
* type of the expression *)
452
and checkExp (isconst: bool) (e: exp) : typ =
454
(fun _ -> dprintf "check%s: %a"
455
(if isconst then "Const" else "Exp") d_exp e)
458
| Const(CInt64 (_, ik, _)) -> TInt(ik, [])
459
| Const(CChr _) -> charType
460
| Const(CStr s) -> charPtrType
461
| Const(CWStr s) -> TPtr(!wcharType,[])
462
| Const(CReal (_, fk, _)) -> TFloat(fk, [])
463
| Const(CEnum (_, _, ei)) -> TEnum(ei, [])
466
ignore (warn "Lval in constant");
470
(* Sizeof cannot be applied to certain types *)
471
checkType t CTSizeof;
472
(match unrollType t with
473
(TFun _ | TVoid _) ->
474
ignore (warn "Invalid operand for sizeof")
479
(* The expression in a sizeof can be anything *)
480
let te = checkExp false e in
481
checkExp isconst (SizeOf(te))
483
| SizeOfStr s -> uintType
485
| AlignOf(t) -> begin
486
(* Sizeof cannot be applied to certain types *)
487
checkType t CTSizeof;
488
(match unrollType t with
489
(TFun _ | TVoid _) ->
490
ignore (warn "Invalid operand for sizeof")
495
(* The expression in an AlignOfE can be anything *)
496
let te = checkExp false e in
497
checkExp isconst (AlignOf(te))
499
| UnOp (Neg, e, tres) ->
500
checkArithmeticType tres; checkExpType isconst e tres; tres
502
| UnOp (BNot, e, tres) ->
503
checkIntegralType tres; checkExpType isconst e tres; tres
505
| UnOp (LNot, e, tres) ->
506
let te = checkExp isconst e in
508
checkIntegralType tres; (* Must check that t is well-formed *)
509
typeMatch tres intType;
512
| BinOp (bop, e1, e2, tres) -> begin
513
let t1 = checkExp isconst e1 in
514
let t2 = checkExp isconst e2 in
517
typeMatch t1 t2; checkArithmeticType tres;
518
typeMatch t1 tres; tres
519
| (Eq|Ne|Lt|Le|Ge|Gt) ->
520
typeMatch t1 t2; checkArithmeticType t1;
521
typeMatch tres intType; tres
522
| Mod|BAnd|BOr|BXor ->
523
typeMatch t1 t2; checkIntegralType tres;
524
typeMatch t1 tres; tres
526
typeMatch t1 t2; checkBooleanType tres;
527
typeMatch t1 tres; tres
528
| Shiftlt | Shiftrt ->
529
typeMatch t1 tres; checkIntegralType t1;
530
checkIntegralType t2; tres
531
| (PlusA | MinusA) ->
532
typeMatch t1 t2; typeMatch t1 tres;
533
checkArithmeticType tres; tres
534
| (PlusPI | MinusPI | IndexPI) ->
535
checkPointerType tres;
537
checkIntegralType t2;
540
checkPointerType t1; checkPointerType t2;
542
typeMatch tres intType;
545
| AddrOf (lv) -> begin
546
let tlv = checkLval isconst lv in
547
(* Only certain types can be in AddrOf *)
548
match unrollType tlv with
550
E.s (bug "AddrOf on improper type");
552
| (TInt _ | TFloat _ | TPtr _ | TComp _ | TFun _ | TArray _ ) ->
555
| TEnum _ -> intPtrType
556
| _ -> E.s (bug "AddrOf on unknown type")
559
| StartOf lv -> begin
560
let tlv = checkLval isconst lv in
561
match unrollType tlv with
562
TArray (t,_, _) -> TPtr(t, [])
563
| _ -> E.s (bug "StartOf on a non-array")
566
| CastE (tres, e) -> begin
567
let et = checkExp isconst e in
568
checkType tres CTExp;
569
(* Not all types can be cast *)
570
match unrollType et with
571
TArray _ -> E.s (bug "Cast of an array type")
572
| TFun _ -> E.s (bug "Cast of a function type")
573
| TComp _ -> E.s (bug "Cast of a composite type")
574
| TVoid _ -> E.s (bug "Cast of a void type")
577
() (* The argument of withContext *)
579
and checkInit (i: init) : typ =
581
(fun _ -> dprintf "checkInit: %a" d_init i)
584
SingleInit e -> checkExp true e
586
| ArrayInit (bt, len, initl) -> begin
587
checkType bt CTSizeof;
588
if List.length initl > len then
589
ignore (warn "Too many initializers in array");
590
List.iter (fun i -> checkInitType i bt) initl;
591
TArray(bt, Some (integer len), [])
594
| CompoundInit (ct, initl) -> begin
595
checkType ct CTSizeof;
596
(match unrollType ct with
597
TArray(bt, Some (Const(CInt64(len, _, _))), _) ->
598
let rec loopIndex i = function
601
ignore (warn "Wrong number of initializers in array")
603
| (Index(Const(CInt64(i', _, _)), NoOffset), ei) :: rest ->
605
ignore (warn "Initializer for index %s when %s was expected\n"
606
(Int64.format "%d" i') (Int64.format "%d" i));
608
loopIndex (Int64.succ i) rest
610
ignore (warn "Malformed initializer for array element")
612
loopIndex Int64.zero initl
614
ignore (warn "Malformed initializer for array")
618
(nextflds: fieldinfo list)
619
(initl: (offset * init) list) : unit =
620
match nextflds, initl with
621
[], [] -> () (* We are done *)
622
| f :: restf, (Field(f', NoOffset), i) :: resti ->
623
if f.fname <> f'.fname then
624
ignore (warn "Expected initializer for field %s and found one for %s\n" f.fname f'.fname);
625
checkInitType i f.ftype;
626
loopFields restf resti
628
ignore (warn "Too many initializers for struct")
630
ignore (warn "Too few initializers for struct")
632
ignore (warn "Malformed initializer for struct")
635
(List.filter (fun f -> f.fname <> missingFieldName)
640
if comp.cfields == [] then begin
642
ignore (warn "Initializer for empty union not empty");
645
[(Field(f, NoOffset), ei)] ->
646
if f.fcomp != comp then
647
ignore (bug "Wrong designator for union initializer");
648
if !msvcMode && f != List.hd comp.cfields then
649
ignore (warn "On MSVC you can only initialize the first field of a union");
650
checkInitType ei f.ftype
653
ignore (warn "Malformed initializer for union")
656
E.s (warn "Type of Compound is not array or struct or union"));
659
() (* The arguments of withContext *)
662
and checkInitType (i: init) (t: typ) : unit =
663
let it = checkInit i in
666
and checkStmt (s: stmt) =
669
(* Print context only for certain small statements *)
671
Loop _ | If _ | Switch _ -> nil
672
| _ -> dprintf "checkStmt: %a" d_stmt s)
674
(* Check the labels *)
675
let checkLabel = function
677
if H.mem labels ln then
678
ignore (warn "Multiply defined label %s" ln);
680
| Case (e, _) -> checkExpType true e intType
681
| _ -> () (* Not yet implemented *)
683
List.iter checkLabel s.labels;
684
(* See if we have seen this statement before *)
685
if List.memq s !statements then
686
ignore (warn "Statement is shared");
687
(* Remember that we have seen this one *)
688
statements := s :: !statements;
690
Break _ | Continue _ -> ()
695
match List.filter (function Label _ -> true | _ -> false)
697
Label (lab, _, _) :: _ -> lab
699
ignore (warn "Goto to block without a label\n");
702
(* Remember it as a target *)
703
gotoTargets := (lab, !gref) :: !gotoTargets
706
| Return (re,l) -> begin
708
match re, !currentReturnType with
710
| _, TVoid _ -> ignore (warn "Invalid return value")
711
| None, _ -> ignore (warn "Invalid return value")
712
| Some re', rt' -> checkExpType false re' rt'
714
| Loop (_, b, l, _, _) -> checkBlock b
715
| Block b -> checkBlock b
716
| If (e, bt, bf, l) ->
718
let te = checkExp false e in
722
| Switch (e, b, cases, l) ->
724
checkExpType false e intType;
725
(* Remember the statements so far *)
726
let prevStatements = !statements in
728
(* Now make sure that all the cases do occur in that block *)
731
if not (List.exists (function Case _ -> true | _ -> false)
733
ignore (warn "Case in switch statment without a \"case\"\n");
734
(* Make sure it is in there *)
735
let rec findCase = function
736
| l when l == prevStatements -> (* Not found *)
738
"Cannot find target of switch statement")
739
| [] -> E.s (E.bug "Check: findCase")
740
| c' :: rest when c == c' -> () (* Found *)
741
| _ :: rest -> findCase rest
743
findCase !statements)
745
| TryFinally (b, h, l) ->
750
| TryExcept (b, (il, e), h, l) ->
753
List.iter checkInstr il;
754
checkExpType false e intType;
757
| Instr i -> checkInstr i)
758
() (* argument of withContext *)
760
and checkBlock (b: block) : unit =
761
List.iter checkStmt b.bstmts
764
and checkInstr (i: instr) =
766
| Set (dest, e, l) ->
768
let t = checkLval false dest in
769
(* Not all types can be assigned to *)
770
(match unrollType t with
771
TFun _ -> ignore (warn "Assignment to a function type")
772
| TArray _ -> ignore (warn "Assignment to an array type")
773
| TVoid _ -> ignore (warn "Assignment to a void type")
775
checkExpType false e t
777
| Call(dest, what, args, l) ->
779
let (rt, formals, isva) =
780
match checkExp false what with
781
TFun(rt, formals, isva, _) -> rt, formals, isva
782
| _ -> E.s (bug "Call to a non-function")
784
(* Now check the return value*)
785
(match dest, unrollType rt with
787
| Some _, TVoid _ -> ignore (warn "void value is assigned")
788
| None, _ -> () (* "Call of function is not assigned" *)
789
| Some destlv, rt' ->
790
let desttyp = checkLval false destlv in
791
if typeSig desttyp <> typeSig rt then begin
792
(* Not all types can be assigned to *)
793
(match unrollType desttyp with
794
TFun _ -> ignore (warn "Assignment to a function type")
795
| TArray _ -> ignore (warn "Assignment to an array type")
796
| TVoid _ -> ignore (warn "Assignment to a void type")
798
(* Not all types can be cast *)
800
TArray _ -> ignore (warn "Cast of an array type")
801
| TFun _ -> ignore (warn "Cast of a function type")
802
| TComp _ -> ignore (warn "Cast of a composite type")
803
| TVoid _ -> ignore (warn "Cast of a void type")
807
(* Now check the arguments *)
808
let rec loopArgs formals args =
809
match formals, args with
810
[], _ when (isva || args = []) -> ()
811
| (fn,ft,_) :: formals, a :: args ->
812
checkExpType false a ft;
813
loopArgs formals args
814
| _, _ -> ignore (warn "Not enough arguments")
816
if formals = None then
817
ignore (warn "Call to function without prototype\n")
819
loopArgs (argsToList formals) args
821
| Asm _ -> () (* Not yet implemented *)
827
let rec checkGlobal = function
834
E.withContext (fun _ -> dprintf "GType(%s)" ti.tname)
836
checkTypeInfo Defined ti;
837
if ti.tname <> "" then defineName ti.tname)
840
| GCompTag (comp, l) ->
842
checkCompInfo Defined comp;
844
| GCompTagDecl (comp, l) ->
846
checkCompInfo Forward comp;
848
| GEnumTag (enum, l) ->
850
checkEnumInfo Defined enum
852
| GEnumTagDecl (enum, l) ->
854
checkEnumInfo Forward enum
856
| GVarDecl (vi, l) ->
858
(* We might have seen it already *)
860
(fun _ -> dprintf "GVarDecl(%s)" (!Cil.output_ident vi.vname))
862
(* If we have seen this vid already then it must be for the exact
864
if H.mem varIdsEnv vi.vid then
868
checkAttributes vi.vattr;
869
checkType vi.vtype CTDecl;
871
vi.vstorage <> Register) then
872
E.s (bug "Invalid declaration of %s"
873
(!Cil.output_ident vi.vname))
877
| GVar (vi, init, l) ->
879
(* Maybe this is the first occurrence *)
880
E.withContext (fun _ -> dprintf "GVar(%s)"
881
(!Cil.output_ident vi.vname))
883
checkGlobal (GVarDecl (vi, l));
884
(* Check the initializer *)
885
begin match init.init with
887
| Some i -> ignore (checkInitType i vi.vtype)
889
(* Cannot be a function *)
890
if isFunctionType vi.vtype then
891
E.s (bug "GVar for a function (%s)\n"
892
(!Cil.output_ident vi.vname));
897
| GFun (fd, l) -> begin
899
(* Check if this is the first occurrence *)
901
let fname = vi.vname in
902
E.withContext (fun _ -> dprintf "GFun(%s)" (!Cil.output_ident fname))
904
checkGlobal (GVarDecl (vi, l));
905
(* Check that the argument types in the type are identical to the
907
let rec loopArgs targs formals =
908
match targs, formals with
910
| (fn, ft, fa) :: targs, fo :: formals ->
911
if fn <> fo.vname || ft != fo.vtype || fa != fo.vattr then
913
"Formal %s not shared (type + locals) in %s"
914
(!Cil.output_ident fo.vname)
915
(!Cil.output_ident fname));
916
loopArgs targs formals
919
E.s (bug "Type has different number of formals for %s"
920
(!Cil.output_ident fname))
922
begin match vi.vtype with
923
TFun (rt, args, isva, a) -> begin
924
currentReturnType := rt;
925
loopArgs (argsToList args) fd.sformals
927
| _ -> E.s (bug "Function %s does not have a function type"
928
(!Cil.output_ident fname))
930
ignore (fd.smaxid >= 0 ||
931
E.s (bug "smaxid < 0 for %s" (!Cil.output_ident fname)));
932
(* Now start a new environment, in a finally clause *)
939
"Local %s has the vglob flag set"
940
(!Cil.output_ident v.vname));
941
if v.vstorage <> NoStorage && v.vstorage <> Register then
943
"Local %s has storage %a\n"
944
(!Cil.output_ident v.vname)
945
d_storage v.vstorage);
946
checkType v.vtype tctx;
947
checkAttributes v.vattr;
950
List.iter (doLocal CTFArg) fd.sformals;
951
List.iter (doLocal CTDecl) fd.slocals;
956
(* Now verify that we have scanned all targets *)
958
(fun (lab, t) -> if not (List.memq t !statements) then
960
"Target of \"goto %s\" statement does not appear in function body" lab))
971
() (* final argument of withContext *)
975
let checkFile flags fl =
976
if !E.verboseFlag then ignore (E.log "Checking file %s\n" fl.fileName);
980
NoCheckGlobalIds -> checkGlobalIds := false)
982
iterGlobals fl (fun g -> try checkGlobal g with _ -> ());
983
(* Check that for all struct/union tags there is a definition *)
985
(fun k (comp, isadef) ->
986
if !isadef = Used then
989
ignore (E.warn "Compinfo %s is referenced but not defined"
993
(* Check that for all enum tags there is a definition *)
995
(fun k (enum, isadef) ->
996
if !isadef = Used then
999
ignore (E.warn "Enuminfo %s is referenced but not defined"
1003
(* Clean the hashes to let the GC do its job *)
1005
H.clear varNamesEnv;
1013
if !E.verboseFlag then
1014
ignore (E.log "Finished checking file %s\n" fl.fileName);
added
removed
cil/src/check.ml
