--- layout: fc_discuss_archives title: Message 41 from Frama-C-discuss on April 2010 ---
On Tue, 20 Apr 2010, Virgile Prevosto wrote: > Le mar. 20 avril 2010 12:19:21 CEST, > Nicholas Mc Guire <der.herr at hofr.at> a ?crit : > > > On Tue, 20 Apr 2010, Pascal Cuoq wrote: > > > > > > the hello.c is really just a trivial example for testing > > > > #include <stdio.h> > > > > > > > > void foo(void) > > > > { > > > > ? ? ? ?printf("hello,world\n"); > > > > > > The notion of "trivial" is relative. Your example includes standard > > > headers that contain horrible stuff, and calls a variadic function. > > > Jessie behaved as well as you can expect on your example: your > > > installation is fine. > > > > not quite - removed the printf and the include and provided a dummy function > > get > > > > rtl26:~/formal_methods/Frama-C/examples# frama-c.byte -jessie hello.c > > [kernel] preprocessing with "gcc -C -E -I. -dD hello.c" > > [jessie] Starting Jessie translation > > [jessie] Producing Jessie files in subdir hello.jessie > > [jessie] File hello.jessie/hello.jc written. > > [jessie] File hello.jessie/hello.cloc written. > > [jessie] Calling Jessie tool in subdir hello.jessie > > Generating Why function foo > > Generating Why function main > > [jessie] Calling VCs generator. > > gwhy-bin [...] why/hello.why > > /bin/sh: gwhy-bin: command not found > > This suggests that the graphical user interface is missing. Do you have > the lablgtk library installed? If not, neither why nor frama-c will > complain (you can see a warning about lablgtk in config.log though), but > they will only build the command-line tools. If you have some provers > installed (e.g. alt-ergo), you can directly select one of them with > -jessie-atp <prover> (e.g. -jessie-atp alt-ergo). I only intend to use the command-line tools - working with a braille inteerface and large-print - not a GUI - so that should be ok. Still some problem with a dirty resolution - any futher hint would be much appreciated. jessie problem description: --------------------------- clean install on Debian-5 still some problems with why - no matter which prover I use (tried simplify, cvc3, z3, alt-ergo - all are shown in why-config as being supported (see below)) - I can post the install procedure if relevant (its a bit long) cvd3/z3: rand1:~/example# frama-c.byte -jessie -jessie-atp cvc3 hello.c [kernel] preprocessing with "gcc -C -E -I. -dD hello.c" [jessie] Starting Jessie translation [jessie] Producing Jessie files in subdir hello.jessie [jessie] File hello.jessie/hello.jc written. [jessie] File hello.jessie/hello.cloc written. [jessie] Calling Jessie tool in subdir hello.jessie Generating Why function max [jessie] Calling VCs generator. why -smtlib [...] why/hello.why Running CVC3 on proof obligations (. = valid * = invalid ? = unknown # = timeout ! = failure) smtlib/hello_why.smt : Uncaught exception: Sys_error("smtlib/hello_why.smt: No such file or directory") make: *** [cvc3] Error 2 [jessie] user error: Jessie subprocess failed: make -f hello.makefile cvc3 simplify: rand1:~/example# frama-c.byte -jessie -jessie-atp simplify hello.c [kernel] preprocessing with "gcc -C -E -I. -dD hello.c" [jessie] Starting Jessie translation [jessie] Producing Jessie files in subdir hello.jessie [jessie] File hello.jessie/hello.jc written. [jessie] File hello.jessie/hello.cloc written. [jessie] Calling Jessie tool in subdir hello.jessie Generating Why function max [jessie] Calling VCs generator. why -simplify [...] why/hello.why Running Simplify on proof obligations (. = valid * = invalid ? = unknown # = timeout ! = failure) simplify/hello_why.sx : Uncaught exception: Sys_error("simplify/hello_why.sx: No such file or directory") make: *** [simplify] Error 2 [jessie] user error: Jessie subprocess failed: make -f hello.makefile simplify why-setup: ---------- why-config gives me: prover version info invocation ------------------------------------------------------ Alt-Ergo 0.9 alt-ergo Simplify 1.5.4 simplify Z3 2.2 z3 -smt Yices not found CVC3 2.2 cvc3 -lang smt CVCL 2.2 (not supported) cvc3 Gappa not found Coq 8.1pl3 (not supported) coqc PVS not found ------------------------------------------------------ test input file: ---------------- The hello.c is now a real simple example (I hope) - cut&past from the tutorial. /*@ ensures \result == ((i < j) ? j : i); @*/ int max(int i, int j) { return (i < j) ? j : i; } tracing the problem: -------------------- going up the execution chain - tried executing why manually to generate the simplify/%_why.sx: target rand1:~/example/hello.jessie# WHYLIB=/usr/local/lib/why strace -f why -simplify -dir simplify -split-user-conj -explain -locs hello.loc /usr/local/lib/why/why/jessie.why why/hello.why this will generate the file simplify/hello but not the expected simplify/hello_why.sx - so patching the rule in the makefile to read example/hello.jessie/hello.makefile simplify/%_why.sx: WHYOPT=-simplify -dir simplify simplify/%_why.sx: why/%.why @echo why: $(WHY) @echo jessielibfiles: $(JESSIELIBFILES) @echo 'why -simplify [...] why/$*.why' && $(WHY) $(JESSIELIBFILES) why/$*.why cp simplify/$* simplify/$*_why.sx results in: AthlongII2X_250_1:~/example/hello.jessie# make -f hello.makefile simplify why -simplify [...] why/hello.why cp simplify/hello simplify/hello_why.sx Running Simplify on proof obligations (. = valid * = invalid ? = unknown # = timeout ! = failure) simplify/hello_why.sx : .? (1/0/1/0/0) total : 2 valid : 1 ( 50%) invalid : 0 ( 0%) unknown : 1 ( 50%) timeout : 0 ( 0%) failure : 0 ( 0%) total wallclock time : 0.08 sec total CPU time : 0.06 sec valid VCs: average CPU time : 0.02 max CPU time : 0.02 invalid VCs: average CPU time : nan max CPU time : 0.00 unknown VCs: average CPU time : 0.04 max CPU time : 0.04 I'm a bit stuck now - as obviously this "hack" in the makefile should not be needed ? but from the tutorial I would guess the output is ok ? - so any further hint what I might have messed up ? thx! hofrat