Goose  Diff

Differences From Artifact [ca2f88807d]:

• File bs/verify/value.cpp — part of check-in [972099a359] at 2020-02-02 21:47:12 on branch trunk — Refinement types: implemented tests and fixed some issues. (user: achavasse size: 12923)

To Artifact [e16ed0aecb]:

• File bs/verify/value.cpp — part of check-in [e814ad7e23] at 2020-04-11 21:01:58 on branch trunk —
  • Implemented load, store and pointers in execute and codegen.
  • Implemented load and pointers in verify.
  • When unifying a local variable against a parameter, generate a reference.
  (user: achavasse size: 13096)

129
130
131
132
133
134
135







136
137
138
139
140
141
142

    }

    template< typename T >
    optional< Z3Val > BuildZ3Op( Builder& b, const T& instr )
    {
        return nullopt;
    }








    // Implemented in call.cpp
    extern optional< Z3Val > BuildZ3Op( Builder& b, const Call& instr );

    optional< Z3Val > BuildZ3Op( Builder& b, const CreateTemporary& instr )
    {
        b.setVar( instr.index(), instr.value() );

>
>
>
>
>
>
>

129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149

    }

    template< typename T >
    optional< Z3Val > BuildZ3Op( Builder& b, const T& instr )
    {
        return nullopt;
    }

    optional< Z3Val > BuildZ3Op( Builder& b, const Load& instr )
    {
        return LoadFromPointer( b, instr.ptr(), instr.type() );
    }

    // TODO: implement store.

    // Implemented in call.cpp
    extern optional< Z3Val > BuildZ3Op( Builder& b, const Call& instr );

    optional< Z3Val > BuildZ3Op( Builder& b, const CreateTemporary& instr )
    {
        b.setVar( instr.index(), instr.value() );