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
Assigned Tocmarche 
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, 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 - 2020 MantisBT Team
Powered by Mantis Bugtracker