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] Jessie - "No code for function <name>, default assigns generated"

  • Subject: [Frama-c-discuss] Jessie - "No code for function <name>, default assigns generated"
  • From: Patrick.Baudin at cea.fr (BAUDIN Patrick)
  • Date: Fri, 05 Nov 2010 15:08:44 +0100
  • In-reply-to: <4CD27DA7.2070100@cea.fr>
  • References: <42050C88D59E144CA358159FF0E6018B090670@TITAN.first.fraunhofer.de> <EFF6534C8F2FC940A9D7929433E12D4E216F70@TITAN.first.fraunhofer.de> <4CD27DA7.2070100@cea.fr>
Hello,

Today, Frama-C kernel generates assigns clauses from the prototype (for 
function without code).
To do nothing is equivalent to virtualy generate "assigns everything".
That is not good for some static analysis (such as Value analysis).
When behaviors are completes and each of them has an assigns clause,
it is possible to generate a more restrictive clause (than "assigns 
everything"), but still correct:
"assigns locs;"
where "locs" is the union of the locations assigned by all behaviors of 
the complete clause.

With your exemple, the clause "assigns *b" can be added to the default 
behavior.
requires \valid(b);
behavior positive:
assumes a > 0;
assigns *b;
ensures *b == 0;
behavior not_positive:
assumes a <= 0;
assigns \nothing;
complete behaviors;
disjoint behaviors;
*/ void foo(int a, int* b);

I will do this modification into the kernel of Frama-C soon.

Regards,
Patrick Baudin

> Hello,
> Since your behaviors are completes and each of them has an assigns 
> clause,
> the kernel of Frama-C shouldn't generate any more assigns.
> The generation of default assigns for function foo can be considered 
> as a bug.
> Feels free to add it into the BTS of Frama-C.
> Regards,
> Patrick
>