Skip to content
Snippets Groups Projects
user avatar
David Bühler authored
[Datatype.Option] defines a different order than [Stdlib.Option.compare].

Type ['state partition] is a map from partition keys to states.
Such maps are converted into lists to be propagated through statements.
Changes in [Key.compare] impact the list order.
The list order impacts the heuristics used to remove redundant states before
propagating them (see Partitioning_index): redundant states may be propagated
or not depending of the list order.
This impacts the number of states propagated at some statements, and thus the
consumed slevel, and the precision of the analysis afterwards.

This commit reverts the change in the comparison of keys only to minimize
changes in the behavior of the analysis partitioning.
1d4fe906
History
Name Last commit Last update
..