Goose  Diff

Differences From Artifact [7d6fc0191f]:

• File bs/analyze/analyze.h — part of check-in [d960d10be9] at 2019-09-24 22:06:40 on branch trunk — Began writing the static analyzer. (user: achavasse size: 291)

To Artifact [27bce2124c]:

• File bs/analyze/analyze.h — part of check-in [7f14d60722] at 2019-09-26 00:27:15 on branch trunk — Static analysis: check that function verification statements are satisfiable and emit relevant error messages if they aren't. (user: achavasse size: 324)

9
10
11
12
13
14
15


16
17

    using namespace ir;
    using namespace llr;

    extern z3::context& GetZ3Context();

    extern optional< z3::expr > BuildZ3ExprFromValue( const Value& val );
}



#endif

>
>

9
10
11
12
13
14
15
16
17
18
19

    using namespace ir;
    using namespace llr;

    extern z3::context& GetZ3Context();

    extern optional< z3::expr > BuildZ3ExprFromValue( const Value& val );
}

#include "verifstmtvalidator.h"

#endif