ESBMC
Efficient SMT-based Context-Bounded Model Checker
Loading...
Searching...
No Matches
kernel.c File Reference
#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>
Include dependency graph for kernel.c:

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]

Macro Definition Documentation

◆ spin_limit

#define spin_limit   80

Function Documentation

◆ __kmalloc()

void * __kmalloc ( size_t size,
gfp_t flags )
static

◆ __kmalloc_large()

void * __kmalloc_large ( size_t size,
gfp_t flags )
static

◆ check_gfp_flags()

void check_gfp_flags ( gfp_t flags)
static

◆ copy_from_user()

unsigned long copy_from_user ( void * to,
void * from,
unsigned long size )

◆ copy_to_user()

unsigned long copy_to_user ( void * to,
void * from,
unsigned long size )

◆ kcalloc()

void * kcalloc ( size_t n,
size_t size,
gfp_t flags )

◆ kfree()

void kfree ( const void * ptr)

◆ kmalloc()

void * kmalloc ( int size,
int flags )

◆ kmalloc_array()

void * kmalloc_array ( size_t n,
size_t size,
gfp_t flags )

◆ spin_lock()

bool spin_lock ( spinlock_t * lock)

◆ spin_lock_init()

void spin_lock_init ( spinlock_t * lock)

◆ spin_unlock()

void spin_unlock ( spinlock_t * lock)

Variable Documentation

◆ kernel_memory

char kernel_memory[KERNEL_MEMORY_SPACE]

◆ user_memory

char user_memory[USER_MEMORY_SPACE]