Goose  Artifact [029322236a]

Artifact 029322236a00486443ed93eb31e9c52ce4ebff495fb617d50299f4ee44dd0185:

• File bs/verify/storage.h — part of check-in [0db147f117] at 2024-09-15 20:24:31 on branch cir-ssa-refactor — Add clang format settings, reformat everything (user: achavasse size: 1457)

#ifndef GOOSE_VERIFY_STORAGE_H
#define GOOSE_VERIFY_STORAGE_H

namespace goose::verify
{
    // Currently, we only synthethize z3 formulas for load/stores to constant addresses.
    // Stores to symbolic addresses are ignored, loads from symbolic addresses return
    // an unknown variable of the requisite type.
    //
    // Therefore the verifier can't currently reason about a possible aliasing between
    // a symbolic address and another address.
    //
    // This should be addressed (...) at higher level by assuming that two addresses tagged
    // with the same lifetime will always alias (ie modifiyng the pointeed from one of them
    // invalidates every other pointee with the same lifetime).
    extern optional< Z3Val > LoadVar( Builder& b, uint32_t index );
    extern optional< Z3Val > LoadVar( Builder& b, uint32_t index, const Term& type );
    extern optional< Z3Val > LoadFromAddress( Builder& b, const Address& addr, const Term& type );
    extern optional< Z3Val > LoadFromAddress( Builder& b, const GhostFuncApplication& gfa );

    extern void StoreToAddress( Builder& b, const Address& addr, Z3Val&& val );
    extern void StoreToAddress( Builder& b, const GhostFuncApplication& gfa, Z3Val&& val );

    extern Z3Val BuildAddressExpr( Builder& b, const Address& addr );

    extern void HavocDataLocation(
        Builder& b, uint32_t bbIndex, const Term& type, const DataLocation& sloc );
} // namespace goose::verify

#endif