2021-01-15 15:54 CET
  

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000655Frama-CKernel > ACSL implementationpublic2010-12-25 19:052014-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)

2010-12-27 12:17

 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)

2011-02-09 14:52

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

~0001473

correnson (manager)

2011-02-10 15:14

 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)

2011-05-06 17:26

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

~0004795

2014-02-12 16:59

 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