-
- Downloads
[Eva] Fixes abstract domains uses of the valuation for recursive calls.
On recursive calls, the substitution to be applied to the domain states is not applied to the valuation given as argument to [start_call]. This commit: - adds comment in the abstract domain signature to reflect this fact; - fixes the domains to properly use the valuation in recursive calls. The equality and octagon domains are now intra-procedural on recursive calls: they always start the analysis of a recursive call with an empty state.
Showing
- src/plugins/value/domains/abstract_domain.mli 10 additions, 1 deletionsrc/plugins/value/domains/abstract_domain.mli
- src/plugins/value/domains/cvalue/cvalue_domain.ml 3 additions, 0 deletionssrc/plugins/value/domains/cvalue/cvalue_domain.ml
- src/plugins/value/domains/cvalue/cvalue_transfer.ml 1 addition, 2 deletionssrc/plugins/value/domains/cvalue/cvalue_transfer.ml
- src/plugins/value/domains/equality/equality_domain.ml 12 additions, 5 deletionssrc/plugins/value/domains/equality/equality_domain.ml
- src/plugins/value/domains/gauges/gauges_domain.ml 2 additions, 2 deletionssrc/plugins/value/domains/gauges/gauges_domain.ml
- src/plugins/value/domains/octagons.ml 12 additions, 5 deletionssrc/plugins/value/domains/octagons.ml
- src/plugins/value/domains/offsm_domain.ml 2 additions, 2 deletionssrc/plugins/value/domains/offsm_domain.ml
- src/plugins/value/domains/symbolic_locs.ml 2 additions, 2 deletionssrc/plugins/value/domains/symbolic_locs.ml
Loading
Please register or sign in to comment