--- layout: fc_discuss_archives title: Message 38 from Frama-C-discuss on May 2010 ---
Tom Hawkins wrote: > On Fri, May 7, 2010 at 9:12 AM, Pascal Cuoq <pascal.cuoq at gmail.com> wrote: > >> Either you did not pay attention to this warning, or you typed "frama-c t.c". >> > > Thanks. I didn't notice this warning. I guess I would have expected > the tool to reject contracts that are in obvious conflict. > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss > Please do not hesitate to fill in a bug report, or feature wish. Initially, you wanted to hide some local side effect from the "public" contract of your function. This is a need I completely understand. Unfortunately checking this is a very difficult theoretical question, because of all the potential sharing/aliasing of data structures. ACSL does not offer such a feature in its current state. - Claude -- Claude March? | tel: +33 1 72 92 59 69 INRIA Saclay - ?le-de-France | mobile: +33 6 33 14 57 93 Parc Orsay Universit? | fax: +33 1 74 85 42 29 4, rue Jacques Monod - B?timent N | http://www.lri.fr/~marche/ F-91893 ORSAY Cedex |