2021-01-15 15:54 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000655Frama-CKernel > ACSL implementationpublic2014-02-12 16:59
Reporterevdenis 
Assigned Tovirgile 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
Product VersionFrama-C Boron-20100401 
Target VersionFixed in VersionFrama-C Nitrogen-20111001 
Summary0000655: using real function ( \max, \min, \abs ) instead of integer one in function contract
Description/*@
  @ ensures \result == \max( a, b );
  @ ensures \result != \min( a, b );
  @ ensures a == \abs( a );
  @*/
unsigned int
max( unsigned int a, unsigned int b )
{
    int i = a > b ? a : b;
    //@ assert i == \max( a, b );
    return i;
}

Jessie output:
uint32 max(uint32 a, uint32 b)
behavior default:
  ensures (C_8 : ((C_9 : (\result == \real_max(a, b))) &&
                   ((C_11 : (\result != \real_min(a, b))) &&
                     (C_12 : (a == \real_abs(a))))));


I don't know exactly is it a bug or a feature.
TagsNo tags attached.
Attached Files
  • c file icon max.c (233 bytes) 2010-12-25 19:05 -
    /*@
      @ ensures \result == \max( a, b );
      @ ensures \result != \min( a, b );
      @ ensures a == \abs( a );
      @*/
    unsigned int
    max( unsigned int a, unsigned int b )
    {
    	int i = a > b ? a : b;
    	//@ assert i == \max( a, b );
    	return i;
    }
    
    c file icon max.c (233 bytes) 2010-12-25 19:05 +

-Relationships
+Relationships

-Notes

~0001358

virgile (developer)

This is a bug. The problem lies in type-checking the ACSL annotation, not in the Jessie translation itself. It seems to be partially solved in Carbon-beta and svn, but in some cases overloading resolution still chooses real instead of integer.

~0001471

virgile (developer)

I don't know why this bug was marked as resolved, but this is not the case in Carbon-20110201

~0001473

correnson (manager)

I made a mistake at commit (655 instead of ...)
655 was not closed immediately, and I thought it is an error in svn+bts synchro ...
Sorry !

~0001850

virgile (developer)

It seems that the first occurrence of \max gets correctly type-checked, but not the later ones.

~0004795

Fix committed to stable/neon branch.
+Notes

-Issue History
Date Modified Username Field Change
2010-12-25 19:05 evdenis New Issue
2010-12-25 19:05 evdenis Status new => assigned
2010-12-25 19:05 evdenis Assigned To => cmarche
2010-12-25 19:05 evdenis File Added: max.c
2010-12-27 12:17 virgile Note Added: 0001358
2010-12-27 12:17 virgile Assigned To cmarche => virgile
2010-12-27 12:17 virgile Status assigned => confirmed
2010-12-27 12:17 virgile Category Plug-in > jessie => Kernel > ACSL implementation
2011-02-01 16:47 svn
2011-02-01 16:47 svn Status confirmed => resolved
2011-02-01 16:47 svn Resolution open => fixed
2011-02-09 14:36 signoles Status resolved => closed
2011-02-09 14:37 signoles Fixed in Version => Frama-C Carbon-20110201
2011-02-09 14:52 virgile Note Added: 0001471
2011-02-09 14:52 virgile Status closed => feedback
2011-02-09 14:52 virgile Resolution fixed => reopened
2011-02-09 14:52 virgile Status feedback => confirmed
2011-02-09 15:57 signoles Fixed in Version Frama-C Carbon-20110201 =>
2011-02-10 15:14 correnson Note Added: 0001473
2011-05-06 17:26 virgile Note Added: 0001850
2011-05-08 18:32 svn
2011-05-08 18:32 svn Status confirmed => resolved
2011-05-08 18:32 svn Resolution reopened => fixed
2011-10-10 14:13 signoles Fixed in Version => Frama-C Nitrogen-20111001
2011-10-10 14:14 signoles Status resolved => closed
2013-12-19 01:12 Source_changeset_attached => framac master e304c4b9
2013-12-19 01:12 correnson Source_changeset_attached => framac master 9d5b1fc2
2014-02-12 16:54 Source_changeset_attached => framac stable/neon e304c4b9
2014-02-12 16:55 correnson Source_changeset_attached => framac stable/neon 9d5b1fc2
2014-02-12 16:59 Note Added: 0004795
2014-02-12 16:59 Status closed => resolved
+Issue History