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 ]
IDProjectCategoryView StatusLast Update
0002482Frama-CPlug-in > wppublic2020-02-17 18:08
Assigned Tocorrenson 
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 +




correnson (manager)

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

Roadmap: in the future « Region » memory model, such hypotheses would be checked by WP on its own.


correnson (manager)

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.


signoles (manager)

Fixed in Frama-C 20.0 (Calcium).

-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