Module `HoareDomain.HoarePO`

Parameters

module E : Lattice.PO

Signature

type bucket = E.t list

type t = bucket Batteries.Map.Int.t

module Map = Batteries.Map.Int

module B : sig ... end

val elements : 'a list Map.t -> 'a list

val merge : 
  [< `Join | `Meet Join ] ->
  ('a -> 'a -> 'a) ->
  'a list Map.t ->
  'a list Map.t ->
  'a list Map.t

val merge_meet : 
  ('a -> 'b -> 'c) ->
  'b list Map.t ->
  'a list Map.t ->
  'c list Map.t

val merge_widen : 
  (E.t -> E.t -> E.t) ->
  E.t list Map.t ->
  E.t list Map.t ->
  E.t list Map.t

val merge_join : 
  (E.t -> E.t -> E.t) ->
  E.t list Map.t ->
  E.t list Map.t ->
  E.t list Map.t

val join : E.t list Map.t -> E.t list Map.t -> E.t list Map.t

val widen : E.t list Map.t -> E.t list Map.t -> E.t list Map.t

val meet : E.t list Map.t -> E.t list Map.t -> E.t list Map.t

val narrow : E.t list Map.t -> E.t list Map.t -> E.t list Map.t

val of_list_by : (E.t -> E.t -> E.t) -> E.t list -> E.t list Map.t

val of_list : E.t list -> E.t list Map.t

val keep_apart : 'a -> 'b -> 'c

val of_list_apart : E.t list -> E.t list Map.t

val singleton : E.t -> E.t list Map.t

val exists : ('a -> bool) -> 'a list Map.t -> bool

val for_all : ('a -> bool) -> 'a list Map.t -> bool

val mem : E.t -> E.t list Map.t -> bool

val choose : 'a list Map.t -> 'a

val apply_list : ('a list -> E.t list) -> 'a list Map.t -> E.t list Map.t

val map : ('a -> E.t) -> 'a list Map.t -> E.t list Map.t

val filter : (E.t -> bool) -> E.t list Map.t -> E.t list Map.t

val remove : E.t -> E.t list Map.t -> E.t list Map.t

val add : E.t -> E.t list Map.t -> E.t list Map.t

val fold : ('a -> 'b -> 'b) -> 'a list Map.t -> 'b -> 'b

val cardinal : 'a list Map.t -> int

val diff : E.t list Map.t -> E.t list Map.t -> E.t list Map.t

val empty : unit -> 'a Map.t

val is_empty : 'a Map.t -> bool

val union : E.t list Map.t -> E.t list Map.t -> E.t list Map.t

val iter : ('a -> unit) -> 'a list Map.t -> unit

val is_element : 'a -> 'a list Map.t -> bool

val bot : unit -> 'a Map.t

val is_bot : 'a Map.t -> bool

val top : unit -> 'a

val is_top : 'a -> bool

val leq : E.t list Map.t -> E.t list Map.t -> bool

val name : unit -> string

val equal : E.t list Map.t -> E.t list Map.t -> bool

val hash : E.t list Map.t -> int

val compare : E.t list Map.t -> E.t list Map.t -> int

val show : E.t list Map.t -> string

val to_yojson : E.t list Map.t -> [> `List of Printable.json list ]

val pretty : unit -> E.t list Map.t -> Pretty.doc

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

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

Install

Dune Dependency

Authors

Maintainers

Sources

doc/goblint.lib/HoareDomain/HoarePO/index.html

Module `HoareDomain.HoarePO`

Parameters

Signature

package goblint

Install

Dune Dependency

Authors

Maintainers

Sources

doc/goblint.lib/HoareDomain/HoarePO/index.html

Module HoareDomain.HoarePO

Parameters

Signature

Module `HoareDomain.HoarePO`