Goose  Artifact [84fedd4859]

Artifact 84fedd48590b8a82227d95b23489793f6f33566869ce2a9f34fe35a554bad51f:

• File bs/verify/verify.h — part of check-in [e607197fe9] at 2022-02-02 01:08:57 on branch trunk — verifier: build and cache z3 declarations for ghost funcs (user: zlodo size: 603)

#ifndef GOOSE_VERIFY_H
#define GOOSE_VERIFY_H

#include <z3++.h>
#include "cir/cir.h"
#include "sema/sema.h"

namespace goose::verify
{
    using namespace eir;
    using namespace cir;

    class Builder;

    extern z3::context& GetZ3Context();

    extern bool VerifyCompTimeExpr( const sema::Context& c, const Value& val );
}

#include "helpers.h"
#include "verifyviz.h"

#include "type.h"
#include "value.h"
#include "storage.h"
#include "remapper.h"
#include "valtracker.h"
#include "builder.h"
#include "propositions.h"
#include "func.h"
#include "ghostfunc.h"

#include "valtracker.inl"

#endif