Skip to content

GitLab

  • Menu
Projects Groups Snippets
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
  • F frama-c
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 208
    • Issues 208
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 0
    • Merge requests 0
  • Deployments
    • Deployments
    • Releases
  • Monitor
    • Monitor
    • Incidents
  • Packages & Registries
    • Packages & Registries
    • Container Registry
  • Analytics
    • Analytics
    • Value stream
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
Collapse sidebar
  • pub
  • frama-c
  • Issues
  • #331

Closed
Open
Created Jun 15, 2017 by Jochen Burghardt@burghardt

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.

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking