Goose  Artifact [72fc02c0e2]

Artifact 72fc02c0e299e81309a11e3ec32e6683d254f6ff617238d1fcdf8009ed645346:

• File bs/verify/verify.h — part of check-in [353fcc252a] at 2020-01-04 15:17:12 on branch trunk —
  • verifier: check compilation-time function calls.
  • verifier: improved error messages wording.
  (user: achavasse size: 418)

#ifndef GOOSE_VERIFY_H
#define GOOSE_VERIFY_H

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

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

    class Builder;

    extern z3::context& GetZ3Context();

    extern bool VerifyCompTimeExpr( const Value& val );
}

#include "z3helpers.h"

#include "value.h"
#include "remapper.h"
#include "builder.h"
#include "condition.h"
#include "func.h"

#endif