| View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
| ID | Project | Category | View Status | Date Submitted | Last Update | ||||
|---|---|---|---|---|---|---|---|---|---|
| 0002414 | Frama-C | Plug-in > wp | public | 2018-12-07 07:44 | 2019-10-17 17:58 | ||||
| Reporter | visq | ||||||||
| Assigned To | correnson | ||||||||
| Priority | normal | Severity | major | Reproducibility | always | ||||
| Status | closed | Resolution | won't fix | ||||||
| Product Version | Frama-C 18-Argon | ||||||||
| Target Version | Fixed in Version | ||||||||
| Summary | 0002414: Mk_addr not defined in Memory.v (coqwp via why3ide) | ||||||||
| 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. | ||||||||
| Steps To Reproduce | cat <<EOF >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 # Select Postcondition Line 2 # Coq # Edit # Replay # => 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 | ||||||||
| Tags | No tags attached. | ||||||||
| Attached Files |
| ||||||||
 Relationships |
|
 Relationships |
| Notes |
|
|
correnson (manager) 2019-10-17 16:24 Last edited: 2019-10-17 16:26 |
Why3 ide is no more supported, and native coq support is deprecated. However, the goal actually compiles with the new upcoming release (Carbon). There remain an implicit coercion type with coq 8.7.2 that could probably be solved in more recent versions. |
| Notes |
| Issue History |
|||
| Date Modified | Username | Field | Change |
|---|---|---|---|
| 2018-12-07 07:44 | visq | New Issue | |
| 2018-12-07 07:44 | visq | Status | new => assigned |
| 2018-12-07 07:44 | visq | Assigned To | => correnson |
| 2019-10-17 16:24 | correnson | Note Added: 0006897 | |
| 2019-10-17 16:25 | correnson | Status | assigned => resolved |
| 2019-10-17 16:25 | correnson | Resolution | open => won't fix |
| 2019-10-17 16:26 | correnson | Note Edited: 0006897 | View Revisions |
| 2019-10-17 17:58 | signoles | Status | resolved => closed |
| Issue History |