--- layout: fc_discuss_archives title: Message 9 from Frama-C-discuss on July 2018 ---
[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