Frama-C Bug Tracking System - Frama-C
View Issue Details
0002313Frama-CDocumentation > manualspublic2017-06-15 15:452017-06-23 10:44
Frama-C 15-Phosphorus 
0002313: suggestions for improvement of Sect.3.6 and 3.7 of the wp manual
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.
No tags attached.
Issue History
2017-06-15 15:45JochenNew Issue
2017-06-15 15:50JochenNote Added: 0006413
2017-06-23 10:44signolesAssigned To => correnson
2017-06-23 10:44signolesStatusnew => assigned

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".