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] Inout analysis question

  • Subject: [Frama-c-discuss] Inout analysis question
  • From: VICTORIA.MOYALAMIEL at atosorigin.com (MOYA LAMIEL Victoria)
  • Date: Thu, 17 Feb 2011 08:52:56 +0000
Hi,

I have the following program :
extern int f_1(const int NbOct);

int main
(int * const taille)
{
  int ret;

  *taille=0;

  if (*taille) return -2;

  if (f_1(*taille)) return -1;

  return 0;
}
and I'm interested in the formal parameter named "taille" which is written then read.

If we use the first if clause in the program :
    if (*taille) return -2;
    we get this Inout analysis :
[kernel] preprocessing with "gcc -C -E -I.  test_I.c"
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
[value] Recording results for main
[value] done for function main
[inout] Out (external) for function main:
          S_taille[0]
[inout] computing for function main
[inout] done for function main
[inout] InOut (with formals) for function main:
        Operational inputs: taille
        Operational inputs on termination: taille
        Sure outputs: S_taille[0]
[inout] Inputs (with formals) for function main:
          taille; S_taille[0]
where our formal parameter is considered as an imperative input but not an operational one.

If we replace the first if clause by the second one :
    if (f_1(*taille)) return -1;
    we get a different analysis :
[kernel] preprocessing with "gcc -C -E -I.  test_I.c"
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
[value] computing for function f_1 <-main.
        Called from test_I.c:10.
[kernel] No code for function f_1, default assigns generated
[value] Done for function f_1
[value] Recording results for main
[value] done for function main
[inout] Out (external) for function main:
          S_taille[0]
[inout] computing for function main
[inout] computing for function f_1 <-main
[inout] done for function f_1
[inout] done for function main
[inout] InOut (with formals) for function main:
        Operational inputs: taille; S_taille[0]
        Operational inputs on termination: taille; S_taille[0]
        Sure outputs: S_taille[0]
[inout] Inputs (with formals) for function main:
          taille; S_taille[0]
In this last case, the formal parameter is considered as an operational input as well as an imperative one.

Could someone explain to me the difference between these two behaviours, please?

The used Frama-C version is " Carbon-20110201" and the command line in both cases "frama-c -context-valid-pointers -input-with-formals -inout-with-formals -out-external test_I.c".

I have attached the tested C file.

Thanks in advance,

Victoria
--



[ATOS ORIGIN LOGO] <http://www.fr.atosorigin.com/fr-fr/>

MOYA LAMIEL Victoria
Ing?nieur en Informatique - Atos Origin Integration
Les espaces Saint-Martin - Bureau 2A24
6, Impasse Alice Guy
31024 Toulouse Cedex 03 - France
Telephone : +33 (0)5 34 36 33 36
Fax : +33 (0)5 34 36 37 00

mailto : victoria.moyalamiel at atosorigin.com<mailto:victoria.moyalamiel at atosorigin.com>
www.atosorigin.fr<http://www.atosorigin.fr>


D?veloppement durable, anticipons pour notre avenir / Sustainability, advance our future
* N'imprimez ce mail que si n?cessaire / Please consider your environmental responsibility before printing this e-mail.

Ce message et les pi?ces jointes sont confidentiels et r?serv?s ? l'usage exclusif de ses destinataires. Il peut ?galement ?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 le d?truire. L'int?grit? du message ne pouvant ?tre assur?e sur Internet, la responsabilit? du groupe Atos Origin ne pourra ?tre recherch?e quant au contenu de ce message. Bien que les meilleurs efforts soient faits pour maintenir cette transmission exempte de tout virus, l'exp?diteur ne donne aucune garantie ? cet ?gard et sa responsabilit? ne saurait ?tre recherch?e pour tout dommage r?sultant d'un virus transmis.

This e-mail and the documents attached are confidential and intended solely for the addressee; it may also be privileged. If you receive this e-mail in error, please notify the sender immediately and destroy it. As its integrity cannot be secured on the Internet, the Atos Origin group liability cannot be triggered for the message content. Although the sender endeavours 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/20110217/a802f277/attachment-0001.htm>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: ao_ioc_sign_dyn.gif
Type: image/gif
Size: 44969 bytes
Desc: ao_ioc_sign_dyn.gif
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20110217/a802f277/attachment-0001.gif>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: test_I.c
Type: text/x-csrc
Size: 184 bytes
Desc: test_I.c
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20110217/a802f277/attachment-0001.c>