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] Jessie : \initialized predicate


Le 02/07/2018 à 17:33, Andre Maroneze a écrit :
> 1. Manually remove all annotations containing the \initialized predicate;
> Solution 1 is a short-term solution that should not have negative 
> side-effects, except for plug-ins such as Eva, which use these annotations.

Yes, or simply do not use the header file proposed by Frama-C and write 
your own version, so that you can think carefully about what 
requirement/specifications you want to rely on concerning functions in 
time.h

>> I know, the message is quite explicit, but isn't there really any way 
>> to use Jessie with a real time program ? ( using the #include 
>> <sys/time.h> ) 

Yes you can! same answer: it is only a matter of understanding the 
requirements/specifications you want to rely on about time functions. 
"only a matter of ... " but it is probably the most important question 
you should ask yourself first: what do you want to prove on your code?

Hope this helps,

- Claude