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. - Frama-C Bug Tracking System

Frama-C Bug Tracking System

View Issue Details [ Jump to Notes ] [ Related Changesets ]

[ 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

Platform

OS

OS Version

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.

Relationships

Notes
(0002520) signoles (manager) 2011-11-30 18:31 edited on: 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.

(0002527) fgarnier (reporter) 2011-12-02 10:33	Thank you for your quick and clear answers, they will be indeed very helpful ! Florent.

(0004689) signoles (manager) 2014-02-12 16:58	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-01-27 10:28	signoles	Relationship added	related to 0000622
2012-05-09 18:27	svn	Checkin
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
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

Copyright © 2000 - 2019 MantisBT Team