Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
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.
Attached Filesc file icon max_ok.c [^] (428 bytes) 2011-11-25 18:34 [Show Content]

- Relationships

-  Notes
(0002508)
virgile (developer)
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 Modified Username Field Change
2011-11-25 18:34 signoles New Issue
2011-11-25 18:34 signoles Status new => assigned
2011-11-25 18:34 signoles Assigned To => cmarche
2011-11-25 18:34 signoles File Added: max_ok.c
2011-11-28 09:39 virgile Note Added: 0002508
2011-11-28 09:39 virgile Assigned To cmarche => virgile
2011-11-28 09:39 virgile Status assigned => confirmed
2011-11-28 09:39 virgile Category Plug-in > jessie => Kernel > ACSL implementation
2012-01-06 13:20 svn Checkin
2012-01-06 13:20 svn Status confirmed => resolved
2012-01-06 13:20 svn Resolution open => fixed
2012-09-19 17:15 signoles Fixed in Version => Frama-C Oxygen-20120901
2012-09-19 17:16 signoles Status resolved => closed
2014-02-12 16:58 Note Added: 0004691
2014-02-12 16:58 Status closed => resolved


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker