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: kerstin.hartig at first.fraunhofer.de (Kerstin Hartig)
  • Date: Wed, 27 Oct 2010 16:52:58 +0200
Hello,

I've got a question regarding the message you sometimes get when running
Jessie:
"No code for function <name>, default assigns generated"

As I experienced it also occurs even if the implementation and specification
(including assigns clauses) of the function are known.
As an example:

/*@
  requires IsValidStack(s);
  ensures  IsValidStack(s);

  behavior not_empty:
    assumes !IsEmptyStack(s);
    assigns s->size;
    ensures SizeOfStack(s) == SizeOfStack{Old}(s) - 1;
    ensures !IsFullStack(s);

  behavior empty:
    assumes IsEmptyStack(s);
    assigns \nothing;

  complete behaviors;
  disjoint behaviors;
*/
void stack_pop(Stack* s);


To get rid of this message I can add another assigns (the line
assigns s->size;) above the behaviors and actually remove the assigns from
the behavior not_empty. 

I wonder if this is how assigns clauses should ideally be used and what is
good or bad practice.
Is it like that: even if there are 2 behaviors that should (are required to)
be complete and disjoint and each one has an assigns clause, still
completeness can not be assumed and that's why a default assigns for
possible other behaviors needs to be generated?

Does the generated default assigns mean that everything may be modified?
Is it bad practice and even dangerous to split assigns to the behaviors like
in the example above?

Thank you in advance,
Kind Regards,
Kerstin