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

  • Subject: [Frama-c-discuss] Jessie : \initialized predicate
  • From: elarif.moha at gmail.com (Elarif Mohamed)
  • Date: Mon, 2 Jul 2018 17:04:25 +0200
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>