package frama-c

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

Register special annotations to locally guide the Eva analysis:

  • slevel annotations: "slevel default", "slevel merge" and "slevel i"
  • loop unroll annotations: "loop unroll term"
  • value partitioning annotations: "split term" and "merge term"
  • subdivision annotations: "subdivide i"
type slevel_annotation =
  1. | SlevelMerge
    (*

    Join all states separated by slevel.

    *)
  2. | SlevelDefault
    (*

    Use the limit defined by -eva-slevel.

    *)
  3. | SlevelLocal of int
    (*

    Use the given limit instead of -eva-slevel.

    *)
  4. | SlevelFull
    (*

    Remove the limit of number of separated states.

    *)

Annotations tweaking the behavior of the -eva-slevel parameter.

type unroll_annotation =
  1. | UnrollAmount of Frama_c_kernel.Cil_types.term
    (*

    Unroll the n first iterations.

    *)
  2. | UnrollFull
    (*

    Unroll amount defined by -eva-default-loop-unroll.

    *)

Loop unroll annotations.

type split_kind =
  1. | Static
  2. | Dynamic
type split_term =
  1. | Expression of Frama_c_kernel.Cil_types.exp
  2. | Predicate of Frama_c_kernel.Cil_types.predicate

Splits can be performed according to a C expression or an ACSL predicate.

type flow_annotation =
  1. | FlowSplit of split_term * split_kind
    (*

    Split states according to a term.

    *)
  2. | FlowMerge of split_term
    (*

    Merge states separated by a previous split.

    *)

Split/merge annotations for value partitioning.

type allocation_kind =
  1. | By_stack
  2. | Fresh
  3. | Fresh_weak
  4. | Imprecise
type domain_scope = string * Frama_c_kernel.Cil_types.varinfo list
val get_slevel_annot : Frama_c_kernel.Cil_types.stmt -> slevel_annotation option
val get_unroll_annot : Frama_c_kernel.Cil_types.stmt -> unroll_annotation list
val get_flow_annot : Frama_c_kernel.Cil_types.stmt -> flow_annotation list
val get_subdivision_annot : Frama_c_kernel.Cil_types.stmt -> int list
val add_slevel_annot : emitter:Frama_c_kernel.Emitter.t -> Frama_c_kernel.Cil_types.stmt -> slevel_annotation -> unit
val add_unroll_annot : emitter:Frama_c_kernel.Emitter.t -> Frama_c_kernel.Cil_types.stmt -> unroll_annotation -> unit
val add_subdivision_annot : emitter:Frama_c_kernel.Emitter.t -> Frama_c_kernel.Cil_types.stmt -> int -> unit
val add_array_segmentation : emitter:Frama_c_kernel.Emitter.t -> Frama_c_kernel.Cil_types.stmt -> array_segmentation -> unit
val add_domain_scope : emitter:Frama_c_kernel.Emitter.t -> Frama_c_kernel.Cil_types.stmt -> domain_scope -> unit
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