Goose  Artifact [27bce2124c]

Artifact 27bce2124cc75c967fee7bcabca0cedb72ba0b22829fbab15dcc259d223a5dd2:

• 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)

#ifndef GOOSE_ANALYZE_H
#define GOOSE_ANALYZE_H

#include "z3++.h"
#include "llr/llr.h"

namespace goose::analyze
{
    using namespace ir;
    using namespace llr;

    extern z3::context& GetZ3Context();

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

#include "verifstmtvalidator.h"

#endif