Goose  Artifact [8b34c0b843]

Artifact 8b34c0b84349a406283bac0dbbde4a9961d4200fbfe19611d576b29fd2d645d9:

• File bs/verify/storage.h — part of check-in [e3b9bd4c1b] at 2020-07-04 13:08:43 on branch trunk —
  • Verifier: fixed havocing of individual members of aggregate types not working.
  • Added verification loop tests (both passing and failing) that modify a tuple inside of the loop.
  (user: achavasse size: 898)

#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 HavocAddress( Builder& b, uint32_t bbIndex, const Term& type, const Address& addr );
}

#endif