--- layout: fc_discuss_archives title: Message 27 from Frama-C-discuss on April 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Question about frama-c behavior on a specific code



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