Frama-C Bug Tracking System - Frama-C
View Issue Details
0002482Frama-CPlug-in > wppublic2019-10-22 19:472019-10-22 23:35
jens 
correnson 
normalminoralways
resolvedno change required 
Linux, macOS
Frama-C 19-Potassium 
 
0002482: WP warning not clear
When 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?
No tags attached.
c f.c (184) 2019-10-22 19:47
https://bts.frama-c.com/file_download.php?file_id=1331&type=bug
Issue History
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.