Goose  Artifact [acb0c86aa5]

Artifact acb0c86aa57c4edb4e123315c130f310a67c68cba2eadb5ab2ab06b53e38d364:

• File bs/verify/storage.h — part of check-in [54ef60956e] at 2020-06-05 18:57:03 on branch trunk — Verifier: loops: instead of tracking and havocing modified variables during loops, track modified addresses, so that modifying only some fields of a tuple will not result in forgetting everything about the other fields. (user: achavasse size: 1349)

#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