Goose  Diff

Differences From Artifact [dde1cd7dda]:

  • File bs/verify/verify.h — part of check-in [036092faf1] at 2020-04-22 23:27:25 on branch trunk — Removed llr::SetVar, now using the more generic llr::Store instead. (user: achavasse size: 437)

To Artifact [53a3286073]:

  • File bs/verify/verify.h — part of check-in [6f98718d3b] at 2020-06-01 01:06:52 on branch trunk — Verifier: refactored type handling and extended it to handle tuple types. (user: achavasse size: 502)

1
2
3
4
5

6
7
8
9
10
11
12
13
14
15
16
17
18
19
20

21
22
23
24
25
26
27
#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 "helpers.h"


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






>










|




>







1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
#ifndef GOOSE_VERIFY_H
#define GOOSE_VERIFY_H

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

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

    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 "condition.h"
#include "func.h"