[Eva] Offsetmap: removes some feedback messages about approximations.
In offsetmaps, removes a reference to change the feedback emitted when approximating the write of large memory locations. Instead, the main offsetmap functor takes an additional parameter about whether such messages should be emitted. Only the offsetmaps build by the Eva cvalue domain emits these messages, as write approximations may have a significant impact on the analysis precision. Offsetmaps used to represent memory zones or dependiencies do not emit these messages, which were most often insignificant and instable (as many plug-ins and Eva domains use memory zones in various ways).
Showing
- src/kernel_services/abstract_interp/cvalue.ml 5 additions, 1 deletionsrc/kernel_services/abstract_interp/cvalue.ml
- src/kernel_services/abstract_interp/lmap_bitwise.ml 0 additions, 4 deletionssrc/kernel_services/abstract_interp/lmap_bitwise.ml
- src/kernel_services/abstract_interp/lmap_bitwise.mli 0 additions, 2 deletionssrc/kernel_services/abstract_interp/lmap_bitwise.mli
- src/kernel_services/abstract_interp/offsetmap.ml 38 additions, 28 deletionssrc/kernel_services/abstract_interp/offsetmap.ml
- src/kernel_services/abstract_interp/offsetmap.mli 9 additions, 4 deletionssrc/kernel_services/abstract_interp/offsetmap.mli
- src/kernel_services/abstract_interp/offsetmap_bitwise_sig.ml 0 additions, 5 deletionssrc/kernel_services/abstract_interp/offsetmap_bitwise_sig.ml
- src/kernel_services/abstract_interp/offsetmap_sig.ml 0 additions, 4 deletionssrc/kernel_services/abstract_interp/offsetmap_sig.ml
- src/plugins/from/from_memory.ml 0 additions, 2 deletionssrc/plugins/from/from_memory.ml
- tests/builtins/oracle/imprecise.res.oracle 0 additions, 8 deletionstests/builtins/oracle/imprecise.res.oracle
- tests/builtins/oracle/linked_list.1.res.oracle 0 additions, 8 deletionstests/builtins/oracle/linked_list.1.res.oracle
- tests/builtins/oracle/memcpy.0.res.oracle 0 additions, 2 deletionstests/builtins/oracle/memcpy.0.res.oracle
- tests/builtins/oracle_equality/imprecise.res.oracle 0 additions, 11 deletionstests/builtins/oracle_equality/imprecise.res.oracle
- tests/builtins/oracle_equality/linked_list.1.res.oracle 0 additions, 24 deletionstests/builtins/oracle_equality/linked_list.1.res.oracle
- tests/builtins/oracle_gauges/linked_list.1.res.oracle 1 addition, 1 deletiontests/builtins/oracle_gauges/linked_list.1.res.oracle
- tests/builtins/oracle_gauges/memcpy.0.res.oracle 2 additions, 2 deletionstests/builtins/oracle_gauges/memcpy.0.res.oracle
- tests/builtins/oracle_octagon/imprecise.res.oracle 0 additions, 11 deletionstests/builtins/oracle_octagon/imprecise.res.oracle
- tests/builtins/oracle_octagon/linked_list.1.res.oracle 0 additions, 18 deletionstests/builtins/oracle_octagon/linked_list.1.res.oracle
- tests/builtins/oracle_symblocs/imprecise.res.oracle 0 additions, 11 deletionstests/builtins/oracle_symblocs/imprecise.res.oracle
- tests/builtins/oracle_symblocs/linked_list.1.res.oracle 0 additions, 18 deletionstests/builtins/oracle_symblocs/linked_list.1.res.oracle
- tests/value/oracle/assigns.res.oracle 0 additions, 2 deletionstests/value/oracle/assigns.res.oracle
Loading
Please register or sign in to comment