Skip to content

*off == off_cpy cannot be proven just after the assignment *off = off_cpy

ID0002130: This issue was created automatically from Mantis Issue 2130. Further discussion may take place here.

Id Project Category View Due Date Updated
ID0002130 Frama-C Plug-in > wp public 2015-06-04 2015-06-29
Reporter loic Assigned To correnson Resolution no change required
Priority normal Severity major Reproducibility always
Platform Linux OS Ubuntu OS Version 12.04.5 LTS
Product Version - Target Version - Fixed in Version -

Description :

Nitrogen-20111001 alt-ergo 0.94

#include <stddef.h>

/*

  • Can memory zones be declared disjoint? For instance:
  • \disjoint(off, buf + *off)
  • wp does not accept and thus gracefully skips the following try:
  • @ requires \forall size_t i;
  • 0 <= i < sizeof(*off) ==> (char *) off != buf + (*off + i);

*/

/*@ @ requires \valid(off) && \valid(buf + *off); @ assigns *off, buf[*off]; @ ensures *off == \old(*off) + 1; @ ensures buf[\old(off)] == '\0'; @/ void alias_testcase_0(char *const buf, size_t *const off) { size_t off_cpy = off; / restricted pointers cannot be required */

buf[off_cpy++] = '\0';
/*@ assert off_cpy - 1 == \at(*off, Pre); */  /* OK */
/*@ assert buf[off_cpy - 1] == '\0';      */  /* OK */

*off = off_cpy;
/*@ assert *off == off_cpy;              */  /* NOK, cannot be proven */
/*@ assert buf[\at(*off, Pre)] == '\0';  */  /* NOK, cannot be proven */

}

Steps To Reproduce :

frama-c -wp -wp-rte on the code above (also as attachment).

Attachments

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