Internal model representation
type address = Bitvector.tval empty : tConstructors
Empty model. * *
Not_found on lookup.
val extract : Smtlib.model -> textract model extracts relevant information in SMT-LIB model concerning registers and memory values. This function takes into account the various "model dialects" spoken by:
val extract_value : ('a * Smtlib.constant) -> Bitvector.textract_value value extracts the value returned by (get-value) the same * way extract returns the model returned by (get-model). * This function currently only supports bitvectors
val yices_extract : string -> tyices_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
val create : ?len:int -> unit -> tval add_var : t -> string -> Bitvector.t -> unitval add_memcell : t -> Bitvector.t -> Bitvector.t -> unitval add_memory_term : t -> (Smtlib.term * Smtlib.term) list -> unitval pp : Stdlib.Format.formatter -> t -> unitval find_variable : t -> identifier -> Bitvector.t optionfind_register model name finds the bitvector value of register name in the model
val find_address_contents : t -> address -> Bitvector.t optionfind_address_contents model addr find the (byte-sized) value of address addr from the model.
val find_address_content :
t ->
address ->
Size.Byte.t ->
Machine.endianness ->
Bitvector.t optionNot yet implemented
val variables : t -> identifier listget_register model gets the list of registers of this model
get_register model gets the list of addresses with specific values of this model
is_memory_set model address checks if the given address is present in the memory of this model
val filter :
?keep_default:bool ->
addr_p:(Bitvector.t -> bool) ->
var_p:(string -> bool) ->
t ->
tfilter ?keep_default ~addr_p ~var_p model creates a new model m with the following properties:
m has the same default value for memory adresses than model if keep_default is true (default is false)m keeps from model all addresses verifying the predicate addr_p and all the variable names verifying var_p