Add conversion from generic floatting point contract to finite one
Showing
- Makefile 1 addition, 0 deletionsMakefile
- headers/header_spec.txt 2 additions, 0 deletionsheaders/header_spec.txt
- src/kernel_services/ast_transformations/contract_finite_float.ml 83 additions, 0 deletions...nel_services/ast_transformations/contract_finite_float.ml
- src/kernel_services/ast_transformations/contract_finite_float.mli 21 additions, 0 deletions...el_services/ast_transformations/contract_finite_float.mli
- src/kernel_services/plugin_entry_points/kernel.ml 10 additions, 0 deletionssrc/kernel_services/plugin_entry_points/kernel.ml
- src/kernel_services/plugin_entry_points/kernel.mli 3 additions, 0 deletionssrc/kernel_services/plugin_entry_points/kernel.mli
- src/plugins/wp/wpo.mli 2 additions, 1 deletionsrc/plugins/wp/wpo.mli
- tests/float/contract_finite_float.c 29 additions, 0 deletionstests/float/contract_finite_float.c
- tests/float/oracle/contract_finite_float.res.oracle 39 additions, 0 deletionstests/float/oracle/contract_finite_float.res.oracle
Loading
Please register or sign in to comment