--- layout: fc_discuss_archives title: Message 40 from Frama-C-discuss on January 2012 ---
Dear list, you will find below a question from John Regehr about the verification of low-level pointer manipulations where the unused bits of the pointer's representation are borrowed by the program to store additional information. For the value analysis, I see no difficulty in having ad-hoc rules for this kind of operation, so that, if a is a variable with alignment 8 bytes (such as a pointer on a LP64 architecture), when p ? {{ &a + [0..7] }} , the expression (long)p & ~7 evaluates to {{ &a }}. In fact, I think I am going to implement this right now. John is asking about Frama-C in general (I think, and if anything, his question may be *only* about deductive verification plug-ins). So anyone familiar with deductive verification, please feel free to opine. Pascal ---------- Forwarded message ---------- From: John Regehr <regehr at cs.utah.edu> Date: Thu, Jan 12, 2012 at 4:22 AM Subject: frama-c question To: Pascal Cuoq <pascal.cuoq at gmail.com> Below is a stupid problem that's part of a C language review assignment that I gave my operating systems class today. Can Frama-C verify it? The entire assignment is easy, but I bet not very fun to verify :) http://www.eng.utah.edu/~**cs5460/hw1/hw1.c<http://www.eng.utah.edu/~cs5460/hw1/hw1.c> John /************************************************************************* * * list_remove() * * specification: * * the argument to list_remove is a modified pointer that stores * non-pointer data in its 3 low-order bits * * of course, for this to work, the original pointer must have been * aligned on an 8-byte boundary (ensuring that this property holds is * not your problem) * * list_remove's argument (after zeroing the 3 low-order bits) points * to the head element of a linked list; the three low-order bits * identify which element of the linked list should be deleted; if that * element is deleted successfully, list_remove() returns 1, otherwise * it returns 0 * * extra requirement 1: make sure there are no memory leaks * * NOTE 1: the argument to list_remove() -- after its low-order bits * are cleared -- is guaranteed to not be the null pointer; in other * words, the argument *must* point to a valid linked list and you * do not need to worry about the case where this does not hold * * NOTE 2: the linked list pointed to by the argument may be a null * pointer, indicating that the list is empty; in this case, of * course, list_remove() must return 0 * * EXAMPLE: assume the head of a linked list lives at 0x7fffffffdb38 * and we wish to remove element number 3 (counting from zero); in * this case we would call: * * list_remove (0x7fffffffdb3b); * * if this linked list contains 0, 1, or 2 elements, list_remove() * will return 0 and have no effect; if the list contains 4 or more * elements, element number 3 (the fourth element in the list) will be * removed and the function will return 1 * *************************************************************************/ int list_remove (struct elt **e) { ... } -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20120121/0e95c71f/attachment.htm>