package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

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

module Instantiator_builder: sig
  (** Builds a [Instantiator] module (used by [Transform]) from a [Generator_sig] *)

  (** Signature for a new instantiator generator.

      In order to support a new function, this module must be implemented and
      registered to the [Transform] module.
  *)
  module type Generator_sig = sig
    (** [Hashtbl] module used by the [Make_instantiator] module to generate the
        function cache. The [key] ([override_key]) must identify a function
        override.
    *)
    module Hashtbl: Datatype.Hashtbl
    type override_key = Hashtbl.key

    (** Name of the implemented instantiator function *)
    val function_name: string

    (** [well_typed_call ret fct args] must return true if and only if the
        corresponding call is well typed in the sens that the generator can
        produce a function override for the corresponding return value and
        parameters, according to their types and/or values.
    *)
    val well_typed_call: lval option -> varinfo -> exp list -> bool

    (** [key_from_call ret fct args] must return an identifier for the
        corresponding call. [key_from_call ret1 fct1 args1] and
        [key_from_call ret2 fct2 args2] must equal if and only if the same
        override function can be used for both call. Any call for which
        [well_typed_call] returns true must be able to give a key.
    *)
    val key_from_call: lval option -> varinfo -> exp list -> override_key

    (** [retype_args key args] must returns a new argument list compatible with
        the function identified by [override_key]. [args] is the list of arguments
        that were given to the call for with [Transform] is currently replacing.
        Most of the time, it will consists in removing/changing some casts. But
        note that arguments can be removed (for example if the override is built
        because some constant have specialized).
    *)
    val retype_args: override_key -> exp list -> exp list

    (** [args_for_original key args] must transform the list of parameters of the
        override function such that the new list can be given to the original
        function. For example, if for a call:
        [foo(x, 0, z)]
        The [Instantiator] module generates an override:
        [void foo_spec(int p1, int p3);]
        The received list of expression is [ p1 ; p3 ] and thus the returned list
        should be [ p1 ; 0 ; p3 ] (so that the replaced call [foo_spec(x, z)] has
        the same behavior).
        Note that there is no need to introduce casts to the original type, it is
        introduced by [Make_instantiator].
    *)
    val args_for_original: override_key -> exp list -> exp list

    (** [generate_prototype key] must generate the name and the type corresponding
        to [key].
    *)
    val generate_prototype: override_key -> (string * typ)

    (** [generate_spec key loc fundec] must generate the specification of the
        [fundec] generated from [key]. The location is the one generated by the
        [Transform] visitor. Note that it must return a [funspec] but should
        {b not} register it in [Annotations] tables.
    *)
    val generate_spec: override_key -> location -> fundec -> funspec
  end
end = Instantiator_builder

module Transform: sig
  (** Registers a new [Instantiator] to the visitor from the [Generator_sig] module
      of this instantiator. Each new instantiator function generator should call this
      globally.
  *)
  val register: (module Instantiator_builder.Generator_sig) -> unit
end = Transform

module Global_context:sig
  (** [get_variable name f] searches for an existing variable [name]. If this
      variable does not exists, it is created using [f].

      The obtained varinfo does not need to be registered, nor [f] needs to
      perform the registration, it will be done by the transformation.
  *)
  val get_variable: string -> (unit -> varinfo) -> varinfo
end = Global_context
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct