--- layout: fc_discuss_archives title: Message 24 from Frama-C-discuss on April 2013 ---
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