static void test_non_empty_stack_peek_shows_correct_value(void) {
  Stack *stack = create_stack(3);
  push(stack, 8);
  int value = peek(stack);

  assert (8 == value && "peeked value should be 8");
  free(stack);
}

static void test_empty_stack_peek(void) {
  Stack *stack = create_stack();

  // Note: You can't tell if a stack is empty by simply peeking, you also have
  // to call "is_empty"
  assert (0 == peek(stack) && "peek at empty stack should show 0");
  destroy_stack(stack);
}

static void test_pop_from_empty_stack_fails(void) {
  Stack *stack = create_stack(3);
  BOOL success;
  pop(stack, &success);

  assert (FALSE == success && "pop should fail");
  free(stack);
}

static void test_push_onto_non_empty_stack_size_is_correct(void) {
  Stack *stack = create_stack();
  push(stack, 5);
  push(stack, 4);

  assert (2 == size(stack) && "stack size after pushes should be 2");
  destroy_stack(stack);
}

void test3() 
//@ requires true;
//@ ensures true;
{
    struct value* v2, v3;
    struct stack* s = create_stack();
    //@ close foreach(nil, value_helper2(27));
    //@ close stack_allClients3(s, nil, 27);
    //@ close stack_unsep(stack_inv3_unsep)(boxed_int(27), s, stack_inv3(s, 27), stack_inv3_sep, nil);
    //@ produce_lemma_function_pointer_chunk(stack_inv3_sep);
    //@ produce_lemma_function_pointer_chunk(stack_inv3_unsep);    
    //@ share_stack(s);
        
    struct value* v = malloc(sizeof(struct value));
    if(v == 0) abort();
    v->val = 27;
    
    //@ close stack_push_context_pre(allClients3_push)(stack_inv3_unsep, s, v, boxed_int(27));
    //@ produce_lemma_function_pointer_chunk(allClients3_push);
    stack_push(s, v);
    //@ leak is_stack_push_context(allClients3_push);
    //@ open stack_push_context_post(allClients3_push)(boxed_int(27));
    
    //@ close stack_try_pop_context_pre(allClients3_try_pop)(stack_inv3_unsep, s, boxed_int(27));
    //@ produce_lemma_function_pointer_chunk(allClients3_try_pop);
    bool result = stack_try_pop(s, &v2);
    //@ leak is_stack_try_pop_context(allClients3_try_pop);
    //@ open stack_try_pop_context_post(allClients3_try_pop)(_, _, boxed_int(27));
    if(result) { 
        //@ open value(v2, 27);
        free(v2); 
    }

    //@ unshare_stack(s);
    //@ open stack_unsep(stack_inv3_unsep)(boxed_int(27), s, stack_inv3(s, 27), stack_inv3_sep, _);
    //@ leak is_stack_sep(stack_inv3_sep);
    //@ leak is_stack_unsep(stack_inv3_unsep);
    
    
    bool hasMore = true;
    while(hasMore)
    //@ invariant stack(s, ?remElems) &*& stack_allClients3(s, remElems, 27) &*& pointer(&v3, _) &*& (hasMore ? true: remElems == nil);
    {
        hasMore = stack_try_pop_sequential(s, &v3);
        if(hasMore) {
            //@ open stack_allClients3(s, remElems, 27);
            //@ open foreach(remElems, value_helper2(27));
            //@ close stack_allClients3(s, tail(remElems), 27);
            //@ open value_helper2(27)(v3);
            //@ open value(v3, 27);
            free((struct value*)v3); 
        }
    }
    
    //@ open stack_allClients3(s, remElems, 27);
    //@ open foreach(remElems, value_helper2(27));
    dispose_stack(s);
}

static void test_pop_from_empty_stack_size_is_zero(void) {
  Stack *stack = create_stack();
  Node *node = NULL;
  pop(stack, &node);

  assert (0 == size(stack) && "stack size should be 0");
  free(node);
  destroy_stack(stack);
}

static void test_pop_from_non_empty_stack_returns_correct_value(void) {
  Stack *stack = create_stack(3);
  push(stack, 8);
  BOOL success;
  int value = pop(stack, &success);

  assert (8 == value && "popped value should be 8");
  free(stack);
}

static void test_pop_from_stack_with_one_element_sets_head_to_negative(void) {
  Stack *stack = create_stack(3);
  push(stack, 8);
  BOOL success;
  pop(stack, &success);

  assert (0 > stack->head && "pop should set head to negative");
  free(stack);
}

static void test_pop_from_non_empty_stack_succeeds(void) {
  Stack *stack = create_stack(3);
  push(stack, 8);
  BOOL success;
  pop(stack, &success);

  assert (TRUE == success && "pop should succeed");
  free(stack);
}

