| View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
| ID | Project | Category | View Status | Date Submitted | Last Update | ||||
|---|---|---|---|---|---|---|---|---|---|
| 0001036 | Frama-C | Documentation > manuals | public | 2011-11-30 17:54 | 2016-06-21 14:20 | ||||
| Reporter | fgarnier | ||||||||
| Assigned To | signoles | ||||||||
| Priority | normal | Severity | feature | Reproducibility | N/A | ||||
| Status | closed | Resolution | fixed | ||||||
| Product Version | Frama-C Nitrogen-20111001 | ||||||||
| Target Version | Fixed in Version | Frama-C Oxygen-20120901 | |||||||
| Summary | 0001036: In section 5.11.5 of the Plugin developper manual : Reference to modules that neither appear in the API nor in Frama-c source. | ||||||||
| Description | In the section 5.11.5, concerning the registration of new internal state, the manual makes some reference to the modules/functors : _Project.Computation.Register, _Computation, _Cil_computation. I can't find them, neither in the html api --even when browsing the list of all modules, nor while browsing both the cil source directory nor the framac kernel directory. Maybe the value those modules and functors used to defined have been moved elsewhere. | ||||||||
| Tags | No tags attached. | ||||||||
| Attached Files |
| ||||||||
 Relationships |
|
 Relationships |
| Notes |
|
|
signoles (manager) 2011-11-30 18:31 Last edited: 2011-11-30 18:31 |
The preambule of Section 5.11 states that this whole section is out-of-date (including subsection 5.11.5). The modules that you search do not exist anymore in recent versions of Frama-C. The correspondance is as follows: - Project.Computation.Register ==> State_builder.Register - Computation ==> State_builder - Cil_computation ==> Cil_state_builder Even if the signatures have changed a little bit, what is said in the manual about the old modules remains roughly true for the new ones. For details, have a look at the API of these modules or ask precise questions on the Frama-C discuss mailing list. Hope this helps. |
|
fgarnier (reporter) 2011-12-02 10:33 |
Thank you for your quick and clear answers, they will be indeed very helpful ! Florent. |
|
signoles (manager) 2014-02-12 16:58 |
Fix committed to stable/neon branch. |
| Notes |
| Issue History |
|||
| Date Modified | Username | Field | Change |
|---|---|---|---|
| 2011-11-30 17:54 | fgarnier | New Issue | |
| 2011-11-30 17:54 | fgarnier | Status | new => assigned |
| 2011-11-30 17:54 | fgarnier | Assigned To | => signoles |
| 2011-11-30 18:31 | signoles | Note Added: 0002520 | |
| 2011-11-30 18:31 | signoles | Status | assigned => confirmed |
| 2011-11-30 18:31 | signoles | Note Edited: 0002520 | |
| 2011-12-02 10:33 | fgarnier | Note Added: 0002527 | |
| 2012-05-09 18:27 | svn | ||
| 2012-05-09 18:27 | svn | Status | confirmed => resolved |
| 2012-05-09 18:27 | svn | Resolution | open => fixed |
| 2012-09-19 17:15 | signoles | Fixed in Version | => Frama-C Oxygen-20120901 |
| 2012-09-19 17:16 | signoles | Status | resolved => closed |
| 2013-12-19 01:11 | signoles | Source_changeset_attached | => framac master 78b92e40 |
| 2014-02-12 16:54 | signoles | Source_changeset_attached | => framac stable/neon 78b92e40 |
| 2014-02-12 16:58 | signoles | Note Added: 0004689 | |
| 2014-02-12 16:58 | signoles | Status | closed => resolved |
| 2016-06-21 14:11 | signoles | Category | Documentation => Documentation > ACSL |
| 2016-06-21 14:20 | signoles | Category | Documentation > ACSL => Documentation > manuals |
| Issue History |