Module expressions 

Enums

BoolExpr 🔒

BoolExprOp 🔒

Expr 🔒

ExprOp 🔒

SymWord 🔒

Functions

bool_const_value 🔒

Returns the bool_const_value symbolic expression helper result.

bool_contains_gasleft 🔒

Returns whether a boolean expression depends on the opaque GAS / gasleft() value.

bool_contains_keccak 🔒

Returns the bool_contains_keccak symbolic expression helper result.

bool_forces_expr_const_with_context 🔒

Returns the bool_forces_expr_const_with_context symbolic expression helper result.

bool_upper_bound_usize 🔒

Returns the bool_upper_bound_usize symbolic expression helper result.

calldata_prefix_condition 🔒

Implements the calldata_prefix_condition symbolic expression helper.

compute_create2_address_word 🔒

Computes the compute_create2_address_word symbolic expression helper result.

compute_create_address_word 🔒

Computes the compute_create_address_word symbolic expression helper result.

concrete_bytes 🔒

Returns the concrete_bytes symbolic expression helper result.

context_forces_masked_expr 🔒

Implements the context_forces_masked_expr symbolic expression helper.

create2_address_word 🔒

Implements the create2_address_word symbolic expression helper.

eval_bool_expr 🔒

Returns the eval_bool_expr symbolic expression helper result.

eval_expr 🔒

Returns the eval_expr symbolic expression helper result.

eval_expr_op 🔒

Returns the eval_expr_op symbolic expression helper result.

eval_keccak_expr 🔒

Returns the concrete keccak value implied by a solver model.

expr_add 🔒

Returns the expr_add symbolic expression helper result.

expr_const_value 🔒

Returns the expr_const_value symbolic expression helper result.

expr_contains_gasleft 🔒

Returns whether a word expression depends on the opaque GAS / gasleft() value.

expr_contains_keccak 🔒

Returns the expr_contains_keccak symbolic expression helper result.

expr_equality_forces_const 🔒

Returns the expr_equality_forces_const symbolic expression helper result.

expr_nonzero_forces_const 🔒

Returns the expr_nonzero_forces_const symbolic expression helper result.

extracted_byte_source 🔒

Implements the extracted_byte_source symbolic expression helper.

function_mock_match_condition 🔒

Implements the function_mock_match_condition symbolic expression helper.

keccak_word 🔒

Computes the keccak_word symbolic expression helper result.

keccak_word_with_len 🔒

Computes the keccak_word_with_len symbolic expression helper result.

low_byte 🔒

Returns the low_byte symbolic expression helper result.

masked_expr_matches 🔒

Returns whether masked_expr_matches holds.

model_bytes 🔒

Returns the model_bytes symbolic expression helper result.

model_word 🔒

Returns the model_word symbolic expression helper result.

read_storage_writes 🔒

Returns the read_storage_writes symbolic expression helper result.

storage_key_eq 🔒

Implements the storage_key_eq symbolic expression helper.

storage_layout_key 🔒

Implements the storage_layout_key symbolic expression helper.

storage_mapping_root_slot 🔒

Returns the root Solidity storage slot for a mapping-style keccak key.

storage_select 🔒

Implements the storage_select symbolic expression helper.

strip_low_byte_mask 🔒

Implements the strip_low_byte_mask symbolic expression helper.

sym_add 🔒

Implements the sym_add symbolic expression helper.

sym_sub 🔒

Implements the sym_sub symbolic expression helper.

symbolic_create2_address_word 🔒

Returns the symbolic_create2_address_word symbolic expression helper result.

symbolic_create_address_word 🔒

Returns the symbolic_create_address_word symbolic expression helper result.

symbolic_hash_word_with_len 🔒

Returns the symbolic_hash_word_with_len symbolic expression helper result.

u256_to_usize 🔒

Returns the u256_to_usize symbolic expression helper result.

word_bytes 🔒

Returns the word_bytes symbolic expression helper result.

word_from_bytes 🔒

Returns the word_from_bytes symbolic expression helper result.

word_from_extracted_bytes 🔒

Returns the word_from_extracted_bytes symbolic expression helper result.