Frama-C:
Plug-ins:
Libraries:

Frama-C API - Position

Position in the analysis

Description of the current position of the analysis.

Local position: a statement and its associated callstack.

type t = private
  1. | RootCall of {
    1. thread : int;
    2. entry_point : Frama_c_kernel.Kernel_function.t;
    }
  2. | GlobalInit of Frama_c_kernel.Cil_types.varinfo
  3. | 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 datatype_name : string

Unique name of the datatype.

val datatype_descr : t Frama_c_kernel.Descr.t

Datatype descriptor.

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.(=).

val compare : t -> t -> int

Comparison: same spec than Stdlib.compare.

val hash : t -> int

Hash function: same spec than Hashtbl.hash.

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

Pretty print each value in an user-friendly way.

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

loc p returns the source location of the given position.

pos p returns the source file of the given position.

kinstr p returns the kinstr associated to the position.

val pretty_loc : Stdlib.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

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

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.

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.