| 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 |
| ||||||||||||
 Relationships |
||||||
|
||||||
 Relationships |
| Notes |
|
|
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. |
| Notes |
| 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 |