Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002248Frama-CKernelpublic2016-10-06 16:112016-12-08 10:16
ReporterJochen 
Assigned Tovirgile 
PrioritynormalSeveritytextReproducibilityalways
StatusassignedResolutionopen 
PlatformOSxubuntuOS Version
Product VersionFrama-C Aluminium 
Target VersionFixed in Version 
Summary0002248: option "-print" prints array upper bound in type before parameter name, rather than after it
DescriptionRunning "frama-c -print ftest.c" on the attached program doesn't reproduce the input program; insteadt, it prints the "[a]" before the "b", not after it.
TagsNo tags attached.
Attached Filesc file icon ftest.c [^] (29 bytes) 2016-10-06 16:11 [Show Content]

- Relationships

-  Notes
(0006269)
yakobowski (manager)
2016-10-07 14:53

The array size information is only stored as a C attribute, pretty-printed in a special way. Displaying it elsewhere is unfortunately not really easy.
(0006308)
yakobowski (manager)
2016-12-08 10:16

After more consideration, I'm not sure anything can be done. We will wait for Virgile's opinion, though.

- Issue History
Date Modified Username Field Change
2016-10-06 16:11 Jochen New Issue
2016-10-06 16:11 Jochen File Added: ftest.c
2016-10-07 14:53 yakobowski Note Added: 0006269
2016-12-08 10:16 yakobowski Assigned To => virgile
2016-12-08 10:16 yakobowski Status new => assigned
2016-12-08 10:16 yakobowski Note Added: 0006308


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker