[Eva] Reworks garbled mix origins.
Origins no longer have a lattice structure. A unique id is associated to each created origin. When multiple origins can be associated to a value, we keep the oldest origin (according to their ids).
Showing
- src/kernel_services/abstract_interp/cvalue.ml 4 additions, 4 deletionssrc/kernel_services/abstract_interp/cvalue.ml
- src/kernel_services/abstract_interp/lmap.ml 1 addition, 1 deletionsrc/kernel_services/abstract_interp/lmap.ml
- src/kernel_services/abstract_interp/locations.ml 4 additions, 4 deletionssrc/kernel_services/abstract_interp/locations.ml
- src/kernel_services/abstract_interp/map_lattice.ml 3 additions, 3 deletionssrc/kernel_services/abstract_interp/map_lattice.ml
- src/kernel_services/abstract_interp/offsetmap.ml 7 additions, 7 deletionssrc/kernel_services/abstract_interp/offsetmap.ml
- src/kernel_services/abstract_interp/origin.ml 72 additions, 236 deletionssrc/kernel_services/abstract_interp/origin.ml
- src/kernel_services/abstract_interp/origin.mli 9 additions, 26 deletionssrc/kernel_services/abstract_interp/origin.mli
- src/plugins/eva/domains/cvalue/builtins_memory.ml 1 addition, 1 deletionsrc/plugins/eva/domains/cvalue/builtins_memory.ml
- src/plugins/variadic/tests/known/oracle/printf.res.oracle 1 addition, 1 deletionsrc/plugins/variadic/tests/known/oracle/printf.res.oracle
- src/plugins/variadic/tests/known/oracle/printf_garbled_mix.res.oracle 1 addition, 1 deletion...variadic/tests/known/oracle/printf_garbled_mix.res.oracle
- tests/builtins/oracle/memcpy.res.oracle 1 addition, 1 deletiontests/builtins/oracle/memcpy.res.oracle
- tests/float/oracle/nonlin.0.res.oracle 2 additions, 2 deletionstests/float/oracle/nonlin.0.res.oracle
- tests/float/oracle/nonlin.1.res.oracle 2 additions, 2 deletionstests/float/oracle/nonlin.1.res.oracle
- tests/float/oracle/nonlin.2.res.oracle 2 additions, 2 deletionstests/float/oracle/nonlin.2.res.oracle
- tests/float/oracle/nonlin.3.res.oracle 2 additions, 2 deletionstests/float/oracle/nonlin.3.res.oracle
- tests/float/oracle/nonlin.4.res.oracle 2 additions, 2 deletionstests/float/oracle/nonlin.4.res.oracle
- tests/float/oracle/nonlin.5.res.oracle 2 additions, 2 deletionstests/float/oracle/nonlin.5.res.oracle
- tests/libc/oracle/signal_h.res.oracle 2 additions, 2 deletionstests/libc/oracle/signal_h.res.oracle
- tests/value/oracle/arith_pointer.res.oracle 2 additions, 4 deletionstests/value/oracle/arith_pointer.res.oracle
- tests/value/oracle/shift.0.res.oracle 1 addition, 1 deletiontests/value/oracle/shift.0.res.oracle
Loading
Please register or sign in to comment