package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

Platform dedicated to the analysis of source code written in C

Install

sha256=d2fbb3b8d0ff83945872e9e6fa258e934a706360e698dae3b4d5f971addf7493

type slevel_annotation =

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

type unroll_annotation =

| UnrollAmount of Frama_c_kernel.Cil_types.term
(*
Unroll the n first iterations.
*)
| UnrollFull
(*
Unroll amount defined by -eva-default-loop-unroll.
*)

Loop unroll annotations.

type split_kind =

type split_term =

type flow_annotation =

| FlowSplit of split_term * split_kind
(*
Split states according to a term.
*)
| FlowMerge of split_term
(*
Merge states separated by a previous split.
*)

Split/merge annotations for value partitioning.

type allocation_kind =

type array_segmentation =
  Frama_c_kernel.Cil_types.varinfo
  * Frama_c_kernel.Cil_types.offset
  * Frama_c_kernel.Cil_types.exp list

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 get_allocation : Frama_c_kernel.Cil_types.stmt -> allocation_kind

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_flow_annot : 
  emitter:Frama_c_kernel.Emitter.t ->
  Frama_c_kernel.Cil_types.stmt ->
  flow_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