[Eva] Improves the precision of the symbolic locations domain.
Changes the criterion according to which the symbolic domain retains the value of an expression: - if the expression is an lvalue with an imprecise location; - if the expression is a binary operation between two expressions, each containing an lvalue with an imprecise (non-singleton) value. Otherwise, the value should always be inferred by the cvalue domain, or can be precisely computed from values inferred by the cvalue domain.
Showing
- src/plugins/value/domains/symbolic_locs.ml 38 additions, 31 deletionssrc/plugins/value/domains/symbolic_locs.ml
- tests/value/oracle_symblocs/downcast.1.res.oracle 8 additions, 0 deletionstests/value/oracle_symblocs/downcast.1.res.oracle
- tests/value/oracle_symblocs/struct2.res.oracle 7 additions, 7 deletionstests/value/oracle_symblocs/struct2.res.oracle
Loading
Please register or sign in to comment