2021-03-02 02:11 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001437Frama-CKernelpublic2013-06-19 10:18
Assigned Tosignoles 
Product VersionFrama-C Fluorine-20130501 
Target VersionFixed in VersionFrama-C Fluorine-20130601 
Summary0001437: Cannot use Frama_C_interval on Fluorine
DescriptionI tried following the instructions on the Fluorine manual to use Frama_C_interval():

frama -c -slevel 100 -val *.c `frama-c -print-share-path`/builtin.c >log 2 >&1

But the file "/usr/share/frama-c/builtin.c" cannot be found. I looked at the ZIP archive and could not find it on the /share folder, nor on any folder for that matter, the closest file is "libc/__fc_builtin.h". However, both builtin.c and builtin.h are present on the Oxygen ZIP archive, and I have successfully used Frama_C_interval with that version.

Has anything changed from Oxygen to Fluorine concerning this?

I tried just declaring the prototype and using it, but the value analysis does not output the expected result, for instance on this program:

int Frama_C_interval(int,int);
int main() {
  int i = Frama_C_interval(0, 20);
  return 0;

$ frama-c -val test.c

(... omitted ...)
[kernel] warning: Neither code nor specification for function Frama_C_interval, generating default assigns from the prototype
[value] using specification for function Frama_C_interval
[value] Done for function Frama_C_interval
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
[value] Values at end of function main:
          i ? [--..--]
          __retres ? {0}
TagsNo tags attached.
Attached Files




signoles (manager)

Thanks for this report. We are already aware of this issue. A fix will be released quickly.

As a workaround, you can use the files builtin.[ch] from Oxygen.


signoles (manager)

Fixed in Fluorine-20130601, aka Fluorine 3.

-Issue History
Date Modified Username Field Change
2013-05-31 12:44 dhekir New Issue
2013-05-31 13:00 signoles Status new => assigned
2013-05-31 13:00 signoles Assigned To => yakobowski
2013-05-31 13:02 signoles Note Added: 0003933
2013-05-31 13:03 signoles Status assigned => confirmed
2013-06-15 18:48 yakobowski Status confirmed => assigned
2013-06-15 18:48 yakobowski Assigned To yakobowski => signoles
2013-06-16 20:02 signoles Status assigned => confirmed
2013-06-19 10:18 signoles Note Added: 0003970
2013-06-19 10:18 signoles Status confirmed => closed
2013-06-19 10:18 signoles Resolution open => fixed
2013-06-19 10:18 signoles Fixed in Version => Frama-C Fluorine-20130601
+Issue History