--- layout: fc_discuss_archives title: Message 41 from Frama-C-discuss on April 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] why-2.24 install question



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