Frama-C Bug Tracking System - Frama-C
View Issue Details
IDProjectCategoryView StatusDate SubmittedLast Update
0001027Frama-CKernel > ACSL implementationpublic2011-11-25 18:342014-02-12 16:58
Reportersignoles 
Assigned Tovirgile 
PrioritynormalSeveritycrashReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Nitrogen-20111001 
Target VersionFixed in VersionFrama-C Oxygen-20120901 
Summary0001027: incompatible types for a correct spec
DescriptionOn the attached file, we get: $ frama-c -jessie max_ok.c File "max_ok.jc", line 53, characters 11-17: typing error: incompatible types: intP[..] and integer Note that the WP plug-in proves this program correct wrt its spec.
Steps To Reproduce
Additional Information
TagsNo tags attached.
Relationships
Attached Filesc max_ok.c (428) 2011-11-25 18:34
https://bts.frama-c.com/file_download.php?file_id=300&type=bug
Issue History
Date ModifiedUsernameFieldChange
2011-11-25 18:34signolesNew Issue
2011-11-25 18:34signolesStatusnew => assigned
2011-11-25 18:34signolesAssigned To => cmarche
2011-11-25 18:34signolesFile Added: max_ok.c
2011-11-28 09:39virgileNote Added: 0002508
2011-11-28 09:39virgileAssigned Tocmarche => virgile
2011-11-28 09:39virgileStatusassigned => confirmed
2011-11-28 09:39virgileCategoryPlug-in > jessie => Kernel > ACSL implementation
2012-01-06 13:20svnCheckin
2012-01-06 13:20svnStatusconfirmed => resolved
2012-01-06 13:20svnResolutionopen => fixed
2012-09-19 17:15signolesFixed in Version => Frama-C Oxygen-20120901
2012-09-19 17:16signolesStatusresolved => closed
2014-02-12 16:58Note Added: 0004691
2014-02-12 16:58Statusclosed => resolved

Notes
(0002508)
virgile   
2011-11-28 09:39   
Arguably, the type-checker should transform assumes r into assumes r != (int *)0 or assumes r != \null instead of simply assumes r != 0 (similarly for assumes !r).
(0004691)
   
2014-02-12 16:58   
Fix committed to stable/neon branch.