2021-03-03 03:31 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0002414Frama-CPlug-in > wppublic2019-10-17 17:58
Assigned Tocorrenson 
StatusclosedResolutionwon't fix 
Product VersionFrama-C 18-Argon 
Target VersionFixed in Version 
Summary0002414: Mk_addr not defined in Memory.v (coqwp via why3ide)
DescriptionMemory.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 Reproducecat <<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;
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 InformationFrama-c Argon 18.0
Coq 8.6
why3 0.88.3
TagsNo tags attached.
Attached Files




correnson (manager)

Last edited: 2019-10-17 16:26

View 2 revisions

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.


-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