Goose  Artifact [36689353d5]

Artifact 36689353d5115dbdce9eb5fad27616c4de2f810a6832a5183dad46279fa7de7d:

• File bs/verify/storage.h — part of check-in [077c944c02] at 2020-06-05 00:35:45 on branch trunk — Verifier: handle "StoreToAddress" for addresses that point to tuple members. (user: achavasse size: 796)

#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 );
}

#endif