[Kernel] Renaming and optimisations
- Renaming [round_to] as [change_format] to avoid confusion with [round] - Renaming [of_float] as [represents ~float ~in_format] to better convey the goal of this module and why we hide the float type - Adding [@@noalloc] to external functions [set_rounding_mode] and [get_rounding_mode] as a (rather small) optimisation
Showing
- src/kernel_services/abstract_interp/fc_float.ml 7 additions, 3 deletionssrc/kernel_services/abstract_interp/fc_float.ml
- src/kernel_services/ast_queries/cil.ml 5 additions, 4 deletionssrc/kernel_services/ast_queries/cil.ml
- src/libraries/floating_point/floating_point.c 1 addition, 1 deletionsrc/libraries/floating_point/floating_point.c
- src/libraries/floating_point/floating_point.ml 23 additions, 19 deletionssrc/libraries/floating_point/floating_point.ml
- src/libraries/floating_point/floating_point.mli 2 additions, 2 deletionssrc/libraries/floating_point/floating_point.mli
- src/plugins/eva/ast/eva_ast_builder.ml 2 additions, 2 deletionssrc/plugins/eva/ast/eva_ast_builder.ml
- src/plugins/eva/ast/eva_ast_printer.ml 1 addition, 1 deletionsrc/plugins/eva/ast/eva_ast_printer.ml
- src/plugins/eva/engine/evaluation.ml 2 additions, 1 deletionsrc/plugins/eva/engine/evaluation.ml
- src/plugins/rte/rte.ml 2 additions, 1 deletionsrc/plugins/rte/rte.ml
- src/plugins/wp/Cfloat.ml 2 additions, 2 deletionssrc/plugins/wp/Cfloat.ml
- src/plugins/wp/ProverWhy3.ml 1 addition, 1 deletionsrc/plugins/wp/ProverWhy3.ml
Loading
Please register or sign in to comment