ESBMC
Efficient SMT-based Context-Bounded Model Checker
Loading...
Searching...
No Matches
uaccess.h
Go to the documentation of this file.
1
2#define PAGE_SIZE 4096 // page size
3#define USER_MEMORY_SPACE 10000 //only for simulate the user memory
4#define KERNEL_MEMORY_SPACE 10000// only for simulate the kernel memory
5extern char user_memory[USER_MEMORY_SPACE]; //mock user memory
6extern char kernel_memory[KERNEL_MEMORY_SPACE];//mock user memory
7//simulate copy_to_user function in kernel space
8unsigned long copy_to_user(void* to, void* from, unsigned long size);
9unsigned long copy_from_user(void* to, void* from, unsigned long size);
10
11
12
char kernel_memory[KERNEL_MEMORY_SPACE]
Definition kernel.c:16
#define USER_MEMORY_SPACE
Definition uaccess.h:3
char user_memory[USER_MEMORY_SPACE]
Definition kernel.c:15
#define KERNEL_MEMORY_SPACE
Definition uaccess.h:4
unsigned long copy_from_user(void *to, void *from, unsigned long size)
Definition kernel.c:105
unsigned long copy_to_user(void *to, void *from, unsigned long size)
Definition kernel.c:86