2021-01-15 15:51 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0002213Frama-CPlug-in > E-ACSLpublic2017-01-18 15:09
ReporterGeorge Karpenkov 
Assigned Tosignoles 
Product VersionFrama-C Magnesium 
Target VersionFixed in VersionFrama-C 14-Silicon 
Summary0002213: Can't install E-ACSL plugin

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




George Karpenkov (reporter)

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


signoles (manager)

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)

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
+Issue History