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 (23)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-29.0-Copper.tar.gz

sha256=d2fbb3b8d0ff83945872e9e6fa258e934a706360e698dae3b4d5f971addf7493

doc/frama-c-eva.core/Eva/Callstack/index.html

Module `Eva.Callstack`Source

type call =
  Frama_c_kernel.Cil_types.kernel_function * Frama_c_kernel.Cil_types.stmt

A call is identified by the function called and the call statement

module Call : Frama_c_kernel.Datatype.S with type t = call

type callstack = {

thread : int;
entry_point : Frama_c_kernel.Cil_types.kernel_function;
(*
The first function function of the callstack.
*)
stack : call list;
(*
A call stack is a list of calls. The head is the latest call.
*)

}

Eva callstacks.

include Frama_c_kernel.Datatype.S_with_collections with type t = callstack

include Frama_c_kernel.Datatype.S with type t = callstack

include Frama_c_kernel.Datatype.S_no_copy with type t = callstack

include Frama_c_kernel.Datatype.Ty with type t = callstack

type t = callstack

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf

val ty : t Frama_c_kernel.Type.t

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf

val name : string

Unique name of the datatype.

val descr : t Frama_c_kernel.Descr.t

Datatype descriptor.

val packed_descr : Frama_c_kernel.Structural_descr.pack

Packed version of the descriptor.

val reprs : t list

List of representants of the descriptor.

val equal : t -> t -> bool

Equality: same spec than Stdlib.(=).

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf

val compare : t -> t -> int

Comparison: same spec than Stdlib.compare.

val hash : t -> int

Hash function: same spec than Hashtbl.hash.

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

Pretty print each value in an user-friendly way.

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf

val mem_project : (Frama_c_kernel.Project_skeleton.t -> bool) -> t -> bool

mem_project f x must return true iff there is a value p of type Project.t in x such that f p returns true.

val copy : t -> t

Deep copy: no possible sharing between x and copy x.

module Set : Frama_c_kernel.Datatype.Set with type elt = t

module Map : Frama_c_kernel.Datatype.Map with type key = t

module Hashtbl : Frama_c_kernel.Datatype.Hashtbl with type key = t

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

Prints a callstack without displaying call sites.

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

Prints a hash of the callstack when '-kernel-msg-key callstack' is enabled (prints nothing otherwise).

val compare_lex : t -> t -> int

compare_lex compares callstack lexicographically, slightly slower than compare but in a more natural order, giving more importance to the function at bottom of the callstack - the first functions called.

val init : ?thread:int -> Frama_c_kernel.Cil_types.kernel_function -> t

val push : 
  Frama_c_kernel.Cil_types.kernel_function ->
  Frama_c_kernel.Cil_types.stmt ->
  t ->
  t

Adds a new call to the top of the callstack.

val pop : t -> t option

Removes the topmost call from the callstack.

val top : 
  t ->
  (Frama_c_kernel.Cil_types.kernel_function * Frama_c_kernel.Cil_types.stmt)
    option

val top_kf : t -> Frama_c_kernel.Cil_types.kernel_function

val top_callsite : t -> Frama_c_kernel.Cil_types.kinstr

val top_call : 
  t ->
  Frama_c_kernel.Cil_types.kernel_function * Frama_c_kernel.Cil_types.kinstr

val top_caller : t -> Frama_c_kernel.Cil_types.kernel_function option

Returns the function that called the topmost function of the callstack.

Conversion

val to_kf_list : t -> Frama_c_kernel.Cil_types.kernel_function list

Gives the list of kf in the callstack from the entry point to the top of the callstack (i.e. reverse order of the call stack).

val to_stmt_list : t -> Frama_c_kernel.Cil_types.stmt list

Gives the list of call statements from the bottom to the top of the callstack (i.e. reverse order of the call stack).

val to_call_list : 
  t ->
  (Frama_c_kernel.Cil_types.kernel_function * Frama_c_kernel.Cil_types.kinstr)
    list

Gives the list of call from the bottom to the top of the callstack (i.e. reverse order of the call stack).

On This Page

Conversion