package frama-c

  1. Overview
  2. Docs

Source file register.ml

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
(**************************************************************************)
(*                                                                        *)
(*  This file is part of Frama-C.                                         *)
(*                                                                        *)
(*  Copyright (C) 2007-2023                                               *)
(*    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_types

let category = File.register_code_transformation_category "variadic"

(* Variadic will create prototype and specifications for some variadic
   functions. Since only prototypes are created, the resulting source code isn't
   compilable. This printer will print the original functions, with the replaced
   prototypes in comments beside the instruction. *)
let change_printer =
  let first = ref true in
  fun () ->
    if !first then begin
      first := false;
      let module Printer_class(X: Printer.PrinterClass) = struct
        class printer = object
          inherit X.printer as super

          method !instr fmt i =
            match i with
            (* If the instruction calls a function that have been replaced,
               then build an instruction with the old function. *)
            | Call(res, ({ enode = Lval(Var vi, o) } as fct), args, loc)
              when Replacements.mem vi ->
              let old_vi = Replacements.find vi in
              let old_vi = { vi with vname = old_vi.vname } in
              let old_instr =
                Call(res, { fct with enode = Lval(Var old_vi, o) }, args, loc)
              in
              Format.fprintf fmt "%a /* %s */" super#instr old_instr vi.vname
            (* Otherwise keep the instruction. *)
            | _ ->
              super#instr fmt i
        end
      end in
      Printer.update_printer (module Printer_class: Printer.PrinterExtension)
    end

let () =
  Cmdline.run_after_extended_stage
    begin fun () ->
      State_dependency_graph.add_dependencies
        ~from:Options.Enabled.self
        [ Ast.self ]
    end;
  Cmdline.run_after_configuring_stage
    begin fun () ->
      let translate file =
        if Options.Enabled.get () then begin
          change_printer ();
          Translate.translate_variadics file
        end
      in
      File.add_code_transformation_before_cleanup category translate
    end