| [aad342c] | 1 | #ifndef _SVCOMP_
|
|---|
| 2 | #define _SVCOMP_
|
|---|
| 3 | #include<gnuc.h>
|
|---|
| 4 |
|
|---|
| 5 | /**************************** types *****************************/
|
|---|
| 6 | // typedef unsigned long int size_t;
|
|---|
| 7 |
|
|---|
| 8 | /**************************** functions *****************************/
|
|---|
| 9 | /* EVENTUALLY DELETE THESE:
|
|---|
| 10 | extern $system[stdio] int printf(const char * restrict format, ...);
|
|---|
| 11 | extern $system[stdlib] void* malloc(size_t size);
|
|---|
| 12 | extern $system[asserts] void assert(_Bool);
|
|---|
| 13 | */
|
|---|
| 14 | void __VERIFIER_error(void);
|
|---|
| 15 | void __VERIFIER_assume(int);
|
|---|
| 16 | extern void __VERIFIER_atomic_begin();
|
|---|
| 17 | extern void __VERIFIER_atomic_end();
|
|---|
| 18 | extern $system void assume(_Bool);
|
|---|
| 19 | int __VERIFIER_nondet_int(void);
|
|---|
| 20 | unsigned int __VERIFIER_nondet_uint(void);
|
|---|
| 21 | void* __VERIFIER_nondet_pointer(void);
|
|---|
| 22 | _Bool __VERIFIER_nondet_bool(void);
|
|---|
| 23 | int __VERIFIER_nondet_int(void);
|
|---|
| 24 | long __VERIFIER_nondet_long(void);
|
|---|
| 25 | unsigned long __VERIFIER_nondet_ulong(void);
|
|---|
| 26 | char __VERIFIER_nondet_char(void);
|
|---|
| 27 | double __VERIFIER_nondet_double(void);
|
|---|
| 28 | float __VERIFIER_nondet_float(void);
|
|---|
| 29 |
|
|---|
| 30 | /*
|
|---|
| 31 | //Undefined functions:
|
|---|
| 32 | typedef unsigned int __u32;
|
|---|
| 33 | typedef unsigned int u32;
|
|---|
| 34 | typedef long long loff_t;
|
|---|
| 35 | typedef u32 phys_addr_t;
|
|---|
| 36 | typedef phys_addr_t resource_size_t;
|
|---|
| 37 |
|
|---|
| 38 | int access_ok(int type, const void *addr, unsigned long size);
|
|---|
| 39 |
|
|---|
| 40 | int alloc_chrdev_region(unsigned int *, unsigned int, unsigned int, const char *);
|
|---|
| 41 |
|
|---|
| 42 | int register_chrdev_region(unsigned int, unsigned, const char *);
|
|---|
| 43 |
|
|---|
| 44 | void unregister_chrdev_region(unsigned int, unsigned);
|
|---|
| 45 |
|
|---|
| 46 | loff_t no_llseek(struct file *file, loff_t offset, int origin);
|
|---|
| 47 |
|
|---|
| 48 | int nonseekable_open(struct inode * inode, struct file * filp);
|
|---|
| 49 |
|
|---|
| 50 | void __release_region(struct resource *, resource_size_t, resource_size_t);
|
|---|
| 51 | */
|
|---|
| 52 | #endif
|
|---|
