Anonymous Login Frama-C issues should now be submitted on Frama-C's GitLab
2021-03-06 02:51 CET
  

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002482Frama-CPlug-in > wppublic2019-10-22 19:472020-02-17 18:08
Reporterjens 
Assigned Tocorrenson 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionno change required 
PlatformOSLinux, macOSOS Version
Product VersionFrama-C 19-Potassium 
Target VersionFixed in VersionFrama-C 20-Calcium 
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?
TagsNo tags attached.
Attached Files
  • c file icon f.c (184 bytes) 2019-10-22 19:47 - 
    
extern int p[2];

/*@
    requires \valid(a);
    //requires \separated(p+(..),a);

    assigns *a;
    assigns *p;
*/
void f(int* a)
{
    int x = *p;
    *p  = *a;
    *a  = x;
}
    c file icon f.c (184 bytes) 2019-10-22 19:47 +

-Relationships
+Relationships

-Notes

~0006914

correnson (manager)

2019-10-22 23:30

Last edited: 2019-10-22 23:32

View 2 revisions

 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 (manager)

2019-10-22 23:34

Last edited: 2019-10-22 23:35

View 2 revisions

 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.

~0006939

signoles (manager)

2020-02-17 18:08

 Fixed in Frama-C 20.0 (Calcium).
+Notes

-Issue History
Date Modified Username Field Change
2019-10-22 19:47 jens New Issue
2019-10-22 19:47 jens Status new => assigned
2019-10-22 19:47 jens Assigned To => correnson
2019-10-22 19:47 jens File Added: f.c
2019-10-22 23:30 correnson Note Added: 0006914
2019-10-22 23:32 correnson Note Edited: 0006914 View Revisions
2019-10-22 23:32 correnson Status assigned => resolved
2019-10-22 23:32 correnson Resolution open => no change required
2019-10-22 23:34 correnson Note Added: 0006915
2019-10-22 23:35 correnson Note Edited: 0006915 View Revisions
2020-02-17 18:06 signoles Fixed in Version => Frama-C 20-Calcium
2020-02-17 18:08 signoles Status resolved => closed
2020-02-17 18:08 signoles Note Added: 0006939
+Issue History