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] Frama-c failing in proving successive simple goals

Hi

You're missing some requires clauses to guarantee that the memory areas
pointed by satmin, satmax and error are valid and separated from each
other, ie: the memory areas do not overlap.

Adding this to the function's contract works for me:

  requires \valid(satmin);
  requires \valid(satmax);
  requires \valid(error);
  requires \separated(satmin, satmax, error);

Proved with Fluorine 2, WP and Alt-ergo 0.95.1


2013/7/11 Tailliar Alice <alice.tailliar at etu.enseeiht.fr>

> Hello,
>
> I contact you because I can't manage to prove all the ensures clauses of
> the function in the attached file.
>
> What is happening is that I can only prove the ensures clauses about the
> last affection, even if I change the order of the three instructions. When
> I try to prove the others ensures clauses by WP, alt-Ergo fails and detects
> a syntax error in a file generated by frama-c.
>
> So I would like to know if there is a problem in my function that prevents
> frama-c from doing its job and how I can fix it, or if the problem comes
> from frama-c.
>
> Thank you for yours answers,
> Best regards
>
> Alice Tailliar
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
>



-- 
Cumprimentos,
Cristiano Sousa
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130711/8d0f282c/attachment.html>