--- layout: fc_discuss_archives title: Message 3 from Frama-C-discuss on November 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Jessie - "No code for function <name>, default assigns generated"



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
>