Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001621Frama-CPlug-in > wppublic2014-01-20 09:572014-01-24 17:10
ReporterAnne 
Assigned Tocorrenson 
PrioritynormalSeverityminorReproducibilityhave not tried
StatusacknowledgedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C Fluorine-20130601 
Target VersionFixed in Version 
Summary0001621: loop invariant as hypothesis
DescriptionNot sure if this is a bug or the intended behavior, but I am surprised that on the example below, I get: [wp] [Alt-Ergo] Goal typed_f_loop_inv_l_nbits_established : Unknown It seems that the loop invariant l_wsize is not used as an hypothesis ?
Steps To Reproducevoid f (unsigned int wsize) { unsigned int nbits = 0; /*@ loop invariant l_wsize: wsize == 4 || wsize == 5 || wsize == 6; @ loop invariant l_nbits: 0 <= nbits < wsize; */ for(int i = 0; i < 10; i++) { } }
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0004445)
correnson (manager)
2014-01-24 16:11

Ha ha ! It is both a bug and a feature ;-) Using model Dump, you can see the following: 1. I_nbits is used for an hypothesis on establishment for I_wsize 2. preservation of I_nbits and I_wsize are proved separately For 1, it is a bug : the list of invariants comes in reverse direction. For 2, it is a (kind of) feature. Actually, it is sound to prove preservation of an invariant by assuming the previous ones. But we deactivate it since a false invariant makes everything apparently proved (but the false one). Obviously, we can improve these behaviors.
(0004446)
correnson (manager)
2014-01-24 16:11

Feature wish

- Issue History
Date Modified Username Field Change
2014-01-20 09:57 Anne New Issue
2014-01-20 09:57 Anne Status new => assigned
2014-01-20 09:57 Anne Assigned To => correnson
2014-01-24 16:11 correnson Note Added: 0004445
2014-01-24 16:11 correnson Note Added: 0004446
2014-01-24 16:11 correnson Status assigned => acknowledged


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker