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