--- layout: fc_discuss_archives title: Message 74 from Frama-C-discuss on March 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Jessie subprocess failed



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