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 <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