prepare_ast.ml 23.8 KB
Newer Older
1
2
(**************************************************************************)
(*                                                                        *)
Patrick Baudin's avatar
Patrick Baudin committed
3
(*  This file is part of the Frama-C's E-ACSL plug-in.                    *)
4
(*                                                                        *)
5
(*  Copyright (C) 2012-2019                                               *)
6
7
8
9
10
11
12
13
14
15
16
17
18
(*    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                 *)
Virgile Prevosto's avatar
Virgile Prevosto committed
19
(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
20
21
22
23
24
(*                                                                        *)
(**************************************************************************)

open Cil_types

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
let dkey = Options.dkey_prepare

(* ********************************************************************** *)
(* Environment *)
(* ********************************************************************** *)

let fct_tbl: unit Kernel_function.Hashtbl.t = Kernel_function.Hashtbl.create 7

let actions = Queue.create ()

(* global table for ensuring that logic info are not shared between a function
   definition and its duplicate *)
module Global: sig
  val add_logic_info: logic_info -> unit
  val mem_logic_info: logic_info -> bool
  val reset: unit -> unit
end = struct

  let tbl = Cil_datatype.Logic_info.Hashtbl.create 7
  let add_logic_info x = Cil_datatype.Logic_info.Hashtbl.add tbl x ()
  let mem_logic_info x = Cil_datatype.Logic_info.Hashtbl.mem tbl x
  let reset () = Cil_datatype.Logic_info.Hashtbl.clear tbl

end

let reset () =
  Kernel_function.Hashtbl.clear fct_tbl;
  Global.reset ();
  Queue.clear actions

(* ********************************************************************** *)
(* Duplicating functions *)
(* ********************************************************************** *)

let dup_funspec tbl bhv spec =
  (*  Options.feedback "DUP SPEC %a" Cil.d_funspec spec;*)
  let o = object
    inherit Cil.genericCilVisitor bhv

    val already_visited = Cil_datatype.Logic_var.Hashtbl.create 7

    method !vlogic_info_use li =
      if Global.mem_logic_info li then
        Cil.ChangeDoChildrenPost
          ({ li with l_var_info = li.l_var_info } (* force a copy *),
           Visitor_behavior.Get.logic_info bhv)
      else
        Cil.JustCopy

    method !vterm_offset _ =
      Cil.DoChildrenPost
        (function (* no way to directly visit fieldinfo and model_info uses *)
          | TField(fi, off) ->
            TField(Visitor_behavior.Get.fieldinfo bhv fi, off)
          | TModel(mi, off) ->
            TModel(Visitor_behavior.Get.model_info bhv mi, off)
          | off ->
            off)

    method !vlogic_var_use orig_lvi =
      match orig_lvi.lv_origin with
      | None ->
        Cil.JustCopy
      | Some vi ->
        try
          let new_lvi =
            Cil_datatype.Logic_var.Hashtbl.find already_visited orig_lvi
          in
          Cil.ChangeTo new_lvi
        with Not_found ->
          Cil.ChangeDoChildrenPost
            ({ orig_lvi with lv_id = orig_lvi.lv_id } (* force a copy *),
             fun lvi ->
               (* using [Visitor_behavior.Get.logic_var bhv lvi] is correct only
                  because the lv_id used to compare the lvi does not change
                  between the original one and this copy *)
               try
                 let new_vi = Cil_datatype.Varinfo.Hashtbl.find tbl vi in
                 Cil_datatype.Logic_var.Hashtbl.add
                   already_visited orig_lvi lvi;
                 lvi.lv_id <- new_vi.vid;
                 lvi.lv_name <- new_vi.vname;
                 lvi.lv_origin <- Some new_vi;
                 new_vi.vlogic_var_assoc <- Some lvi;
                 lvi
               with Not_found ->
                 assert vi.vglob;
                 Visitor_behavior.Get.logic_var bhv lvi)

    method !videntified_term _ =
      Cil.DoChildrenPost Logic_const.refresh_identified_term

    method !videntified_predicate _ =
      Cil.DoChildrenPost Logic_const.refresh_predicate
  end in
  Cil.visitCilFunspec o spec

let dup_fundec loc spec bhv sound_verdict_vi kf vi new_vi =
  new_vi.vdefined <- true;
  let formals = Kernel_function.get_formals kf in
  let mk_formal vi =
    let name =
      if vi.vname = "" then
        (* unnamed formal parameter: must generate a fresh name since a fundec
           cannot have unnamed formals (see bts #2303). *)
        Varname.get
          ~scope:Varname.Function
          (Functions.RTL.mk_gen_name "unamed_formal")
      else
        vi.vname
    in
    Cil.copyVarinfo vi name
  in
  let new_formals = List.map mk_formal formals in
  let res =
    let ty = Kernel_function.get_return_type kf in
    if Cil.isVoidType ty then None
    else Some (Cil.makeVarinfo false false ~referenced:true "__retres" ty)
  in
  let return =
    Cil.mkStmt ~valid_sid:true
      (Return(Extlib.opt_map (Cil.evar ~loc) res, loc))
  in
  let stmts =
    let l =
      [ Cil.mkStmtOneInstr ~valid_sid:true
          (Call(Extlib.opt_map Cil.var res,
                Cil.evar ~loc vi,
                List.map (Cil.evar ~loc) new_formals,
                loc));
        return ]
    in
    if Functions.instrument kf then
      l
    else
      (* set the 'unsound_verdict' variable to 'false' whenever required *)
      let unsound =
        Cil.mkStmtOneInstr ~valid_sid:true
          (Set((Var sound_verdict_vi, NoOffset), Cil.zero ~loc, loc))
      in
      unsound :: l
  in
  let locals = match res with None -> [] | Some r -> [ r ] in
  let body = Cil.mkBlock stmts in
  body.blocals <- locals;
  let tbl = Cil_datatype.Varinfo.Hashtbl.create 7 in
  List.iter2 (Cil_datatype.Varinfo.Hashtbl.add tbl) formals new_formals;
  let new_spec = dup_funspec tbl bhv spec in
  let fundec =
    { svar = new_vi;
      sformals = new_formals;
      slocals = locals;
      smaxid = List.length new_formals;
      sbody = body;
      smaxstmtid = None;
      sallstmts = [];
      sspec = new_spec }
  in
  (* compute the CFG of the new [fundec] *)
  Cfg.clearCFGinfo ~clear_id:false fundec;
  Cfg.cfgFun fundec;
  fundec

let dup_global loc actions spec bhv sound_verdict_vi kf vi new_vi =
  let name = vi.vname in
  Options.feedback ~dkey ~level:2 "entering in function %s" name;
  let fundec = dup_fundec loc spec bhv sound_verdict_vi kf vi new_vi  in
  let fct = Definition(fundec, loc) in
  let new_spec = fundec.sspec in
  let new_kf = { fundec = fct; spec = new_spec } in
  Queue.add (fun () ->
      Kernel_function.Hashtbl.add fct_tbl new_kf ();
      Globals.Functions.register new_kf;
      Globals.Functions.replace_by_definition new_spec fundec loc;
      Annotations.register_funspec new_kf;
      if new_vi.vname = "main" then begin
        (* recompute the info about the old main since its name has changed;
           see the corresponding part in the main visitor *)
        Globals.Functions.remove vi;
        Globals.Functions.register kf
      end)
    actions;
  Options.feedback ~dkey ~level:2 "function %s" name;
  (* remove the specs attached to the previous kf iff it is a definition:
     it is necessary to keep stable the number of annotations in order to get
     [Keep_status] working fine. *)
  let kf = Visitor_behavior.Get.kernel_function bhv kf in
  if Kernel_function.is_definition kf then begin
    Queue.add
      (fun () ->
         let bhvs =
           Annotations.fold_behaviors (fun e b acc -> (e, b) :: acc) kf []
         in
         List.iter
           (fun (e, b) -> Annotations.remove_behavior ~force:true e kf b)
           bhvs;
         Annotations.iter_decreases
           (fun e _ -> Annotations.remove_decreases e kf)
           kf;
         Annotations.iter_terminates
           (fun e _ -> Annotations.remove_terminates e kf)
           kf;
         Annotations.iter_complete
           (fun e l -> Annotations.remove_complete e kf l)
           kf;
         Annotations.iter_disjoint
           (fun e l -> Annotations.remove_disjoint e kf l)
           kf)
      actions
  end;
  GFun(fundec, loc), GFunDecl(new_spec, new_vi, loc)

(* ********************************************************************** *)
(* Alignment *)
(* ********************************************************************** *)

241
242
243
exception Alignment_error of string
let align_error s = raise (Alignment_error s)

244
245
246
247
(* Returns true if the list of attributes [attrs] contains an [align] attribute
   of [algn] or greater. Returns false otherwise.
   Throws an exception if
   - [attrs] contains several [align] attributes specifying different
Julien Signoles's avatar
Julien Signoles committed
248
     alignments
249
   - [attrs] has a single align attribute with a value which is less than
Julien Signoles's avatar
Julien Signoles committed
250
     [algn] *)
251
let sufficiently_aligned attrs algn =
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
  let alignment =
    List.fold_left
      (fun acc attr ->
         match attr with
         | Attr("align", [AInt i]) ->
           let alignment = Integer.to_int i in
           if acc <> 0 && acc <> alignment then
             (* multiple align attributes with different values *)
             align_error "Multiple alignment attributes"
           else if alignment < algn then
             (* if there is an alignment attribute it should be greater or equal
                to [algn] *)
             align_error "Insufficient alignment"
           else
             alignment
         | Attr("align", _) ->
           (* align attribute with an argument other than a single number,
              should not happen really *)
           assert false
         | _ -> acc)
      0
      attrs
  in
  alignment > 0
276
277

(* Given the type and the list of attributes of [varinfo] ([fieldinfo]) return
278
279
   true if that [varinfo] ([fieldinfo]) requires to be aligned at the boundary
   of [algn] (i.e., less than [algn] bytes and has no alignment attribute *)
280
let require_alignment typ attrs algn =
281
  Cil.bitsSizeOf typ < algn*8 && not (sufficiently_aligned attrs algn)
282

283
284
285
286
287
288
(* ********************************************************************** *)
(* Visitor *)
(* ********************************************************************** *)

type position = Before_gmp | Gmpz | After_gmp | Memory_model | Code

289
290
291
292
class prepare_visitor = object (self)
  inherit Visitor.frama_c_inplace

  val mutable has_new_stmt_in_fundec = false
293
294
295
296
297

  (* ---------------------------------------------------------------------- *)
  (* visitor's local variable *)
  (* ---------------------------------------------------------------------- *)

298
  val terms = Misc.Id_term.Hashtbl.create 7
299
  (* table for ensuring absence of term sharing *)
300

301
302
303
304
305
306
307
308
309
310
311
  val unduplicable_functions =
    let white_list =
      [ "__builtin_va_arg";
        "__builtin_va_end";
        "__builtin_va_start";
        "__builtin_va_copy" ]
    in
    List.fold_left
      (fun acc s -> Datatype.String.Set.add s acc)
      Datatype.String.Set.empty
      white_list
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
  val fct_tbl = Cil_datatype.Varinfo.Hashtbl.create 7
  val mutable before_memory_model = Before_gmp
  val mutable new_definitions: global list = []
  (* new definitions of the annotated functions which will contain the
     translation of the E-ACSL contract *)

  val mutable sound_verdict_vi =
    let name = Functions.RTL.mk_api_name "sound_verdict" in
    let vi = Cil.makeGlobalVar name Cil.intType in
    vi.vstorage <- Extern;
    vi.vreferenced <- true;
    vi

  (* ---------------------------------------------------------------------- *)
  (* visitor's private methods *)
  (* ---------------------------------------------------------------------- *)

  method private is_variadic_function vi =
    match Cil.unrollType vi.vtype with
    | TFun(_, _, variadic, _) -> variadic
    | _ -> true

  method private before_memory_model = match before_memory_model with
    | Before_gmp | Gmpz | After_gmp -> true
    | Memory_model | Code -> false

  method private next () =
    match before_memory_model with
    | Before_gmp -> ()
    | Gmpz -> before_memory_model <- After_gmp
    | After_gmp -> ()
    | Memory_model -> before_memory_model <- Code
    | Code -> ()
346

347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
  (* IMPORTANT: for keeping property statuses, we must preserve the ordering of
     translation, see function [Translate.translate_pre_spec] and
     [Translate.translate_post_spec]: be careful when modifying it. *)

  method private push_pre_spec s =
    let kf = Extlib.the self#current_kf in
    let kinstr = self#current_kinstr in
    let open Keep_status in
    Extlib.may
      (fun v -> push kf K_Decreases (Property.ip_of_decreases kf kinstr v))
      s.spec_variant;
    Extlib.may
      (fun t -> push kf K_Terminates (Property.ip_of_terminates kf kinstr t))
      s.spec_terminates;
    List.iter
      (fun l ->
Julien Signoles's avatar
lint  
Julien Signoles committed
363
         push kf K_Complete (Property.ip_of_complete kf kinstr ~active:[] l))
364
365
366
      s.spec_complete_behaviors;
    List.iter
      (fun l ->
Julien Signoles's avatar
lint  
Julien Signoles committed
367
         push kf K_Disjoint (Property.ip_of_disjoint kf kinstr ~active:[] l))
368
369
370
      s.spec_disjoint_behaviors;
    List.iter
      (fun b ->
Julien Signoles's avatar
lint  
Julien Signoles committed
371
372
373
         List.iter
           (fun p -> push kf K_Requires (Property.ip_of_requires kf kinstr b p))
           b.b_requires)
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
      s.spec_behavior

  method private push_post_spec spec =
    let do_behavior b =
      let kf = Extlib.the self#current_kf in
      let ki = match self#current_stmt with
        | None -> Kglobal
        | Some stmt -> Kstmt stmt
      in
      let open Keep_status in
      Extlib.may
        (push kf K_Assigns)
        (Property.ip_of_assigns
           kf
           ki
           (Property.Id_contract (Datatype.String.Set.empty (* TODO *), b))
           b.b_assigns);
      List.iter
        (fun p -> push kf K_Ensures (Property.ip_of_ensures kf ki b p))
        b.b_post_cond
    in
    (* fix ordering of behaviors' iterations *)
    let bhvs =
      List.sort
        (fun b1 b2 -> String.compare b1.b_name b2.b_name)
        spec.spec_behavior
    in
    List.iter do_behavior bhvs

  method private push_pre_code_annot a =
    let kf = Extlib.the self#current_kf in
    let stmt = Extlib.the self#current_stmt in
    let push_single k a =
      Keep_status.push kf k (Property.ip_of_code_annot_single kf stmt a)
    in
    let open Keep_status in
    match a.annot_content with
    | AAssert _ -> push_single K_Assert a
    | AStmtSpec(_ (* TODO *), s) -> self#push_pre_spec s
    | AInvariant _ -> push_single K_Invariant a
    | AVariant v ->
      push kf K_Variant (Property.ip_of_decreases kf (Kstmt stmt) v)
    | AAssigns _ ->
417
      (* TODO: should be a postcondition, but considered as an unhandled
418
419
420
421
422
423
424
425
426
         precondition in translate.ml right now; and we need to preserve the
         same ordering *)
      Extlib.may
        (push kf K_Assigns)
        (Property.ip_assigns_of_code_annot kf (Kstmt stmt) a)
    | AAllocation(_ (* TODO *), alloc) ->
      Extlib.may
        (push kf K_Allocation)
        (Property.ip_of_allocation kf (Kstmt stmt) (Property.Id_loop a) alloc)
427
428
429
430
431
432
    | APragma _ ->
      (* not yet translated *)
      ()
    | AExtended _ ->
      (* never translate extensions *)
      ()
433
434

  method private push_post_code_annot a = match a.annot_content with
Julien Signoles's avatar
lint  
Julien Signoles committed
435
436
437
438
439
440
441
442
    | AStmtSpec(_ (* TODO *), s) -> self#push_post_spec s
    | AAssert _
    | AInvariant _
    | AVariant _
    | AAssigns _
    | AAllocation _
    | APragma _
    | AExtended _ -> ()
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
  (* ---------------------------------------------------------------------- *)
  (* visitor's method overloading *)
  (* ---------------------------------------------------------------------- *)

  method !vlogic_info_decl li =
    Global.add_logic_info li;
    Cil.SkipChildren

  method !vvrbl vi =
    try
      let new_vi = Cil_datatype.Varinfo.Hashtbl.find fct_tbl vi in
      (* replace functions at callsite by its duplicated version *)
      Cil.ChangeTo new_vi
    with Not_found ->
      Cil.SkipChildren

  method !vterm _t =
    Cil.DoChildrenPost
      (fun t ->
         if Misc.Id_term.Hashtbl.mem terms t then
           (* remove term sharing for soundness of E-ACSL typing
              (see typing.ml) *)
           { t with term_node = t.term_node }
         else begin
           Misc.Id_term.Hashtbl.add terms t ();
           t
         end)

  (* Add align attributes to local variables (required by temporal analysis) *)
  method !vblock _ =
    if Options.Temporal_validity.get () then
      Cil.DoChildrenPost
        (fun blk ->
           List.iter
             (fun vi ->
                (* 4 bytes alignment is required to allow sufficient space for
                   storage of 32-bit timestamps in a 1:1 shadow. *)
                if require_alignment vi.vtype vi.vattr 4 then begin
                  vi.vattr <- Attr("aligned", [ AInt Integer.four ]) :: vi.vattr
                end)
             blk.blocals;
           blk)
    else
      Cil.DoChildren

489
  method !vstmt_aux stmt =
490
491
    Annotations.iter_code_annot
      (fun _ a -> self#push_pre_code_annot a)
492
      stmt;
493
    Cil.DoChildrenPost
494
      (fun _ ->
Julien Signoles's avatar
lint  
Julien Signoles committed
495
496
         Annotations.iter_code_annot
           (fun _ a -> self#push_post_code_annot a)
497
498
499
           stmt;
         (* move variable declared in the body of a switch statement to the
            outer scope *)
Julien Signoles's avatar
lint  
Julien Signoles committed
500
501
502
         match stmt.skind with
         | Switch(_,sw_blk,_,_) ->
           let new_blk = Cil.mkBlock [ stmt ] in
503
           let new_stmt = Cil.mkStmt ~valid_sid:true (Block new_blk) in
Julien Signoles's avatar
lint  
Julien Signoles committed
504
505
           new_blk.blocals <- sw_blk.blocals;
           sw_blk.blocals <- [];
506
           has_new_stmt_in_fundec <- true;
Julien Signoles's avatar
lint  
Julien Signoles committed
507
           new_stmt
508
509
510
511
512
513
514
515
516
517
518
519
520
         | _ ->
           stmt)

  method !vfunc fundec =
    Cil.DoChildrenPost
      (fun _ ->
         if has_new_stmt_in_fundec then begin
           has_new_stmt_in_fundec <- false;
           (* recompute the CFG *)
           Cfg.clearCFGinfo ~clear_id:false fundec;
           Cfg.cfgFun fundec;
         end;
         fundec)
521
522

  method !vglob_aux = function
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
    | GFunDecl(_, vi, loc) | GFun({ svar = vi }, loc)
      when (* duplicate a function iff: *)
        not (Cil_datatype.Varinfo.Hashtbl.mem fct_tbl vi)
        (* it is not already duplicated *)
        && not (Datatype.String.Set.mem vi.vname unduplicable_functions)
        (* it is duplicable *)
        && not (self#is_variadic_function vi)
        (* it is not a variadic function *)
        && not (Misc.is_library_loc loc) (* it is not in the E-ACSL's RTL *)
        && not (Misc.is_fc_or_compiler_builtin vi) (* it is not a built-in *)
        &&
        (let kf =
           try Globals.Functions.get vi with Not_found -> assert false
         in
         not (Functions.instrument kf)
         (* either explicitely listed as to be not instrumented *)
         ||
         (* or: *)
         (not (Cil.is_empty_funspec
                 (Annotations.funspec ~populate:false
                    (Extlib.the self#current_kf)))
          (* it has a function contract *)
          && Functions.check kf
          (* its annotations must be monitored *)))
      ->
      self#next ();
      let name = Functions.RTL.mk_gen_name vi.vname in
      let new_vi = Cil.makeGlobalVar name vi.vtype in
      Cil_datatype.Varinfo.Hashtbl.add fct_tbl vi new_vi;
      Cil.DoChildrenPost
        (fun l -> match l with
           | [ GFunDecl(_, vi, _) | GFun({ svar = vi }, _) as g ]
             ->
             let kf = Extlib.the self#current_kf in
             (match g with
              | GFunDecl _ ->
                if not (Kernel_function.is_definition kf)
                && vi.vname <> "malloc" && vi.vname <> "free"
                then
                  Options.warning "@[annotating undefined function `%a':@ \
                                   the generated program may miss memory \
                                   instrumentation@ if there are \
                                   memory-related annotations.@]"
                    Printer.pp_varinfo vi
              | GFun _ -> ()
              | _ -> assert false);
             let spec = Annotations.funspec ~populate:false kf in
             self#push_pre_spec spec;
             self#push_post_spec spec;
             let tmp = vi.vname in
             if tmp = "main" then begin
               (* the new function becomes the new main: *)
               (* 1. swap the name of both functions *)
               vi.vname <- new_vi.vname;
               new_vi.vname <- tmp;
               (* 2. force recomputation of the entry point if necessary *)
               if Kernel.MainFunction.get () = tmp then begin
                 let selection =
                   State_selection.with_dependencies Kernel.MainFunction.self
                 in
                 Project.clear ~selection ()
               end
               (* 3. recompute what is necessary in [Globals.Functions]:
                  done in [dup_global] *)
             end;
             let new_g, new_decl =
               dup_global
                 loc
                 self#get_filling_actions
                 spec
                 self#behavior
                 sound_verdict_vi
                 kf
                 vi
                 new_vi
             in
             (* postpone the introduction of the new function definition to the
                end *)
             new_definitions <- new_g :: new_definitions;
             (* put the declaration before the original function in order to
                solve issue with recursive functions *)
             [ new_decl; g ]
           | _ -> assert false)

    | GVarDecl(_, loc) | GFunDecl(_, _, loc) | GFun(_, loc)
      when Misc.is_library_loc loc ->
      (match before_memory_model with
       | Before_gmp -> before_memory_model <- Gmpz
       | Gmpz | Memory_model -> ()
       | After_gmp -> before_memory_model <- Memory_model
       | Code -> () (* still processing the GMP and memory model headers,
                       but reading some libc code *));
      Cil.DoChildren

    | GVarDecl(vi, _) | GFunDecl(_, vi, _) | GFun({ svar = vi }, _)
      when Misc.is_fc_or_compiler_builtin vi ->
      self#next ();
      Cil.DoChildren

Julien Signoles's avatar
lint  
Julien Signoles committed
622
    | GVarDecl(vi, loc) | GFunDecl(_, vi, loc) | GFun({ svar = vi }, loc)
623
      when not (self#is_variadic_function vi)
Julien Signoles's avatar
lint  
Julien Signoles committed
624
      ->
625
626
      assert (* handle by the 2 cases above *)
        (not (Misc.is_library_loc loc || Misc.is_fc_or_compiler_builtin vi));
Julien Signoles's avatar
lint  
Julien Signoles committed
627
628
      let kf = Extlib.the self#current_kf in
      let s = Annotations.funspec ~populate:false kf in
629
      self#next ();
Julien Signoles's avatar
lint  
Julien Signoles committed
630
631
632
633
634
      Cil.DoChildrenPost
        (fun f ->
           self#push_pre_spec s;
           self#push_post_spec s;
           f)
635

Julien Signoles's avatar
lint  
Julien Signoles committed
636
    | _ ->
637
      self#next ();
Julien Signoles's avatar
lint  
Julien Signoles committed
638
      Cil.DoChildren
639

640
  method !vfile f =
641
    Cil.DoChildrenPost
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
      (fun _ ->
         match new_definitions with
         | [] -> f
         | _ :: _ ->
           (* add the generated definitions of libc at the end of [l]. This way,
              we are sure that they have access to all of it (in particular, the
              memory model, GMP and the soundness variable). Also add the
              [__e_acsl_sound_verdict] variable at the beginning *)
           let new_globals =
             GVarDecl(sound_verdict_vi, Cil_datatype.Location.unknown)
             :: f.globals
             @ new_definitions
           in
           f.globals <- new_globals;
           f)

  initializer
    reset ()
660

Julien Signoles's avatar
lint  
Julien Signoles committed
661
end
662
663
664

let prepare () =
  Options.feedback ~level:2 "prepare AST for E-ACSL transformations";
665
666
667
  Visitor.visitFramacFile (new prepare_visitor) (Ast.get ());
  Queue.iter (fun f -> f ()) actions;
  Ast.mark_as_grown ()
668
669
670

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