Cannot use Frama_C_interval on Fluorine

ID0001437: This issue was created automatically from Mantis Issue 1437. Further discussion may take place here.

---

Id	Project	Category	View	Due Date	Updated
ID0001437	Frama-C	Kernel	public	2013-05-31	2013-06-19

Reporter	dhekir	Assigned To	signoles	Resolution	fixed
Priority	normal	Severity	major	Reproducibility	always
Platform	-	OS	-	OS Version	-
Product Version	Frama-C Fluorine-20130501	Target Version	-	Fixed in Version	Frama-C Fluorine-20130601

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}