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)

  • Subject: [Frama-c-discuss] how to deal with malloc in frama-c (boron)
  • From: magaud at unistra.fr (Nicolas Magaud)
  • Date: Wed, 28 Jul 2010 16:57:01 +0200
Hello,

We try to use frama-c to prove simple properties about linked-lists. We use Alt-Ergo as the automated theorem prover to solve the proof obligations. However we have some issues with the system. One of our experiments can be seen in the attached file malloc.c .

We use the C function "malloc" to allocate memory when inserting new elements in the list. Because the memory changes when malloc is performed, it seems that basic information including the fact "c", which is equal to "l->next" verifies the "br_valid" condition disappears.

To avoid this inconvenience, we choose to define an alternate function 'my_malloc' which is a function we do not prove but instead simply specify using pre- and post-conditions. We assume that every list which verifies the "br_valid" property before the call to the malloc function still verifies this property.

Especially, we do not know how to maintain the connection between in modified objects in "alloc_table" and  "alloc_table0".
Intuitively, executing malloc should not modify what is already defined in the memory. So the properties of the objects known in "alloc_table" should be propagated into "alloc_table0", right ?

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. It leads to various syntax errors with jessie, frama-c, why and caduceus. Maybe a good idea would be to include the command line to compile at the beginning of the C file.We also noted a new keyword \fresh which seems to express that a pointer is a new one (no aliases), but it seems not to be implemented yet. Can you confirm that ?

Any hints on how to proceed would be greatly appreciated,
Thanks in advance,

Nicolas Magaud


-------------- next part --------------
A non-text attachment was scrubbed...
Name: malloc.c
Type: application/octet-stream
Size: 1164 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20100728/d4471d57/attachment.obj>