Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002213Frama-CPlug-in > E-ACSLpublic2016-02-26 14:082017-01-18 15:09
ReporterGeorge Karpenkov 
Assigned Tosignoles 
PlatformOSOS Version
Product VersionFrama-C Magnesium 
Target VersionFixed in VersionFrama-C 14-Silicon 
Summary0002213: Can't install E-ACSL plugin
DescriptionHi, Is E-ACSL 0.5 supposed to work with Frama-C Magnesium? The installation instructions for E-ACSL still read "Frama-C = Sodium-20150201 (no warranty that this plug-in works with a more recent version of Frama-C)". I've tried updating Frama-C and E-ACSL through OPAM, but E-ACSL description in OPAM requires the previous version of Frama-C. After changing the E-ACSL metadata I could get it installed, but running "frama-c -e-acsl" reported "option ... is unknown". I've also tried to install E-ACSL plug-in manually, but running ./configure reports "configure: WARNING: e_acsl disabled because rtegen unknown." after which running "make" does nothing.
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
George Karpenkov (reporter)
2016-02-26 14:23

I've tried changing e-acsl "configure" script not to try to search for "rtegen", as it can't find it for some reason. Now I'm hitting actual backwards incompatibility: File "", line 284, characters 4-24: Error: The constructor GVarDecl expects 2 argument(s), but is applied here to 3 argument(s) The Frama-C changelog even conveniently highlights this change: o! Kernel [2015/03/10] AST change: split GVarDecl into GVarDecl and GFunDecl
signoles (manager)
2016-02-26 15:15

E-ACSL 0.5 is not compatible with Magnesium. A new Magnesium-compatible release of E-ACSL is ready to be released but one issue with our website currently prevent us to put it online. It will be done as soon as possible.
signoles (manager)
2017-01-18 15:09

Fixed in E-ACSL 0.8 compatible with Frama-C Silicon.

- Issue History
Date Modified Username Field Change
2016-02-26 14:08 George Karpenkov New Issue
2016-02-26 14:08 George Karpenkov Status new => assigned
2016-02-26 14:08 George Karpenkov Assigned To => signoles
2016-02-26 14:23 George Karpenkov Note Added: 0006165
2016-02-26 15:15 signoles Note Added: 0006166
2016-02-26 15:15 signoles Status assigned => resolved
2016-02-26 15:15 signoles Fixed in Version => Frama-C Magnesium
2016-02-26 15:15 signoles Resolution open => fixed
2017-01-18 15:09 signoles Fixed in Version Frama-C Magnesium => Frama-C 14-Silicon
2017-01-18 15:09 signoles Note Added: 0006341
2017-01-18 15:09 signoles Status resolved => closed

Copyright © 2000 - 2020 MantisBT Team
Powered by Mantis Bugtracker