[Eva] Register_builtin takes the type of the builtin as optional argument.
If provided, the expected type is compared to the actual type of the C function to be replaced by the builtin. In case of inconsistency, the builtin is not used and a warning is emitted.
Showing
- src/kernel_services/plugin_entry_points/db.ml 2 additions, 1 deletionsrc/kernel_services/plugin_entry_points/db.ml
- src/kernel_services/plugin_entry_points/db.mli 22 additions, 17 deletionssrc/kernel_services/plugin_entry_points/db.mli
- src/plugins/value/domains/cvalue/builtins.ml 37 additions, 13 deletionssrc/plugins/value/domains/cvalue/builtins.ml
- src/plugins/value/domains/cvalue/builtins.mli 9 additions, 3 deletionssrc/plugins/value/domains/cvalue/builtins.mli
- src/plugins/value/domains/cvalue/builtins_float.ml 8 additions, 9 deletionssrc/plugins/value/domains/cvalue/builtins_float.ml
- src/plugins/value/domains/cvalue/builtins_malloc.ml 2 additions, 2 deletionssrc/plugins/value/domains/cvalue/builtins_malloc.ml
Loading
Please register or sign in to comment