Benjamin, On Thu, Aug 27, 2009 at 07:49:18PM +0200, Benjamin Monate wrote: > Indeed Frama-C is meant to be able to handle the case you mention. > We had to preserve some informations about the possibly undefined > behaviours coming from the original code. They one has to prove that > these behaviours never occur.
Since you seem to have mastered the Standard far beyond what I managed, would you mind explaining why the behavior is indeed undefined in the cases discussed above? I read the relevant sections over and over for at least an hour and couldn't be convinced by either conclusion (defined or undefined): I found half a dozen potential "undefined behavior" related to "++", assignments and sequence points, but no one is obvious here. In other words, are you positive that CIL is not wrong here, or do we indeed have a bug? Thanks in advance. Regards, -- Gabriel Kerneis ------------------------------------------------------------------------------ Let Crystal Reports handle the reporting - Free Crystal Reports 2008 30-Day trial. Simplify your report design, integration and deployment - and focus on what you do best, core application coding. Discover what's new with Crystal Reports now. http://p.sf.net/sfu/bobj-july _______________________________________________ CIL-users mailing list CIL-users@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/cil-users
