[Eva] Improves warnings about garbled mix writes.
These warnings are emitted when a garbled mix is written through an assignment or an assigns clause. This commit: - rephrases the warnings to be clearer and less verbose. - emits the warning only for garbled mix created at the current statement, according to their origin. Do not emit warnings for each propagation of previous garbled mixes. - emits the warning when assigning garbled mix to the formal parameters of a function from the arguments of a call.
Showing
- src/kernel_services/abstract_interp/origin.ml 16 additions, 11 deletionssrc/kernel_services/abstract_interp/origin.ml
- src/kernel_services/abstract_interp/origin.mli 7 additions, 2 deletionssrc/kernel_services/abstract_interp/origin.mli
- src/plugins/dive/tests/dive/oracle/exceptional.res.oracle 2 additions, 8 deletionssrc/plugins/dive/tests/dive/oracle/exceptional.res.oracle
- src/plugins/eva/domains/cvalue/cvalue_transfer.ml 29 additions, 55 deletionssrc/plugins/eva/domains/cvalue/cvalue_transfer.ml
- src/plugins/eva/engine/transfer_specification.ml 6 additions, 6 deletionssrc/plugins/eva/engine/transfer_specification.ml
- src/plugins/variadic/tests/defined/oracle/sum_with_unspecified_sequence.res.oracle 0 additions, 12 deletions...s/defined/oracle/sum_with_unspecified_sequence.res.oracle
- src/plugins/variadic/tests/known/oracle/printf_garbled_mix.res.oracle 1 addition, 2 deletions...variadic/tests/known/oracle/printf_garbled_mix.res.oracle
- tests/builtins/oracle/alloc.0.res.oracle 1 addition, 2 deletionstests/builtins/oracle/alloc.0.res.oracle
- tests/builtins/oracle/alloc.1.res.oracle 1 addition, 2 deletionstests/builtins/oracle/alloc.1.res.oracle
- tests/builtins/oracle/imprecise-malloc-free.res.oracle 9 additions, 2 deletionstests/builtins/oracle/imprecise-malloc-free.res.oracle
- tests/builtins/oracle/imprecise.res.oracle 2 additions, 4 deletionstests/builtins/oracle/imprecise.res.oracle
- tests/builtins/oracle/memcpy.res.oracle 9 additions, 0 deletionstests/builtins/oracle/memcpy.res.oracle
- tests/builtins/oracle/memset.res.oracle 2 additions, 0 deletionstests/builtins/oracle/memset.res.oracle
- tests/builtins/oracle/strchr.res.oracle 4 additions, 2 deletionstests/builtins/oracle/strchr.res.oracle
- tests/builtins/oracle_equality/imprecise.res.oracle 4 additions, 4 deletionstests/builtins/oracle_equality/imprecise.res.oracle
- tests/builtins/oracle_octagon/imprecise.res.oracle 3 additions, 3 deletionstests/builtins/oracle_octagon/imprecise.res.oracle
- tests/builtins/oracle_symblocs/imprecise.res.oracle 3 additions, 3 deletionstests/builtins/oracle_symblocs/imprecise.res.oracle
- tests/float/oracle/builtins.res.oracle 2 additions, 3 deletionstests/float/oracle/builtins.res.oracle
- tests/float/oracle/nonlin.0.res.oracle 2 additions, 5 deletionstests/float/oracle/nonlin.0.res.oracle
- tests/float/oracle/nonlin.1.res.oracle 2 additions, 5 deletionstests/float/oracle/nonlin.1.res.oracle
Loading
Please register or sign in to comment