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] Ergo and problem with integer type

  • Subject: [Frama-c-discuss] Ergo and problem with integer type
  • From: doan.thanh.nam.1988 at gmail.com (nam nam)
  • Date: Fri, 22 Jan 2010 07:26:30 -0800
When I do simple test:

/*@ensures
  @ \result == (a+b+c);
  @*/

float triangle(float a, float b, float c){
    float t ;
    t = a+b+c;
    return t;
}

using Frama C and Ergo the result is ok. But when I try to modify it a
little:

/*@ensures
  @ \result == (a+b+c);
  @*/

int triangle(int a, int b, int c){
    int t ;
    t = a+b+c;
    return t;
}

the result is so different valid:20% and unknown 80%.

I am using jessie 2.19 and ergo 0.9. Did I do something wrong?
By the way, is there any difference between grammar for pre & post condition
of WHY and FRAMA C?

Thank you. And have a nice weekend.
-- 
?o?n Th?nh Nam
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20100122/29ec751b/attachment.htm