Mk_addr not defined in Memory.v (coqwp via why3ide)
ID0002414: This issue was created automatically from Mantis Issue 2414. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002414 | Frama-C | Plug-in > wp | public | 2018-12-07 | 2019-10-17 |
| Reporter | visq | Assigned To | correnson | Resolution | won't fix |
| Priority | normal | Severity | major | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C 18-Argon | Target Version | - | Fixed in Version | - |
Description :
Memory.Mk_addr is needed for Coq proofs but not in Memory.v (it is present in Memory.why). As a consequence, Coq fails to compile the generated proof scripts for a null pointer check:
Error: The reference Memory.Mk_addr was not found in the current environment.
Additional Information :
Frama-c Argon 18.0 Coq 8.6 why3 0.88.3
Steps To Reproduce :
cat <id.c /*@ requires \valid(p); ensures *p == \old(p); / void id(int p) { int tmp; if (p == (int)0) return; tmp = *p; *p = ~~tmp; } EOF frama-c -wp -wp-rte -wp-split -wp-prover why3ide id.c