2021-03-02 02:33 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001036Frama-CDocumentation > manualspublic2016-06-21 14:20
Assigned Tosignoles 
Product VersionFrama-C Nitrogen-20111001 
Target VersionFixed in VersionFrama-C Oxygen-20120901 
Summary0001036: In section 5.11.5 of the Plugin developper manual : Reference to modules that neither appear in the API nor in Frama-c source.
DescriptionIn the section 5.11.5, concerning the registration of new internal state, the
manual makes some reference to the modules/functors :


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
TagsNo tags attached.
Attached Files




signoles (manager)

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)

Thank you for your quick and clear answers, they will be indeed very helpful !



signoles (manager)

Fix committed to stable/neon branch.

-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