Module `E_ACSL.Logic_functions`

Generate C implementations of user-defined logic functions. A logic function can have multiple C implementations depending on the types computed for its arguments. Eg: Consider the following definition: integer g(integer x) = x with the following calls: g(5) and g(10*INT_MAX) They will respectively generate the C prototypes int g_1(int) and long g_2(long)

val reset : unit -> unit

val app_to_exp : 
  adata:Assert.t ->
  loc:Frama_c_kernel.Cil_types.location ->
  ?tapp:Frama_c_kernel.Cil_types.term ->
  Frama_c_kernel.Cil_types.kernel_function ->
  Env.t ->
  ?eargs:Frama_c_kernel.Cil_types.exp list ->
  Frama_c_kernel.Cil_types.logic_info ->
  Frama_c_kernel.Cil_types.term list ->
  Frama_c_kernel.Cil_types.exp * Assert.t * Env.t

Translate a Tapp term or a Papp predicate to an expression. If the optional argument eargs is provided, then these expressions are used as arguments of the fonction. The optional argument tapp is the term corresponding to the call, in case we are translating a term

val add_generated_functions : 
  Frama_c_kernel.Cil_types.global list ->
  Frama_c_kernel.Cil_types.global list

val predicate_to_exp_ref : 
  (adata:Assert.t ->
    Frama_c_kernel.Cil_types.kernel_function ->
    Env.t ->
    Frama_c_kernel.Cil_types.predicate ->
    Frama_c_kernel.Cil_types.exp * Assert.t * Env.t)
    ref

val term_to_exp_ref : 
  (adata:Assert.t ->
    Frama_c_kernel.Cil_types.kernel_function ->
    Env.t ->
    Frama_c_kernel.Cil_types.term ->
    Frama_c_kernel.Cil_types.exp * Assert.t * Env.t)
    ref

Install

Dune Dependency

Authors

Maintainers

Sources

doc/frama-c-e-acsl.core/E_ACSL/Logic_functions/index.html

Module `E_ACSL.Logic_functions`

package frama-c

Install

Dune Dependency

Authors

Maintainers

Sources

doc/frama-c-e-acsl.core/E_ACSL/Logic_functions/index.html

Module E_ACSL.Logic_functions

Module `E_ACSL.Logic_functions`