package soteria

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

Module S_map.Mk_concrete_key

Lifts a concrete key type into the symbolic realm.

Parameters

module Symex : Symex.Base

Signature

type t = K.t
include Map.OrderedType with type t := t
val compare : t -> t -> int

A total ordering function over the keys. This is a two-argument function f such that f e1 e2 is zero if the keys e1 and e2 are equal, f e1 e2 is strictly negative if e1 is smaller than e2, and f e1 e2 is strictly positive if e1 is greater than e2. Example: a suitable ordering function is the generic structural comparison function Stdlib.compare.

include Key(Symex).Abstr.Sem_eq with type t := t
val sem_eq : t -> t -> Symex.Value.sbool Symex.Value.t
include Key(Symex).Abstr.Simplifiable with type t := t
val simplify : t -> t Symex.t
val distinct_seq : t Seq.t -> Symex.Value.sbool Symex.Value.t