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] Code proved with Fluorine is more proved with Neon

Lo?c Correnson <loic.correnson at cea.fr> writes:

> This code is quite cryptic at a first sight, and I personally don?t
> have time to look at it deeply.

We are trying to prove an existing code and we want to modify this code
a minima. The extracted code corresponds to a compilation unit dealing
with time represented by a struct in which seconds and nanoseconds are
separated in two fields and the extracted function is just an addition
of two such structures (with of course two behaviors depending on the
nanosecond field).

> As a recommandation, may I suggest you to insert intermediate
> assertions in the code to find where the proof does not work?  Start
> by copying the ensures into assertions at the end of each branch, then
> try to infer some intermediate results.

I have begun this work, I hope I can solve this problem rapidly.

Thanks,

Christophe

-- 
Christophe Garion          ISAE/DMIA - SUPAERO/IN
garion at isae.fr             10 avenue Edouard Belin
T?l : (33)5 61 33 80 57    BP 54032
Fax : (33)5 61 33 83 45    31055 Toulouse Cedex 4