package frama-c

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

Declarations that are useful for plugins written on top of the results of Value.

Value call-site. A callsite (f,p) represents a call at function f invoked from program point p.

type callstack = call_site list

Value callstacks, as used e.g. in Db.Value hooks.

The head call site (f,p) is the most recent one, where current function f has been called from program point p.

Therefore, the tail call site is expected to be (main,Kglobal) where main is the global entry point.

Moreover, given two consecutive call-sites …(_,p);(g,_)… in a callstack, program point p is then expected to live in function g.

module Callstack : sig ... end
type 'a callback_result =
  1. | Normal of 'a
  2. | NormalStore of 'a * int
  3. | Reuse of int
type call_froms = (Function_Froms.froms * Locations.Zone.t) option

If not None, the froms of the function, and its sure outputs; i.e. the dependencies of the result, and the dependencies of each zone written to.

Dependencies for the evaluation of a term or a predicate: for each program point involved, sets of zones that must be read

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