0000240: Problems with solver configuration - Frama-C Bug Tracking System

Frama-C Bug Tracking System

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

ID

Project

Category

View Status

Date Submitted

Last Update

0000240

Frama-C

Plug-in > jessie

public

2009-09-11 15:51

2010-12-22 18:04

Reporter

Christoph

Assigned To

cmarche

Priority

normal

Severity

minor

Reproducibility

N/A

Status

closed

Resolution

fixed

Platform

OS

OS Version

Product Version

Frama-C Beryllium-20090901

Target Version

Fixed in Version

Frama-C Carbon-20101202-beta2

Summary

0000240: Problems with solver configuration

Description

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 .)

Additional Information

using multiple versions of the same prover will be available in Why3,
released in december.

This will not be available in Why2

Tags

No tags attached.

Relationships

Notes
(0000393) Christoph (reporter) 2009-09-11 15:52	This one concernes the GUI of the jessie plugin.

(0001351) signoles (manager) 2010-12-22 18:04	Available in Why3.

Issue History
Date Modified	Username	Field	Change
2009-09-11 15:51	Christoph	New Issue
2009-09-11 15:52	Christoph	Note Added: 0000393
2009-09-12 07:16	signoles	Category	graphical user interface => plug-in > jessie
2009-09-12 07:16	signoles	Description Updated
2009-09-12 07:16	signoles	Status	new => assigned
2009-09-12 07:16	signoles	Assigned To	=> cmarche
2010-09-16 14:51	cmarche	Status	assigned => resolved
2010-09-16 14:51	cmarche	Resolution	open => fixed
2010-09-16 14:51	cmarche	Description Updated
2010-09-16 14:51	cmarche	Additional Information Updated
2010-12-22 18:04	signoles	Note Added: 0001351
2010-12-22 18:04	signoles	Status	resolved => closed
2010-12-22 18:04	signoles	Fixed in Version	=> Frama-C Carbon-20101202-beta2

Copyright © 2000 - 2019 MantisBT Team