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] Help with -wp-init-const and static evaluation of constants

  • Subject: [Frama-c-discuss] Help with -wp-init-const and static evaluation of constants
  • From: rod at proteancode.com (Roderick Chapman)
  • Date: Wed, 17 Jul 2019 17:00:00 +0100
Seeking help again... consider the following code:

include <stddef.h>

static const size_t c1 = 300;
static const size_t c2 = c1 + 1;

size_t f (size_t y)
{
   size_t tmp2 = (y / c2);
   return tmp2;
}

Using Frama-C 19, I find that

frama-c -wp -wp-rte -wp-init-const

does _not_ prove that c2 != 0 in the division operator.  Why not? Is it 
not able to deduce that c2 == 301? This seems like a rather strange this 
not to do.

Secondly, can anyone explain the exact meaning of -wp-init-const please? 
There appears to be no mention of it at all in the 19.0 WP manual...

Many thanks,

  Rod


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20190717/9591c74c/attachment.html>