Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001103Frama-CKernelpublic2012-02-22 09:522014-07-11 12:50
ReporterAnne 
Assigned Tovirgile 
PrioritynormalSeverityfeatureReproducibilityhave not tried
StatusassignedResolutionopen 
PlatformOSOS Version
Product Version 
Target VersionFixed in Version 
Summary0001103: Default @requires property for the [main] function
DescriptionI think that it would be great to generate a default @requires property for the 'main' function, wouldn't it ?
Additional InformationThe one from [tests/aorai/test_recursion1.c] for instance seems ok.
TagsNo tags attached.
Attached Files

- Relationships
related to 0001831closedsignoles Command line arguments (argc/argv) are not marked as valid 

-  Notes
(0002722)
virgile (developer)
2012-02-23 10:40

I guess that you mean that the main function should have as requires the fact that globals are initialized to 0 (provided we're not in -lib-entry mode)?
(0002723)
Anne (reporter)
2012-02-23 12:07

No, not exactly. As I said, it is more about argc and argv like in the file [tests/aorai/test_recursion1.c] for instance.

- Issue History
Date Modified Username Field Change
2012-02-22 09:52 Anne New Issue
2012-02-22 15:11 signoles Status new => assigned
2012-02-22 15:11 signoles Assigned To => virgile
2012-02-23 10:40 virgile Note Added: 0002722
2012-02-23 12:07 Anne Note Added: 0002723
2014-07-11 12:27 yakobowski Relationship added related to 0001831


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker