Goose  Diff

Differences From Artifact [1d2e8dfb82]:

• File bs/verify/value.cpp — part of check-in [b3ff9af3c2] at 2021-10-09 15:52:33 on branch trunk —
  • Fixed a couple of verification bugs and added related tests
  • Added some tests for currently broken verification scenarios involving template functions
  (user: zlodo size: 15588) [more...]

To Artifact [5e6e976df9]:

• File bs/verify/value.cpp — part of check-in [c066339928] at 2021-11-28 13:34:49 on branch trunk — Verification: fixed incorrect handling of type predicates in function parameters (user: zlodo size: 15521)

176
177
178
179
180
181
182
183

184
185
186
187
188
189
190
191
192

176
177
178
179
180
181
182

183


184
185
186
187
188
189
190

-
+
-
-

    {
        auto zv = LoadFromAddress( b, *instr.addr() );
        if( !zv )
            return nullopt;

        ForEachPredicate( b, instr.type(), zv->expr, [&]( auto&& z3expr, auto locId )
        {
            if( b.mustLoadCheck() )
            if( b.mustLoadAssume() )
                b.checkAssertion( z3expr, locId );
            else
                b.assume( z3expr );
        } );

        return zv;
    }

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