Frama-C Bug Tracking System - Frama-C | |||||
| View Issue Details | |||||
| ID | Project | Category | View Status | Date Submitted | Last Update |
| 0001437 | Frama-C | Kernel | public | 2013-05-31 12:44 | 2013-06-19 10:18 |
| Reporter | dhekir | ||||
| Assigned To | signoles | ||||
| Priority | normal | Severity | major | Reproducibility | always |
| Status | closed | Resolution | fixed | ||
| Platform | OS | OS Version | |||
| Product Version | Frama-C Fluorine-20130501 | ||||
| Target Version | Fixed in Version | Frama-C Fluorine-20130601 | |||
| Summary | 0001437: Cannot use Frama_C_interval on Fluorine | ||||
| Description | I 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} | ||||
| Steps To Reproduce | |||||
| Additional Information | |||||
| Tags | No tags attached. | ||||
| Relationships | |||||
| Attached Files | |||||
| 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 | ||
| Notes | |||||
|
|
|||||
|
|
||||
|
|
|||||
|
|
||||