rec_malloc_ex11_true-termination.c.i

typedef long unsigned int size_t;

void * __attribute__((__cdecl__)) malloc (size_t __size) ;
void __attribute__((__cdecl__)) free (void *) ;

extern int __VERIFIER_nondet_int(void);

int rec(int *op) {
	if(*op < 0) {
		int r = *op;
		free(op);
		return r;
	}
	int *ip = malloc(sizeof(int));
	
	*ip = (*op) - 1;
	free(op);
	
	return rec(ip);
	
	
}

int main() {
	int *qq = malloc(sizeof(int));
	*qq = __VERIFIER_nondet_int();
	
	while (*qq > 1) {
		int *pp = malloc(sizeof(int));
		*pp = __VERIFIER_nondet_int();
		
		if(*pp < 0) {
			return 0;
		} 
		
		*qq += (rec(pp) == -1 ? -1 : 1);   
	}
	
	free(qq);

}