Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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