Goose  Diff

Differences From Artifact [f0db41882f]:

  • File bs/verify/value.cpp — part of check-in [036092faf1] at 2020-04-22 23:27:25 on branch trunk — Removed llr::SetVar, now using the more generic llr::Store instead. (user: achavasse size: 12185)

To Artifact [a7fb30eb03]:

  • File bs/verify/value.cpp — part of check-in [0b4eb97a44] at 2020-05-03 15:32:25 on branch trunk — Simplified the llr address representation. (user: achavasse size: 12187)

132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
    optional< Z3Val > BuildZ3Op( Builder& b, const T& instr )
    {
        return nullopt;
    }

    optional< Z3Val > BuildZ3Op( Builder& b, const Load& instr )
    {
        return LoadFromPointer( b, instr.ptr(), instr.type() );
    }

    optional< Z3Val > BuildZ3Op( Builder& b, const Store& instr )
    {
        StoreToPointer( b, instr.ptr(), instr.val() );
        return nullopt;
    }

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

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







|




|







132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
    optional< Z3Val > BuildZ3Op( Builder& b, const T& instr )
    {
        return nullopt;
    }

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

    optional< Z3Val > BuildZ3Op( Builder& b, const Store& instr )
    {
        StoreToAddress( b, instr.addr(), instr.val() );
        return nullopt;
    }

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

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