|
ESBMC
Efficient SMT-based Context-Bounded Model Checker
|
#include <stdlib.h>#include <string.h>#include <ctype.h>#include <limits.h>#include <errno.h>#include <stdbool.h>#include <ubuntu20.04/kernel_5.15.0-76/include/linux/slab.h>#include <ubuntu20.04/kernel_5.15.0-76/include/linux/spinlock.h>#include <ubuntu20.04/kernel_5.15.0-76/include/asm/uaccess.h>#include <assert.h>Macros | |
| #define | spin_limit 80 |
Functions | |
| static void | check_gfp_flags (gfp_t flags) |
| static void * | __kmalloc (size_t size, gfp_t flags) |
| static void * | __kmalloc_large (size_t size, gfp_t flags) |
| void * | kmalloc (int size, int flags) |
| void | kfree (const void *ptr) |
| void * | kmalloc_array (size_t n, size_t size, gfp_t flags) |
| void * | kcalloc (size_t n, size_t size, gfp_t flags) |
| unsigned long | copy_to_user (void *to, void *from, unsigned long size) |
| unsigned long | copy_from_user (void *to, void *from, unsigned long size) |
| void | spin_lock_init (spinlock_t *lock) |
| bool | spin_lock (spinlock_t *lock) |
| void | spin_unlock (spinlock_t *lock) |
Variables | |
| char | user_memory [USER_MEMORY_SPACE] |
| char | kernel_memory [KERNEL_MEMORY_SPACE] |
| #define spin_limit 80 |
|
static |
| unsigned long copy_from_user | ( | void * | to, |
| void * | from, | ||
| unsigned long | size ) |
| unsigned long copy_to_user | ( | void * | to, |
| void * | from, | ||
| unsigned long | size ) |
| void kfree | ( | const void * | ptr | ) |
| bool spin_lock | ( | spinlock_t * | lock | ) |
| void spin_lock_init | ( | spinlock_t * | lock | ) |
| void spin_unlock | ( | spinlock_t * | lock | ) |
| char kernel_memory[KERNEL_MEMORY_SPACE] |
| char user_memory[USER_MEMORY_SPACE] |