-
Notifications
You must be signed in to change notification settings - Fork 0
Witness example
zhuyt edited this page Oct 14, 2021
·
3 revisions
complex_data_creation_test01-1.i
extern void abort(void);
extern void __assert_fail (const char *__assertion, const char *__file,
unsigned int __line, const char *__function)
__attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
extern void __assert_perror_fail (int __errnum, const char *__file,
unsigned int __line, const char *__function)
__attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
extern void __assert (const char *__assertion, const char *__file, int __line)
__attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
void reach_error() { ((void) sizeof ((0) ? 1 : 0), __extension__ ({ if (0) ; else __assert_fail ("0", "complex_data_creation_test01-1.c", 3, __extension__ __PRETTY_FUNCTION__); })); }
typedef unsigned int size_t;
typedef long int wchar_t;
typedef struct
{
int quot;
int rem;
} div_t;
typedef struct
{
long int quot;
long int rem;
} ldiv_t;
__extension__ typedef struct
{
long long int quot;
long long int rem;
} lldiv_t;
extern size_t __ctype_get_mb_cur_max (void) __attribute__ ((__nothrow__ , __leaf__)) ;
extern double atof (const char *__nptr)
__attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__pure__)) __attribute__ ((__nonnull__ (1))) ;
extern int atoi (const char *__nptr)
__attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__pure__)) __attribute__ ((__nonnull__ (1))) ;
extern long int atol (const char *__nptr)
__attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__pure__)) __attribute__ ((__nonnull__ (1))) ;
__extension__ extern long long int atoll (const char *__nptr)
__attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__pure__)) __attribute__ ((__nonnull__ (1))) ;
extern double strtod (const char *__restrict __nptr,
char **__restrict __endptr)
__attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
extern float strtof (const char *__restrict __nptr,
char **__restrict __endptr) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
extern long double strtold (const char *__restrict __nptr,
char **__restrict __endptr)
__attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
extern long int strtol (const char *__restrict __nptr,
char **__restrict __endptr, int __base)
__attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
extern unsigned long int strtoul (const char *__restrict __nptr,
char **__restrict __endptr, int __base)
__attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
__extension__
extern long long int strtoq (const char *__restrict __nptr,
char **__restrict __endptr, int __base)
__attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
__extension__
extern unsigned long long int strtouq (const char *__restrict __nptr,
char **__restrict __endptr, int __base)
__attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
__extension__
extern long long int strtoll (const char *__restrict __nptr,
char **__restrict __endptr, int __base)
__attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
__extension__
extern unsigned long long int strtoull (const char *__restrict __nptr,
char **__restrict __endptr, int __base)
__attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
extern char *l64a (long int __n) __attribute__ ((__nothrow__ , __leaf__)) ;
extern long int a64l (const char *__s)
__attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__pure__)) __attribute__ ((__nonnull__ (1))) ;
typedef unsigned char __u_char;
typedef unsigned short int __u_short;
typedef unsigned int __u_int;
typedef unsigned long int __u_long;
typedef signed char __int8_t;
typedef unsigned char __uint8_t;
typedef signed short int __int16_t;
typedef unsigned short int __uint16_t;
typedef signed int __int32_t;
typedef unsigned int __uint32_t;
__extension__ typedef signed long long int __int64_t;
__extension__ typedef unsigned long long int __uint64_t;
__extension__ typedef long long int __quad_t;
__extension__ typedef unsigned long long int __u_quad_t;
__extension__ typedef __u_quad_t __dev_t;
__extension__ typedef unsigned int __uid_t;
__extension__ typedef unsigned int __gid_t;
__extension__ typedef unsigned long int __ino_t;
__extension__ typedef __u_quad_t __ino64_t;
__extension__ typedef unsigned int __mode_t;
__extension__ typedef unsigned int __nlink_t;
__extension__ typedef long int __off_t;
__extension__ typedef __quad_t __off64_t;
__extension__ typedef int __pid_t;
__extension__ typedef struct { int __val[2]; } __fsid_t;
__extension__ typedef long int __clock_t;
__extension__ typedef unsigned long int __rlim_t;
__extension__ typedef __u_quad_t __rlim64_t;
__extension__ typedef unsigned int __id_t;
__extension__ typedef long int __time_t;
__extension__ typedef unsigned int __useconds_t;
__extension__ typedef long int __suseconds_t;
__extension__ typedef int __daddr_t;
__extension__ typedef int __key_t;
__extension__ typedef int __clockid_t;
__extension__ typedef void * __timer_t;
__extension__ typedef long int __blksize_t;
__extension__ typedef long int __blkcnt_t;
__extension__ typedef __quad_t __blkcnt64_t;
__extension__ typedef unsigned long int __fsblkcnt_t;
__extension__ typedef __u_quad_t __fsblkcnt64_t;
__extension__ typedef unsigned long int __fsfilcnt_t;
__extension__ typedef __u_quad_t __fsfilcnt64_t;
__extension__ typedef int __fsword_t;
__extension__ typedef int __ssize_t;
__extension__ typedef long int __syscall_slong_t;
__extension__ typedef unsigned long int __syscall_ulong_t;
typedef __off64_t __loff_t;
typedef __quad_t *__qaddr_t;
typedef char *__caddr_t;
__extension__ typedef int __intptr_t;
__extension__ typedef unsigned int __socklen_t;
typedef __u_char u_char;
typedef __u_short u_short;
typedef __u_int u_int;
typedef __u_long u_long;
typedef __quad_t quad_t;
typedef __u_quad_t u_quad_t;
typedef __fsid_t fsid_t;
typedef __loff_t loff_t;
typedef __ino_t ino_t;
typedef __dev_t dev_t;
typedef __gid_t gid_t;
typedef __mode_t mode_t;
typedef __nlink_t nlink_t;
typedef __uid_t uid_t;
typedef __off_t off_t;
typedef __pid_t pid_t;
typedef __id_t id_t;
typedef __ssize_t ssize_t;
typedef __daddr_t daddr_t;
typedef __caddr_t caddr_t;
typedef __key_t key_t;
typedef __clock_t clock_t;
typedef __time_t time_t;
typedef __clockid_t clockid_t;
typedef __timer_t timer_t;
typedef unsigned long int ulong;
typedef unsigned short int ushort;
typedef unsigned int uint;
typedef int int8_t __attribute__ ((__mode__ (__QI__)));
typedef int int16_t __attribute__ ((__mode__ (__HI__)));
typedef int int32_t __attribute__ ((__mode__ (__SI__)));
typedef int int64_t __attribute__ ((__mode__ (__DI__)));
typedef unsigned int u_int8_t __attribute__ ((__mode__ (__QI__)));
typedef unsigned int u_int16_t __attribute__ ((__mode__ (__HI__)));
typedef unsigned int u_int32_t __attribute__ ((__mode__ (__SI__)));
typedef unsigned int u_int64_t __attribute__ ((__mode__ (__DI__)));
typedef int register_t __attribute__ ((__mode__ (__word__)));
static __inline unsigned int
__bswap_32 (unsigned int __bsx)
{
return __builtin_bswap32 (__bsx);
}
static __inline __uint64_t
__bswap_64 (__uint64_t __bsx)
{
return __builtin_bswap64 (__bsx);
}
typedef int __sig_atomic_t;
typedef struct
{
unsigned long int __val[(1024 / (8 * sizeof (unsigned long int)))];
} __sigset_t;
typedef __sigset_t sigset_t;
struct timespec
{
__time_t tv_sec;
__syscall_slong_t tv_nsec;
};
struct timeval
{
__time_t tv_sec;
__suseconds_t tv_usec;
};
typedef __suseconds_t suseconds_t;
typedef long int __fd_mask;
typedef struct
{
__fd_mask __fds_bits[1024 / (8 * (int) sizeof (__fd_mask))];
} fd_set;
typedef __fd_mask fd_mask;
extern int select (int __nfds, fd_set *__restrict __readfds,
fd_set *__restrict __writefds,
fd_set *__restrict __exceptfds,
struct timeval *__restrict __timeout);
extern int pselect (int __nfds, fd_set *__restrict __readfds,
fd_set *__restrict __writefds,
fd_set *__restrict __exceptfds,
const struct timespec *__restrict __timeout,
const __sigset_t *__restrict __sigmask);
__extension__
extern unsigned int gnu_dev_major (unsigned long long int __dev)
__attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__));
__extension__
extern unsigned int gnu_dev_minor (unsigned long long int __dev)
__attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__));
__extension__
extern unsigned long long int gnu_dev_makedev (unsigned int __major,
unsigned int __minor)
__attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__));
typedef __blksize_t blksize_t;
typedef __blkcnt_t blkcnt_t;
typedef __fsblkcnt_t fsblkcnt_t;
typedef __fsfilcnt_t fsfilcnt_t;
typedef unsigned long int pthread_t;
union pthread_attr_t
{
char __size[36];
long int __align;
};
typedef union pthread_attr_t pthread_attr_t;
typedef struct __pthread_internal_slist
{
struct __pthread_internal_slist *__next;
} __pthread_slist_t;
typedef union
{
struct __pthread_mutex_s
{
int __lock;
unsigned int __count;
int __owner;
int __kind;
unsigned int __nusers;
__extension__ union
{
struct
{
short __espins;
short __elision;
} __elision_data;
__pthread_slist_t __list;
};
} __data;
char __size[24];
long int __align;
} pthread_mutex_t;
typedef union
{
char __size[4];
int __align;
} pthread_mutexattr_t;
typedef union
{
struct
{
int __lock;
unsigned int __futex;
__extension__ unsigned long long int __total_seq;
__extension__ unsigned long long int __wakeup_seq;
__extension__ unsigned long long int __woken_seq;
void *__mutex;
unsigned int __nwaiters;
unsigned int __broadcast_seq;
} __data;
char __size[48];
__extension__ long long int __align;
} pthread_cond_t;
typedef union
{
char __size[4];
int __align;
} pthread_condattr_t;
typedef unsigned int pthread_key_t;
typedef int pthread_once_t;
typedef union
{
struct
{
int __lock;
unsigned int __nr_readers;
unsigned int __readers_wakeup;
unsigned int __writer_wakeup;
unsigned int __nr_readers_queued;
unsigned int __nr_writers_queued;
unsigned char __flags;
unsigned char __shared;
signed char __rwelision;
unsigned char __pad2;
int __writer;
} __data;
char __size[32];
long int __align;
} pthread_rwlock_t;
typedef union
{
char __size[8];
long int __align;
} pthread_rwlockattr_t;
typedef volatile int pthread_spinlock_t;
typedef union
{
char __size[20];
long int __align;
} pthread_barrier_t;
typedef union
{
char __size[4];
int __align;
} pthread_barrierattr_t;
extern long int random (void) __attribute__ ((__nothrow__ , __leaf__));
extern void srandom (unsigned int __seed) __attribute__ ((__nothrow__ , __leaf__));
extern char *initstate (unsigned int __seed, char *__statebuf,
size_t __statelen) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (2)));
extern char *setstate (char *__statebuf) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
struct random_data
{
int32_t *fptr;
int32_t *rptr;
int32_t *state;
int rand_type;
int rand_deg;
int rand_sep;
int32_t *end_ptr;
};
extern int random_r (struct random_data *__restrict __buf,
int32_t *__restrict __result) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
extern int srandom_r (unsigned int __seed, struct random_data *__buf)
__attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (2)));
extern int initstate_r (unsigned int __seed, char *__restrict __statebuf,
size_t __statelen,
struct random_data *__restrict __buf)
__attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (2, 4)));
extern int setstate_r (char *__restrict __statebuf,
struct random_data *__restrict __buf)
__attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
extern int rand (void) __attribute__ ((__nothrow__ , __leaf__));
extern void srand (unsigned int __seed) __attribute__ ((__nothrow__ , __leaf__));
extern int rand_r (unsigned int *__seed) __attribute__ ((__nothrow__ , __leaf__));
extern double drand48 (void) __attribute__ ((__nothrow__ , __leaf__));
extern double erand48 (unsigned short int __xsubi[3]) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
extern long int lrand48 (void) __attribute__ ((__nothrow__ , __leaf__));
extern long int nrand48 (unsigned short int __xsubi[3])
__attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
extern long int mrand48 (void) __attribute__ ((__nothrow__ , __leaf__));
extern long int jrand48 (unsigned short int __xsubi[3])
__attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
extern void srand48 (long int __seedval) __attribute__ ((__nothrow__ , __leaf__));
extern unsigned short int *seed48 (unsigned short int __seed16v[3])
__attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
extern void lcong48 (unsigned short int __param[7]) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
struct drand48_data
{
unsigned short int __x[3];
unsigned short int __old_x[3];
unsigned short int __c;
unsigned short int __init;
__extension__ unsigned long long int __a;
};
extern int drand48_r (struct drand48_data *__restrict __buffer,
double *__restrict __result) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
extern int erand48_r (unsigned short int __xsubi[3],
struct drand48_data *__restrict __buffer,
double *__restrict __result) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
extern int lrand48_r (struct drand48_data *__restrict __buffer,
long int *__restrict __result)
__attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
extern int nrand48_r (unsigned short int __xsubi[3],
struct drand48_data *__restrict __buffer,
long int *__restrict __result)
__attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
extern int mrand48_r (struct drand48_data *__restrict __buffer,
long int *__restrict __result)
__attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
extern int jrand48_r (unsigned short int __xsubi[3],
struct drand48_data *__restrict __buffer,
long int *__restrict __result)
__attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
extern int srand48_r (long int __seedval, struct drand48_data *__buffer)
__attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (2)));
extern int seed48_r (unsigned short int __seed16v[3],
struct drand48_data *__buffer) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
extern int lcong48_r (unsigned short int __param[7],
struct drand48_data *__buffer)
__attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
extern void *malloc (size_t __size) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__malloc__)) ;
extern void *calloc (size_t __nmemb, size_t __size)
__attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__malloc__)) ;
extern void *realloc (void *__ptr, size_t __size)
__attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__warn_unused_result__));
extern void free (void *__ptr) __attribute__ ((__nothrow__ , __leaf__));
extern void cfree (void *__ptr) __attribute__ ((__nothrow__ , __leaf__));
extern void *alloca (size_t __size) __attribute__ ((__nothrow__ , __leaf__));
extern void *valloc (size_t __size) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__malloc__)) ;
extern int posix_memalign (void **__memptr, size_t __alignment, size_t __size)
__attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ;
extern void *aligned_alloc (size_t __alignment, size_t __size)
__attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__malloc__)) __attribute__ ((__alloc_size__ (2))) ;
extern void abort (void) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
extern int atexit (void (*__func) (void)) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
extern int at_quick_exit (void (*__func) (void)) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
extern int on_exit (void (*__func) (int __status, void *__arg), void *__arg)
__attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
extern void exit (int __status) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
extern void quick_exit (int __status) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
extern void _Exit (int __status) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
extern char *getenv (const char *__name) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ;
extern int putenv (char *__string) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
extern int setenv (const char *__name, const char *__value, int __replace)
__attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (2)));
extern int unsetenv (const char *__name) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
extern int clearenv (void) __attribute__ ((__nothrow__ , __leaf__));
extern char *mktemp (char *__template) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
extern int mkstemp (char *__template) __attribute__ ((__nonnull__ (1))) ;
extern int mkstemps (char *__template, int __suffixlen) __attribute__ ((__nonnull__ (1))) ;
extern char *mkdtemp (char *__template) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ;
extern int system (const char *__command) ;
extern char *realpath (const char *__restrict __name,
char *__restrict __resolved) __attribute__ ((__nothrow__ , __leaf__)) ;
typedef int (*__compar_fn_t) (const void *, const void *);
extern void *bsearch (const void *__key, const void *__base,
size_t __nmemb, size_t __size, __compar_fn_t __compar)
__attribute__ ((__nonnull__ (1, 2, 5))) ;
extern void qsort (void *__base, size_t __nmemb, size_t __size,
__compar_fn_t __compar) __attribute__ ((__nonnull__ (1, 4)));
extern int abs (int __x) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__)) ;
extern long int labs (long int __x) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__)) ;
__extension__ extern long long int llabs (long long int __x)
__attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__)) ;
extern div_t div (int __numer, int __denom)
__attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__)) ;
extern ldiv_t ldiv (long int __numer, long int __denom)
__attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__)) ;
__extension__ extern lldiv_t lldiv (long long int __numer,
long long int __denom)
__attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__)) ;
extern char *ecvt (double __value, int __ndigit, int *__restrict __decpt,
int *__restrict __sign) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3, 4))) ;
extern char *fcvt (double __value, int __ndigit, int *__restrict __decpt,
int *__restrict __sign) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3, 4))) ;
extern char *gcvt (double __value, int __ndigit, char *__buf)
__attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3))) ;
extern char *qecvt (long double __value, int __ndigit,
int *__restrict __decpt, int *__restrict __sign)
__attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3, 4))) ;
extern char *qfcvt (long double __value, int __ndigit,
int *__restrict __decpt, int *__restrict __sign)
__attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3, 4))) ;
extern char *qgcvt (long double __value, int __ndigit, char *__buf)
__attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3))) ;
extern int ecvt_r (double __value, int __ndigit, int *__restrict __decpt,
int *__restrict __sign, char *__restrict __buf,
size_t __len) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3, 4, 5)));
extern int fcvt_r (double __value, int __ndigit, int *__restrict __decpt,
int *__restrict __sign, char *__restrict __buf,
size_t __len) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3, 4, 5)));
extern int qecvt_r (long double __value, int __ndigit,
int *__restrict __decpt, int *__restrict __sign,
char *__restrict __buf, size_t __len)
__attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3, 4, 5)));
extern int qfcvt_r (long double __value, int __ndigit,
int *__restrict __decpt, int *__restrict __sign,
char *__restrict __buf, size_t __len)
__attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3, 4, 5)));
extern int mblen (const char *__s, size_t __n) __attribute__ ((__nothrow__ , __leaf__));
extern int mbtowc (wchar_t *__restrict __pwc,
const char *__restrict __s, size_t __n) __attribute__ ((__nothrow__ , __leaf__));
extern int wctomb (char *__s, wchar_t __wchar) __attribute__ ((__nothrow__ , __leaf__));
extern size_t mbstowcs (wchar_t *__restrict __pwcs,
const char *__restrict __s, size_t __n) __attribute__ ((__nothrow__ , __leaf__));
extern size_t wcstombs (char *__restrict __s,
const wchar_t *__restrict __pwcs, size_t __n)
__attribute__ ((__nothrow__ , __leaf__));
extern int rpmatch (const char *__response) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ;
extern int getsubopt (char **__restrict __optionp,
char *const *__restrict __tokens,
char **__restrict __valuep)
__attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2, 3))) ;
extern int getloadavg (double __loadavg[], int __nelem)
__attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
extern int __VERIFIER_nondet_int(void);
struct data_struct {
int number;
int *array;
int hasNextPartReference;
struct data_struct *nextData;
};
typedef struct data_struct *Data;
struct node_t {
Data data;
struct node_t *next;
};
static Data create_data(Data prevData) {
if(prevData != ((void *)0) && prevData->hasNextPartReference) {
return prevData->nextData;
}
Data data = malloc(sizeof *data);
data->array = (int*) malloc(20 * sizeof(data->array));
int counter = 0;
for(counter = 0; counter < 20; counter++) {
data->array[counter] = __VERIFIER_nondet_int();
}
data->number = 0;
int userInput = __VERIFIER_nondet_int();
while(__VERIFIER_nondet_int() && data->number < 200 && data->number > -200 && userInput < 200 && userInput > -200) {
data->number = data->number + __VERIFIER_nondet_int();
userInput = __VERIFIER_nondet_int();
}
if(__VERIFIER_nondet_int()) {
Data nextData = malloc(sizeof *data);
nextData->array = ((void *)0);
nextData->number = data->number - 200;
data->number = 200;
data->hasNextPartReference = 1;
data->nextData = nextData;
data->hasNextPartReference = 0;
data->nextData = ((void *)0);
} else {
data->hasNextPartReference = 0;
data->nextData = ((void *)0);
}
return data;
}
static void freeData(Data data) {
free(data->array);
free(data);
}
static void append(struct node_t **pointerToList) {
struct node_t *node = malloc(sizeof *node);
node->next = *pointerToList;
if(*pointerToList == ((void *)0)) {
node->data = create_data(((void *)0));
} else {
node->data = create_data(node->next->data);
}
*pointerToList = node;
}
int main() {
struct node_t *list = ((void *)0);
int dataNotFinished = 0;
do {
append(&list);
dataNotFinished = list->data != ((void *)0) && list->data->hasNextPartReference;
} while(dataNotFinished || __VERIFIER_nondet_int());
while (list) {
struct node_t *next = list->next;
freeData(list->data);
free(list);
list = next;
}
return 0;
}<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<graphml xmlns="http://graphml.graphdrawing.org/xmlns" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance">
<key attr.name="isViolationNode" attr.type="boolean" for="node" id="violation">
<default>false</default>
</key>
<key attr.name="isEntryNode" attr.type="boolean" for="node" id="entry">
<default>false</default>
</key>
<key attr.name="isSinkNode" attr.type="boolean" for="node" id="sink">
<default>false</default>
</key>
<key attr.name="enterLoopHead" attr.type="boolean" for="edge" id="enterLoopHead">
<default>false</default>
</key>
<key attr.name="violatedProperty" attr.type="string" for="node" id="violatedProperty"/>
<key attr.name="sourcecodeLanguage" attr.type="string" for="graph" id="sourcecodelang"/>
<key attr.name="programFile" attr.type="string" for="graph" id="programfile"/>
<key attr.name="programHash" attr.type="string" for="graph" id="programhash"/>
<key attr.name="specification" attr.type="string" for="graph" id="specification"/>
<key attr.name="architecture" attr.type="string" for="graph" id="architecture"/>
<key attr.name="producer" attr.type="string" for="graph" id="producer"/>
<key attr.name="creationTime" attr.type="string" for="graph" id="creationtime"/>
<key attr.name="startline" attr.type="int" for="edge" id="startline"/>
<key attr.name="endline" attr.type="int" for="edge" id="endline"/>
<key attr.name="startoffset" attr.type="int" for="edge" id="startoffset"/>
<key attr.name="endoffset" attr.type="int" for="edge" id="endoffset"/>
<key attr.name="originFileName" attr.type="string" for="edge" id="originfile">
<default>./complex_data_creation_test01-1.i</default>
</key>
<key attr.name="control" attr.type="string" for="edge" id="control"/>
<key attr.name="assumption" attr.type="string" for="edge" id="assumption"/>
<key attr.name="assumption.scope" attr.type="string" for="edge" id="assumption.scope"/>
<key attr.name="enterFunction" attr.type="string" for="edge" id="enterFunction"/>
<key attr.name="returnFromFunction" attr.type="string" for="edge" id="returnFrom"/>
<key attr.name="witness-type" attr.type="string" for="graph" id="witness-type"/>
<key attr.name="inputWitnessHash" attr.type="string" for="graph" id="inputwitnesshash"/>
<graph edgedefault="directed">
<data key="witness-type">violation_witness</data>
<data key="sourcecodelang">C</data>
<data key="producer">CPAchecker 2.0</data>
<data key="specification">CHECK( init(main()), LTL(G valid-memtrack) )</data>
<data key="specification">CHECK( init(main()), LTL(G valid-deref) )</data>
<data key="specification">CHECK( init(main()), LTL(G valid-free) )</data>
<data key="programfile">./complex_data_creation_test01-1.i</data>
<data key="programhash">52769785b06238c88fd6b21b09d77c08165e59529f322f93adf725e9d68e47df</data>
<data key="architecture">32bit</data>
<data key="creationtime">2021-10-13T16:46:22+08:00</data>
<node id="A0">
<data key="entry">true</data>
</node>
<node id="A528"/>
<edge source="A0" target="A528">
<data key="startline">596</data>
<data key="endline">596</data>
<data key="startoffset">24194</data>
<data key="endoffset">24204</data>
<data key="enterFunction">main</data>
</edge>
<node id="A532"/>
<edge source="A528" target="A532">
<data key="startline">598</data>
<data key="endline">598</data>
<data key="startoffset">24246</data>
<data key="endoffset">24268</data>
<data key="assumption">dataNotFinished == (0);</data>
<data key="assumption.scope">main</data>
</edge>
<node id="A536"/>
<edge source="A532" target="A536">
<data key="startline">600</data>
<data key="endline">600</data>
<data key="startoffset">24282</data>
<data key="endoffset">24293</data>
<data key="enterFunction">append</data>
</edge>
<node id="A546"/>
<edge source="A536" target="A546">
<data key="startline">589</data>
<data key="endline">589</data>
<data key="startoffset">24028</data>
<data key="endoffset">24056</data>
<data key="control">condition-true</data>
</edge>
<node id="sink">
<data key="sink">true</data>
</node>
<edge source="A536" target="sink">
<data key="startline">589</data>
<data key="endline">589</data>
<data key="startoffset">24028</data>
<data key="endoffset">24056</data>
<data key="control">condition-false</data>
</edge>
<node id="A548"/>
<edge source="A546" target="A548">
<data key="startline">590</data>
<data key="endline">590</data>
<data key="startoffset">24078</data>
<data key="endoffset">24101</data>
<data key="enterFunction">create_data</data>
</edge>
<node id="A552"/>
<edge source="A548" target="A552">
<data key="startline">552</data>
<data key="endline">552</data>
<data key="startoffset">22812</data>
<data key="endoffset">22834</data>
<data key="control">condition-false</data>
</edge>
<edge source="A548" target="sink">
<data key="startline">552</data>
<data key="endline">552</data>
<data key="startoffset">22812</data>
<data key="endoffset">22834</data>
<data key="control">condition-true</data>
</edge>
<node id="A560"/>
<edge source="A552" target="A560">
<data key="startline">557</data>
<data key="endline">557</data>
<data key="startoffset">23003</data>
<data key="endoffset">23017</data>
<data key="assumption">counter == (0);</data>
<data key="assumption.scope">create_data</data>
</edge>
<node id="A564"/>
<edge source="A560" target="A564">
<data key="enterLoopHead">true</data>
<data key="startline">558</data>
<data key="endline">558</data>
<data key="startoffset">23026</data>
<data key="endoffset">23036</data>
<data key="assumption">counter == (0);</data>
<data key="assumption.scope">create_data</data>
</edge>
<node id="A566"/>
<edge source="A564" target="A566">
<data key="startline">558</data>
<data key="endline">558</data>
<data key="startoffset">23039</data>
<data key="endoffset">23050</data>
<data key="control">condition-true</data>
<data key="assumption">counter == (0);</data>
<data key="assumption.scope">create_data</data>
</edge>
<edge source="A564" target="sink">
<data key="startline">558</data>
<data key="endline">558</data>
<data key="startoffset">23039</data>
<data key="endoffset">23050</data>
<data key="control">condition-false</data>
</edge>
<node id="A572"/>
<edge source="A566" target="A572">
<data key="enterLoopHead">true</data>
<data key="startline">558</data>
<data key="endline">558</data>
<data key="startoffset">23053</data>
<data key="endoffset">23061</data>
<data key="assumption">counter == (1);</data>
<data key="assumption.scope">create_data</data>
</edge>
<node id="A574"/>
<edge source="A572" target="A574">
<data key="startline">558</data>
<data key="endline">558</data>
<data key="startoffset">23039</data>
<data key="endoffset">23050</data>
<data key="control">condition-true</data>
<data key="assumption">counter == (1);</data>
<data key="assumption.scope">create_data</data>
</edge>
<edge source="A572" target="sink">
<data key="startline">558</data>
<data key="endline">558</data>
<data key="startoffset">23039</data>
<data key="endoffset">23050</data>
<data key="control">condition-false</data>
</edge>
<node id="A580"/>
<edge source="A574" target="A580">
<data key="enterLoopHead">true</data>
<data key="startline">558</data>
<data key="endline">558</data>
<data key="startoffset">23053</data>
<data key="endoffset">23061</data>
<data key="assumption">counter == (2);</data>
<data key="assumption.scope">create_data</data>
</edge>
<node id="A582"/>
<edge source="A580" target="A582">
<data key="startline">558</data>
<data key="endline">558</data>
<data key="startoffset">23039</data>
<data key="endoffset">23050</data>
<data key="control">condition-true</data>
<data key="assumption">counter == (2);</data>
<data key="assumption.scope">create_data</data>
</edge>
<edge source="A580" target="sink">
<data key="startline">558</data>
<data key="endline">558</data>
<data key="startoffset">23039</data>
<data key="endoffset">23050</data>
<data key="control">condition-false</data>
</edge>
<node id="A588"/>
<edge source="A582" target="A588">
<data key="enterLoopHead">true</data>
<data key="startline">558</data>
<data key="endline">558</data>
<data key="startoffset">23053</data>
<data key="endoffset">23061</data>
<data key="assumption">counter == (3);</data>
<data key="assumption.scope">create_data</data>
</edge>
<node id="A590"/>
<edge source="A588" target="A590">
<data key="startline">558</data>
<data key="endline">558</data>
<data key="startoffset">23039</data>
<data key="endoffset">23050</data>
<data key="control">condition-true</data>
<data key="assumption">counter == (3);</data>
<data key="assumption.scope">create_data</data>
</edge>
<edge source="A588" target="sink">
<data key="startline">558</data>
<data key="endline">558</data>
<data key="startoffset">23039</data>
<data key="endoffset">23050</data>
<data key="control">condition-false</data>
</edge>
<node id="A596"/>
<edge source="A590" target="A596">
<data key="enterLoopHead">true</data>
<data key="startline">558</data>
<data key="endline">558</data>
<data key="startoffset">23053</data>
<data key="endoffset">23061</data>
<data key="assumption">counter == (4);</data>
<data key="assumption.scope">create_data</data>
</edge>
<node id="A598"/>
<edge source="A596" target="A598">
<data key="startline">558</data>
<data key="endline">558</data>
<data key="startoffset">23039</data>
<data key="endoffset">23050</data>
<data key="control">condition-true</data>
<data key="assumption">counter == (4);</data>
<data key="assumption.scope">create_data</data>
</edge>
<edge source="A596" target="sink">
<data key="startline">558</data>
<data key="endline">558</data>
<data key="startoffset">23039</data>
<data key="endoffset">23050</data>
<data key="control">condition-false</data>
</edge>
<node id="A604"/>
<edge source="A598" target="A604">
<data key="enterLoopHead">true</data>
<data key="startline">558</data>
<data key="endline">558</data>
<data key="startoffset">23053</data>
<data key="endoffset">23061</data>
<data key="assumption">counter == (5);</data>
<data key="assumption.scope">create_data</data>
</edge>
<node id="A606"/>
<edge source="A604" target="A606">
<data key="startline">558</data>
<data key="endline">558</data>
<data key="startoffset">23039</data>
<data key="endoffset">23050</data>
<data key="control">condition-true</data>
<data key="assumption">counter == (5);</data>
<data key="assumption.scope">create_data</data>
</edge>
<edge source="A604" target="sink">
<data key="startline">558</data>
<data key="endline">558</data>
<data key="startoffset">23039</data>
<data key="endoffset">23050</data>
<data key="control">condition-false</data>
</edge>
<node id="A612"/>
<edge source="A606" target="A612">
<data key="enterLoopHead">true</data>
<data key="startline">558</data>
<data key="endline">558</data>
<data key="startoffset">23053</data>
<data key="endoffset">23061</data>
<data key="assumption">counter == (6);</data>
<data key="assumption.scope">create_data</data>
</edge>
<node id="A614"/>
<edge source="A612" target="A614">
<data key="startline">558</data>
<data key="endline">558</data>
<data key="startoffset">23039</data>
<data key="endoffset">23050</data>
<data key="control">condition-true</data>
<data key="assumption">counter == (6);</data>
<data key="assumption.scope">create_data</data>
</edge>
<edge source="A612" target="sink">
<data key="startline">558</data>
<data key="endline">558</data>
<data key="startoffset">23039</data>
<data key="endoffset">23050</data>
<data key="control">condition-false</data>
</edge>
<node id="A620"/>
<edge source="A614" target="A620">
<data key="enterLoopHead">true</data>
<data key="startline">558</data>
<data key="endline">558</data>
<data key="startoffset">23053</data>
<data key="endoffset">23061</data>
<data key="assumption">counter == (7);</data>
<data key="assumption.scope">create_data</data>
</edge>
<node id="A622"/>
<edge source="A620" target="A622">
<data key="startline">558</data>
<data key="endline">558</data>
<data key="startoffset">23039</data>
<data key="endoffset">23050</data>
<data key="control">condition-true</data>
<data key="assumption">counter == (7);</data>
<data key="assumption.scope">create_data</data>
</edge>
<edge source="A620" target="sink">
<data key="startline">558</data>
<data key="endline">558</data>
<data key="startoffset">23039</data>
<data key="endoffset">23050</data>
<data key="control">condition-false</data>
</edge>
<node id="A628"/>
<edge source="A622" target="A628">
<data key="enterLoopHead">true</data>
<data key="startline">558</data>
<data key="endline">558</data>
<data key="startoffset">23053</data>
<data key="endoffset">23061</data>
<data key="assumption">counter == (8);</data>
<data key="assumption.scope">create_data</data>
</edge>
<node id="A630"/>
<edge source="A628" target="A630">
<data key="startline">558</data>
<data key="endline">558</data>
<data key="startoffset">23039</data>
<data key="endoffset">23050</data>
<data key="control">condition-true</data>
<data key="assumption">counter == (8);</data>
<data key="assumption.scope">create_data</data>
</edge>
<edge source="A628" target="sink">
<data key="startline">558</data>
<data key="endline">558</data>
<data key="startoffset">23039</data>
<data key="endoffset">23050</data>
<data key="control">condition-false</data>
</edge>
<node id="A636"/>
<edge source="A630" target="A636">
<data key="enterLoopHead">true</data>
<data key="startline">558</data>
<data key="endline">558</data>
<data key="startoffset">23053</data>
<data key="endoffset">23061</data>
<data key="assumption">counter == (9);</data>
<data key="assumption.scope">create_data</data>
</edge>
<node id="A638"/>
<edge source="A636" target="A638">
<data key="startline">558</data>
<data key="endline">558</data>
<data key="startoffset">23039</data>
<data key="endoffset">23050</data>
<data key="control">condition-true</data>
<data key="assumption">counter == (9);</data>
<data key="assumption.scope">create_data</data>
</edge>
<edge source="A636" target="sink">
<data key="startline">558</data>
<data key="endline">558</data>
<data key="startoffset">23039</data>
<data key="endoffset">23050</data>
<data key="control">condition-false</data>
</edge>
<node id="A644"/>
<edge source="A638" target="A644">
<data key="enterLoopHead">true</data>
<data key="startline">558</data>
<data key="endline">558</data>
<data key="startoffset">23053</data>
<data key="endoffset">23061</data>
<data key="assumption">counter == (10);</data>
<data key="assumption.scope">create_data</data>
</edge>
<node id="A646"/>
<edge source="A644" target="A646">
<data key="startline">558</data>
<data key="endline">558</data>
<data key="startoffset">23039</data>
<data key="endoffset">23050</data>
<data key="control">condition-true</data>
<data key="assumption">counter == (10);</data>
<data key="assumption.scope">create_data</data>
</edge>
<edge source="A644" target="sink">
<data key="startline">558</data>
<data key="endline">558</data>
<data key="startoffset">23039</data>
<data key="endoffset">23050</data>
<data key="control">condition-false</data>
</edge>
<node id="A652"/>
<edge source="A646" target="A652">
<data key="enterLoopHead">true</data>
<data key="startline">558</data>
<data key="endline">558</data>
<data key="startoffset">23053</data>
<data key="endoffset">23061</data>
<data key="assumption">counter == (11);</data>
<data key="assumption.scope">create_data</data>
</edge>
<node id="A654"/>
<edge source="A652" target="A654">
<data key="startline">558</data>
<data key="endline">558</data>
<data key="startoffset">23039</data>
<data key="endoffset">23050</data>
<data key="control">condition-true</data>
<data key="assumption">counter == (11);</data>
<data key="assumption.scope">create_data</data>
</edge>
<edge source="A652" target="sink">
<data key="startline">558</data>
<data key="endline">558</data>
<data key="startoffset">23039</data>
<data key="endoffset">23050</data>
<data key="control">condition-false</data>
</edge>
<node id="A660"/>
<edge source="A654" target="A660">
<data key="enterLoopHead">true</data>
<data key="startline">558</data>
<data key="endline">558</data>
<data key="startoffset">23053</data>
<data key="endoffset">23061</data>
<data key="assumption">counter == (12);</data>
<data key="assumption.scope">create_data</data>
</edge>
<node id="A662"/>
<edge source="A660" target="A662">
<data key="startline">558</data>
<data key="endline">558</data>
<data key="startoffset">23039</data>
<data key="endoffset">23050</data>
<data key="control">condition-true</data>
<data key="assumption">counter == (12);</data>
<data key="assumption.scope">create_data</data>
</edge>
<edge source="A660" target="sink">
<data key="startline">558</data>
<data key="endline">558</data>
<data key="startoffset">23039</data>
<data key="endoffset">23050</data>
<data key="control">condition-false</data>
</edge>
<node id="A668"/>
<edge source="A662" target="A668">
<data key="enterLoopHead">true</data>
<data key="startline">558</data>
<data key="endline">558</data>
<data key="startoffset">23053</data>
<data key="endoffset">23061</data>
<data key="assumption">counter == (13);</data>
<data key="assumption.scope">create_data</data>
</edge>
<node id="A670"/>
<edge source="A668" target="A670">
<data key="startline">558</data>
<data key="endline">558</data>
<data key="startoffset">23039</data>
<data key="endoffset">23050</data>
<data key="control">condition-true</data>
<data key="assumption">counter == (13);</data>
<data key="assumption.scope">create_data</data>
</edge>
<edge source="A668" target="sink">
<data key="startline">558</data>
<data key="endline">558</data>
<data key="startoffset">23039</data>
<data key="endoffset">23050</data>
<data key="control">condition-false</data>
</edge>
<node id="A676"/>
<edge source="A670" target="A676">
<data key="enterLoopHead">true</data>
<data key="startline">558</data>
<data key="endline">558</data>
<data key="startoffset">23053</data>
<data key="endoffset">23061</data>
<data key="assumption">counter == (14);</data>
<data key="assumption.scope">create_data</data>
</edge>
<node id="A678"/>
<edge source="A676" target="A678">
<data key="startline">558</data>
<data key="endline">558</data>
<data key="startoffset">23039</data>
<data key="endoffset">23050</data>
<data key="control">condition-true</data>
<data key="assumption">counter == (14);</data>
<data key="assumption.scope">create_data</data>
</edge>
<edge source="A676" target="sink">
<data key="startline">558</data>
<data key="endline">558</data>
<data key="startoffset">23039</data>
<data key="endoffset">23050</data>
<data key="control">condition-false</data>
</edge>
<node id="A684"/>
<edge source="A678" target="A684">
<data key="enterLoopHead">true</data>
<data key="startline">558</data>
<data key="endline">558</data>
<data key="startoffset">23053</data>
<data key="endoffset">23061</data>
<data key="assumption">counter == (15);</data>
<data key="assumption.scope">create_data</data>
</edge>
<node id="A686"/>
<edge source="A684" target="A686">
<data key="startline">558</data>
<data key="endline">558</data>
<data key="startoffset">23039</data>
<data key="endoffset">23050</data>
<data key="control">condition-true</data>
<data key="assumption">counter == (15);</data>
<data key="assumption.scope">create_data</data>
</edge>
<edge source="A684" target="sink">
<data key="startline">558</data>
<data key="endline">558</data>
<data key="startoffset">23039</data>
<data key="endoffset">23050</data>
<data key="control">condition-false</data>
</edge>
<node id="A692"/>
<edge source="A686" target="A692">
<data key="enterLoopHead">true</data>
<data key="startline">558</data>
<data key="endline">558</data>
<data key="startoffset">23053</data>
<data key="endoffset">23061</data>
<data key="assumption">counter == (16);</data>
<data key="assumption.scope">create_data</data>
</edge>
<node id="A694"/>
<edge source="A692" target="A694">
<data key="startline">558</data>
<data key="endline">558</data>
<data key="startoffset">23039</data>
<data key="endoffset">23050</data>
<data key="control">condition-true</data>
<data key="assumption">counter == (16);</data>
<data key="assumption.scope">create_data</data>
</edge>
<edge source="A692" target="sink">
<data key="startline">558</data>
<data key="endline">558</data>
<data key="startoffset">23039</data>
<data key="endoffset">23050</data>
<data key="control">condition-false</data>
</edge>
<node id="A700"/>
<edge source="A694" target="A700">
<data key="enterLoopHead">true</data>
<data key="startline">558</data>
<data key="endline">558</data>
<data key="startoffset">23053</data>
<data key="endoffset">23061</data>
<data key="assumption">counter == (17);</data>
<data key="assumption.scope">create_data</data>
</edge>
<node id="A702"/>
<edge source="A700" target="A702">
<data key="startline">558</data>
<data key="endline">558</data>
<data key="startoffset">23039</data>
<data key="endoffset">23050</data>
<data key="control">condition-true</data>
<data key="assumption">counter == (17);</data>
<data key="assumption.scope">create_data</data>
</edge>
<edge source="A700" target="sink">
<data key="startline">558</data>
<data key="endline">558</data>
<data key="startoffset">23039</data>
<data key="endoffset">23050</data>
<data key="control">condition-false</data>
</edge>
<node id="A708"/>
<edge source="A702" target="A708">
<data key="enterLoopHead">true</data>
<data key="startline">558</data>
<data key="endline">558</data>
<data key="startoffset">23053</data>
<data key="endoffset">23061</data>
<data key="assumption">counter == (18);</data>
<data key="assumption.scope">create_data</data>
</edge>
<node id="A710"/>
<edge source="A708" target="A710">
<data key="startline">558</data>
<data key="endline">558</data>
<data key="startoffset">23039</data>
<data key="endoffset">23050</data>
<data key="control">condition-true</data>
<data key="assumption">counter == (18);</data>
<data key="assumption.scope">create_data</data>
</edge>
<edge source="A708" target="sink">
<data key="startline">558</data>
<data key="endline">558</data>
<data key="startoffset">23039</data>
<data key="endoffset">23050</data>
<data key="control">condition-false</data>
</edge>
<node id="A716"/>
<edge source="A710" target="A716">
<data key="enterLoopHead">true</data>
<data key="startline">558</data>
<data key="endline">558</data>
<data key="startoffset">23053</data>
<data key="endoffset">23061</data>
<data key="assumption">counter == (19);</data>
<data key="assumption.scope">create_data</data>
</edge>
<node id="A718"/>
<edge source="A716" target="A718">
<data key="startline">558</data>
<data key="endline">558</data>
<data key="startoffset">23039</data>
<data key="endoffset">23050</data>
<data key="control">condition-true</data>
<data key="assumption">counter == (19);</data>
<data key="assumption.scope">create_data</data>
</edge>
<edge source="A716" target="sink">
<data key="startline">558</data>
<data key="endline">558</data>
<data key="startoffset">23039</data>
<data key="endoffset">23050</data>
<data key="control">condition-false</data>
</edge>
<node id="A724"/>
<edge source="A718" target="A724">
<data key="enterLoopHead">true</data>
<data key="startline">558</data>
<data key="endline">558</data>
<data key="startoffset">23053</data>
<data key="endoffset">23061</data>
<data key="assumption">counter == (20);</data>
<data key="assumption.scope">create_data</data>
</edge>
<node id="A726"/>
<edge source="A724" target="A726">
<data key="startline">558</data>
<data key="endline">558</data>
<data key="startoffset">23039</data>
<data key="endoffset">23050</data>
<data key="control">condition-false</data>
<data key="assumption">counter == (20);</data>
<data key="assumption.scope">create_data</data>
</edge>
<edge source="A724" target="sink">
<data key="startline">558</data>
<data key="endline">558</data>
<data key="startoffset">23039</data>
<data key="endoffset">23050</data>
<data key="control">condition-true</data>
</edge>
<node id="A728"/>
<edge source="A726" target="A728">
<data key="startline">561</data>
<data key="endline">561</data>
<data key="startoffset">23124</data>
<data key="endoffset">23139</data>
<data key="assumption">(data->number) == (0);</data>
<data key="assumption.scope">create_data</data>
</edge>
<node id="A732"/>
<edge source="A728" target="A732">
<data key="enterLoopHead">true</data>
<data key="startline">562</data>
<data key="endline">562</data>
<data key="startoffset">23158</data>
<data key="endoffset">23182</data>
</edge>
<edge source="A732" target="sink">
<data key="startline">563</data>
<data key="endline">563</data>
<data key="startoffset">23265</data>
<data key="endoffset">23279</data>
<data key="control">condition-true</data>
</edge>
<node id="A750"/>
<edge source="A732" target="A750">
<data key="startline">563</data>
<data key="endline">563</data>
<data key="startoffset">23265</data>
<data key="endoffset">23279</data>
<data key="control">condition-false</data>
</edge>
<edge source="A732" target="sink">
<data key="startline">563</data>
<data key="endline">563</data>
<data key="startoffset">23193</data>
<data key="endoffset">23260</data>
<data key="control">condition-false</data>
</edge>
<edge source="A750" target="sink">
<data key="startline">567</data>
<data key="endline">567</data>
<data key="startoffset">23413</data>
<data key="endoffset">23435</data>
<data key="control">condition-false</data>
</edge>
<node id="A758"/>
<edge source="A750" target="A758">
<data key="startline">567</data>
<data key="endline">567</data>
<data key="startoffset">23413</data>
<data key="endoffset">23435</data>
<data key=<?xml version='1.0' encoding='UTF-8'?>
<graphml>
<graph edgedefault="directed">
<data key="witness-type">violation_witness</data>
<data key="sourcecodelang">C</data>
<data key="producer">Symbiotic</data>
<data key="specification">memsafety</data>
<data key="programfile">/opt/symbiotic/install/bin/test.c</data>
<data key="programhash">6b0831b861e7e75ec685dc6603ffc32fa134723c</data>
<data key="architecture">64bit</data>
<node id="0">
<data key="entry">true</data>
<data key="violation">true</data>
</node>
</graph>
</graphml>"control">condition-true</data>
</edge>
<node id="A766"/>
<edge source="A758" target="A766">
<data key="startline">570</data>
<data key="endline">570</data>
<data key="startoffset">23521</data>
<data key="endoffset">23557</data>
<data key="assumption">(nextData->number) == (-200);</data>
<data key="assumption.scope">create_data</data>
</edge>
<node id="A768"/>
<edge source="A766" target="A768">
<data key="startline">571</data>
<data key="endline">571</data>
<data key="startoffset">23564</data>
<data key="endoffset">23581</data>
<data key="assumption">(data->number) == (200);</data>
<data key="assumption.scope">create_data</data>
</edge>
<node id="A780">
<data key="violation">true</data>
<data key="violatedProperty">valid-memtrack</data>
</node>
<edge source="A768" target="A780">
<data key="startline">580</data>
<data key="endline">580</data>
<data key="startoffset">23808</data>
<data key="endoffset">23818</data>
<data key="returnFrom">create_data</data>
</edge>
</graph>
</graphml><?xml version='1.0' encoding='UTF-8'?>
<graphml>
<graph edgedefault="directed">
<data key="witness-type">violation_witness</data>
<data key="sourcecodelang">C</data>
<data key="producer">Symbiotic</data>
<data key="specification">memsafety</data>
<data key="programfile">/opt/symbiotic/install/bin/test.c</data>
<data key="programhash">6b0831b861e7e75ec685dc6603ffc32fa134723c</data>
<data key="architecture">64bit</data>
<node id="0">
<data key="entry">true</data>
<data key="violation">true</data>
</node>
</graph>
</graphml>file: bubblesort_unsafe.c
extern int __VERIFIER_nondet_int(void);
void bubbleSort(int numbers[], int array_size)
{
int i, j, temp;
for (i = (array_size - 1); i >= 0; i--) {
for (j = 1; j <= i; j++) {
if (numbers[j-1] > numbers[j]) {
temp = numbers[j-1];
numbers[j-1] = numbers[j];
numbers[j] = temp;
}
}
}
}
int main() {
int* numbers;
int array_size = __VERIFIER_nondet_int();
bubbleSort(numbers, array_size);
return 0;
}<?xml version="1.0" encoding="UTF-8"?>
<graphml xmlns="http://graphml.graphdrawing.org/xmlns" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xsi:schemaLocation="http://graphml.graphdrawing.org/xmlns http://graphml.graphdrawing.org/xmlns/1.0/graphml.xsd">
<key id="programfile" attr.name="programfile" for="graph"/>
<key id="programhash" attr.name="programhash" for="graph"/>
<key id="sourcecodelang" attr.name="sourcecodelang" for="graph"/>
<key id="producer" attr.name="producer" for="graph"/>
<key id="specification" attr.name="specification" for="graph"/>
<key id="creationtime" attr.name="creationtime" for="graph"/>
<key id="witness-type" attr.name="witness-type" for="graph"/>
<key id="architecture" attr.name="architecture" for="graph"/>
<key id="entry" attr.name="entry" for="node">
<default>false</default>
</key>
<key id="nodetype" attr.name="nodetype" for="node">
<default>path</default>
</key>
<key id="violation" attr.name="violation" for="node">
<default>false</default>
</key>
<key id="cyclehead" attr.name="cyclehead" for="node">
<default>false</default>
</key>
<key id="invariant" attr.name="invariant" for="node">
<default>true</default>
</key>
<key id="threadId" attr.name="threadId" for="edge"/>
<key id="endline" attr.name="endline" for="edge"/>
<key id="enterLoopHead" attr.name="enterLoopHead" for="edge">
<default>false</default>
</key>
<key id="createThread" attr.name="createThread" for="edge"/>
<key id="enterFunction" attr.name="enterFunction" for="edge"/>
<key id="startline" attr.name="startline" for="edge"/>
<key id="returnFrom" attr.name="returnFrom" for="edge"/>
<key id="assumption" attr.name="assumption" for="edge"/>
<key id="tokens" attr.name="tokens" for="edge"/>
<key id="control" attr.name="control" for="edge"/>
<key id="originfile" attr.name="originfile" for="edge">
<default>/home/center/Project/uautomizer/UAutomizer-linux/bubblesort_unsafe.c</default>
</key>
<key id="sourcecode" attr.name="sourcecode" for="edge"/>
<graph edgedefault="directed">
<data key="programfile">/home/center/Project/uautomizer/UAutomizer-linux/bubblesort_unsafe.c</data>
<data key="programhash">e06dd3d11d320ef89a2d2c8c527408fda05cf2ff</data>
<data key="sourcecodelang">C</data>
<data key="producer">Automizer</data>
<data key="specification">CHECK( init(main()), LTL(G valid-free) )
CHECK( init(main()), LTL(G valid-deref) )
CHECK( init(main()), LTL(G valid-memtrack) )
</data>
<data key="creationtime">2021-10-13T09:27:14</data>
<data key="witness-type">violation_witness</data>
<data key="architecture">64bit</data>
<node id="N0">
<data key="entry">true</data>
</node>
<node id="N1"/>
<node id="N2"/>
<node id="N3"/>
<node id="N4"/>
<node id="N5"/>
<node id="N6"/>
<node id="N7">
<data key="violation">true</data>
</node>
<edge id="E0" source="N0" target="N1">
<data key="endline">19</data>
<data key="startline">19</data>
<data key="originfile">/home/center/Project/uautomizer/UAutomizer-linux/bubblesort_unsafe.c</data>
<data key="sourcecode">int* numbers;</data>
</edge>
<edge id="E1" source="N1" target="N2">
<data key="endline">20</data>
<data key="startline">20</data>
<data key="originfile">/home/center/Project/uautomizer/UAutomizer-linux/bubblesort_unsafe.c</data>
<data key="sourcecode">int array_size = __VERIFIER_nondet_int();</data>
</edge>
<edge id="E2" source="N2" target="N3">
<data key="endline">21</data>
<data key="enterFunction">bubbleSort</data>
<data key="startline">21</data>
<data key="originfile">/home/center/Project/uautomizer/UAutomizer-linux/bubblesort_unsafe.c</data>
<data key="sourcecode">bubbleSort(numbers, array_size)</data>
</edge>
<edge id="E3" source="N3" target="N4">
<data key="endline">5</data>
<data key="startline">5</data>
<data key="originfile">/home/center/Project/uautomizer/UAutomizer-linux/bubblesort_unsafe.c</data>
<data key="sourcecode">int i, j, temp;</data>
</edge>
<edge id="E4" source="N4" target="N5">
<data key="endline">7</data>
<data key="startline">7</data>
<data key="assumption">array_size==2;i==1;</data>
<data key="originfile">/home/center/Project/uautomizer/UAutomizer-linux/bubblesort_unsafe.c</data>
<data key="sourcecode">i = (array_size - 1)</data>
</edge>
<edge id="E5" source="N5" target="N6">
<data key="endline">8</data>
<data key="startline">8</data>
<data key="assumption">j==1;i==1;array_size==2;</data>
<data key="originfile">/home/center/Project/uautomizer/UAutomizer-linux/bubblesort_unsafe.c</data>
<data key="sourcecode">j = 1</data>
</edge>
<edge id="E6" source="N6" target="N7">
<data key="endline">9</data>
<data key="startline">9</data>
<data key="originfile">/home/center/Project/uautomizer/UAutomizer-linux/bubblesort_unsafe.c</data>
<data key="sourcecode">numbers[j-1]</data>
</edge>
</graph>
</graphml>file: memsafety-ext3/freeAlloca.c
typedef unsigned int size_t;
extern void *alloca(size_t size);
extern void free(void*);
extern char __VERIFIER_nondet_char(void);
int main(void){
char *p = alloca(10 * sizeof(char));
for (int i = 0; i < 10; i++) {
p[i] = __VERIFIER_nondet_char();
}
if (p[2] == 'a')
free(p);
return 0;
}<?xml version='1.0' encoding='UTF-8'?>
<graphml xmlns="http://graphml.graphdrawing.org/xmlns" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance">
<graph edgedefault="directed">
<node id="0">
<data key="entry">true</data>
</node>
<node id="1"/>
<edge source="0" target="1">
<data key="assumption">\result==0</data>
<data key="assumption.resultfunction">__VERIFIER_nondet_char</data>
<data key="startline">10</data>
</edge>
<node id="2"/>
<edge source="1" target="2">
<data key="assumption">\result==0</data>
<data key="assumption.resultfunction">__VERIFIER_nondet_char</data>
<data key="startline">10</data>
</edge>
<node id="3"/>
<edge source="2" target="3">
<data key="assumption">\result==97</data>
<data key="assumption.resultfunction">__VERIFIER_nondet_char</data>
<data key="startline">10</data>
</edge>
<node id="4"/>
<edge source="3" target="4">
<data key="assumption">\result==0</data>
<data key="assumption.resultfunction">__VERIFIER_nondet_char</data>
<data key="startline">10</data>
</edge>
<node id="5"/>
<edge source="4" target="5">
<data key="assumption">\result==0</data>
<data key="assumption.resultfunction">__VERIFIER_nondet_char</data>
<data key="startline">10</data>
</edge>
<node id="6"/>
<edge source="5" target="6">
<data key="assumption">\result==0</data>
<data key="assumption.resultfunction">__VERIFIER_nondet_char</data>
<data key="startline">10</data>
</edge>
<node id="7"/>
<edge source="6" target="7">
<data key="assumption">\result==0</data>
<data key="assumption.resultfunction">__VERIFIER_nondet_char</data>
<data key="startline">10</data>
</edge>
<node id="8"/>
<edge source="7" target="8">
<data key="assumption">\result==0</data>
<data key="assumption.resultfunction">__VERIFIER_nondet_char</data>
<data key="startline">10</data>
</edge>
<node id="9"/>
<edge source="8" target="9">
<data key="assumption">\result==0</data>
<data key="assumption.resultfunction">__VERIFIER_nondet_char</data>
<data key="startline">10</data>
</edge>
<node id="10"/>
<edge source="9" target="10">
<data key="assumption">\result==0</data>
<data key="assumption.resultfunction">__VERIFIER_nondet_char</data>
<data key="startline">10</data>
</edge>
<node id="11">
<data key="violation">true</data>
</node>
<edge source="10" target="11"/>
<data key="witness-type">violation_witness</data><data key="sourcecodelang">C</data><data key="producer">Symbiotic</data><data key="specification">CHECK( init(main()), LTL(G valid-free) )</data><data key="specification">CHECK( init(main()), LTL(G valid-deref) )</data><data key="specification">CHECK( init(main()), LTL(G valid-memtrack) )</data><data key="programfile">/tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_7c39dd4b-a77a-494f-936e-598b823b6765/tmp/cvtremote_vn9vq3jm/sv-benchmarks/c/memsafety-ext3/freeAlloca.c</data><data key="programhash">cb3174b12ccafcfa2421015218ce7e009c2319e912e783d4246aed1266b2586b</data><data key="architecture">32bit</data><data key="creationtime">2021-10-14T04:55:54</data></graph>
<key id="witness-type" for="graph" attr.type="string" attr.name="witness-type"/><key id="specification" for="graph" attr.type="string" attr.name="specification"/><key id="programfile" for="graph" attr.type="string" attr.name="programfile"/><key id="sourcecodelang" for="graph" attr.type="string" attr.name="sourcecodelang"/><key id="producer" for="graph" attr.type="string" attr.name="producer"/><key id="creationtime" for="graph" attr.type="string" attr.name="creationtime"/><key id="architecture" for="graph" attr.type="string" attr.name="architecture"/><key id="programhash" for="graph" attr.type="string" attr.name="programhash"/><key id="entry" for="node" attr.type="string" attr.name="entry"/><key id="violation" for="node" attr.type="string" attr.name="violation"/><key id="assumption" for="edge" attr.type="string" attr.name="assumption"/><key id="assumption.resultfunction" for="edge" attr.type="string" attr.name="assumption.resultfunction"/><key id="startline" for="edge" attr.type="string" attr.name="startline"/><key id="cyclehead" for="node" attr.type="boolean" attr.name="cyclehead"><default>false</default></key><key id="enterLoopHead" for="edge" attr.type="boolean" attr.name="enterLoopHead"><default>false</default></key></graphml>