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] Re: questions about FRAMA-C

  • Subject: [Frama-c-discuss] Re: questions about FRAMA-C
  • From: yannick.moy at gmail.com (Yannick Moy)
  • Date: Fri Oct 31 14:51:35 2008
  • In-reply-to: <31561357.1225295872424.JavaMail.www@wwumf0102>
  • References: <31561357.1225295872424.JavaMail.www@wwumf0102>
Hi,

I tried the last version released (Lithium) on your struct example, it works
properly and all VC are proved with any of Alt-Ergo, Simplify or Z3 prover
(but not Yices).

On your enum examples, I got an error in function p1:

Error: Casting from type int  to type struct enum___anonenum_RESULTAT_1_P *
not allowed

This is because you assign [last] instead of [*last].
Then, for the case without function, I had to rewrite function
[function2_res] to add an obvious cast to [RESULTAT]

/*@ predicate function2_res{L}(int n) =
  @  result((RESULTAT)OK,n);
  @*/

This is a bug (no cast should be needed here), for which I have filled bug
6622 in the public BTS of Frama-C.
Except that, some VC are not proved because not provable.

On your last enum example with function, the verification proceeds
adequately. Of course, some VC are not proved because not provable.

HTH,

-- 
Yannick
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20081031/94052e85/attachment.htm