--- layout: fc_discuss_archives title: Message 24 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,

I am a beginner in Frama-C and I have a question on VCs generation by
Frama-C/Jessie on a short source code:
I am using Frama-C Boron version with Jessie on Windows XP operating system.

My source code is following:

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.

For information mogpr_current_context is a pointer on structure of
structures quite complex.

Thanks for your idea

Best regards