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
|
|
|
|
|
>
>
|
|
|
|
|
|
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 Value& addr );
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 void StoreToAddress( Builder& b, const Value& addr, Z3Val&& val );
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 HavocAddress( Builder& b, uint32_t bbIndex, const Term& type, const cir::Instruction& addr );
}
#endif
|