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.kernel/Frama_c_kernel/Origin/index.html

Module `Frama_c_kernel.Origin`

This module is used to track the origin of very imprecise values (namely "garbled mix", created on imprecise or unsupported operations on addresses) propagated by an Eva analysis.

include Datatype.S

include Datatype.S_no_copy

include Datatype.Ty

type t

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

val ty : t Type.t

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

val name : string

Unique name of the datatype.

val packed_descr : 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 : (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.

type kind =

| Misalign_read
| Misalign_write
| Leaf
| Merge
| Arith

val current : kind -> t

Creates an origin of the given kind, associated with the current source location extracted from Current_loc.

val well : t

Origin for garbled mix created in the initial state of the analysis (not associated to a source location).

val unknown : t

Unknown origin.

val is_unknown : t -> bool

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

Pretty-print because of <origin> if the origin is not Unknown, or nothing otherwise.

val descr : t -> string

Short description of an origin.

val join : t -> t -> t

val register : Base.SetLattice.t -> t -> unit

Records the creation of an imprecise value of the given bases.

val register_write : Base.SetLattice.t -> t -> bool

Records the write of an imprecise value of the given bases, with the given origin. Returns true if the given origin has never been written before, and if it is related to the current location — in which case a warning should probably be emitted.

val register_read : Base.SetLattice.t -> t -> unit

Records the read of an imprecise value of the given bases, with the given origin.

val pretty_history : Format.formatter -> unit

Pretty-print a summary of the origins of imprecise values recorded by register_write and register_read above.

val clear : unit -> unit

Clears the history of origins saved by register_write and register_read above.