Spinroot

A forum for Spin users

You are not logged in.

#1 2014-03-16 21:08:29

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

Offline

#2 2014-03-17 01:29:49

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

Offline

#3 2014-03-18 06:46:43

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?

Offline

#4 2014-03-18 16:54:14

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)"

Offline

Board footer

Powered by FluxBB