suggestions for improvement of Sect.3.6 and 3.7 of the wp manual
ID0002313: This issue was created automatically from Mantis Issue 2313. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002313 | Frama-C | Documentation > manuals | public | 2017-06-15 | 2017-06-23 |
| Reporter | Jochen | Assigned To | correnson | Resolution | open |
| Priority | normal | Severity | text | Reproducibility | N/A |
| Platform | wp-manual-Phosphorus-20170501.pd | OS | n/a | OS Version | - |
| Product Version | Frama-C 15-Phosphorus | Target Version | - | Fixed in Version | - |
Description :
In 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.