View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | ||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|
0001103 | Frama-C | Kernel | public | 2012-02-22 09:52 | 2014-07-11 12:50 | ||||||||
Reporter | Anne | ||||||||||||
Assigned To | virgile | ||||||||||||
Priority | normal | Severity | feature | Reproducibility | have not tried | ||||||||
Status | assigned | Resolution | open | ||||||||||
Product Version | |||||||||||||
Target Version | Fixed in Version | ||||||||||||
Summary | 0001103: Default @requires property for the [main] function | ||||||||||||
Description | I think that it would be great to generate a default @requires property for the 'main' function, wouldn't it ? | ||||||||||||
Additional Information | The one from [tests/aorai/test_recursion1.c] for instance seems ok. | ||||||||||||
Tags | No tags attached. | ||||||||||||
Attached Files |
|
![]() |
||||||
|
![]() |
|
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)? |
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. |
![]() |
|||
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 |