Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] how to deal with malloc in frama-c (boron)

Hello,

On Wed, Jul 28, 2010 at 4:57 PM, Nicolas Magaud <magaud at unistra.fr> wrote:
> We try to use frama-c to prove simple properties about linked-lists.

While technically true, a more useful statement is that you use Jessie.
And while we are on the subject of petty remarks, if you include
system headers from your computer in your examples, the results may
not be reproducible on another computer, and you mean "ens
my_malloc(void) {" to say that it expects zero arguments, instead of
"()" which means that the programmer can apply my_malloc any way
he/she pleases.

You are tackling a very difficult problem.

I do not think you can write

/*@ assigns \nothing;
   ...
  @*/
ens my_malloc(void){

because that would imply that two consecutive calls to my_malloc
return the same thing.

> Intuitively, executing malloc should not modify what is already defined in the memory.

You could try with a "transparent" specification of your my_malloc
function, i.e., choose a naive implementation of my_malloc (taking ens
cells from a large pre-defined array) and using a specification that
hides nothing from this implementation (showing that the index in the
array that malloc returns is incrementing). Then the information would
be available that each cell returned by a different call to my_malloc
is separate from the others. I do not think this will take you very
far, however?

> In addition, we try and look at the examples available in
> the directory examples-c, especially puf/ but we did not
> figure out how to compile these examples.

The files in puf/ are Caduceus examples, not Jessie examples. Oh, and
they also specify allocation functions with assigns \nothing. So if my
colleagues have an explanation of why it's not wrong to use that
clause in ACSL for a function that obviously has internal
side-effects, I would be eager to hear it.

I would also welcome an explanation of what "\forall ref *p;" means in
ACSL and if it is still allowed (in ACSL) to use it in the same way it
is used in puf/parray.c.

Pascal