--- layout: fc_discuss_archives title: Message 38 from Frama-C-discuss on May 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Uncaught exception



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                    |