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] relationship of separated and restrict qualifier

  • Subject: [Frama-c-discuss] relationship of separated and restrict qualifier
  • From: jens.gerlach at first.fraunhofer.de (Jens Gerlach)
  • Date: Sun, 13 Dec 2009 21:42:35 +0100
Hi,

the ACSL specification introduces (experimentally) the "\separated" annotation (?2.7.2).
I understand that it serves the purpose of expressing that different pointers point to different memory locations.
Is there a major difference between "\separated" and the "restrict" type qualifier of C99 
(see http://developers.sun.com/solaris/articles/cc_restrict.html)?

Regards Jens