--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on February 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Arithmetics in finite fields



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?