Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002041Frama-CPlug-in > wppublic2014-12-28 10:052015-06-29 17:26
Reporterjens 
Assigned Tocorrenson 
PrioritynormalSeverityminorReproducibilityalways
StatusacknowledgedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C Neon-20140301 
Target VersionFixed in Version 
Summary0002041: unable to use lemma separated_region
DescriptionI am using two Frama-C installation:

1.) Neon-20140301 installed through opam under OS X
2.) Neon-20140301+dev-stance manually installed under Linix

In both installations the lemma separated_region in file FRAMAC_SHARE/wp/coqwp/Memory.v
is unaccessible because it is put in comments.
I suspect that this is the reason why I cannot prove that a local struct variable is separated from one
that a function receives as an argument.

What is the reason that this lemma is not available?
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0005966)
correnson (manager)
2015-06-29 17:23

Thanks for report. I will investigate.

- Issue History
Date Modified Username Field Change
2014-12-28 10:05 jens New Issue
2014-12-28 10:05 jens Status new => assigned
2014-12-28 10:05 jens Assigned To => correnson
2015-06-29 17:23 correnson Note Added: 0005966
2015-06-29 17:26 correnson Status assigned => acknowledged


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker