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] Assumes got status invalid

  • Subject: [Frama-c-discuss] Assumes got status invalid
  • From: divya84 at gmail.com (Divya Muthukumaran)
  • Date: Mon, 16 Jul 2018 11:34:15 +0100
Hello,

While performing impact analysis on nginx, I get a result saying that the
function where I have the impact pragma *ngx_alloc* is unreachable. So I
looked at the output and see lots of `got status invalid` messages for
preconditions. This is the first one of those messages.

[value] src/core/ngx_times.c:91:

  function gettimeofday, behavior tz_not_null: assumes got status invalid;
behavior not evaluated

When I look inside frama-c/libc/sys/time.h I see four behaviours defined
for the `getttimeofday` functions which should be the complete
specification for the `tz` and `tv` values, so I don't understand what
`assumes got invalid` here means. Could you please explain this? Hopefully,
this will also help me understand the others that follow.

Thanks,
Divya
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20180716/a1ae0c13/attachment.html>