Allocating and Deallocating Memory

Our next topic is programs that use dynamically allocated heap memory.

Malloc and Free

Heap-using programs in CN can be written in almost exactly the same way as in vanilla C. The only difference is that, instead of calling malloc and free, programs should call cn_malloc and cn_free_sized. These are CN-specific versions of the usual malloc and free that do some testing-related bookkeeping in addition to their main job of allocating or deallocating heap memory. The second argument to cn_free_sized is the size of the structure being freed, same as the argument to cn_malloc.

exercises/cn_malloc.h

#include <stddef.h>

extern void* cn_malloc(size_t size);
extern void  cn_free_sized(void *ptr, size_t size);

Using cn_malloc and cn_free_sized, we can write higher-level programs that manipulate the heap, as usual.

exercises/slf17_get_and_free.test.c

#include "cn_malloc.h"

unsigned int *malloc_and_set (unsigned int x)
/*@ ensures take P = RW<unsigned int>(return);
            P == x;
@*/
{
  unsigned int *p = cn_malloc(sizeof(unsigned int));
  *p = x;
  return p;
}

unsigned int get_and_free (unsigned int *p)
/*@ requires take P = RW<unsigned int>(p);
    ensures return == P;
@*/
{
  unsigned int v = *p;
  cn_free_sized(p, sizeof(unsigned int));
  return v;
}

unsigned int tester()
/*@ requires true;
    ensures return == 42u32;
@*/
{
  unsigned int *p = malloc_and_set(42);
  unsigned int v = get_and_free(p);
  return v;
}

Exercises

Exercise: Write a specification for the following program that returns a pointer to a number that is the number pointed to by its argument + 1.

exercises/slf_greater.test.c

#include "cn_malloc.h"

unsigned int *incr (unsigned int *p)
{
  unsigned int* q = cn_malloc(sizeof(unsigned int));
  *q = *p + 1;
  return q;
}