--- layout: fc_discuss_archives title: Message 42 from Frama-C-discuss on November 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] lots of unproved goals for simple example



I should add that I'm getting similar results (mostly unproved goals) for 
*really* trivial examples like below.  Curiously, for each goal either all 
solvers rapidly prove it or else all solvers timeout. I suspect I just 
installed something incorrectly but I don't know how to debug it.

John


#include <stdint.h>

/*@ requires (r > 0) && (r < 32) */
uint32_t rotate_left (uint32_t x, uint32_t r)
{
   return (x << r) | (x >> (32-r));
}