--- layout: fc_discuss_archives title: Message 8 from Frama-C-discuss on March 2009 ---
Hello, Le lun 02 mar 2009 17:27:47 CET, David MENTRE <dmentre at linux-france.org> a ?crit : > > >> First of all, what does exactly mean "No code for function xxxxxx, > >> default assigns generated"? > > > > You can look at ACSL manual, section 2.3.5. The point is that since a > > function like read() has no code given, nor contract, then it could be > > possible that it modifies every location in the heap. So it should be > > given a contract. > > Thank you for the precise reference to ACSL manual. I'll look at it. > Maybe this should be given in the error message? > To be completely clear, the warning says that Frama-C's kernel is generating an assigns clause based on the function prototype, because supposing that every location in the heap might be changed by a function call would prevent the analyses saying something useful. The issue is that this generated clause is not guaranteed to be correct. For instance, given the prototype void f(int* x,int l), there's no way to know if x is a pointer to a single int (which could be assigned l for instance), or to a block of several ints (whose length could be l for instance). It is thus important to review the generated clauses (e.g. with the -print option. They are also visible in the GUI), or better to give an appropriate contract to each prototype which has no associated definition. -- E tutto per oggi, a la prossima volta. Virgile