0001437: Cannot use Frama_C_interval on Fluorine

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

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 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}

Tags

No tags attached.

Attached Files

Relationships

Notes
(0003933) signoles (manager) 2013-05-31 13:02	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.

(0003970) signoles (manager) 2013-06-19 10:18	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