--- layout: fc_discuss_archives title: Message 55 from Frama-C-discuss on July 2010 ---
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