metrics_cilast.ml 23 KB
Newer Older
Loïc Correnson's avatar
Loïc Correnson committed
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
(**************************************************************************)
(*                                                                        *)
(*  This file is part of Frama-C.                                         *)
(*                                                                        *)
(*  Copyright (C) 2007-2018                                               *)
(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
(*         alternatives)                                                  *)
(*                                                                        *)
(*  you can redistribute it and/or modify it under the terms of the GNU   *)
(*  Lesser General Public License as published by the Free Software       *)
(*  Foundation, version 2.1.                                              *)
(*                                                                        *)
(*  It is distributed in the hope that it will be useful,                 *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
(*  GNU Lesser General Public License for more details.                   *)
(*                                                                        *)
(*  See the GNU Lesser General Public License version 2.1                 *)
(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
(*                                                                        *)
(**************************************************************************)

open Cil_datatype
open Cil_types
open Metrics_base
;;

type cilast_metrics = {
  fundecl_calls: int Metrics_base.VInfoMap.t;
  fundef_calls: int Metrics_base.VInfoMap.t;
  extern_global_vars: Metrics_base.VInfoSet.t;
  basic_metrics: BasicMetrics.t
}

(** Syntactic metrics
   =================
   The goal is to collect various (syntactic) information about the source code
   (slocs, assignments, loops, ...).
   From those one can compute McCabe's cyclomatic complexity.
*)
class type sloc_visitor = object
  inherit Visitor.generic_frama_c_visitor

  (* Get the number of times a function has been called if it has been
     defined (fundef) or not (fundecl).
  *)
  method fundecl_calls: int Metrics_base.VInfoMap.t
  method fundef_calls: int Metrics_base.VInfoMap.t
  (* Global variables with 'Extern' storage *)
  method extern_global_vars: Metrics_base.VInfoSet.t

  (* Get the computed metrics *)
  method get_metrics: BasicMetrics.t

  (* Print the metrics of a file [string] to a formatter
     Yields a fatal error if the file does not exist (or has no metrics).
  *)
  method pp_file_metrics: Format.formatter -> string -> unit

  method pp_detailed_text_metrics: Format.formatter -> unit
  (** Print results of all file and functions to the given formatter as text *)

  method print_stats: Format.formatter -> unit
  (** Print computed metrics to a formatter *)
end

(* Various metrics computing visitor on Cil AST.
   These metrics are a necessary step to compute cyclomatic complexity.
*)
open BasicMetrics ;;
class slocVisitor ~libc : sloc_visitor = object(self)
  inherit Visitor.frama_c_inplace


  (* Global metrics store for this Cil AST *)
  val global_metrics = ref BasicMetrics.empty_metrics
  (* Local metrics in computation *)
  val local_metrics = ref BasicMetrics.empty_metrics

  (* Local metrics are kept stored after computation in this map of maps.
     Its storing hierarchy is as follows: filename -> function_name -> metrics
  *)
  val mutable metrics_map:
      (BasicMetrics.t Datatype.String.Map.t) Datatype.String.Map.t =
    Datatype.String.Map.empty

  val mutable seen_vars = Varinfo.Set.empty;

  val fundecl_calls: int VInfoMap.t ref = ref VInfoMap.empty;
  val fundef_calls: int VInfoMap.t ref = ref VInfoMap.empty;
  val extern_global_vars = ref VInfoSet.empty

  (* Getters/setters *)
  method fundecl_calls = !fundecl_calls
  method fundef_calls = !fundef_calls
  method extern_global_vars = !extern_global_vars
  method get_metrics = !global_metrics

  method private update_metrics_map filename strmap =
    metrics_map <- Datatype.String.Map.add filename strmap metrics_map

  (* Utility method to increase metrics counts *)
  method private incr_both_metrics f =
    apply_then_set f global_metrics;
    apply_then_set f local_metrics

  method private add_map map vinfo value =
    map := VInfoMap.add vinfo value !map

  method private stats_of_filename filename =
    try Datatype.String.Map.find filename metrics_map
    with
      | Not_found ->
        Metrics_parameters.fatal "Metrics for file %s not_found@." filename

  method pp_file_metrics fmt filename =
    Format.fprintf fmt "@[<v 0>%a@]"
      (fun fmt filename ->
        let fun_tbl = self#stats_of_filename filename in
        Datatype.String.Map.iter (fun _fun_name fmetrics ->
          Format.fprintf fmt "@ %a" pp_base_metrics fmetrics)
          fun_tbl;
      ) filename

  method pp_detailed_text_metrics fmt =
    Datatype.String.Map.iter
      (fun filename _func_tbl ->
        Format.fprintf fmt "%a" self#pp_file_metrics filename) metrics_map

  method print_stats fmt =
    Format.pp_set_formatter_tag_functions fmt Metrics_base.html_tag_functions;
    Format.pp_set_tags fmt true;
    let pr_hdr fmt hdr_name =
      Format.fprintf fmt "@{<th>%s@}" hdr_name in
    Datatype.String.Map.iter
      (fun filename func_tbl ->
        Metrics_parameters.result ~level:2 "%a" self#pp_file_metrics filename;
        if func_tbl <> Datatype.String.Map.empty then
          begin
            Format.fprintf fmt
              "@[<v 0>@{<h3>%s@}<br/>@ \
               @{<table>\
               @[<v 2>@ \
                 @[<v 2>@{<tbody>@ \
                    @{<tr>@[<v 2>@ \
                       %a@ %a@ %a@ %a@ %a@ %a@ %a@ %a@ %a@ @]@}@ \
                       %a@ \
                       @}@]@]@ @} \
               @]@ "
              filename
              pr_hdr "Function" pr_hdr "#If stmts" pr_hdr "#Assignments"
              pr_hdr "#Loops" pr_hdr "#Calls" pr_hdr "#Gotos"
              pr_hdr "#Pointer dereferencing" pr_hdr "#Exits"
              pr_hdr "Cyclomatic value"
              (fun fmt fun_tbl ->
                Datatype.String.Map.iter
                  (fun _fname fmetrics ->
                    Format.fprintf fmt "%a"
                      pp_base_metrics_as_html_row fmetrics;
                  ) fun_tbl
              ) func_tbl;
          end
        else 
	  Metrics_parameters.warning
	    "Filename <%s> has no functions@." filename)
      metrics_map

(* Save the local metrics currently computed.
   Clears it before starting a new metrics computation (e.g. when entering a new
   function definition.
   Global metrics are never reset as they define metrics on the whole Cil.file.
*)
  method private record_and_clear_function_metrics metrics =
    let filename = metrics.cfile_name in
    let funcname = metrics.cfunc_name in
    local_metrics := BasicMetrics.set_cyclo !local_metrics
           (BasicMetrics.compute_cyclo !local_metrics);
    global_metrics := BasicMetrics.set_cyclo !global_metrics
           (!global_metrics.ccyclo + !local_metrics.ccyclo);
    (try
       let fun_tbl = Datatype.String.Map.find filename metrics_map in
       self#update_metrics_map filename
         (Datatype.String.Map.add funcname !local_metrics fun_tbl);
     with
       | Not_found ->
         let new_stringmap =
           Datatype.String.Map.add funcname !local_metrics
             Datatype.String.Map.empty
         in self#update_metrics_map filename new_stringmap;
    );
    local_metrics := empty_metrics;

  method! vvdec vi =
    if not (Varinfo.Set.mem vi seen_vars) then (
      if Cil.isFunctionType vi.vtype then (
        if consider_function ~libc vi then begin
          global_metrics := incr_funcs !global_metrics;
          (* Mark the function as seen, adding 0 to the number of calls *)
          self#update_call_maps vi 0;
        end
      ) else (
        if vi.vglob && not vi.vtemp &&
           Metrics_base.consider_variable ~libc vi
        then (
          global_metrics:= incr_glob_vars !global_metrics;
          if vi.vstorage = Extern then
            extern_global_vars := VInfoSet.add vi !extern_global_vars
        )
      );
      seen_vars <- Varinfo.Set.add vi seen_vars;
    );
    Cil.SkipChildren
      
  method! vfunc fdec =
    if consider_function ~libc fdec.svar then
      begin
        (* Here, we get to a fundec definition.this function has a body,
           let's put it to the "function with source" table. *)
        local_metrics :=
          {!local_metrics with
            cfile_name = file_of_fundef fdec;
            cfunc_name = fdec.svar.vname;
            cfuncs = 1; (* Only one function is indeed being defined here *)};
        let fvinfo = fdec.svar in
        (if not (VInfoMap.mem fvinfo !fundef_calls) then
           (* Never seen before, including never been called *)
            self#add_map fundef_calls fvinfo 0);
        (* On return record the analysis of the function. *)
        Cil.ChangeDoChildrenPost
          (fdec,
           fun _ ->
             begin
               if !local_metrics <> empty_metrics
               then self#record_and_clear_function_metrics !local_metrics;
               fdec;
             end
          );
      end
    else Cil.SkipChildren

  method! vlval (host, _) =
    begin
      match host with
        | Mem _ -> self#incr_both_metrics incr_ptrs;
        | _ -> ()
    end;
    Cil.DoChildren

  method! vstmt s =
    self#incr_both_metrics incr_slocs;
    let do_children =
      match s.skind with
        | If _ ->
            self#incr_both_metrics incr_ifs;
            self#incr_both_metrics incr_dpoints;
            true
        | Loop _ -> self#incr_both_metrics incr_loops; true
        | Goto _ -> self#incr_both_metrics incr_gotos; true
        | Return _ -> self#incr_both_metrics incr_exits; true
        | Switch (_, _, _slist, _) -> true
        (* The catching block is one more possible flow alternative *)
        | TryFinally _
        | TryExcept _ -> self#incr_both_metrics incr_dpoints; true
        | UnspecifiedSequence l ->
            List.iter 
              (fun (s,_,_,_,_) ->
                ignore
                  (Visitor.visitFramacStmt (self:>Visitor.frama_c_visitor) s))
              l;
            false
        | _ -> true
    in
    (* Default cases are not path choice points, as normal labels.
       Non-default cases are ... just like if statements.
    *)
    let rec has_case_label labels =
      match labels with
        | (Case _) :: _->
          self#incr_both_metrics incr_dpoints;
        | _ :: labels -> has_case_label labels
        | [] -> ()
    in has_case_label s.labels;
    if do_children then Cil.DoChildren else Cil.SkipChildren

  method! vexpr e =
    begin
      (* Logical ands and ors are lazy and generate two different paths *)
      match e.enode with
        | BinOp ((LAnd | LOr), _, _, _) ->
          self#incr_both_metrics incr_dpoints;
        | _ -> ()
    end;
    Cil.DoChildren

  method private image (glob:global) =
    (* extract just the name of the global , for printing purposes *)
    match glob with
      | GVar (v, _, _) -> v.vname ^ " (GVar) "
      | GVarDecl (v, _) -> v.vname ^ " (GVarDecl) "
      | GFunDecl (_, v, _) -> v.vname ^ " (GFunDecl) "
      | GFun (fdec, _) -> fdec.svar.vname ^ " (GFun) "
      | GType (ty, _) -> ty.tname
      | GCompTag (ci, _) | GCompTagDecl (ci, _) -> ci.cname
      | GEnumTagDecl (ei, _) | GEnumTag (ei, _) -> ei.ename
      | GAsm (_, _) | GPragma _ | GText _ -> ""
      | GAnnot (an,_) ->
        begin
          match an with
            | Dfun_or_pred (li, _) -> li.l_var_info.lv_name
            | Dvolatile (_, _, _, _, _) -> " (Volatile) "
            | Daxiomatic (s, _, _, _) -> s
            | Dtype (lti, _) ->  lti.lt_name
            | Dlemma (ln, _, _, _, _, _, _) ->  ln
            | Dinvariant (toto, _) -> toto.l_var_info.lv_name
            | Dtype_annot (ta, _) -> ta.l_var_info.lv_name
            | Dmodel_annot (mi, _) -> mi.mi_name
            | Dcustom_annot (_c, _n, _, _) -> " (Custom) "
        end

  method private images (globs:global list) =
    (* extract just the names of the globals, for printing purposes *)
    let les_images = List.map self#image globs in
    String.concat "," les_images

  method private update_call_maps vinfo increment =
    if consider_function ~libc vinfo then
      let update_call_map funcmap =
        self#add_map funcmap vinfo
          (increment + try VInfoMap.find vinfo !funcmap with Not_found-> 0)
      in
      if vinfo.vdefined
      then update_call_map fundef_calls
      else update_call_map fundecl_calls


  method! vinst i =
    begin match i with
      | Call(v, e, _, _) ->
        self#incr_both_metrics incr_calls;
        (match e.enode with
          | Lval(Var vinfo, NoOffset) -> self#update_call_maps vinfo 1
          | _ -> ());
        (match v with
         | Some _ -> self#incr_both_metrics incr_assigns
         | None -> ());
      | Set _ -> self#incr_both_metrics incr_assigns;
      | Local_init (_, AssignInit _, _) -> self#incr_both_metrics incr_assigns
      | Local_init (_, ConsInit(f,_, k),_) ->
        (* if f takes the address of the initialized variable as first
           argument, there's no explicit assignment in the current function. *)
        (match k with
         | Plain_func -> self#incr_both_metrics incr_assigns
         | Constructor -> ());
        self#incr_both_metrics incr_calls;
        self#update_call_maps f 1
      | Asm _ | Skip _ | Code_annot _ -> ()
    end;
    Cil.DoChildren

end


let dump_html fmt cil_visitor =
  (* Activate tagging for html *)
  Format.pp_set_formatter_tag_functions fmt html_tag_functions;
  Format.pp_set_tags fmt true;

  let pr_row s fmt n =
    Format.fprintf fmt
      "@{<tr>@[<v 1>@ \
              @{<td class=\"entry\">%s@}@ \
              @{<td class=\"stat\">%d@}@]@ @} " s n
  in
  let pr_stats fmt visitor =
    let metrics = visitor#get_metrics in
    Format.fprintf fmt "@[<v 0>@{<table>%a@}@]"
      (fun fmt metrics ->
        List.iter2 (fun text value -> pr_row text fmt value)
          ["SLOC"; "Number of if statements"; "Number of assignments";
           "Number of loops"; "Number of calls"; "Number of gotos";
           "Number of pointer accesses";]
          [metrics.cslocs; metrics.cifs; metrics.cassigns;
           metrics.cloops; metrics.ccalls; metrics.cgotos;
           metrics.cptrs;]) metrics
  in
  let pr_prelude fmt cil_visitor =
    Format.fprintf fmt "@[<v 0>\
        @{<div>@ \
        @{<h1>@{<span>Metrics@}@}@ \
        @{<h2>Synthetic results@}@ <br/>@ \
        @{<span>Defined function(s)@} (%d): <br/>@ \
        @[&nbsp; %a@]@ <br/>@ <br/>@ \
        @{<span>Undefined function(s)@} (%d):@ <br/>@ \
        @[&nbsp; %a@]@ <br>@ <br/>@ \
        @{<span>'Extern' global variable(s)@} (%d):@ <br/>@ \
        @[&nbsp; %a@]@ <br>@ <br/>@ \
        @{<span>Potential entry point(s)@} (%d):@ <br/>@ \
        @[&nbsp; %a@]@ <br/>@ <br/>@ \
        @}@]"
      (VInfoMap.cardinal cil_visitor#fundef_calls)
      Metrics_base.pretty_set cil_visitor#fundef_calls
      (VInfoMap.cardinal cil_visitor#fundecl_calls)
      Metrics_base.pretty_set cil_visitor#fundecl_calls
      (VInfoSet.cardinal cil_visitor#extern_global_vars)
      Metrics_base.pretty_extern_vars cil_visitor#extern_global_vars
      (Metrics_base.number_entry_points cil_visitor#fundef_calls)
      Metrics_base.pretty_entry_points cil_visitor#fundef_calls
  in
  let pr_detailed_results fmt cil_visitor =
    Format.fprintf fmt "@[<v 0>\
        @{<div style=\"text-align: left;\">\
        @[<v 2>@ \
          @{<h2>Detailed results@}@ \
          @[<v 0>%a@ @]\
        @]@}"
      (fun fmt cil_visitor -> cil_visitor#print_stats fmt) cil_visitor
  in
  Format.fprintf fmt "@[<v 0>\
      <!DOCTYPE HTML PUBLIC \"-//W3C//DTD HTML 4.01//EN\"\
          \"http://www.w3.org/TR/html4/strict.dtd\">@ \
      @{<html>@ \
      @{<head>@ \
       @{<title>%s@}@ \
       <meta content=\"text/html; charset=iso-8859-1\" \
        http-equiv=\"Content-Type\"/>@ \
        @{<style type=\"text/css\">%s@}@ \
      @}@ \
        @{<body>\
         @[<v 2>@ \
         %a@ \
         %a@ \
         %a@ \
         @]@}@}@]@?"
    "Metrics"
    Css_html.css
    pr_prelude cil_visitor
    pr_stats cil_visitor
    pr_detailed_results cil_visitor
;;

let pp_funinfo fmt vis =
  let nfundef = VInfoMap.cardinal vis#fundef_calls in
  let nfundecl = VInfoMap.cardinal vis#fundecl_calls in
  let nextern = VInfoSet.cardinal vis#extern_global_vars in
  let fundef_hdr = Format.sprintf "Defined functions (%d)" nfundef
  and fundecl_hdr = Format.sprintf "Undefined functions (%d)" nfundecl
  and extern_hdr = Format.sprintf "'Extern' global variables (%d)" nextern
  and entry_pts_hdr = Format.sprintf "Potential entry points (%d)"
    (Metrics_base.number_entry_points vis#fundef_calls) in
  Format.fprintf fmt
    "@[<v 0>@[<v 1>%a@ @[%a@]@]@ @ \
            @[<v 1>%a@ @[%a@]@]@ @ \
            @[<v 1>%a@ @[%a@]@]@ @ \
            @[<v 1>%a@ @[%a@]@]@ \
     @]"
    (Metrics_base.mk_hdr 1) fundef_hdr
    Metrics_base.pretty_set vis#fundef_calls
    (Metrics_base.mk_hdr 1) fundecl_hdr
    Metrics_base.pretty_set vis#fundecl_calls
    (Metrics_base.mk_hdr 1) extern_hdr
    Metrics_base.pretty_extern_vars vis#extern_global_vars
    (Metrics_base.mk_hdr 1) entry_pts_hdr
    Metrics_base.pretty_entry_points vis#fundef_calls
;;

let pp_with_funinfo fmt cil_visitor =
  Format.fprintf fmt "@[<v 0>%a@ %a@]"
    pp_funinfo cil_visitor
    pp_base_metrics cil_visitor#get_metrics
;;

let get_metrics ~libc =
  let file = Ast.get () in
   (* Do as before *)
  let cil_visitor = new slocVisitor ~libc in
  Visitor.visitFramacFileSameGlobals
    (cil_visitor:>Visitor.frama_c_visitor) file;
  cil_visitor#get_metrics
;;

let get_cilast_metrics ~libc =
  let file = Ast.get () in
  (* Do as before *)
  let cil_visitor = new slocVisitor ~libc in
  Visitor.visitFramacFileSameGlobals
    (cil_visitor:>Visitor.frama_c_visitor) file;
  {
    fundecl_calls = cil_visitor#fundecl_calls;
    fundef_calls = cil_visitor#fundef_calls;
    extern_global_vars = cil_visitor#extern_global_vars;
    basic_metrics = cil_visitor#get_metrics;
  }
;;

let compute_on_cilast ~libc =
  let file = Ast.get () in
  (* Do as before *)
  let cil_visitor = new slocVisitor ~libc in
  Visitor.visitFramacFileSameGlobals
    (cil_visitor:>Visitor.frama_c_visitor) file;
  if Metrics_parameters.ByFunction.get () then
    Metrics_parameters.result
      "@[<v 0>Cil AST@ %t@]" cil_visitor#pp_detailed_text_metrics;
(*  let r =  metrics_to_result cil_visitor in *)
  (* Print the result to file if required *)
  let out_fname = Metrics_parameters.OutputFile.get () in
  begin
    if out_fname <> "" then
      try
        let oc = open_out_bin out_fname in
        let fmt = Format.formatter_of_out_channel oc in
        (match Metrics_base.get_file_type out_fname with
          | Html -> dump_html fmt cil_visitor
          | Text -> pp_with_funinfo fmt cil_visitor
        );
        close_out oc;
      with Sys_error _ ->
        Metrics_parameters.failure "Cannot open file %s.@." out_fname
    else Metrics_parameters.result "%a" pp_with_funinfo cil_visitor
  end

(* Visitor for the recursive estimation of a stack size.
   Its arguments are the function currently being visited and the current
   callstack, as a list of kernel functions.
   The callstack is used to detect recursive calls.
   TODO: this computation is far from optimal; for instance, locals_size could
   be cached for each function. Also, it does not consider calls via function
   pointers. *)
class locals_size_visitor kf callstack = object

  val mutable locals_size_no_temps = Integer.zero
  method get_locals_size_no_temps = locals_size_no_temps

  val mutable locals_size_temps = Integer.zero
  method get_locals_size_temps = locals_size_temps

  val mutable max_size_calls_no_temps = Integer.zero
  method get_max_size_calls_no_temps = max_size_calls_no_temps

  val mutable max_size_calls_temps = Integer.zero
  method get_max_size_calls_temps = max_size_calls_temps

  inherit Visitor.frama_c_inplace

  method! vinst i = match i with
    | Call (_, { enode = Lval(Var vi, NoOffset) }, _, _)
    | Local_init(_, ConsInit(vi,_,_),_) ->
      begin
        try
          let kf' = Globals.Functions.find_by_name vi.vname in
          Metrics_parameters.debug
            "@[function %a:@;computing call to function %a@]"
            Kernel_function.pretty kf Kernel_function.pretty kf';
          let new_cs = kf' :: callstack in
          if List.mem kf' callstack then
            Metrics_parameters.abort
              "@[unsupported recursive call detected:@;%a@]"
              (Pretty_utils.pp_list ~sep:"@ <-@ " Kernel_function.pretty)
              (List.rev new_cs);
          let new_vis = new locals_size_visitor kf' new_cs in
          ignore (Visitor.visitFramacKf
                    (new_vis :> Visitor.frama_c_visitor) kf');
          let call_size_no_temps =
            Integer.add new_vis#get_max_size_calls_no_temps
              new_vis#get_locals_size_no_temps
          in
          let call_size_temps =
            Integer.add new_vis#get_max_size_calls_temps
              new_vis#get_locals_size_temps
          in
          max_size_calls_no_temps <-
            Integer.max max_size_calls_no_temps call_size_no_temps;
          max_size_calls_temps <-
            Integer.max max_size_calls_temps call_size_temps
        with Not_found ->
          (* should not happen *)
          Metrics_parameters.fatal ~current:true
            "@[function not found:@;%s@]" vi.vname;
      end;
      Cil.DoChildren
    | _ -> Cil.DoChildren

  method! vvdec vi =
    if not vi.vglob && not vi.vghost && vi.vstorage = NoStorage then
      begin
        let size_exp = Cil.sizeOf ~loc:vi.vdecl vi.vtype in
        match Cil.constFoldToInt size_exp with
        | None -> Metrics_parameters.error
                    "@[in function %a,@;cannot compute sizeof %a (type %a)@]"
                    Kernel_function.pretty kf Printer.pp_varinfo vi
                    Printer.pp_typ vi.vtype
        | Some size ->
          Metrics_parameters.debug "@[function %a:@;sizeof(%a) = %a (%s)@]"
            Kernel_function.pretty kf
            Printer.pp_varinfo vi (Integer.pretty ~hexa:false) size
            (if vi.vtemp then "temp" else "non-temp");
          if vi.vtemp then
            locals_size_temps <- Integer.add locals_size_temps size
          else
            locals_size_no_temps <- Integer.add locals_size_no_temps size
      end;
    Cil.DoChildren

end

(* Requires a computed Cil AST *)
let compute_locals_size kf =
  let vis = new locals_size_visitor kf [kf] in
  ignore (Visitor.visitFramacKf (vis :> Visitor.frama_c_visitor) kf);
  Metrics_parameters.result "@[%a\t%a\t%a\t%a\t%a@]"
    Kernel_function.pretty kf
    (Integer.pretty ~hexa:false) vis#get_locals_size_no_temps
    (Integer.pretty ~hexa:false)
    (Integer.add vis#get_locals_size_no_temps vis#get_locals_size_temps)
    (Integer.pretty ~hexa:false) vis#get_max_size_calls_no_temps
    (Integer.pretty ~hexa:false)
    (Integer.add vis#get_max_size_calls_no_temps vis#get_max_size_calls_temps)
;;

(*
Local Variables:
compile-command: "make -C ../../.."
End:
*)