2021-01-17 22:50 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001103Frama-CKernelpublic2014-07-11 12:50
Assigned Tovirgile 
PrioritynormalSeverityfeatureReproducibilityhave not tried
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

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



virgile (developer)

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)?


Anne (reporter)

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
+Issue History