Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000614Frama-CPlug-in > jessiepublic2010-10-22 17:182010-10-22 17:18
ReporterJochen 
Assigned Tocmarche 
PrioritynormalSeverityminorReproducibilityalways
StatusassignedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C Boron-20100401 
Target VersionFixed in Version 
Summary0000614: "\valid(&aaa)" unprovable for global variable aaa - missing antecedens in proof obligation?
DescriptionSee attached program. Jessie generates the proof obligation "(FORALL (int_P_alloc_table) (IMPLIES TRUE (<= (offset_min int_P_alloc_table aaa) 0)))" for the assert in line 8, and a similar one for offset_max.
Neither of them can be proved by any automatic prover.

I guess, the reason is that the name "aaa" appears unbound in the conclusions of both obligations, but does not appear anywhere else in the file ftest1_why.sx, so nothing is known (by the provers) about it.

If I make "aaa" a local rather than a global variable, the generated proof obligations look completely different; I feel unable to summarize the differences.
TagsNo tags attached.
Attached Filesc file icon ftest1.c [^] (90 bytes) 2010-10-22 17:18 [Show Content]

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2010-10-22 17:18 Jochen New Issue
2010-10-22 17:18 Jochen Status new => assigned
2010-10-22 17:18 Jochen Assigned To => cmarche
2010-10-22 17:18 Jochen File Added: ftest1.c


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker