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] 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