Module LibraryFunctions

This allows us to query information about library functions.

type categories = [
  1. | `Malloc of Prelude.Ana.exp
  2. | `Calloc of Prelude.Ana.exp * Prelude.Ana.exp
  3. | `Realloc of Prelude.Ana.exp * Prelude.Ana.exp
  4. | `Assert of Prelude.Ana.exp
  5. | `Lock of bool * bool * bool
  6. | `Unlock
  7. | `ThreadCreate of Prelude.Ana.exp * Prelude.Ana.exp * Prelude.Ana.exp
  8. | `ThreadJoin of Prelude.Ana.exp * Prelude.Ana.exp
  9. | `Unknown of string
]

Categories of special functions

val classify : string -> Prelude.Ana.exp list -> categories
type action = [
  1. | `Write
    (*

    argument may be read or written to

    *)
  2. | `Read
    (*

    argument may be read

    *)
]

Specifies what is known about an argument.

val get_invalidate_action : string -> (action -> Prelude.Ana.exp list -> Prelude.Ana.exp list) option

Returns None if nothing is known about given function. * Otherwise will return function that filters out arguments * that may be read or also written to.

val get_threadsafe_inv_ac : string -> (action -> Prelude.Ana.exp list -> Prelude.Ana.exp list) option

Same as get_invalidate_action, but replaces arguments for thread-safe functions.

val add_lib_funs : string list -> unit
val add_effects : (string -> Cil.exp list -> (Cil.lval * ValueDomain.Compound.t) list option) -> unit
val effects_for : string -> Cil.exp list -> (Cil.lval * ValueDomain.Compound.t) list list
val use_special : string -> bool

This is for when we need to use special transfer function on functions calls that have definitions.

val osek_renames : bool Prelude.Ana.ref
val is_safe_uncalled : string -> bool