package goblint

You can search for identifiers within the package.

in-package search v0.2.0

Static analysis framework for C

Install

Dune Dependency

goblint.in.tum.de Readme Changelog Edit opam file Versions (8)

Authors

Maintainers

Sources

goblint-1.1.1.tbz

sha256=999272bfbd3b9b96fcd58987b237ac6e9fa6d92ef935cc89f1ea2b4205185141

sha512=f3bf6ab71cf8c258d3290da4bf9f6fe42d7c671822e0efeb0fc50afdff078ab15e352237e5c1db31c5aa3a9d430691268ed2e5e00da10f2615835f672f91683d

doc/goblint.lib/LvalMapDomain/Value/index.html

Module `LvalMapDomain.Value`

Parameters

module Impl : sig ... end

Signature

include Lattice.S

include Lattice.PO

include Printable.S

type t

val equal : t -> t -> bool

val hash : t -> int

val compare : t -> t -> int

val show : t -> string

val pretty : unit -> t -> Pretty.doc

val printXml : 'a BatInnerIO.output -> t -> unit

val name : unit -> string

val to_yojson : t -> Printable.json

val invariant : Invariant.context -> t -> Invariant.t

val tag : t -> int

Unique ID, given by HConsed, for context identification in witness

val arbitrary : unit -> t QCheck.arbitrary

val relift : t -> t

val leq : t -> t -> bool

val join : t -> t -> t

val meet : t -> t -> t

val widen : t -> t -> t

widen x y assumes leq x y. Solvers guarantee this by calling widen old (join old new).

val narrow : t -> t -> t

val pretty_diff : unit -> (t * t) -> Pretty.doc

If leq x y = false, then pretty_diff () (x, y) should explain why.

val bot : unit -> t

val is_bot : t -> bool

val top : unit -> t

val is_top : t -> bool

type k = Lval.CilLval.t

type s = Impl.s

type r

val string_of : t -> string

val string_of_key : k -> string

val string_of_record : r -> string

val make : k -> Cil.location list -> s -> t

val map : (r -> r) -> t -> t

val filter : (r -> bool) -> t -> t

val union : t -> t -> t

val set_key : k -> t -> t

val set_state : s -> t -> t

val remove_state : s -> t -> t

val split : t -> r Prelude.Set.t * r Prelude.Set.t

val map' : (r -> 'a) -> t -> 'a Prelude.Set.t * 'a Prelude.Set.t

val filter' : (r -> bool) -> t -> r Prelude.Set.t * r Prelude.Set.t

val length : t -> int * int

val must : (r -> bool) -> t -> bool

val may : (r -> bool) -> t -> bool

val key : r -> k

val loc : r -> Cil.location list

val edit_loc : (Cil.location list -> Cil.location list) -> r -> r

val state : r -> s

val in_state : s -> r -> bool

val get_record : t -> r option

val make_var : k -> t

val from_tuple : (r Prelude.Set.t * r Prelude.Set.t) -> t

val is_alias : t -> bool

val get_alias : t -> k

val make_alias : k -> t

On This Page

Parameters
Signature