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

dune-project

Dependency

sha256=5b13574a16a58971c27909bee94ae7f37b17d897852b40c768a3d4e2e09e39d2

State_builder.of outputs. That is over-approximation of zones written by each function.

include INOUT with type t = Locations.Zone.t

include INOUTKF with type t = Locations.Zone.t

type t = Locations.Zone.t

val self_internal : State.t ref

val self_external : State.t ref

val compute : (Cil_types.kernel_function -> unit) ref

val get_internal : (Cil_types.kernel_function -> t) ref

Inputs/Outputs with local and formal variables

val get_external : (Cil_types.kernel_function -> t) ref

Inputs/Outputs without either local or formal variables

val display : (Format.formatter -> Cil_types.kernel_function -> unit) ref

val pretty : Format.formatter -> t -> unit

val statement : (Cil_types.stmt -> t) ref

val kinstr : Cil_types.kinstr -> t option

val display_external : 
  (Format.formatter -> Cil_types.kernel_function -> unit) ref