| View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] |
| ID | Project | Category | View Status | Date Submitted | Last Update |
| 0000820 | Frama-C | Plug-in > Eva | public | 2011-05-11 14:13 | 2011-10-10 14:14 |
|
| Reporter | ddelmas | |
| Assigned To | pascal | |
| Priority | normal | Severity | crash | Reproducibility | always |
| Status | closed | Resolution | fixed | |
| Platform | | OS | | OS Version | |
| Product Version | Frama-C Carbon-20110201 | |
| Target Version | | Fixed in Version | Frama-C Nitrogen-20111001 | |
|
| Summary | 0000820: Value analysis crashes in lib-entry mode with peculiar context |
| Description | A crash occurs with command :
frama-c -val -lib-entry -main F -context-width 1 -context-depth 0 crash_align.c |
| Additional Information | The analysis does not crash with -context-depth 1. |
| Tags | No tags attached. |
|
| Attached Files |  crash_align.c [^] (462 bytes) 2011-05-11 14:13 [Show Content] [Hide Content]typedef unsigned char *MESSAGE_ADDR_TYPE;
void DD_check_alignment
(MESSAGE_ADDR_TYPE /* Array */ /* in out */ MESSAGE_ADDR)
{
if (!( Frama_C_is_base_aligned(MESSAGE_ADDR, 4)
&& Frama_C_offset(MESSAGE_ADDR) % 4 == 0
))
Frama_C_show_each_Alignment("WARNING: address possibly non word aligned", MESSAGE_ADDR);
}
void F
(MESSAGE_ADDR_TYPE * const /* out */ donnees)
{
DD_check_alignment(*donnees);
}
|
|
Relationships 
Relationships