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