package frama-c

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

Signature for a new instantiator generator.

In order to support a new function, this module must be implemented and registered to the Transform module.

Hashtbl module used by the Make_instantiator module to generate the function cache. The key (override_key) must identify a function override.

type override_key = Hashtbl.key
val function_name : string

Name of the implemented instantiator function

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.

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.

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).

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 generate_prototype : override_key -> string * Frama_c_kernel.Cil_types.typ

generate_prototype key must generate the name and the type corresponding to key.

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 not register it in Annotations tables.

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events Blog 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