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

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 );
                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