Frama-C Bug Tracking System - Frama-C
View Issue Details
0002414Frama-CPlug-in > wppublic2018-12-07 07:442018-12-07 07:44
visq 
correnson 
normalmajoralways
assignedopen 
Frama-C 18-Argon 
 
0002414: Mk_addr not defined in Memory.v (coqwp via why3ide)
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.
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.
Frama-c Argon 18.0
Coq 8.6
why3 0.88.3
No tags attached.
Issue History
2018-12-07 07:44visqNew Issue
2018-12-07 07:44visqStatusnew => assigned
2018-12-07 07:44visqAssigned To => correnson

There are no notes attached to this issue.