--- layout: fc_discuss_archives title: Message 34 from Frama-C-discuss on January 2010 ---
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