void push(int val, Stack *s)
{
	Stack new_s = create_stack(val);	
	
	if(s != NULL)
		new_s->next = *s;
	
	*s = new_s;
}

static void test_pop_from_empty_stack_node_is_null(void) {
  Stack *stack = create_stack();
  Node *node = NULL;
  pop(stack, &node);

  assert (NULL == node && "popped node should be NULL");
  free(node);
  destroy_stack(stack);
}

void
rust_task::new_stack(size_t requested_sz) {
    LOG(this, mem, "creating new stack for task %" PRIxPTR, this);
    if (stk) {
        ::check_stack_canary(stk);
    }

    // The minimum stack size, in bytes, of a Rust stack, excluding red zone
    size_t min_sz = thread->min_stack_size;

    // Try to reuse an existing stack segment
    while (stk != NULL && stk->next != NULL) {
        size_t next_sz = user_stack_size(stk->next);
        if (min_sz <= next_sz && requested_sz <= next_sz) {
            LOG(this, mem, "reusing existing stack");
            stk = stk->next;
            return;
        } else {
            LOG(this, mem, "existing stack is not big enough");
            stk_seg *new_next = stk->next->next;
            free_stack(stk->next);
            stk->next = new_next;
            if (new_next) {
                new_next->prev = stk;
            }
        }
    }

    // The size of the current stack segment, excluding red zone
    size_t current_sz = 0;
    if (stk != NULL) {
        current_sz = user_stack_size(stk);
    }
    // The calculated size of the new stack, excluding red zone
    size_t rust_stk_sz = get_next_stack_size(min_sz,
                                             current_sz, requested_sz);

    if (total_stack_sz + rust_stk_sz > thread->env->max_stack_size) {
        LOG_ERR(this, task, "task %" PRIxPTR " ran out of stack", this);
        fail();
    }

    size_t sz = rust_stk_sz + RED_ZONE_SIZE;
    stk_seg *new_stk = create_stack(&local_region, sz);
    LOGPTR(thread, "new stk", (uintptr_t)new_stk);
    new_stk->task = this;
    new_stk->next = NULL;
    new_stk->prev = stk;
    if (stk) {
        stk->next = new_stk;
    }
    LOGPTR(thread, "stk end", new_stk->end);

    stk = new_stk;
    total_stack_sz += user_stack_size(new_stk);
}

static void test_push_onto_full_stack_fails(void) {
  Stack *stack = create_stack(3);
  push(stack, 8);
  push(stack, 7);
  push(stack, 6);
  BOOL pushed = push(stack, 5);

  assert (FALSE == pushed && "push should fail");
  free(stack);
}

static void test_pop_from_stack_with_one_node_value_is_correct(void) {
  Stack *stack = create_stack();
  push(stack, 5);
  Node *node = NULL;
  pop(stack, &node);

  assert (5 == node->value && "popped value should be 5");
  free(node);
  destroy_stack(stack);
}

static void test_pop_from_stack_with_one_node_size_is_correct(void) {
  Stack *stack = create_stack();
  push(stack, 5);
  Node *node = NULL;
  pop(stack, &node);

  assert (0 == size(stack) && "stack size after pop should be 0");
  free(node);
  destroy_stack(stack);
}

static void test_stack_peek_after_pop(void) {
  Stack *stack = create_stack();
  push(stack, 4);
  push(stack, 5);
  Node *node;
  pop(stack, &node);

  assert (4 == peek(stack) && "peek at stack should show 4");
  free(node);
  destroy_stack(stack);
}

static void test_pop_from_non_empty_stack_value_is_correct(void) {
  Stack *stack = create_stack();
  push(stack, 5);
  push(stack, 4);
  Node *node = NULL;
  pop(stack, &node);

  assert (4 == node->value && "popped value should be 4");
  free(node);
  destroy_stack(stack);
}

void assert_each() {
  int data[] = {456, 370, 316};
  Stack *stack = create_stack();
  stack_push(stack, 316);
  stack_push(stack, 370);
  stack_push(stack, 456);

  int test(Element e, int i) {
    assert(e == data[i]);
    return 0;
  }

t_stack	*push(t_stack *top, char *c)
{
	t_stack	*elem;

	elem = NULL;
	elem = create_stack(c);
	if (elem && top)
	{
		elem->next = top;
	}
	return (elem);
}

int main()
    //@ requires true;
    //@ ensures true;
{
    struct stack *s = create_stack();
    stack_push(s, 10);
    stack_push(s, 20);
    stack_pop(s);
    stack_pop(s);
    stack_dispose(s);
    return 0;
}