Frama-C Bug Tracking System - Frama-C
View Issue Details
0002261Frama-CPlug-in > wppublic2016-12-14 11:572016-12-16 10:19
vlad 
virgile 
normalminoralways
assignedopen 
WindowsWindows 7
Frama-C 14-Silicon 
 
0002261: wp: the example from Getting Started guide doesn't work (all goals are Unknown)
I'm trying to reproduce ASCL example from frama-c manual. For some reason all goals sent to alt-ergo end up with unknown result. Code: $ cat frama-c-test.c /*@ requires \valid(a) && \valid(b); @ ensures A: *a == \old(*b); @ ensures B: *b == \old(*a); @ assigns *a,*b; @*/ void swap(int * a, int * b); void swap(int *a,int *b) { int tmp = *a ; *a = *b ; *b = tmp ; return ; } Frama-C result: $ frama-c -wp -wp-rte frama-c-test.c [kernel] Parsing .opam/4.02.3+mingw32c/share/frama-c/libc/__fc_builtin_for_normalization.i (no preprocessing) [kernel] Parsing frama-c-test.c (with preprocessing) [wp] Running WP plugin... [rte] annotating function swap [wp] 4 goals scheduled [wp] [Alt-Ergo] Goal typed_swap_assert_rte_mem_access_4 : Unknown (65ms) [wp] [Alt-Ergo] Goal typed_swap_assert_rte_mem_access_3 : Unknown (64ms) [wp] [Alt-Ergo] Goal typed_swap_assert_rte_mem_access_2 : Unknown (61ms) [wp] [Alt-Ergo] Goal typed_swap_assert_rte_mem_access : Unknown (60ms) [wp] Proved goals: 0 / 4 Alt-Ergo: 0 (unknown: 4) The exact same code works with Frama-C Aluminum on Linux. I'm running Frama-C on Windows 7 (with cygwin).
$ alt-ergo -version 1.30 $ frama-c --version Silicon-20161101
No tags attached.
Issue History
2016-12-14 11:57vladNew Issue
2016-12-14 11:57vladStatusnew => assigned
2016-12-14 11:57vladAssigned To => correnson
2016-12-14 16:26virgileNote Added: 0006313
2016-12-14 16:26virgileAssigned Tocorrenson => virgile
2016-12-14 16:26virgileStatusassigned => feedback
2016-12-15 07:43vladNote Added: 0006314
2016-12-15 07:43vladStatusfeedback => assigned
2016-12-15 08:01vladNote Edited: 0006314View Revisions
2016-12-15 08:10virgileNote Added: 0006315
2016-12-15 08:24vladNote Added: 0006316
2016-12-15 09:05virgileNote Added: 0006317
2016-12-15 09:16vladNote Added: 0006318
2016-12-15 09:18vladNote Edited: 0006318View Revisions
2016-12-16 08:36virgileNote Added: 0006319
2016-12-16 10:19vladNote Added: 0006322

Notes
(0006313)
virgile   
2016-12-14 16:26   
What is the result of frama-c frama-c-test.c -print? I somehow suspect that the function contract is ignored. Indeed, the output you give mentions only the 4 assert generated by RTE, but not the goals coming from ensures and assigns: there should be 9 goals in total (4 RTE assertions, 2 post-conditions and 3 assigns) with WP's default options
(0006314)
vlad   
2016-12-15 07:43   
(edited on: 2016-12-15 08:01)
$ frama-c frama-c-test.c -print [kernel] Parsing .opam/4.02.3+mingw32c/share/frama-c/libc/__fc_builtin_for_normalization.i (no preprocessing) [kernel] Parsing frama-c-test.c (with preprocessing) /* Generated by Frama-C */ void swap(int *a, int *b); void swap(int *a, int *b) { int tmp; tmp = *a; *a = *b; *b = tmp; return; }
(0006315)
virgile   
2016-12-15 08:10   
Thanks for confirming my thoughts. Does the issue still appear if you rename frama-c-test.c as frama-c-test.i? .i indicates a file that has already been pre-processed, and a possible cause of your symptoms could be that the pre-processor that is used by your installation of Frama-C Silicon does not preserve comments (on the contrary to Aluminium). If everything is fine with the .i file, frama-c -kernel-msg-key pp frama-c-test.c will output the preprocessing command that is used by Frama-C. In particular, it should include an option to preserve comments in the preprocessor output (-C for gcc).
(0006316)
vlad   
2016-12-15 08:24   
Renaming file to frama-c-test.i helps. Preprocessing command: [kernel:pp] preprocessing with "i686-w64-mingw32-cpp.exe -D__FRAMAC__ -D__FC_MACHDEP_X86_32 -IC:/Software/cygwin/home/Vlad/.opam/4.02.3+mingw32c/share/frama-c/libc frama-c-test.c" There is no option to keep comments.
(0006317)
virgile   
2016-12-15 09:05   
Thanks for this information. Do you happen to have CPP environment variable set? Otherwise, this looks like an issue in the way the preprocessor is detected at configure time, which indeed changed between Aluminium and Silicon. We'll try to reproduce that on a system similar to yours. In the mean time, a workaround would be to systematically add -cpp-extra-args="-C" to the Frama-C command line
(0006318)
vlad   
2016-12-15 09:16   
(edited on: 2016-12-15 09:18)
Thank you, this seems to be a solution. I do have $CPP set after `opam config env`. I tried unsetting it and "-C" flag appeared in preprocessor arguments. Adding -C as extra flag (-cpp-extra-args) works too. Thank you again!
(0006319)
virgile   
2016-12-16 08:36   
OK, thanks for the report. Indeed, Frama-C considers that if CPP is set, then the variable contains the whole command, including any needed option. Hence, Frama-C does not try to add the implicit options that it normally uses. It might make sense to change that behavior, since if CPP is set externally, it is unlikely to have the specific -C flag. I'd suggest that we can have a FRAMA_CPP environment variable, for which the old behavior would apply. If FRAMA_CPP is not set but CPP is, the value of $CPP would then be considered as being a pure pre-processor, to which -C (in case it looks like GNU cpp) should be added. Does it make sense to you?
(0006322)
vlad   
2016-12-16 10:19   
Yes, it does. However, since frama-c has options to specify whether the compiler is compatible with GNU options, I think it's safe to assume $CPP is just compiler command, and additional options should be passed using -cpp-extra-args (or perhaps $CFLAGS, like it's done in some build systems).