--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on February 2010 ---
We have applications where we do arithmetics in GF(2^32). This is easily done with unsigned integers and the standard operations +, *. However, Jessie isn't able to verify arithmetic safety because it doesn't know that we want to compute in GF(2^32). For example, nothing bad can happen in this code const unsigned long m = 0x10000; unsigned int foo(unsigned int a) { return (((a+1) % m) * ((a+1) % m)) % m; } Which is equivalent to unsigned int foo(unsigned int a) { return (a+1)*(a+1); } On a platform that uses 32-bit integers. Is there a way to verify arithmetics in GF(2^32) with Frama-C/Jessie?