--- layout: fc_discuss_archives title: Message 36 from Frama-C-discuss on December 2009 ---
Suppose we have a function foo in a file tst1.c and a header file tst1.h to export that function. I discovered that it is possible to have different contracts for foo in these files. Jessie is able to verify tst1.c from below. Given only the precondition of foo in tst1.h however, the bug hidden in tst1.c can be encountered. In the same vein, a caller relying on the postcondition of foo in tst1.h may receive an a with a==11. Is this a source for nasty bugs? ------------------------------------- // tst1.h /*@ requires 0 <= a <= 11; ensures 0 <= \result <= 10; */ int foo(int a); ------------------------------------- // tst1.c #include "tst1.h" /*@ requires 0 <= a <= 10; ensures 0 <= \result <= 11; */ int foo(int a) { if(a==11) return 1/(a-11); return a; }