Goose  Diff

Differences From Artifact [a94f9d8ce2]:

• File bs/verify/value.cpp — part of check-in [26c691ecb9] at 2021-01-02 18:24:23 on branch trunk — Yet one more reference/address refactor: each calculation step (getting temp addr, getting var addr, selecting a member) is now a separate cir instruction. We need this level of generalization to be able to obtain addresses from anywhere, including variables and function parameters. (user: achavasse size: 13331)

To Artifact [d91f9d5915]:

• File bs/verify/value.cpp — part of check-in [4cc7a833f8] at 2021-01-03 15:44:11 on branch trunk — cir: load, store and select store their base addresses directly as cir instructiions, rather than wrapped into eir values, which is useless there. (user: achavasse size: 13333)

150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170

    optional< Z3Val > BuildZ3Op( Builder& b, const T& instr )
    {
        return nullopt;
    }

    optional< Z3Val > BuildZ3Op( Builder& b, const Load& instr )
    {
        return LoadFromAddress( b, instr.addr() );
    }

    optional< Z3Val > BuildZ3Op( Builder& b, const Store& instr )
    {
        if( auto zv = BuildZ3ExprFromValue( b, instr.val() ) )
            StoreToAddress( b, instr.addr(), move( *zv ) );
        return nullopt;
    }

    // Implemented in call.cpp
    extern optional< Z3Val > BuildZ3Op( Builder& b, const Call& instr );

    optional< Z3Val > BuildZ3Op( Builder& b, const CreateTemporary& instr )

|





|

150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170

    optional< Z3Val > BuildZ3Op( Builder& b, const T& instr )
    {
        return nullopt;
    }

    optional< Z3Val > BuildZ3Op( Builder& b, const Load& instr )
    {
        return LoadFromAddress( b, *instr.addr() );
    }

    optional< Z3Val > BuildZ3Op( Builder& b, const Store& instr )
    {
        if( auto zv = BuildZ3ExprFromValue( b, instr.val() ) )
            StoreToAddress( b, *instr.addr(), move( *zv ) );
        return nullopt;
    }

    // Implemented in call.cpp
    extern optional< Z3Val > BuildZ3Op( Builder& b, const Call& instr );

    optional< Z3Val > BuildZ3Op( Builder& b, const CreateTemporary& instr )