--- layout: fc_discuss_archives title: Message 74 from Frama-C-discuss on March 2009 ---
Hi, removing swap.jessie/ solved the problem. Thank you for your help! I discovered that the problem appears again if I run frama-c, followed by frama-c-gui or frama-c-gui, followed by frama-c. While I can repeatedly run either frama-c or frama-c-gui after removing swap.jessie without errors, mixing the two fails: (I use Windows XP with cygwin and bash) ~/progs/fc/swap> frama-c -jessie-analysis swap.c Parsing [preprocessing] running gcc -C -E -I. -include C:\Frama-C\share\frama-c\jessie\jessie_prolog.h -dD swap.c Cleaning unused parts Symbolic link Starting semantical analysis Starting Jessie translation Producing Jessie files in subdir swap.jessie File swap.jessie/swap.jc written. File swap.jessie/swap.cloc written. Calling Jessie tool in subdir swap.jessie Generating Why function Swap Generating Why function main Calling VCs generator. make: Warning: File `swap.makefile' has modification time 0.0077 s in the future why -simplify [...] why/swap.why Running Simplify on proof obligations (. = valid * = invalid ? = unknown # = timeout ! = failure) simplify/swap_why.sx : ................ (16/0/0/0/0) total : 16 valid : 16 (100%) invalid : 0 ( 0%) unknown : 0 ( 0%) timeout : 0 ( 0%) failure : 0 ( 0%) total wallclock time : 3.14 sec total CPU time : 0.00 sec valid VCs: average CPU time : 0.00 max CPU time : 0.00 invalid VCs: average CPU time : -1.#J max CPU time : 0.00 unknown VCs: average CPU time : -1.#J max CPU time : 0.00 make: warning: Clock skew detected. Your build may be incomplete. ~/progs/fc/swap> frama-c-gui -jessie-analysis swap.c Parsing [preprocessing] running gcc -C -E -I. -include C:\Frama-C\share\frama-c\jessie\jessie_prolog.h -dD swap.c Cleaning unused parts Symbolic link Starting semantical analysis Starting Jessie translation Producing Jessie files in subdir swap.jessie File swap.jessie/swap.jc written. File swap.jessie/swap.cloc written. Calling Jessie tool in subdir swap.jessie Generating Why function Swap Generating Why function main Calling VCs generator. make: Warning: File `swap.makefile' has modification time 0.15 s in the future why -simplify [...] why/swap.why Fatal error: exception Sys_error("File exists") make: *** [simplify/swap_why.sx] Error 2 Jessie subprocess failed: make -f swap.makefile simplify ~/progs/fc/swap> frama-c-gui -jessie-analysis swap.c Parsing [preprocessing] running gcc -C -E -I. -include C:\Frama-C\share\frama-c\jessie\jessie_prolog.h -dD swap.c Cleaning unused parts Symbolic link Starting semantical analysis Starting Jessie translation Producing Jessie files in subdir swap.jessie File swap.jessie/swap.jc written. File swap.jessie/swap.cloc written. Calling Jessie tool in subdir swap.jessie Generating Why function Swap Generating Why function main Calling VCs generator. make: Warning: File `swap.makefile' has modification time 0.47 s in the future why -simplify [...] why/swap.why Running Simplify on proof obligations (. = valid * = invalid ? = unknown # = timeout ! = failure) simplify/swap_why.sx : ................ (16/0/0/0/0) total : 16 valid : 16 (100%) invalid : 0 ( 0%) unknown : 0 ( 0%) timeout : 0 ( 0%) failure : 0 ( 0%) total wallclock time : 3.05 sec total CPU time : 0.00 sec valid VCs: average CPU time : 0.00 max CPU time : 0.00 invalid VCs: average CPU time : -1.#J max CPU time : 0.00 unknown VCs: average CPU time : -1.#J max CPU time : 0.00 make: warning: Clock skew detected. Your build may be incomplete. ~/progs/fc/swap> frama-c -jessie-analysis swap.c Parsing [preprocessing] running gcc -C -E -I. -include C:\Frama-C\share\frama-c\jessie\jessie_prolog.h -dD swap.c Cleaning unused parts Symbolic link Starting semantical analysis Starting Jessie translation Producing Jessie files in subdir swap.jessie File swap.jessie/swap.jc written. File swap.jessie/swap.cloc written. Calling Jessie tool in subdir swap.jessie Generating Why function Swap Generating Why function main Calling VCs generator. make: Warning: File `swap.makefile' has modification time 0.36 s in the future why -simplify [...] why/swap.why Fatal error: exception Sys_error("File exists") make: *** [simplify/swap_why.sx] Error 2 Jessie subprocess failed: make -f swap.makefile simplify