1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
|
#ifndef GOOSE_VERIFY_STORAGE_H
#define GOOSE_VERIFY_STORAGE_H
namespace goose::verify
{
extern optional< Z3Val > LoadFromAddress( Builder& b, const llr::CalcAddress& addr );
extern optional< Z3Val > LoadFromAddress( Builder& b, const BaseAddress& baseAddr );
extern optional< Z3Val > LoadFromAddress( Builder& b, const llr::TemporaryBaseAddr& ta );
extern optional< Z3Val > LoadFromAddress( Builder& b, const llr::VarBaseAddr& va );
extern void StoreToAddress( Builder& b, const llr::CalcAddress& addr, Z3Val&& val );
extern void StoreToAddress( Builder& b, const BaseAddress& baseAddr, Z3Val&& val );
extern void StoreToAddress( Builder& b, const llr::TemporaryBaseAddr& ta, Z3Val&& val );
extern void StoreToAddress( Builder& b, const llr::VarBaseAddr& va, Z3Val&& val );
extern void HavocAddress( Builder& b, uint32_t bbIndex, const Term& type, const llr::CalcAddress& addr );
}
#endif
|
|
|
|
|
|
|
|
|
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
|
#ifndef GOOSE_VERIFY_STORAGE_H
#define GOOSE_VERIFY_STORAGE_H
namespace goose::verify
{
extern optional< Z3Val > LoadFromAddress( Builder& b, const cir::CalcAddress& addr );
extern optional< Z3Val > LoadFromAddress( Builder& b, const BaseAddress& baseAddr );
extern optional< Z3Val > LoadFromAddress( Builder& b, const cir::TemporaryBaseAddr& ta );
extern optional< Z3Val > LoadFromAddress( Builder& b, const cir::VarBaseAddr& va );
extern void StoreToAddress( Builder& b, const cir::CalcAddress& addr, Z3Val&& val );
extern void StoreToAddress( Builder& b, const BaseAddress& baseAddr, Z3Val&& val );
extern void StoreToAddress( Builder& b, const cir::TemporaryBaseAddr& ta, Z3Val&& val );
extern void StoreToAddress( Builder& b, const cir::VarBaseAddr& va, Z3Val&& val );
extern void HavocAddress( Builder& b, uint32_t bbIndex, const Term& type, const cir::CalcAddress& addr );
}
#endif
|