[Kernel] Rewriting [Floating_point] module
The module now handles explicitly the floating point formats using the type system, thus ensuring strict manipulation of float numbers.
Showing
- src/dune 1 addition, 1 deletionsrc/dune
- src/kernel_internals/typing/cabs2cil.ml 7 additions, 6 deletionssrc/kernel_internals/typing/cabs2cil.ml
- src/kernel_services/abstract_interp/fc_float.ml 104 additions, 95 deletionssrc/kernel_services/abstract_interp/fc_float.ml
- src/kernel_services/abstract_interp/float_sig.ml 1 addition, 0 deletionssrc/kernel_services/abstract_interp/float_sig.ml
- src/kernel_services/abstract_interp/fval.ml 16 additions, 20 deletionssrc/kernel_services/abstract_interp/fval.ml
- src/kernel_services/abstract_interp/ival.ml 26 additions, 45 deletionssrc/kernel_services/abstract_interp/ival.ml
- src/kernel_services/abstract_interp/widen_type.ml 4 additions, 4 deletionssrc/kernel_services/abstract_interp/widen_type.ml
- src/kernel_services/ast_building/cil_builder.ml 1 addition, 1 deletionsrc/kernel_services/ast_building/cil_builder.ml
- src/kernel_services/ast_printing/cil_printer.ml 6 additions, 7 deletionssrc/kernel_services/ast_printing/cil_printer.ml
- src/kernel_services/ast_queries/cil.ml 14 additions, 26 deletionssrc/kernel_services/ast_queries/cil.ml
- src/kernel_services/ast_queries/logic_const.ml 3 additions, 5 deletionssrc/kernel_services/ast_queries/logic_const.ml
- src/kernel_services/ast_queries/logic_utils.ml 16 additions, 17 deletionssrc/kernel_services/ast_queries/logic_utils.ml
- src/libraries/floating_point/floating_point.c 325 additions, 0 deletionssrc/libraries/floating_point/floating_point.c
- src/libraries/floating_point/floating_point.ml 535 additions, 0 deletionssrc/libraries/floating_point/floating_point.ml
- src/libraries/floating_point/floating_point.mli 256 additions, 0 deletionssrc/libraries/floating_point/floating_point.mli
- src/libraries/utils/c_bindings.c 0 additions, 217 deletionssrc/libraries/utils/c_bindings.c
- src/libraries/utils/floating_point.ml 0 additions, 435 deletionssrc/libraries/utils/floating_point.ml
- src/libraries/utils/floating_point.mli 0 additions, 131 deletionssrc/libraries/utils/floating_point.mli
- src/plugins/aorai/aorai_utils.ml 2 additions, 1 deletionsrc/plugins/aorai/aorai_utils.ml
- src/plugins/e-acsl/src/libraries/interval_utils.ml 9 additions, 25 deletionssrc/plugins/e-acsl/src/libraries/interval_utils.ml
Loading
Please register or sign in to comment