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);
}