#ifndef GOOSE_VERIFY_STORAGE_H
#define GOOSE_VERIFY_STORAGE_H

namespace goose::verify
{
    extern optional< Z3Val > LoadFromAddress( Builder& b, const Address& addr );
    extern optional< Z3Val > LoadFromAddress( Builder& b, const BaseAddress& baseAddr );
    extern optional< Z3Val > LoadFromAddress( Builder& b, const llr::TemporaryAddress& ta );
    extern optional< Z3Val > LoadFromAddress( Builder& b, const llr::VarAddress& va );

    extern void StoreToAddress( Builder& b, const Address& addr, Z3Val&& val );
    extern void StoreToAddress( Builder& b, const BaseAddress& baseAddr, Z3Val&& val );
    extern void StoreToAddress( Builder& b, const llr::TemporaryAddress& ta, Z3Val&& val );
    extern void StoreToAddress( Builder& b, const llr::VarAddress& va, Z3Val&& val );

    extern void StoreToAddressForBB( Builder& b, uint32_t bbIndex, const Address& addr, Z3Val&& valToStore );
    extern void StoreToAddressForBB( Builder& b, uint32_t bbIndex, const BaseAddress& baseAddr, Z3Val&& val );
    extern void StoreToAddressForBB( Builder& b, uint32_t bbIndex, const llr::TemporaryAddress& ta, Z3Val&& val );
    extern void StoreToAddressForBB( Builder& b, uint32_t bbIndex, const llr::VarAddress& va, Z3Val&& val );

    extern void HavocAddressForBB( Builder& b, uint32_t bbIndex, const Term& type, const Address& addr );
}

#endif
