--- layout: fc_discuss_archives title: Message 55 from Frama-C-discuss on December 2008 ---
Dear all, Congratulations for new frama-c release and thanks a lot for your support and improvement of the tool. The new Jessie manual is very cool J I installed the new release in windows, and I?m getting problems with it. For example, for this simple program: #pragma JessieIntegerModel(exact) //@ ensures *p >= 0; void abs1(int *p) { if (*p < 0) *p = -*p; } /*@ requires \valid(p); @ ensures *p >= 0 @ ; @*/ void abs2(int *p) { if (*p < 0) *p = -*p; } That I took from Frama-C distribution, running the command: frama-c ?jessie-analysis sample.c it gives the following output : Parsing [preprocessing] running gcc -C -E -I. -include C:\Frama-C\share\frama-c\jessie\jessie_prolog.h -dD little_sample.c Cleaning unused parts Symbolic link Starting semantical analysis Starting Jessie translation Producing Jessie files in subdir little_sample.jessie File little_sample.jessie/little_sample.jc written. File little_sample.jessie/little_sample.cloc written. Calling Jessie tool in subdir little_sample.jessie File "little_sample.jc", line 6, characters 18-19: syntax error Jessie subprocess failed: jessie -why-opt -split-user-conj -v -locs little_sample.cloc little_sample.jc This error is presented for every file. I tried examples that I had created to the beta release that are not working here. Is there something that I?m doing wrong ?! I also installed the new release in Linux (Ubuntu), and the same example worked very well. So I think that the problem is in Windows version. But I have another example with axiomatic definitions, that was working in the beta version, that is not working any more( in Linux and in Windows). For this axiomatic definition: /*@ axiomatic valid_range{ @ axiom valid_range_ax1a: @ \forall unsigned long k; k>=0 ==> 0<=(k >> 3L)<=k; @ } @*/ It presents the following output: Parsing [preprocessing] running gcc -C -E -I. -include /usr/local/share/frama-c/jessie/jessie_prolog.h -dD rc4_acsl_1.4.c Cleaning unused parts Symbolic link Starting semantical analysis Starting Jessie translation Producing Jessie files in subdir rc4_acsl_1.4.jessie File rc4_acsl_1.4.jessie/rc4_acsl_1.4.jc written. File rc4_acsl_1.4.jessie/rc4_acsl_1.4.cloc written. Calling Jessie tool in subdir rc4_acsl_1.4.jessie File "rc4_acsl_1.4.jc", line 370, characters 2-102: typing error: axiom valid_range_ax1a should contain at least one occurrence of a symbol declared in axiomatic valid_range Jessie subprocess failed: jessie -why-opt -split-user-conj -v -locs rc4_acsl_1.4.cloc rc4_acsl_1.4.jc How I can define now an axiom? Best regards, B?rbara -------------- next part -------------- An HTML attachment was scrubbed... URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20081217/ba067200/attachment.htm