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] Question about frama-c behavior on a specific code

  • Subject: [Frama-c-discuss] Question about frama-c behavior on a specific code
  • From: virgile.prevosto at m4x.org (Virgile Prevosto)
  • Date: Wed, 10 Apr 2013 15:36:14 +0200
  • In-reply-to: <CANCfvvA-9fs=VrQVCgGRrdciDrJRdQ+djzCdYZJ3+EUX6-UODw@mail.gmail.com>
  • References: <CANCfvvA-9fs=VrQVCgGRrdciDrJRdQ+djzCdYZJ3+EUX6-UODw@mail.gmail.com>
Hello Julien

2013/4/10 Julien Izquierdo <julien.izquierdo at gmail.com>:

>
> GLvoid glColor3f(
>                  GLfloat par_f_red,
>                  GLfloat par_f_green,
>                  GLfloat par_f_blue
>                  )
> {
>    Typ_r_gl_color *loc_pr_color;
>
>     if( par_f_red < 0.0f )
>     {
>         par_f_red = 0.0f;
>     }
>
>     loc_pr_color          = &mogpr_current_context->r_sendable_states.r_color;
>     loc_pr_color->f_red   = par_f_red;
>     loc_pr_color->f_alpha = 1.0f;
>     mogpr_current_context->r_flushable_states.b_color = GL_TRUE;
> }
>
> Setting the if block in comments, there are 3 VCs generated on offset
> of mogpr_current_context and loc_pr_color.
> I do not understand why the "if block" leads to 3 news VCs, and why
> there are quite similar to the first 3 VCs generated.
> I dont see how the if instruction of par_f_red could have an impact on
> offset of mogpr_current_context.

That's normal. In its default setting, for each annotation to prove
(ensures, assertion, ...) Jessie/Why will generate one proof
obligation per possible execution path, so that each 'if' will double
the number of proof obligations. You may want to have a look at
-fast-wp option of Why for a  strategy  generating fewer (but more
complex) proof obligations.

Best regards
--
E tutto per oggi, a la prossima volta
Virgile