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

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.

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:20svn
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
2013-12-19 01:11Source_changeset_attached => framac master 06b8e72d
2014-02-12 16:54Source_changeset_attached => framac stable/neon 06b8e72d
2014-02-12 16:58Note Added: 0004691
2014-02-12 16:58Statusclosed => resolved