Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002414Frama-CPlug-in > wppublic2018-12-07 07:442018-12-07 07:44
Reportervisq 
Assigned Tocorrenson 
PrioritynormalSeveritymajorReproducibilityalways
StatusassignedResolutionopen 
PlatformOSOS Version
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;
}
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 InformationFrama-c Argon 18.0
Coq 8.6
why3 0.88.3
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
There are no notes attached to this issue.

- 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


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker