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

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