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:442019-10-17 17:58
Reportervisq 
Assigned Tocorrenson 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionwon't fix 
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
(0006897)
correnson (manager)
2019-10-17 16:24
edited on: 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.

- 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


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker