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] low-level pointer manipulation question

  • Subject: [Frama-c-discuss] low-level pointer manipulation question
  • From: pascal.cuoq at gmail.com (Pascal Cuoq)
  • Date: Sat, 21 Jan 2012 17:01:29 +0100
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>