Spinroot

maryam

Member

Registered: 2012-03-27

Posts: 16

Dynamic allocation using embedded C code

Is dynamic allocation allowed in embedded c code?

I have used realloc() (for an array with dynamic length) in my model, but there is a "core dumped" error. If I change the code as the array's length is static, everything works fine.

I know that when the lenght of array is one, realloc() free it. But then it points to a place of memory which is not initialized, and I don't know how it is created!!!

Is there a way to debug the code to locate exactly the line that results in error?

Thanks a lot,
Maryam

spinroot

forum

Registered: 2010-11-18

Posts: 691

Website

Re: Dynamic allocation using embedded C code

you can do so, but you'll have to write your own malloc routine and
c_track the heap you're using....
the library malloc will not work (or realloc) since the heap memory isn't
seen by the model checker

maryam

Member

Registered: 2012-03-27

Posts: 16

Re: Dynamic allocation using embedded C code

Thank you very much for the reply.

With my own realloc() routine:

1. As the array is a NULL pointer at first, second argument of c_track is zero indeed. Then, since c_track is a global primitive, I cannot understand how can I track the array whenever I change its size (in a d_step block)?

2. Does SPIN have an automatic garbage collection?

spinroot

forum

Registered: 2010-11-18

Posts: 691

Website

Re: Dynamic allocation using embedded C code

I'd recommend doing something like this.
(I didn't check this for syntax errors etc -- but you'll get the idea.)

In the C code:

char heap[HEAPSIZE];
int heap_ptr = 0;

char *mymalloc(int n)
{    int o_ptr = heap_ptr;

   if (n >= HEAPSIZE - heap_ptr) {
         Uerror("out of memory on heap");
   }
   heap_ptr += n;
   return &heap[o_ptr];
}

and in the model:

c_decl { extern char heap[HEAPSIZE]; extern int heap_ptr; }

c_track "heap" "sizeof(heap)"