Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] don't want unitialized padding fields, -initialized-padding-globals

Hello David,

1/ The reason is that I'm checking uninitialized var usage with Frama-C and uninitialized fields in padding are source of false alarms in that usage.

2/ Thank you for the tip
It is correct and works on small variable:
        Before this statement:
         G2.a[0..2] IN [--..--]
           .[bits 24 to 31] IN UNINITIALIZED
           .b IN [--..--]
        After this statement:
         G2 IN [--..--]

But not on larger variable:

        After this statement:
         Gtab1[0].a[0..2] IN [--..--]
              [0].[bits 24 to 31] IN [--..--] or UNINITIALIZED
              {[0].b; [1].a[0..2]} IN [--..--]

Here is the example:

typedef struct {
  char a[3];
  int b;
} T_S1;

typedef T_S1 T_T1[1000];

T_T1 Gtab1;
T_S1 G2;

void f1(T_S1* p1)
{
  Frama_C_make_unknown(Gtab1, sizeof(T_T1)); // NOK
  Frama_C_make_unknown(&G2, sizeof(T_S1));  // OK
}

Regards,

St?phane


-----Original Message-----
From: Frama-c-discuss [mailto:frama-c-discuss-bounces at lists.gforge.inria.fr] On Behalf Of David MENTRE
Sent: Thursday, November 06, 2014 10:43 AM
To: frama-c-discuss at lists.gforge.inria.fr
Subject: Re: [Frama-c-discuss] don't want unitialized padding fields, -initialized-padding-globals

Hello,

Le 05/11/2014 21:57, DUPRAT, STEPHANE a ?crit :
> I don?t want the padding fields of structs in global variable at
> uninitialized state.

Out of curiosity, why?

> I?m also using the option -initialized-padding-globals, but these
> uninitialized fields are still remaining (Neon release).
> Is there a workaround to have the entire location at  [--..--] ? Even
> for very large variables ?

A possible workaround: initialize your global variables in the analysis driver using following function:

"""
extern int Frama_C_entropy_source;

/*@ requires \valid(p + (0 .. l-1));
     assigns p[0 .. l-1] \from Frama_C_entropy_source;
     assigns Frama_C_entropy_source \from Frama_C_entropy_source;
     ensures \initialized(p + (0 .. l-1)); */ void Frama_C_make_unknown(char *p, size_t l); """

For example "Frama_C_make_unknown(&my_var, 32);".

I hope it helps,
Best regards,
david

_______________________________________________
Frama-c-discuss mailing list
Frama-c-discuss at lists.gforge.inria.fr
http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
Ce message et toutes les pi?ces jointes (ci-apr?s le "message") sont ?tablis ? l?intention exclusive des destinataires d?sign?s. Il contient des informations confidentielles et pouvant ?tre prot?g? par le secret professionnel. Si vous recevez ce message par erreur, merci d'en avertir imm?diatement l'exp?diteur et de d?truire le message. Toute utilisation de ce message non conforme ? sa destination, toute diffusion ou toute publication, totale ou partielle, est interdite, sauf autorisation expresse de l??metteur. L'internet ne garantissant pas l'int?grit? de ce message lors de son acheminement, Atos (et ses filiales) d?cline(nt) toute responsabilit? au titre de son contenu. Bien que ce message ait fait l?objet d?un traitement anti-virus lors de son envoi, l??metteur ne peut garantir l?absence totale de logiciels malveillants dans son contenu et ne pourrait ?tre tenu pour responsable des dommages engendr?s par la transmission de l?un d?eux.

This message and any attachments (the "message") are intended solely for the addressee(s). It contains confidential information, that may be privileged. If you receive this message in error, please notify the sender immediately and delete the message. Any use of the message in violation of its purpose, any dissemination or disclosure, either wholly or partially is strictly prohibited, unless it has been explicitly authorized by the sender. As its integrity cannot be secured on the internet, Atos and its subsidiaries decline any liability for the content of this message. Although the sender endeavors to maintain a computer virus-free network, the sender does not warrant that this transmission is virus-free and will not be liable for any damages resulting from any virus transmitted.