Frama-C Bug Tracking System - Frama-C
View Issue Details
0000240Frama-CPlug-in > jessiepublic2009-09-11 15:512010-12-22 18:04
Frama-C Beryllium-20090901 
Frama-C Carbon-20101202-beta2 
0000240: Problems with solver configuration
Using the prover named alt-ergo v 0.9 no proof can be computed. Why-config recognizes alt-ergo as version 0.9 correctly. Solution?!: Renaming alt-ergo to ergo, the proof can be computed. In both cases the GUI shows version 0.8 instead of 0.9. But, since alt-ergo and ergo are both valid, which will be used? (I would like to be able to add multiple version of alt ergo and to distinguish them by the names I have given them .)
using multiple versions of the same prover will be available in Why3, released in december. This will not be available in Why2
No tags attached.
Issue History
2009-09-11 15:51ChristophNew Issue
2009-09-11 15:52ChristophNote Added: 0000393
2009-09-12 07:16signolesCategorygraphical user interface => plug-in > jessie
2009-09-12 07:16signolesDescription Updated
2009-09-12 07:16signolesStatusnew => assigned
2009-09-12 07:16signolesAssigned To => cmarche
2010-09-16 14:51cmarcheStatusassigned => resolved
2010-09-16 14:51cmarcheResolutionopen => fixed
2010-09-16 14:51cmarcheDescription Updated
2010-09-16 14:51cmarcheAdditional Information Updated
2010-12-22 18:04signolesNote Added: 0001351
2010-12-22 18:04signolesStatusresolved => closed
2010-12-22 18:04signolesFixed in Version => Frama-C Carbon-20101202-beta2

2009-09-11 15:52   
This one concernes the GUI of the jessie plugin.
2010-12-22 18:04   
Available in Why3.