--- layout: fc_discuss_archives title: Message 13 from Frama-C-discuss on June 2017 ---
When using a specification instead of a function, it seems that EVA propagates postconditions for double variables but not for float variables. With the following example, we obtain : x in [-1.79769313486e+308 .. 1.79769313486e+308] y in {1.} /*@  @ assigns \nothing;  @ ensures \result == 1.0f;  @*/ float foo(); /*@  @ assigns \nothing;  @ ensures \result == 1.0;  @*/ double foo_d(); int main(int argc, char *argv[]) {    float x = foo();    double y = foo_d();    return 0; } Regards, Arthur --   Arthur CLAVIÃRE Elève ingénieur SUPAERO - 2A ISAE SUPAERO - Institut Supérieur de l'Aéronautique et de l'Espace 10 avenue Edouard Belin - BP 54032 - 31055 TOULOUSE CEDEX 4 FRANCE - http://www.isae-supaero.fr Tel +33 5 61 33 80 80 - Fax (+33) 5 61 33 83 30 Plan d'accès/Access map -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20170622/00539c53/attachment.html>