Frama-C Bug Tracking System - Frama-C
View Issue Details
0002213Frama-CPlug-in > E-ACSLpublic2016-02-26 14:082017-01-18 15:09
George Karpenkov 
signoles 
normalminoralways
closedfixed 
Frama-C Magnesium 
Frama-C 14-Silicon 
0002213: Can't install E-ACSL plugin
Hi, 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.
No tags attached.
Issue History
2016-02-26 14:08George KarpenkovNew Issue
2016-02-26 14:08George KarpenkovStatusnew => assigned
2016-02-26 14:08George KarpenkovAssigned To => signoles
2016-02-26 14:23George KarpenkovNote Added: 0006165
2016-02-26 15:15signolesNote Added: 0006166
2016-02-26 15:15signolesStatusassigned => resolved
2016-02-26 15:15signolesFixed in Version => Frama-C Magnesium
2016-02-26 15:15signolesResolutionopen => fixed
2017-01-18 15:09signolesFixed in VersionFrama-C Magnesium => Frama-C 14-Silicon
2017-01-18 15:09signolesNote Added: 0006341
2017-01-18 15:09signolesStatusresolved => closed

Notes
(0006165)
George Karpenkov   
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 "dup_functions.ml", 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
(0006166)
signoles   
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.
(0006341)
signoles   
2017-01-18 15:09   
Fixed in E-ACSL 0.8 compatible with Frama-C Silicon.