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

[Frama-c-discuss] Alt-ergo Problems



Hello,

I have some problems with the new version.

My observations:

When I am executing why-config, frama-c looks for alt-ergo as well as ergo.
This should be fixed.

Why-config recognizes alt-ergo as version 0.9 correctly. It also recognizes
the file renamed to ergo.

The problem:

Using the alt-ergo file no proof can be computed. 

Solution?!:
Renaming alt-ergo to ergo, the proof can be computed.

In both cases the GUI shows version 0.8 instead of 0.9.

Another irritating problem is, that I seemingly  cannot use  alt-ergo 0.8
and 0.9 simultaneously because I could not distinguish between both. It
could be helpful if the title of each column would be named after each
prover-file, but I do not know how this would affect other platforms.
Anyway, I would like to use several provers and be able to distinguish them.

I also do not know the difference between seemingly equal columns like
alt-ergo and alt-ergo (select).

I hope this feedback is helpful.

Sincerely 

Christoph
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/ms-tnef
Size: 3258 bytes
Desc: not available
Url : http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090911/6d66af7b/attachment.bin