module greed.memory.partial_concrete_storage

class PartialConcreteStorage

This class represents a partial concrete storage. When using the partial concrete storage, reads from the contract storage (SLOADs) are initialized with the concrete value on-chain (at the given block number).

To use this, we need a web3 connection to the blockchain, the address of the contract and the block number.

method __init__

__init__(tag=None, value_sort=None, state=None, partial_init=False)

Initialize the partial concrete storage.

Args:

  • tag: The unique identifier of the storage
  • value_sort: The sort of the values stored in the storage
  • state: The SimState associated with this storage
  • partial_init: If true, the storage is partially initialized (used for copy)

Raises:

  • GreedException: If the partial concrete storage is not initialized with the contract address and block number
  • AssertionError: If the partial concrete storage is not initialized with the tag and value sort
  • AssertionError: If w3 is not connected

property constraints

property layer_level

method add_constraint

add_constraint(formula)

Add a constraint to the storage.

Args:

  • formula: The constraint to add

method add_constraints

add_constraints(formulas)

Add a list of constraints to the storage.

Args:

  • formulas: The list of constraints to add

method copy

copy(new_state)

Copy the partial concrete storage.

Args:

  • new_state: The new SimState associated with the new storage

This file was automatically generated via lazydocs.