2021-01-15 18:26 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001621Frama-CPlug-in > wppublic2014-01-24 17:10
Assigned Tocorrenson 
PrioritynormalSeverityminorReproducibilityhave not tried
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




correnson (manager)

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.


correnson (manager)

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
+Issue History