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

[Frama-c-discuss] Jessie - behavior-specific loop invariants



Hello Kerstin,

Le lun. 08 nov. 2010 13:59:08 CET,
"Kerstin Hartig" <kerstin.hartig at first.fraunhofer.de> a ?crit :

> As we usually divide spec. and impl. I experienced the following problem:
> Including the specification file to the implementation file results in some
> unknown behavior error.
> 
> Is this a bug? Or is there something I overlooked?
> 

This is a bug. In fact, it is fixed in the current development version
and Frama-C Carbon will behave as you expect.

Best regards,
-- 
E tutto per oggi, a la prossima volta.
Virgile