floats bugs [cz]

[mchalupa]

• floats-cbmc-regression/float14_true-unreach-call.i prepare odstrani __isinff, bez prepare da klee spravny vysledek
• floats-cbmc-regression/float4_true-unreach-call.i klee vola __isnan a __isinf s argumentem 0 (konkretizoval?)
• floats-cbmc-regression/float4_true-unreach-call.i prepare odstrani volani __isinf - klee bez prepare spadne na nepodporovane instrukci
• floats-cbmc-regression/float-rounding1_true-unreach-call.i prepare odstrani fesetround, ale klee da spatny vysledek jak s prepare tak bez prepare

[xvitovs1]

• floats-cbmc-regression/float14_true-unreach-call.i opraveno
• floats-cbmc-regression/float-flags-simp1_true-unreach-call.c chyba v if(!(isinf(HUGE_VAL))) __VERIFIER_error(); odreze se if a zustane jenom __VERIFIER_error(); pouziva nedefinovanou promennou d
• floats-cbmc-regression/float4_true-unreach-call.c pouziva nedefinovane promenne f a f2