Goose  Diff

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

To Artifact [a02e5ff5dd]:

• File bs/verify/value.cpp — part of check-in [b2945b5bb1] at 2021-03-05 17:56:37 on branch trunk — Implemented refinement type predicate unification. Predicate violations by variable initialization are now properly detected. (user: achavasse size: 13861)

161
162
163
164
165
166
167


168
169
170



171
172
173
174
175
176
177

    {
        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

>
>
|
|
|
>
>
>

161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182

    {
        auto zv = BuildZ3ExprFromValue( b, instr.val() );
        if( !zv )
            return nullopt;

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

        StoreToAddress( b, *instr.addr(), move( *zv ) );
        return nullopt;
    }

    // Implemented in call.cpp