--- layout: fc_discuss_archives title: Message 12 from Frama-C-discuss on June 2017 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] \is_finite and \is_NaN assert



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>