Module Smt_model

module Smt_model: sig .. end
Internal model representation

type t 

Model types


type address = int64 
type identifier = string 
val empty : t

Constructors

Empty model. Any lookup in it will raise Not_found

val extract : Smtlib_ast.model -> t
extract model extracts relevant information in SMT-LIB model concerning ** registers and memory values. ** This function takes into account the various "model dialects" spoken by: ** - Z3; ** - CVC4; ** - Boolector
val yices_extract : string -> t
yices_extract s extracts the same information as extract but for a ** yices-smt2 produced model ** yices-smt2 models use another syntax and are parsed on their own ** s is expected to be the raw string of the model and not, for example, a ** filename

Pretty-printer


val pp : Format.formatter -> t -> unit

Accessors


val find_register : t -> identifier -> Bitvector.t
find_register model name finds the bitvector value of register name in ** the model ** Raise Not_found
val find_address_contents : t -> address -> int
find_address_contents model addr find the (byte-sized) value of address ** addr from the model. ** Raise Not_found
val find_address_content : t ->
address -> Basic_types.ByteSize.t -> Dba.endianness -> Bitvector.t
Not yet implemented
val registers : t -> identifier list
get_register model gets the list of registers of this model
val memory_addresses : t -> address list
get_register model gets the list of addresses with specific values of this ** model
val is_memory_set : t -> address -> bool
is_memory_set model address checks if the given address is present in the ** memory of this model