Frama-C Bug Tracking System - Frama-C
View Issue Details
IDProjectCategoryView StatusDate SubmittedLast Update
0002482Frama-CPlug-in > wppublic2019-10-22 19:472019-10-22 23:35
Reporterjens 
Assigned Tocorrenson 
PrioritynormalSeverityminorReproducibilityalways
StatusresolvedResolutionno change required 
PlatformOSLinux, macOSOS Version
Product VersionFrama-C 19-Potassium 
Target VersionFixed in Version 
Summary0002482: WP warning not clear
DescriptionWhen I run frama-c -wp -wp-rte -wp-model Typed f.c on the attached file, I obtain the warning [wp] Warning: Memory model hypotheses for function 'f': /*@ behavior typed: requires \separated(p+(..),a); */ void f(int *a); However, when I add this requirement by removing the corresponding comment in the contract, then the warning still occurs. What can I do to make this warning disappear?
Steps To Reproduce
Additional Information
TagsNo tags attached.
Relationships
Attached Filesc f.c (184) 2019-10-22 19:47
https://bts.frama-c.com/file_download.php?file_id=1331&type=bug
Issue History
Date ModifiedUsernameFieldChange
2019-10-22 19:47jensNew Issue
2019-10-22 19:47jensStatusnew => assigned
2019-10-22 19:47jensAssigned To => correnson
2019-10-22 19:47jensFile Added: f.c
2019-10-22 23:30corrensonNote Added: 0006914
2019-10-22 23:32corrensonNote Edited: 0006914View Revisions
2019-10-22 23:32corrensonStatusassigned => resolved
2019-10-22 23:32corrensonResolutionopen => no change required
2019-10-22 23:34corrensonNote Added: 0006915
2019-10-22 23:35corrensonNote Edited: 0006915View Revisions

Notes
(0006914)
correnson   
2019-10-22 23:30   
(edited on: 2019-10-22 23:32)
These warnings are emitted because WP is not able to verify them on its own since it assumes these assumptions (or something weaker) to proceed. If you are confident that such requirements are still valid, you can turn off their emission with option -wp-(no)-warn-memory-model. Roadmap: in the future « Region » memory model, such hypotheses would be checked by WP on its own.
(0006915)
correnson   
2019-10-22 23:34   
(edited on: 2019-10-22 23:35)
Side note: some requirements are too strong as they are printed. For instance, you can see a requirement like « \valid(a + (..)) » although maybe it is sufficient to have « \valid(a + (0..n)) » for some well-chosen « n ». The same for separation hypotheses. This is why we do not add them to preconditions automatically.