A path.

A symbolic state (see State.S).

A symbolic state (see State.VALUE).

A concrete assignment (see State.MODEL)

id p returns the unique identifier of the path p.

addr p returns the current program counter of the path p.

symbolize p v assigns the variable v with a new symbolic value.

Each call to symbolize records the new value on top of the symbols history.

assign p v e assigns the variable v with the expression e.

assign p v e assigns the variable v with a new symbolic value.

Clobbered variables are expected to not be used by the program and are not recorded in the symbols history.

load p v m ~addr d assigns the variable v with the bytes read at the address addr from the memory array m.

When m is None, the load is performed from the main memory @.

The bit size of v should be a multiple of the size of a byte (8). The byte order is determined by the endianness d.

store p m ~addr e d writes the expression e at the address addr in the memory array m.

When m is None, the write is performed in the main memory @.

The bit size of e should be a multiple of the size of a byte (8). The byte order is determined by the endianness d.

memcpy p m ~addr len content initializes the memory array m at the address addr with len bytes from the zero extended buffer content.

When m is None, the write is performed in the main memory @.

predicate p returns the path predicate as a list of boolean value.

is_symbolic p e checks if the expression e may depend on symbolic values.

When it returns false, the path predicate of p implies that e has a single value. This value can be obtained via eval.

Otherwise, it means that e syntactically depends on a symbolic value. Use enumerate with n = 2 to prove or disprove that it can take several values.

is_zero p e checks if the boolean expression e may depend on symbolic values.

It returns True when the path predicate implies e is false and False when the path predicate implies e is true.

Otherwise, it returns Unknown, that means that e syntactically depends on a symbolic value. Use enumerate with n = 2 to prove or disprove that it can take several values.

assume p e tests if the condition e can be true. If so, it returns a witness model (Some) and updates the symbolic predicate. Otherwise, nothing is updated and it returns None.

• raises State.Unknown

  when the symboloc engine fails to give an answer.

check_sat_assuming p ~retain e tests if the condition e can be true. If so, it returns a witness model (Some), otherwise, it returns None.

If retain is true (default), the model is saved into the path p.

• raises State.Unknown

  when the symbolic engine fails to give an answer.

partition p e tests if the condition e can be true and update its internal symbolic state accordingly.

It returns True when the path predicate implies e is true and False when the path predicate implies e is false.

It returns Trueish when the path predicate allows e to be true but may allow false too, and Falsish when the path predicate allows e to be false but may allow true too. The returned state can be used to check the other assumption.

It returns Split when the path predicate allows e to be both true and false. The current path keeps models for which e evaluates to true (same as assume) while the returned state comes with a list of models for which e evaluates to false.

enumerate p ~retain ~n ~accumulator ~assuming e lists the possible values of the expression e.

It returns a map of up to n new possible values that are not already present in accumulator, together with their respective model witnesses. When n is omitted, the enumeration is unbounded.

The new models satisfy the predicate assuming when present.

If retain is true (default), new models are saved into the path p.

• raises State.Unknown

  when the symbolic engine fails to give an answer.

check_model p ~retain m returns true if the model m is a witness for the path predicate of p.

If retain is true (default), the model is saved into the path p when the function returns true.

eval p e evaluates the expression e in the last witness model.

The returned values are consistent with each other as long as the witness model is not updated via assume, check_sat_assuming, enumerate, check_model or partition.

get_value p e evaluates the expression e to its symbolic value.

lookup p v evaluates the content of the variable v to its symbolic value.

read p m ~addr n d reads the content of the memory array m at the address addr.

When m is None, the load is performed from the main memory.

Returns a value of n bytes. The byte order is determined by the endianness d.

symbols p returns the (reverse) history of symbols created by symbolize.

A key entry associated to a value of type 'a.

get p k returns the associated value of the key k.

set p k v replaces the associated value of the key k by v.

Same as assign but with value input.

Same as load but with value input.

Same as store but with value input.

Same as memcpy but with value input.

Same as is_symbolic but with value input.

Same as is_zero but with value input.

Same as assume but with value input.

Same as check_sat_assuming_v but with value input.

Same as partition but with value input.

Same as enumerate but with value input.

Same as eval but with value input.

Same as read but with value input.

set_pc p v replaces the current program counter of p by v.

models p returns the list of the witness models of p.

set_models p l replaces the witness models of p by the ones in l.

Warning. It is the caller responsibility to ensure that l is non-empty and that each model in l is consistent with the current symbolic state state.

state p returns the symbolic state of p.

set_state p s replaces the symbolic state of p by s.

Warning. It is the caller responsibility to ensure that each model in models is consistent with the new symbolic state s.

transform_state p f is equivalent to set_state p (f (state p)).