--- layout: fc_discuss_archives title: Message 40 from Frama-C-discuss on January 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] low-level pointer manipulation question



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>