let frama_C_compare_cos state actuals = match actuals with [_, arg, _; _, res, _; _, eps, _] -> begin try let iarg = Cvalue_type.V.project_ival arg in let farg = Ival.project_float iarg in let larg,uarg = Ival.Float_abstract.min_and_max_float farg in let larg = Ival.F.to_float larg in let uarg = Ival.F.to_float uarg in let ires = Cvalue_type.V.project_ival res in let fres = Ival.project_float ires in let lres,ures = Ival.Float_abstract.min_and_max_float fres in let lres = Ival.F.to_float lres in let ures = Ival.F.to_float ures in let ieps = Cvalue_type.V.project_ival eps in let feps = Ival.project_float ieps in let _,ueps = Ival.Float_abstract.min_and_max_float feps in let ueps = Ival.F.to_float ueps in (* crlibm_init(); let lref = cos_rd uarg in (* cos is decreasing *) let uref = cos_ru larg in (* cos is decreasing *) *) Ival.set_round_nearest_even(); (* system cos probably isn't designed for non-default rounding *) let lref = cos uarg in let uref = cos larg in Ival.set_round_upward(); let lallow = uref -. ueps in Ival.set_round_downward(); let uallow = lref +. ueps in if lallow <= lres && ures <= uallow then Value_parameters.result "CC %1.16f %1.16f %1.16f %1.16f %1.16f %1.16f OK" larg uarg lres ures lref uref else Value_parameters.result "CC %1.16f %1.16f %1.16f %1.16f %1.16f %1.16f KO" larg uarg lres ures lref uref; None, state, Location_Bits.Top_Param.bottom with _ -> Value_parameters.error "Invalid argument for Frama_C_compare_cos function"; do_degenerate None; raise Db.Value.Aborted end | _ -> Value_parameters.error "Invalid argument for Frama_C_compare_cos function"; do_degenerate None; raise Db.Value.Aborted let () = register_builtin "Frama_C_compare_cos" frama_C_compare_cos