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 Dependency

frama-c.com Readme Edit opam file Versions (25)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-31.0-beta-Gallium.tar.gz

sha256=095ffbb3086a6cd963a03e3defab4f0dc32e9a43f026e552ec9ae346a6e20522

doc/frama-c-eva.gui/Eva_gui/Gui_eval/Make/argument-1-X/Compute/index.html

Module `X.Compute`

type state = Dom.t

type loc = Loc.location

type value = Val.t

val compute_from_entry_point : 
  Frama_c_kernel.Cil_types.kernel_function ->
  lib_entry:bool ->
  unit

Analysis of a program from the given main function. Computed states for each statement are stored in the result tables of each enabled abstract domain. This is called by Analysis.compute. The initial abstract state is computed according to lib_entry:

if false, non-volatile global variables are initialized according to their initializers (zero if no explicit initializer).
if true, non-const global variables are initialized at top.

val compute_from_init_state : 
  Frama_c_kernel.Cil_types.kernel_function ->
  state ->
  unit

Analysis of a program from the given main function and initial state.

val compute_call : 
  Frama_c_kernel.Cil_types.stmt ->
  (loc, value) Eva.Eval.call ->
  Eva.Eval.recursion option ->
  state ->
  state Eva__.Engine_sig.call_result

Analysis of a function call during the Eva analysis. This function is called by Transfer_stmt when interpreting a call statement. compute_call stmt call recursion state analyzes the call call at statement stmt in the input abstract state state. If recursion is not None, the call is a recursive call.