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

[Frama-c-discuss] JessieIntegerModel question



Ok, one more question, hopefully smarter than the last one.

If I understand correctly, Jessie's three integer models are:

- math -- infinite range
- modulo -- both signed and unsigned behave as if two's complement
- strict -- no overflow permitted

The problem is that none of these is a match for C. In C, unsigned 
integers follow the modulo rules and signed integers follow the strict 
rules. Is there a way to get the C integer model in Jessie?  Otherwise 
it seems like I might be stuck with some strange tradeoffs.

Thanks,

John Regehr