package goblint

  1. Overview
  2. Docs
package goblint
Legend:
Library
Module
Module type
Parameter
Class
Class type
module M = Messages
val is_ignorable_type : Cil.typ -> bool
val is_ignorable : (Cil.varinfo * 'a) option -> bool
module Ident : Printable.S with type t = string
module LabeledString : sig ... end
module LSSet : sig ... end
module LSSSet : sig ... end
module PartAccessResult : sig ... end
val unsound : bool Batteries.ref
val init : Cil.file -> unit
type offs = [
  1. | `NoOffset
  2. | `Index of offs
  3. | `Field of CilType.Fieldinfo.t * offs
]
val equal_offs : offs -> offs -> Ppx_deriving_runtime.bool
val remove_idx : Cil.offset -> offs
val addOffs : [< `Field of CilType.Fieldinfo.t * 'a | `Index of 'a | `NoOffset ] as 'a -> offs -> offs
val d_offs : unit -> offs -> Pretty.doc
type acc_typ = [
  1. | `Type of CilType.Typ.t
  2. | `Struct of CilType.Compinfo.t * offs
]
val equal_acc_typ : acc_typ -> acc_typ -> Ppx_deriving_runtime.bool
val d_acct : unit -> [< `Struct of Cil.compinfo * offs | `Type of Cil.typ ] -> Pretty.doc
val file_re : Str.regexp
val d_loc : unit -> CilType.Location.t -> Pretty.doc
val d_memo : unit -> ([< `Struct of Cil.compinfo * offs | `Type of Cil.typ ] * (Cil.varinfo * offs) option) -> Pretty.doc
val get_type : Cil.typ -> Cil.exp -> acc_typ
module HtF (T : Batteries.Hashtbl.HashedType) : sig ... end
module Ht : sig ... end
module TypeHash : sig ... end
module LvalOptHash : sig ... end
module PartOptHash : sig ... end
type var_o = Cil.varinfo option
type off_o = Cil.offset option
type part = LSSSet.t * LSSet.t
val get_val_type : Cil.exp -> var_o -> off_o -> acc_typ
val some_accesses : bool Batteries.ref
val add_one : Cil.exp -> bool -> int -> acc_typ -> (Cil.varinfo * offs) option -> part -> unit
val type_from_type_offset : acc_typ -> Cil.typ
val add_struct : Cil.exp -> bool -> int -> acc_typ -> (Cil.varinfo * offs) option -> part -> unit
val add_propagate : Cil.exp -> bool -> int -> acc_typ -> 'a -> part -> unit
val distribute_access_lval : (bool -> bool -> 'a -> Cil.exp -> 'b) -> bool -> bool -> 'a -> Cil.lval -> unit
val distribute_access_lval_addr : (bool -> bool -> 'a -> Cil.exp -> 'b) -> bool -> bool -> 'a -> Cil.lval -> unit
val distribute_access_offset : (bool -> bool -> 'a -> Cil.exp -> 'b) -> 'a -> Cil.offset -> unit
val distribute_access_exp : (bool -> bool -> 'a -> Cil.exp -> 'b) -> bool -> bool -> 'a -> Cil.exp -> unit
val add : Cil.exp -> bool -> int -> var_o -> off_o -> part -> unit
val partition_race : 'a option -> (('b * bool * 'c * 'd * 'e) Batteries.Set.t * LSSet.t) -> bool
val only_read : 'a -> (('b * bool * 'c * 'd * 'e) Batteries.Set.t * 'f) -> bool
val common_resource : 'a -> ('b * LSSet.t) -> bool
val bot_partition : 'a option -> 'b -> bool
val check_accs : ('a option * LSSet.t * bool) -> ('a * bool * 'b * 'c * LSSet.t) -> 'a option * LSSet.t * bool
val check_safe : 'a option -> (('b * bool * 'c * 'd * LSSet.t) Batteries.Set.t * 'e) -> 'b option -> 'b option
val is_all_safe : unit -> bool
val print_summary : unit -> unit
val print_accesses : unit -> unit
val print_result : unit -> unit