Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002337Frama-CDocumentationpublic2017-12-14 13:432017-12-29 12:02
ReporterJochen 
Assigned Tocorrenson 
PrioritynormalSeveritytextReproducibilityN/A
StatusassignedResolutionopen 
PlatformSulfur-20171101OSOS Version
Product Version 
Target VersionFixed in Version 
Summary0002337: explain wp's syntactic restrictions on "inductive" definitions
DescriptionIn Sect.2.6.3 "Inductive predicates" (p.50) of the manual "acsl-implementation-Sulfur-20171101.pdf", it is announced that "tools might enforce syntactic conditions on the form of inductive definitions". However, in the Wp manual (file "wp-manual-Sulfur-20171101.pdf") the string "inductive" doesn't occur at all. It should be explained there what restrictions Wp enforces on "inductive" definitions; in case it doesn't restrict them at all, this should be mentioned, too. I didn't check other plugin manuals for the occurrence of the string "inductive".

As a side remark: From a user's point of view, the freedom of each plugin to give its own semantics to (details of) ACSL constructs is confusing, and sometimes even annoying. From a software engineer's point of view, admitting too much freedom to plugins gives away the advantages of a integerated framework/plugin architecture. Having different semantics for ACSL details may compromise the interoperability of plugins.
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0006500)
signoles (manager)
2017-12-29 12:02

The semantics of ACSL is (or should be) the same for all plug-ins. About inductive definitions, the ACSL manual only warns the user that plug-ins might add __syntactic__ restrictions because most of them cannot handle the most general form of ACSL inductive definition.

- Issue History
Date Modified Username Field Change
2017-12-14 13:43 Jochen New Issue
2017-12-29 11:57 signoles Assigned To => correnson
2017-12-29 11:57 signoles Status new => assigned
2017-12-29 12:02 signoles Note Added: 0006500


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker