-
Notifications
You must be signed in to change notification settings - Fork 5
/
rv_array_assume.h
executable file
·69 lines (61 loc) · 1.73 KB
/
rv_array_assume.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
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
#ifndef RV_ARRAY_ASSUME_H
#define RV_ARRAY_ASSUME_H
#include <cstdio>
#include <iostream>
#include <string>
#include <fstream>
#include <sstream>
#include <vector>
#include <list>
#include <cstring>
#include <cstdlib>
#include <cassert>
#include <algorithm>
#include <vector>
#include <ctool/decl.h>
#include <ctool/stemnt.h>
#include <ctool/project.h>
#include <ctool/express.h>
#include <ctool/symbol.h>
#include <ctool/Traversal.h>
#include <ctool/PrintTraversal.h>
#include <rv_ctool.h>
#include <rv_traversal.h>
class assume1 {
public:
std::string line_str;
int line_nm;
assume1(int l_nm, std::string l_str)
{
line_nm = l_nm;
line_str= l_str;
}
~assume1() {}
};
class RvArrAssume : public PrintTraversal {
public:
RvArrAssume(std::ostream &, bool, RvTraversal *);
virtual void traverse_binary(BinaryExpr *);
virtual void traverse_function_definition(FunctionDef *node);
virtual void traverse_index(IndexExpr *node);
virtual void block(Statement *);
virtual void traverse_expression(ExpressionStemnt *);
virtual void traverse_if(IfStemnt *);
virtual void traverse_switch(SwitchStemnt *);
virtual void traverse_for(ForStemnt *);
virtual void traverse_while(WhileStemnt *);
virtual void traverse_do_while(DoWhileStemnt *);
virtual void traverse_return(ReturnStemnt *node);
void insert_assumption(int line_num) ;
RvTraversal *arrhooks;
int curr_ind;
int pass;
std::vector<assume1 *> assumptions;
void set_pass(int p) {pass = p;}
~RvArrAssume() {}
private:
std::ostream &out;
bool show_base;
};
/* ############################################################### */
#endif /* RV_ARRAY_ASSUME_H */