package frama-c

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

Utility functions for generating C implementations.

val must_translate : Frama_c_kernel.Property.t -> bool
  • returns

    true if the given property must be translated (ie. if the valid properties must be translated or if its status is not True), false otherwise.

val must_translate_opt : Frama_c_kernel.Property.t option -> bool

Same than must_translate but for Property.t option. Return false if the option is None.

Translate the given GMP integer to an expression of type size_t. RTE checks are generated to ensure that the GMP value holds in this type. The parameter name is used to generate relevant predicate names. If check_lower_bound is set to false, then the GMP value is assumed to be positive. If pp is provided, this term is used in the messages of the RTE checks.

comparison_to_exp ~data ~loc kf env ity ?e1 ?name bop t1 t2 topt generates the C code equivalent to t1 bop t2 in the given environment with the given assertion context. ity is the number type of the comparison when comparing scalar numbers. e1 is the expression representing t1 if the term has already been translated. name is used to generate temporary variable names. topt is the term holding the result of the comparison.

conditional_to_exp ?name ~loc kf t_opt e1 (e2, env2) (e3, env3) generates the C code equivalent to e1 ? e2 : e3 in the given environment. env2 and env3 are the environment respectively for e2 and e3. t_opt is the term holding the result of the conditional.

env_of_li ~adata ~loc kf env li translates the logic info li in the given environment with the given assertion 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