2021-02-24 19:07 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000820Frama-CPlug-in > Evapublic2011-10-10 14:14
Reporterddelmas 
Assigned Topascal 
PrioritynormalSeveritycrashReproducibilityalways
StatusclosedResolutionfixed 
Product VersionFrama-C Carbon-20110201 
Target VersionFixed in VersionFrama-C Nitrogen-20111001 
Summary0000820: Value analysis crashes in lib-entry mode with peculiar context
DescriptionA crash occurs with command :
frama-c -val -lib-entry -main F -context-width 1 -context-depth 0 crash_align.c
Additional InformationThe analysis does not crash with -context-depth 1.
TagsNo tags attached.
Attached Files
  • c file icon crash_align.c (462 bytes) 2011-05-11 14:13 -
    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);
    }
    
    c file icon crash_align.c (462 bytes) 2011-05-11 14:13 +

-Relationships
+Relationships

-Notes

~0001867

pascal (reporter)

Fixed by commit 13394
+Notes

-Issue History
Date Modified Username Field Change
2011-05-11 14:13 ddelmas New Issue
2011-05-11 14:13 ddelmas Status new => assigned
2011-05-11 14:13 ddelmas Assigned To => pascal
2011-05-11 14:13 ddelmas File Added: crash_align.c
2011-05-11 14:17 pascal Note Added: 0001867
2011-05-11 14:17 pascal Status assigned => resolved
2011-05-11 14:17 pascal Resolution open => fixed
2011-10-10 14:13 signoles Fixed in Version => Frama-C Nitrogen-20111001
2011-10-10 14:14 signoles Status resolved => closed
2018-01-12 14:26 signoles Category Plug-in > value analysis => Plug-in > Eva
+Issue History