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] Strange behaviour of Yices

Hi,

This is a bug we know about, in the jessie tool itself which comes with 
the Why platform. This is corrected in the current version hence should 
not come up anymore in the next release.

For the moment, I suggest just to ignore Yices answers, and sorry for 
the inconvenience.

- Claude

jean-baptiste.jeannin@hispano-suiza-sa.com wrote:
> Hi all,
> 
> I have question on a very strange behaviour I just got using Frama-C. I 
> think the problem is probably more with Yices than with Frama-C, but maybe 
> you will have a hint. I typed a file (say file.c) containing only the two 
> following lines:
> 
> /*@ lemma aaa: \forall int i; i<0 && i>0 && i==0;
>   @*/
> 
> Of course I don't expect the lemma to be proven, but if I compile the file 
> with:
> $ frama-c -jessie-analysis -jessie-gui file.c
> and then try to prove the lemma, all the automatic provers fail, except 
> Yices which succeeds. It seems pretty strange to me; do you have an idea 
> of what's happening?
> I am using Frama-C Helium-20080701 with Yices 1.0.13.
> 
> Thanks,
> Jean-Baptiste Jeannin
> #
> " This e-mail and any attached documents may contain confidential or proprietary information. If you are not the intended recipient, please advise the sender immediately and delete this e-mail and all attached documents from your computer system. Any unauthorised disclosure, distribution or copying hereof is prohibited."
> 
>  " Ce courriel et les documents qui y sont attaches peuvent contenir des informations confidentielles. Si vous n'etes  pas le destinataire escompte, merci d'en informer l'expediteur immediatement et de detruire ce courriel  ainsi que tous les documents attaches de votre systeme informatique. Toute divulgation, distribution ou copie du present courriel et des documents attaches sans autorisation prealable de son emetteur est interdite."
> #
> 
> 
> 
> ------------------------------------------------------------------------
> 
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss@lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss

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