1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
|
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
|
+
+
|
#ifndef GOOSE_VERIFY_STORAGE_H
#define GOOSE_VERIFY_STORAGE_H
namespace goose::verify
{
extern optional< Z3Val > LoadFromAddress( Builder& b, const cir::Instruction& addr );
extern optional< Z3Val > LoadFromAddress( Builder& b, const cir::VarAddr& va );
extern optional< Z3Val > LoadFromAddress( Builder& b, const cir::TempAddr& ta );
extern optional< Z3Val > LoadFromAddress( Builder& b, const cir::Select& s );
extern optional< Z3Val > LoadFromAddress( Builder& b, const cir::GhostCall& gc );
extern void StoreToAddress( Builder& b, const cir::Instruction& addr, Z3Val&& val );
extern void StoreToAddress( Builder& b, const cir::VarAddr& va, Z3Val&& val );
extern void StoreToAddress( Builder& b, const cir::TempAddr& ta, Z3Val&& val );
extern void StoreToAddress( Builder& b, const cir::Select& s, Z3Val&& val );
extern void StoreToAddress( Builder& b, const cir::GhostCall& gc, Z3Val&& val );
extern void HavocAddress( Builder& b, uint32_t bbIndex, const Term& type, const cir::Instruction& addr );
}
#endif
|