package goblint

  1. Overview
  2. Docs
package goblint
Legend:
Library
Module
Module type
Parameter
Class
Class type

This functor creates an array representation by the indexes of all null bytes * the array must and may contain. This is useful to analyze strings, i.e. null- * terminated char arrays, and particularly to determine if operations on strings * could lead to a buffer overflow. Concrete values from Val are not interesting * for this domain. It additionally tracks the array size.

Parameters

module Idx : IntDomain.Z

Signature

include S0 with type value = Val.t with type idx = Idx.t
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 -> Printable.Pretty.doc
val printXml : 'a BatInnerIO.output -> t -> unit
val name : unit -> string
val to_yojson : t -> Yojson.Safe.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) -> Lattice.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 idx = Idx.t

The abstract domain used to index on arrays.

type value = Val.t

The abstract domain of values stored in the array.

val set : VDQ.t -> t -> (Basetype.CilExp.t option * idx) -> value -> t

Returns a new abstract value, where the given index is replaced with the * given element.

val make : ?varAttr:GoblintCil.Cil.attributes -> ?typAttr:GoblintCil.Cil.attributes -> idx -> value -> t

make l e creates an abstract representation of an array of length l * containing the element e.

val length : t -> idx option

returns length of array if known

val move_if_affected : ?replace_with_const:bool -> VDQ.t -> t -> GoblintCil.Cil.varinfo -> (GoblintCil.Cil.exp -> int option) -> t

changes the way in which the array is partitioned if this is necessitated by a change * to the variable *

val get_vars_in_e : t -> GoblintCil.Cil.varinfo list

returns the variables occuring in the expression according to which the * array was partitioned (if any)

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

Apply a function to all elements of the array.

val fold_left : ('a -> value -> 'a) -> 'a -> t -> 'a

Left fold (like List.fold_left) over the arrays elements

val smart_join : (GoblintCil.Cil.exp -> IntOps.BigIntOps.t option) -> (GoblintCil.Cil.exp -> IntOps.BigIntOps.t option) -> t -> t -> t
val smart_widen : (GoblintCil.Cil.exp -> IntOps.BigIntOps.t option) -> (GoblintCil.Cil.exp -> IntOps.BigIntOps.t option) -> t -> t -> t
val smart_leq : (GoblintCil.Cil.exp -> IntOps.BigIntOps.t option) -> (GoblintCil.Cil.exp -> IntOps.BigIntOps.t option) -> t -> t -> bool
val update_length : idx -> t -> t
val project : ?varAttr:GoblintCil.Cil.attributes -> ?typAttr:GoblintCil.Cil.attributes -> VDQ.t -> t -> t
val invariant : value_invariant: (offset:GoblintCil.Cil.offset -> lval:GoblintCil.Cil.lval -> value -> Invariant.t) -> offset:GoblintCil.Cil.offset -> lval:GoblintCil.Cil.lval -> t -> Invariant.t
type ret =
  1. | Null
  2. | NotNull
  3. | Maybe
type substr =
  1. | IsNotSubstr
  2. | IsSubstrAtIndex0
  3. | IsMaybeSubstr
val get : VDQ.t -> t -> (Basetype.CilExp.t option * idx) -> ret
val to_null_byte_domain : string -> t
val to_string_length : t -> idx

Returns length of string represented by input abstract value

val string_copy : t -> t -> int option -> t

string_copy dest src n returns an abstract value representing the copy of string src * into array dest, taking at most n bytes of src if present

val string_concat : t -> t -> int option -> t

string_concat s1 s2 n returns a new abstract value representing the string * concatenation of the input abstract values s1 and s2, taking at most n bytes of * s2 if present

val substring_extraction : t -> t -> substr

substring_extraction haystack needle returns IsNotSubstr if the string represented by * the abstract value needle surely isn't a substring of haystack, IsSubstrAtIndex0 if * needle is the empty string, else IsMaybeSubstr

val string_comparison : t -> t -> int option -> idx

string_comparison s1 s2 n returns a negative / positive idx element if the string * represented by s1 is less / greater than the one by s2 or zero if they are equal; * only compares the first n bytes if present

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct