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 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
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
+Relationships

-Notes

~0006165

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

~0006166

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.

~0006341

signoles (manager)

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

-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