Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000841Frama-CKernel > ACSL implementationpublic2011-05-27 16:132011-10-10 14:14
ReporterJochen 
Assigned Tovirgile 
PrioritynormalSeveritytweakReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Carbon-20110201 
Target VersionFixed in VersionFrama-C Nitrogen-20111001 
Summary0000841: no conversion int[] to int* for logic fct arg; exprs a and &a[0] treated differently
DescriptionIn the attached program, the logic function p expects an int* argument.

When supplied the int[] argument (a), the kernel reports a user error (line 8), which is at least unfamiliar to C programmers.

Supplying the argument (&a[0]) causes no error message (line 7).
TagsNo tags attached.
Attached Filesc file icon ftest.c [^] (135 bytes) 2011-05-27 16:13 [Show Content]

- Relationships

-  Notes
(0001989)
virgile (developer)
2011-06-22 13:47

ACSL states specifically that a conversion from a C array to a pointer must be done explicitly (either through a cast or by taking the address of the first element). I'll change the error message to a more specific one in this case.

- Issue History
Date Modified Username Field Change
2011-05-27 16:13 Jochen New Issue
2011-05-27 16:13 Jochen File Added: ftest.c
2011-05-27 16:50 signoles Status new => assigned
2011-05-27 16:50 signoles Assigned To => virgile
2011-05-27 16:50 signoles Category Kernel => Kernel > ACSL implementation
2011-06-15 20:07 monate Status assigned => acknowledged
2011-06-22 13:47 virgile Note Added: 0001989
2011-06-22 14:12 svn Checkin
2011-06-22 14:12 svn Status acknowledged => resolved
2011-06-22 14:12 svn Resolution open => fixed
2011-10-10 14:13 signoles Fixed in Version => Frama-C Nitrogen-20111001
2011-10-10 14:14 signoles Status resolved => closed


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker