[Eva] Base: rewrites is_valid_offset and valid_offset.
- shares and moves the functions [reduce_offset_by_validity] of Locations and Precise_locs into base.ml. - replaces the boolean argument ~for_writing into the new type access, that represents Read, Write or No_access. Without any access, offsets must point into or just beyond the base validity. - fixes the support of accesses of size 0: they are now invalid: + in bases with Invalid validity; + one past a base validity unless the base ends with an empty struct.
Showing
- src/kernel_services/abstract_interp/base.ml 68 additions, 17 deletionssrc/kernel_services/abstract_interp/base.ml
- src/kernel_services/abstract_interp/base.mli 19 additions, 4 deletionssrc/kernel_services/abstract_interp/base.mli
- src/kernel_services/abstract_interp/locations.ml 40 additions, 57 deletionssrc/kernel_services/abstract_interp/locations.ml
- src/kernel_services/abstract_interp/locations.mli 13 additions, 7 deletionssrc/kernel_services/abstract_interp/locations.mli
- src/plugins/from/from_compute.ml 3 additions, 3 deletionssrc/plugins/from/from_compute.ml
- src/plugins/inout/derefs.ml 1 addition, 1 deletionsrc/plugins/inout/derefs.ml
- src/plugins/inout/operational_inputs.ml 3 additions, 3 deletionssrc/plugins/inout/operational_inputs.ml
- src/plugins/pdg/build.ml 1 addition, 4 deletionssrc/plugins/pdg/build.ml
- src/plugins/value/domains/cvalue/builtins_memory.ml 7 additions, 8 deletionssrc/plugins/value/domains/cvalue/builtins_memory.ml
- src/plugins/value/domains/cvalue/builtins_string.ml 2 additions, 2 deletionssrc/plugins/value/domains/cvalue/builtins_string.ml
- src/plugins/value/domains/cvalue/cvalue_specification.ml 1 addition, 1 deletionsrc/plugins/value/domains/cvalue/cvalue_specification.ml
- src/plugins/value/domains/equality/equality_domain.ml 2 additions, 4 deletionssrc/plugins/value/domains/equality/equality_domain.ml
- src/plugins/value/domains/inout_domain.ml 1 addition, 1 deletionsrc/plugins/value/domains/inout_domain.ml
- src/plugins/value/domains/symbolic_locs.ml 2 additions, 3 deletionssrc/plugins/value/domains/symbolic_locs.ml
- src/plugins/value/engine/transfer_specification.ml 1 addition, 1 deletionsrc/plugins/value/engine/transfer_specification.ml
- src/plugins/value/gui_files/gui_eval.ml 4 additions, 5 deletionssrc/plugins/value/gui_files/gui_eval.ml
- src/plugins/value/legacy/eval_op.ml 3 additions, 3 deletionssrc/plugins/value/legacy/eval_op.ml
- src/plugins/value/legacy/eval_op.mli 1 addition, 1 deletionsrc/plugins/value/legacy/eval_op.mli
- src/plugins/value/legacy/eval_terms.ml 22 additions, 21 deletionssrc/plugins/value/legacy/eval_terms.ml
- src/plugins/value/legacy/eval_terms.mli 2 additions, 2 deletionssrc/plugins/value/legacy/eval_terms.mli
Loading
Please register or sign in to comment