--- layout: fc_discuss_archives title: Message 24 from Frama-C-discuss on March 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] embedded loops



Hello,

Le lun. 07 mars 2011 20:16:51 CET,
Romain Jobredeaux <Romain.Jobredeaux at supelec.fr> a ?crit :

> The annotations are also very similar, however for some reason  
> alt-ergo proves every obligation on or_scalar, but doesn't even seem  
> to try to prove the outer loop invariant on equal_scalar...
> 

Which versions of Frama-C and alt-ergo are you using? Carbon beta 2 and
alt-ergo 0.92.2 do not seem to have any issue with either function.

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