Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002313Frama-CDocumentation > manualspublic2017-06-15 15:452017-06-23 10:44
ReporterJochen 
Assigned Tocorrenson 
PrioritynormalSeveritytextReproducibilityN/A
StatusassignedResolutionopen 
Platformwp-manual-Phosphorus-20170501.pdOSn/aOS Version
Product VersionFrama-C 15 Phosphorus 
Target VersionFixed in Version 
Summary0002313: suggestions for improvement of Sect.3.6 and 3.7 of the wp manual
DescriptionIn the WP manual, section 3.6 "The Typed Memory Model", instead of explaining the "Typed" memory model, refers to an old "Store" memory model and only describes the differences. However, few (and increasingly fewer) users are familiar with that old model, let alone availability issues of old WP manuals. Therefore, the "Typed" model should be described from scratch. Also, the section should initially state that it is about the model named "Typed".

In section 3.7, I found the following senteces hard to understand, and added my questions in "{}":

This detection is more clever than the standard one {That is, the one of the "Typed" model?} since it only takes into account local usage {What is local and global usage of a function? How can an approach being more clever than another one although it is based on less information?} of each function (not global ones).
Additionally, the Caveat memory model of Frama-C performs a local allocation {What is a local allocation? Shouldn't Frama-C's allocation reflect those made by the C compiler, which pushes actual parameters on the local stack in a new stack-frame, and expects formal parameters on the local stack in the current stack frame?} of formal parameters with pointer types that cannot be treated as reference parameters.

This makes explicit the separation hypothesis of memory regions pointed by formals in the Caveat tool. The major benefit of the WP version {Compared to what? To the Caveat tool? To the plain "Typed" model?} is that aliases are taken into account by the Typed memory model, hence, there are no more suspicious aliasing warnings.
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0006413)
Jochen (reporter)
2017-06-15 15:50

BTW: Section 2.4.3 "Model Selection" says

These options modify the underlying memory model that is used for computing weakest preconditions. See chapter 4 for details.

This should be "memory and arithmetic model", and "chapter 3 and 4".

- Issue History
Date Modified Username Field Change
2017-06-15 15:45 Jochen New Issue
2017-06-15 15:50 Jochen Note Added: 0006413
2017-06-23 10:44 signoles Assigned To => correnson
2017-06-23 10:44 signoles Status new => assigned


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker