package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Constructors
Conversions
Accessors
Setters

Platform dedicated to the analysis of source code written in C

Install

dune-project

Dependency

frama-c.com Edit opam file Versions (30)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-33.0-Arsenic.tar.gz

sha256=9c1cbffd28bb33c17a668107e39c96e4ae7378a3d8249f69b47afc7ee964e9b8

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

Module `Eva.Position`

Position in the analysis

Description of the current position of the analysis.

type local = Frama_c_kernel.Cil_types.stmt * Callstack.t

Local position: a statement and its associated callstack.

type t = private

| RootCall of {
1. thread : int;
2. entry_point : Frama_c_kernel.Kernel_function.t;
}
| GlobalInit of Frama_c_kernel.Cil_types.varinfo
| Local of local

General position.

module type S = sig ... end

module Local : sig ... end

include S with type t := t

include Frama_c_kernel.Datatype.S_with_collections with type t := t

include Frama_c_kernel.Datatype.S with type t := t

include Frama_c_kernel.Datatype.S_no_copy with type t := t

include Frama_c_kernel.Datatype.Ty with type t := t

val ty : t Frama_c_kernel.Type.t

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

val datatype_name : string

Unique name of the datatype.

val datatype_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 loc : t -> Frama_c_kernel.Cil_types.location

loc p returns the source location of the given position.

val pos : t -> Frama_c_kernel.Filepos.t

pos p returns the source file of the given position.

val kinstr : t -> Frama_c_kernel.Cil_types.kinstr

kinstr p returns the kinstr associated to the position.

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

Pretty-print the position as a location in a source file. In the case of a local position, the short callstack leading to that position is also printed.

Constructors

val local : Frama_c_kernel.Cil_types.stmt -> Callstack.t -> t

local stmt cs creates a local position.

val root_call : 
  thread:int ->
  entry_point:Frama_c_kernel.Cil_types.kernel_function ->
  t

root_call ~thread ~entry_point creates a position pointing to the root call of the analysis.

val global_init : Frama_c_kernel.Cil_types.varinfo -> t

global_init vi creates a position pointing to the global variable vi's initialization.

Conversions

val of_kinstr : Frama_c_kernel.Cil_types.kinstr -> Callstack.t -> t

of_kinstr ki callstack creates a position at the given kinstr and the given callstack. If kinstr is Kstmt, it will be a local position. Otherwise, the position will be the top of the callstack or a global position if the callstack is empty.

val of_local : local -> t

of_local lpos coerces a local position into a general position.

Accessors

val is_local : t -> bool

is_local p returns true if p is a local position.

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

kf p returns the kernel function of a local position p or None if it is a global position.

val stmt : t -> Frama_c_kernel.Cil_types.stmt option

stmt p returns the stmt of a local position p or None if it is a global position.

val callstack : t -> Callstack.t option

callstack p returns the callstack of a local position or None if it is a global position.

Setters

val set_stmt : Frama_c_kernel.Cil_types.stmt -> t -> t option

set_stmt stmt p changes the statement of a local or root call position p to stmt and returns the updated position, or returns None if it is a global position.

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

push_kf kf p, if p is a local position, returns an updated local position where the given kf has been pushed on the callstack and the statement points to the first statement of the given kf. The function returns None if p is a global position.