Frama-C-discuss mailing list archives

stephane.duprat at atos.net (DUPRAT, STEPHANE) · Mon, 17 Nov 2014 11:43:02 +0000

Hello,

Thank you Boris for the explanations.
To make progress on our process we are modifying struct definitions to make disappear these padding elts.

Regard,

St?phane

From: Frama-c-discuss [mailto:frama-c-discuss-bounces at lists.gforge.inria.fr] On Behalf Of Boris Yakobowski
Sent: Friday, November 14, 2014 2:23 PM
To: Frama-C public discussion
Subject: Re: [Frama-c-discuss] don't want unitialized padding fields, -initialized-padding-globals

Hello St?phane,

Is there a workaround to have the entire location at  [--..--] ? Even for very large variables ?

Not currently. There is an upper limit on the number of bytes that can be initialized using a specification, to avoid problematic analysis time.

Hello Pascal,

You example is also working well also on my side.

But the result is different with these options:

The difference you observe is due to option -lib-entry. Padding bits in the initial state are handled in very different ways, depending on whether -lib-entry is set or not. We are aware of the current semantics, which may indeed be problematic for some use cases. There have been some changes in the way padding bits are treated in the Sodium version of Frama-C, but only when copying structs.

Hope this helps,

On Thu, Nov 13, 2014 at 11:27 PM, DUPRAT, STEPHANE <stephane.duprat at atos.net<mailto:stephane.duprat at atos.net>> wrote:
Hello,

Shall I post this to the tracker ?

St?phane

From: Frama-c-discuss [mailto:frama-c-discuss-bounces at lists.gforge.inria.fr<mailto:frama-c-discuss-bounces at lists.gforge.inria.fr>] On Behalf Of DUPRAT, STEPHANE
Sent: Thursday, November 06, 2014 2:33 PM

To: Frama-C public discussion
Subject: Re: [Frama-c-discuss] don't want unitialized padding fields, -initialized-padding-globals

Hello Pascal,

You example is also working well also on my side.

But the result is different with these options:

frama-c -val t.c -main f1 -val-warn-copy-indeterminate @all -pp-annot -no-val-show-initial-state -initialized-padding-globals -lib-entry -no-unicode -continue-annot-error -context-valid-pointers -context-depth 2 -context-width 1 -val-print-callstacks -slevel 400

[value] ====== VALUES COMPUTED ======
[value] Values at end of function f1:
  Frama_C_entropy_source IN [--..--]
  Gtab1[0].a[0..2] IN [--..--]
       [0].[bits 24 to 31] IN [--..--] or UNINITIALIZED
       {[0].b; [1].a[0..2]} IN [--..--]
       [1].[bits 24 to 31] IN [--..--] or UNINITIALIZED
       {[1].b; [2].a[0..2]} IN [--..--]

Regards,

St?phane

From: Frama-c-discuss [mailto:frama-c-discuss-bounces at lists.gforge.inria.fr] On Behalf Of Pascal Cuoq
Sent: Thursday, November 06, 2014 1:25 PM
To: Frama-C public discussion
Subject: Re: [Frama-c-discuss] don't want unitialized padding fields, -initialized-padding-globals

It works for me. Did you provide the specification for Frama_C_make_unknown that David gave? It doesn't work if it's not provided.

~ $ cat t.c

int Frama_C_entropy_source;

typedef unsigned long size_t;

/*@ 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);

typedef struct {

  char a[3];

  int b;

} T_S1;

typedef T_S1 T_T1[1000];

T_T1 Gtab1;

T_T1 Gtab_witness;

T_S1 G2;

void f1(T_S1* p1)

{

  Frama_C_make_unknown(Gtab1, sizeof(T_T1));

  Frama_C_make_unknown(&G2, sizeof(T_S1));

  Frama_C_dump_each();

}

~ $ frama-c -val t.c -main f1

?

[value] DUMPING STATE of file t.c line 27

        Frama_C_entropy_source ? [--..--]

        Gtab1[0..999] ? [--..--]

        Gtab_witness[0..999] ? {0}

        G2 ? [--..--]

        p1 ? {‌{ NULL ; &S_p1[0] }‌}

        S_p1[0].a[0..2] ? [--..--]

            [0].[bits 24 to 31] ? UNINITIALIZED

            {[0].b; [1].a[0..2]} ? [--..--]

            [1].[bits 24 to 31] ? UNINITIALIZED

            [1].b ? [--..--]

        =END OF DUMP==

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

_______________________________________________
Frama-c-discuss mailing list
Frama-c-discuss at lists.gforge.inria.fr<mailto:Frama-c-discuss at lists.gforge.inria.fr>
http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss

--
Boris
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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20141117/e02cd7c3/attachment-0001.html>