[Eva] Changes the type of cvalue builtins.
- [cacheable] is given at the registration of a builtin, and not separately for each result of the builtin. - Removes the offsetmap for the arguments: no builtin were using it anyway. - Returns a Cvalue.V.t for the result instead of an offsetmap. - Builtins can also return: + only the value of the result, in which case the post-state from the interpretation of the specification is used with the resulting value computed by the builtin. + only the post-states for functions with no froms dependency (other than the result and arguments) and no write of local variable addresses. Simplifies some builtins accordingly.
Showing
- src/plugins/value/domains/cvalue/builtins.ml 80 additions, 77 deletionssrc/plugins/value/domains/cvalue/builtins.ml
- src/plugins/value/domains/cvalue/builtins.mli 20 additions, 20 deletionssrc/plugins/value/domains/cvalue/builtins.mli
- src/plugins/value/domains/cvalue/builtins_float.ml 39 additions, 53 deletionssrc/plugins/value/domains/cvalue/builtins_float.ml
- src/plugins/value/domains/cvalue/builtins_malloc.ml 35 additions, 50 deletionssrc/plugins/value/domains/cvalue/builtins_malloc.ml
- src/plugins/value/domains/cvalue/builtins_memory.ml 63 additions, 108 deletionssrc/plugins/value/domains/cvalue/builtins_memory.ml
- src/plugins/value/domains/cvalue/builtins_misc.ml 18 additions, 23 deletionssrc/plugins/value/domains/cvalue/builtins_misc.ml
- src/plugins/value/domains/cvalue/builtins_print_c.ml 4 additions, 12 deletionssrc/plugins/value/domains/cvalue/builtins_print_c.ml
- src/plugins/value/domains/cvalue/builtins_split.ml 36 additions, 67 deletionssrc/plugins/value/domains/cvalue/builtins_split.ml
- src/plugins/value/domains/cvalue/builtins_string.ml 25 additions, 35 deletionssrc/plugins/value/domains/cvalue/builtins_string.ml
- src/plugins/value/domains/cvalue/builtins_string.mli 3 additions, 3 deletionssrc/plugins/value/domains/cvalue/builtins_string.mli
- src/plugins/value/domains/cvalue/builtins_watchpoint.ml 5 additions, 8 deletionssrc/plugins/value/domains/cvalue/builtins_watchpoint.ml
- src/plugins/value/engine/compute_functions.ml 4 additions, 3 deletionssrc/plugins/value/engine/compute_functions.ml
- src/plugins/value/legacy/eval_terms.ml 28 additions, 38 deletionssrc/plugins/value/legacy/eval_terms.ml
- src/plugins/value/utils/value_util.ml 1 addition, 1 deletionsrc/plugins/value/utils/value_util.ml
- src/plugins/value/utils/value_util.mli 1 addition, 1 deletionsrc/plugins/value/utils/value_util.mli
Loading
Please register or sign in to comment