Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002261Frama-CPlug-in > wppublic2016-12-14 11:572016-12-16 10:19
Assigned Tovirgile 
PlatformWindowsOSWindows 7OS Version
Product VersionFrama-C 14-Silicon 
Target VersionFixed in Version 
Summary0002261: wp: the example from Getting Started guide doesn't work (all goals are Unknown)
DescriptionI'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).
Additional Information$ alt-ergo -version 1.30 $ frama-c --version Silicon-20161101
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
virgile (developer)
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
vlad (reporter)
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; }
virgile (developer)
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).
vlad (reporter)
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.
virgile (developer)
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
vlad (reporter)
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!
virgile (developer)
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?
vlad (reporter)
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).

- Issue History
Date Modified Username Field Change
2016-12-14 11:57 vlad New Issue
2016-12-14 11:57 vlad Status new => assigned
2016-12-14 11:57 vlad Assigned To => correnson
2016-12-14 16:26 virgile Note Added: 0006313
2016-12-14 16:26 virgile Assigned To correnson => virgile
2016-12-14 16:26 virgile Status assigned => feedback
2016-12-15 07:43 vlad Note Added: 0006314
2016-12-15 07:43 vlad Status feedback => assigned
2016-12-15 08:01 vlad Note Edited: 0006314 View Revisions
2016-12-15 08:10 virgile Note Added: 0006315
2016-12-15 08:24 vlad Note Added: 0006316
2016-12-15 09:05 virgile Note Added: 0006317
2016-12-15 09:16 vlad Note Added: 0006318
2016-12-15 09:18 vlad Note Edited: 0006318 View Revisions
2016-12-16 08:36 virgile Note Added: 0006319
2016-12-16 10:19 vlad Note Added: 0006322

Copyright © 2000 - 2020 MantisBT Team
Powered by Mantis Bugtracker