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: julien.izquierdo at gmail.com (Julien Izquierdo)
  • Date: Wed, 10 Apr 2013 11:52:20 +0200
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