package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

Platform dedicated to the analysis of source code written in C

Install

dune-project

Dependency

frama-c.com Readme Edit opam file Versions (26)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-32.0-beta-Germanium.tar.gz

sha256=868d57ef8007fe6c0836cd151d8c294003af34aa678285eff9547662cad36aa3

doc/src/frama-c-acsl-importer.core/register.ml.html

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
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
(**************************************************************************)
(*                                                                        *)
(*  SPDX-License-Identifier LGPL-2.1                                      *)
(*  Copyright (C)                                                         *)
(*  CEA (Commissariat à l'énergie atomique et aux énergies alternatives)  *)
(*                                                                        *)
(**************************************************************************)

(** {1 API [ACSL_importer.paste_global_annot].} *)

let paste_global_annot pfile pline cfile s ast =
  Paste.paste_global_annot ~pfile ~pline ~cfile s ast
let paste_global_annot =
  Dynamic.register
    ~plugin:"ACSL_importer"
    "paste_global_annot"
    (Datatype.func
       ~label:("pfile",None) Datatype.string
       (Datatype.func
          ~label:("pline",None) Datatype.int
          (Datatype.func
             ~label:("cfile",None) Filepath.ty
             (Datatype.func
                Datatype.string
                (Datatype.func
                   Cil_datatype.File.ty
                   Datatype.unit)))))
    paste_global_annot

let paste_global_annot
    ?(pfile="ACSL-importer-buffer") ?(pline=1) ?(cfile=Filepath.empty)
    s ast =
  paste_global_annot pfile pline cfile s ast

(** {1 API [ACSL_importer.paste_fun_spec].} *)

let paste_fun_spec kf pfile pline cfile s ast =
  Paste.paste_fun_spec kf ~pfile ~pline ~cfile s ast
let paste_fun_spec =
  Dynamic.register
    ~plugin:"ACSL_importer"
    "paste_fun_spec"
    (Datatype.func
       Kernel_function.ty
       (Datatype.func
          ~label:("pfile",None) Datatype.string
          (Datatype.func
             ~label:("pline",None) Datatype.int
             (Datatype.func
                ~label:("cfile",None) Filepath.ty
                (Datatype.func
                   Datatype.string
                   (Datatype.func
                      Cil_datatype.File.ty
                      Datatype.unit))))))
    paste_fun_spec

let get_cfile kf =
  let glob = Kernel_function.get_global kf in
  let file = (fst (Cil_datatype.Global.loc glob)).Filepath.pos_path in
  file

let paste_fun_spec
    kf ?(pfile="ACSL-importer-buffer") ?(pline=1) ?(cfile=(get_cfile kf))
    s ast =
  paste_fun_spec kf pfile pline cfile s ast

(** {1 API [ACSL_importer.paste_code_annot].} *)

let paste_code_annot kf stmt pfile pline cfile s ast =
  Paste.paste_code_annot kf stmt ~pfile ~pline ~cfile s ast

let paste_code_annot =
  Dynamic.register
    ~plugin:"ACSL_importer"
    "paste_code_annot"
    (Datatype.func
       Kernel_function.ty
       (Datatype.func
          Cil_datatype.Stmt.ty
          (Datatype.func
             ~label:("pfile",None) Datatype.string
             (Datatype.func
                ~label:("pline",None) Datatype.int
                (Datatype.func
                   ~label:("cfile",None) Filepath.ty
                   (Datatype.func
                      Datatype.string
                      (Datatype.func
                         Cil_datatype.File.ty
                         Datatype.unit)))))))
    paste_code_annot

let paste_code_annot
    kf stmt ?(pfile="ACSL-importer-buffer")
    ?(pline=1) ?(cfile=(get_cfile kf)) s ast =
  paste_code_annot kf stmt pfile pline cfile s ast

(** {1 API [ACSL_importer.import].} *)

(** Import process. *)
let import ~iDir ast nb pfile =
  Import.import ~iDir ~pfile ~init_typenames:(nb==0) ast ;
  nb+1

let import iDir files ast =
  if not (files = []) then
    begin
      let close_importation () =
        Paste.SymbolIndex.clear_temporary_table () ;
        Logic_env.reset_typenames ();
        (* importation may put additional dependencies between globals.
             Just ask for a reordering at the end of the process.
        *)
        File.reorder_custom_ast ast
        (* File.pretty_ast () *)
      in
      (*        try *)
      let nb = List.fold_left (import ~iDir ast) 0 files in
      close_importation () ;
      (*        with e ->
                  close_importation () ;
                  raise e *)
      Options.feedback "Done: %d file%s.@."
        nb
        (if nb > 1 then "s" else "")
    end

let import files1 files2 ast =
  import
    (Options.Idirs.get ())
    (files1 @ (Options.Import.get ()) @ files2)
    ast;
  Options.set_importation_off ()

let import =
  Dynamic.register
    ~plugin:"ACSL_importer"
    "import"
    (Datatype.func (Datatype.list Datatype.string)
       (Datatype.func (Datatype.list Datatype.string)
          (Datatype.func Cil_datatype.File.ty Datatype.unit)))
    import

(** {1 API [ACSL_importer.import_from_cmdline].} *)

(** Import from the cmdline process. *)
let import_from_cmdline ast =
  Options.feedback ~level:2 "Importing..." ;
  import [] [] ast;
  Options.set_importation_off ()

let import_from_cmdline =
  Dynamic.register
    ~plugin:"ACSL_importer"
    "import_from_cmdline"
    (Datatype.func Cil_datatype.File.ty Datatype.unit)
    import_from_cmdline

(** {1 API [ACSL_importer.main].} *)

let dkey = Options.register_category "trace-job"

(** The main entry point. *)
let main ast =
  Options.debug ~level:2 ~dkey "Start ACSL_importer plugin...@." ;
  if Options.is_importation_on () then import_from_cmdline ast ;
  Options.debug ~level:2 ~dkey "Stop ACSL_importer plugin...@."

(** Register the function [main] as a main entry point. *)
let () =
  let main =
    Dynamic.register
      ~plugin:"ACSL_importer"
      "main"
      (Datatype.func Cil_datatype.File.ty Datatype.unit)
      main
  in
  File.add_code_transformation_after_cleanup
    ~deps:[(module Options.Import:Parameter_sig.S);
           (module Options.Run:Parameter_sig.S)]
    ~before:[Unfold_loops.transform] Options.main_import main