Goose  Diff

Differences From 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)

To Artifact [4e064f694e]:

• File bs/verify/value.cpp — part of check-in [3cf6ab5249] at 2021-03-04 21:47:51 on branch trunk —
  • Refactored and simplified the way integer and string constants are handled: we no longer try to resolve them during typechecking, this breaks when parametric types are involved and also it makes no sense, typechecking is about types, not values
  • Fixed multiple places where locationIds weren't propagated
  • Verifier: variable assignments now verify the destination variable type's refinement conditions
  • Fixed a test where the above change detected a bug, kept the bugged version as a new verification failure test
  (user: achavasse size: 13689)

155
156
157
158
159
160
161
162










163
164
165
166
167
168
169
170

    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 )

|
>
>
>
>
>
>
>
>
>
>
|

155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180

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

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

        ForEachPredicate( b, instr.type(), zv->expr, [&]( auto&& z3expr, auto locId )
        {
            DiagnosticsContext dc( instr.destLocId(), "...to this." );
            DiagnosticsContext dc2( instr.val().locationId(), "When assigning this..." );
            b.checkAssertion( z3expr, locId );
        } );

        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 )