package goblint

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

Module IntDomTuple.IntDomTupleImpl

include module type of struct include Printable.Std end
val tag : 'a -> 'b
type int_t = Z.t
module I1 : sig ... end
module I3 : sig ... end
module I4 : sig ... end
module I5 : sig ... end
module I6 : sig ... end
type t = I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option
val equal : t -> t -> Ppx_deriving_runtime.bool
val compare : t -> t -> Ppx_deriving_runtime.int
val hash : t -> int
val name : unit -> string
type 'a m = (module IntDomain0.SOverflow with type t = 'a)
type 'a m2 = (module IntDomain0.SOverflow with type int_t = int_t and type t = 'a)
type 'b poly_in = {
  1. fi : 'a. 'a m -> 'b -> 'a;
}
type 'b poly2_in = {
  1. fi2 : 'a. 'a m2 -> 'b -> 'a;
}
type 'b poly2_in_ovc = {
  1. fi2_ovc : 'a. 'a m2 -> 'b -> 'a * IntDomain0.overflow_info;
}
type 'b poly_pr = {
  1. fp : 'a. 'a m -> 'a -> 'b;
}
type 'b poly_pr2 = {
  1. fp2 : 'a. 'a m2 -> 'a -> 'b;
}
type 'b poly2_pr = {
  1. f2p : 'a. 'a m -> ?no_ov:bool -> 'a -> 'a -> 'b;
}
type poly1 = {
  1. f1 : 'a. 'a m -> ?no_ov:bool -> 'a -> 'a;
}
type poly1_ovc = {
  1. f1_ovc : 'a. 'a m -> ?no_ov:bool -> 'a -> 'a * IntDomain0.overflow_info;
}
type poly2 = {
  1. f2 : 'a. 'a m -> ?no_ov:bool -> 'a -> 'a -> 'a;
}
type poly2_ovc = {
  1. f2_ovc : 'a. 'a m -> ?no_ov:bool -> 'a -> 'a -> 'a * IntDomain0.overflow_info;
}
type 'b poly3 = {
  1. f3 : 'a. 'a m -> 'a option;
}
val create : 'a poly_in -> 'a -> I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option
val create2 : 'a poly2_in -> 'a -> I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option
val no_overflow : 'a -> ('b * IntDomain0.overflow_info) option -> bool
val check_ov : ?suppress_ovwarn:bool -> cast:bool -> GoblintCil.Cil.ikind -> (I2.t * IntDomain0.overflow_info) option -> (I5.t * IntDomain0.overflow_info) option -> (I6.t * IntDomain0.overflow_info) option -> bool
val create2_ovc : GoblintCil.Cil.ikind -> 'a poly2_in_ovc -> 'a -> I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option
val opt_map2 : (?no_ov:'a -> 'b -> 'c -> 'd) -> ?no_ov:'a -> 'b option -> 'c option -> 'd option
val to_list : ('a option * 'a option * 'a option * 'a option * 'a option * 'a option) -> 'a list
val to_list_some : ('a option option * 'a option option * 'a option option * 'a option option * 'a option option * 'a option option) -> 'a list
val exists : (bool option * bool option * bool option * bool option * bool option * bool option) -> bool
val for_all : (bool option * bool option * bool option * bool option * bool option * bool option) -> bool
val bot : unit -> I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option
val top_of : GoblintCil.Cil.ikind -> I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option
val bot_of : GoblintCil.Cil.ikind -> I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option
val of_bool : GoblintCil.Cil.ikind -> bool -> I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option
val of_excl_list : GoblintCil.Cil.ikind -> int_t list -> I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option
val of_int : GoblintCil.Cil.ikind -> int_t -> I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option
val starting : ?suppress_ovwarn:bool -> GoblintCil.Cil.ikind -> int_t -> I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option
val ending : ?suppress_ovwarn:bool -> GoblintCil.Cil.ikind -> int_t -> I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option
val of_interval : ?suppress_ovwarn:bool -> GoblintCil.Cil.ikind -> (int_t * int_t) -> I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option
val of_congruence : GoblintCil.Cil.ikind -> (int_t * int_t) -> I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option
val of_bitfield : GoblintCil.Cil.ikind -> (int_t * int_t) -> I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option
val refine_with_congruence : GoblintCil.Cil.ikind -> t -> (int_t * int_t) option -> t
val refine_with_interval : GoblintCil.Cil.ikind -> (I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option) -> (I6.int_t * I6.int_t) option -> I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option
val refine_with_bitfield : GoblintCil.Cil.ikind -> (I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option) -> (I6.int_t * I6.int_t) -> I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option
val refine_with_excl_list : GoblintCil.Cil.ikind -> (I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option) -> (I6.int_t list * (int64 * int64)) option -> I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option
val refine_with_incl_list : GoblintCil.Cil.ikind -> (I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option) -> I6.int_t list option -> I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option
val mapp : 'a poly_pr -> (I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option) -> 'a option * 'a option * 'a option * 'a option * 'a option * 'a option
val mapp2 : 'a poly_pr2 -> (I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option) -> 'a option * 'a option * 'a option * 'a option * 'a option * 'a option
val is_bot : (I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option) -> bool
val is_top_of : GoblintCil.Cil.ikind -> (I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option) -> bool
val is_excl_list : (I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option) -> bool
val map2p : 'a poly2_pr -> (I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option) -> (I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option) -> 'a option * 'a option * 'a option * 'a option * 'a option * 'a option
val (%%) : ('a -> 'b) -> ('c -> 'd -> 'a) -> 'c -> 'd -> 'b
val leq : (I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option) -> (I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option) -> bool
val flat : ('a list -> 'b) -> ('a option option * 'a option option * 'a option option * 'a option option * 'a option option * 'a option option) -> 'b option
val to_excl_list : (I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option) -> (int_t list * (int64 * int64)) option
val to_incl_list : (I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option) -> int_t list option
val to_bitfield : GoblintCil.Cil.ikind -> (I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option) -> Z.t * Z.t
val same : ('a -> string) -> ('a option option * 'a option option * 'a option option * 'a option option * 'a option option * 'a option option) -> 'a option
val to_int : (I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option) -> int_t option
val pretty : unit -> (I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option) -> GoblintCil.Pretty.doc
val refine_functions : GoblintCil.Cil.ikind -> (t -> t) list
val refine : GoblintCil.Cil.ikind -> t -> t
val mapovc : ?suppress_ovwarn:bool -> ?cast:bool -> GoblintCil.Cil.ikind -> poly1_ovc -> (I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option) -> t
val map2ovc : ?cast:bool -> GoblintCil.Cil.ikind -> poly2_ovc -> (I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option) -> (I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option) -> t
val map2 : ?norefine:bool -> GoblintCil.Cil.ikind -> poly2 -> (I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option) -> (I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option) -> t
val neg : ?no_ov:'a -> GoblintCil.Cil.ikind -> (I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option) -> t
val lognot : GoblintCil.Cil.ikind -> (I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option) -> t
val c_lognot : GoblintCil.Cil.ikind -> (I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option) -> t
val cast_to : ?suppress_ovwarn:bool -> ?torg:GoblintCil.Cil.typ -> ?no_ov:'a -> GoblintCil.Cil.ikind -> (I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option) -> t
val equal_to : int_t -> (I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option) -> [> `Eq | `Neq | `Top ]
val to_bool : (I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option) -> bool option
val minimal : (I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option) -> int_t option
val maximal : (I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option) -> int_t option
val show : (I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option) -> string
val to_yojson : (I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option) -> [> `List of Yojson.Safe.t list ]
val opt_map : bool -> 'a option -> 'a option -> bool -> 'a option
val map : keep:bool -> 'a poly3 -> (I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option) -> (bool * bool * bool * bool * bool * bool) -> I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option
val project : GoblintCil.Cil.ikind -> PrecisionUtil.int_precision -> (I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option) -> I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option

Project tuple t to precision p * We have to deactivate IntDomains after the refinement, since we might * lose information if we do it before. E.g. only "Interval" is active * and shall be projected to only "Def_Exc". By seting "Interval" to None * before refinement we have no information for "Def_Exc". * * Thus we have 3 Steps: * 1. Add padding to t by setting `None` to `I.top_of ik` if p is true for this element * 2. Refine the padded t * 3. Set elements of t to `None` if p is false for this element * * Side Note: * ~keep is used to reuse `map/opt_map` for Step 1 and 3. * ~keep:true will keep elements that are `Some x` but should be set to `None` by p. * This way we won't loose any information for the refinement. * ~keep:false will set the elements to `None` as defined by p

val join : GoblintCil.Cil.ikind -> (I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option) -> (I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option) -> t
val meet : GoblintCil.Cil.ikind -> (I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option) -> (I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option) -> t
val widen : GoblintCil.Cil.ikind -> (I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option) -> (I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option) -> t
val narrow : GoblintCil.Cil.ikind -> (I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option) -> (I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option) -> t
val add : ?no_ov:'a -> GoblintCil.Cil.ikind -> (I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option) -> (I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option) -> t
val sub : ?no_ov:'a -> GoblintCil.Cil.ikind -> (I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option) -> (I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option) -> t
val mul : ?no_ov:'a -> GoblintCil.Cil.ikind -> (I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option) -> (I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option) -> t
val div : ?no_ov:'a -> GoblintCil.Cil.ikind -> (I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option) -> (I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option) -> t
val rem : GoblintCil.Cil.ikind -> (I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option) -> (I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option) -> t
val lt : GoblintCil.Cil.ikind -> (I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option) -> (I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option) -> t
val gt : GoblintCil.Cil.ikind -> (I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option) -> (I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option) -> t
val le : GoblintCil.Cil.ikind -> (I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option) -> (I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option) -> t
val ge : GoblintCil.Cil.ikind -> (I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option) -> (I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option) -> t
val eq : GoblintCil.Cil.ikind -> (I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option) -> (I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option) -> t
val ne : GoblintCil.Cil.ikind -> (I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option) -> (I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option) -> t
val logand : GoblintCil.Cil.ikind -> (I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option) -> (I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option) -> t
val logor : GoblintCil.Cil.ikind -> (I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option) -> (I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option) -> t
val logxor : GoblintCil.Cil.ikind -> (I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option) -> (I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option) -> t
val shift_left : GoblintCil.Cil.ikind -> (I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option) -> (I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option) -> t
val shift_right : GoblintCil.Cil.ikind -> (I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option) -> (I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option) -> t
val c_logand : GoblintCil.Cil.ikind -> (I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option) -> (I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option) -> t
val c_logor : GoblintCil.Cil.ikind -> (I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option) -> (I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option) -> t
val pretty_diff : unit -> ((I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option) * (I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option)) -> GoblintCil.Pretty.doc
val printXml : 'a BatInnerIO.output -> (I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option) -> unit
val invariant_ikind : GoblintCil.Cil.exp -> GoblintCil.Cil.ikind -> (I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option) -> Invariant.t
val arbitrary : GoblintCil.Cil.ikind -> (I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option) QCheck.arbitrary
val relift : (I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option) -> I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option