--- layout: fc_discuss_archives title: Message 37 from Frama-C-discuss on May 2014 ---
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