Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000655Frama-CKernel > ACSL implementationpublic2010-12-25 19:052014-02-12 16:59
Reporterevdenis 
Assigned Tovirgile 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
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 Filesc file icon max.c [^] (233 bytes) 2010-12-25 19:05 [Show Content]

- 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.

- 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 Checkin
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 Checkin
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
2014-02-12 16:59 Note Added: 0004795
2014-02-12 16:59 Status closed => resolved


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker