Goose  Artifact [1e62b306a5]

Artifact 1e62b306a50edefab12fbd918aa7279a65729f8ca1bb03aaae73145f3c95bb51:

• File bs/verify/verify.h — part of check-in [1c335aeb04] at 2021-11-22 20:22:35 on branch trunk — Function pre-conditions and post-conditions now use the same proposition lists as type predicates (user: zlodo size: 506)

#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 "type.h"
#include "value.h"
#include "storage.h"
#include "remapper.h"
#include "builder.h"
#include "propositions.h"
#include "func.h"

#endif