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] 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