--- layout: fc_discuss_archives title: Message 1 from Frama-C-discuss on July 2018 ---
Hi, I know this must have already been asked, but i can't find the thread. Here's my problem : I'm trying to process an annoted c source file, dealing with real time functions, and the sys/time.h header. Jessie, when called, use frama-c's own annoted time.h header, which contains a \initialized predicate, unsupported by Jessie. And then the translation from annoted C to .jc results with an error : -$ frama-c -cpp-extra-args="-DPOSIX -D_POSIX_SOURCE -D_GNU_SOURCE -Wall -W" -jessie -jessie-gen-only my_time.c FRAMAC_SHARE/libc/time.h:92:[jessie] failure: \initialized operator [jessie] user error: Unsupported feature(s). Jessie plugin can not be used on your code. 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> ) Maybe using older versions of Frama-C ? My Why/Why3/Frama-C suite tools works perfectly on other annoted source files (without real time), but here's my versions : Why 2.40 Why3 0.88.3 Frama-C Sulfur-20171101 Sorry if the answer is obvious, but i'm quite new to Frama-C and Jessie, and would appreciate any help ! Best regards, Elarif MOHAMED. -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20180702/a8f8b847/attachment.html>