--- layout: fc_discuss_archives title: Message 12 from Frama-C-discuss on June 2017 ---
It seems to me that 0/0 produces a NaN but in the following program, using wp and the float model, I can prove the \is_finite assert and the \is_NaN assert remains unknown. What is it due to ? void main(int argc, char *argv[]){       float x = 0.0f/0.0f;    //@ assert \is_finite(x);    //@ assert \is_NaN(x);    } Regards, --   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/20170620/bf24f0dd/attachment.html>