Goose  Diff

Differences From Artifact [b78ea33802]:

• File bs/verify/call.cpp — part of check-in [b00c682e34] at 2020-06-03 23:08:17 on branch trunk —
  • Verifier: a bunch of refactoring to better keep track of the types of the z3 expressions stored in variables.
  • Verifier: handle "LoadFromAddress" for addresses that point to tuple members.
  (user: achavasse size: 3570)

To Artifact [ace936b55b]:

• File bs/verify/call.cpp — part of check-in [c3f897359f] at 2020-06-20 14:32:02 on branch trunk —
  • Got rid of the gross system of performing unifications twice in all cases. It's only really needed when invoking template functions.
  • Since the above had the unexpected side effect of fixing the tuple Initialize() overloads not being called, fixed those (which were actually broken).
  (user: achavasse size: 3560)

13
14
15
16
17
18
19
20
21
22
23
24
25
26
27

            return nullopt;

        const auto& ft = func->type();
        const auto& fvi = ft.verifInfos();
        if( !fvi )
            return nullopt;

        auto retExpr = BuildZ3ConstantFromType( b.context(), ft.returnType(), format( "r{}", b.newUniqueId() ) );

        // Create a temporary builder to construct the z3 expressions out of the
        // function's pre-conditions and postconditions, configured
        // to perform the necessary replacements for arguments and for the
        // return value placeholder.
        Builder cb( b.context(), *b.solver(), b.remapper() );

|

13
14
15
16
17
18
19
20
21
22
23
24
25
26
27

            return nullopt;

        const auto& ft = func->type();
        const auto& fvi = ft.verifInfos();
        if( !fvi )
            return nullopt;

        auto retExpr = BuildZ3ConstantFromType( b, ft.returnType(), format( "r{}", b.newUniqueId() ) );

        // Create a temporary builder to construct the z3 expressions out of the
        // function's pre-conditions and postconditions, configured
        // to perform the necessary replacements for arguments and for the
        // return value placeholder.
        Builder cb( b.context(), *b.solver(), b.remapper() );