Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Different contracts in declaration and implementation

  • Subject: [Frama-c-discuss] Different contracts in declaration and implementation
  • From: Boris.Hollas at de.bosch.com (Hollas Boris (CR/AEY1))
  • Date: Thu, 3 Dec 2009 10:01:16 +0100
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;
}