--- layout: fc_discuss_archives title: Message 3 from Frama-C-discuss on November 2010 ---
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 >