Difference: Map: Reversed (top or Set (address (lval (offset (IntDomLifter(intdomtuple)))) * booleans)) * bottom or map:({}, mapping {
}) =
Map: messages =
trivial arrays: Array: mapping {
addr_type -> Uninitialized
data -> {}
descriptor -> Uninitialized
if_index -> Uninitialized
length -> Uninitialized
local_addr ->
(If you see this, you are special!, Unknown)
remote_addr ->
(If you see this, you are special!, Unknown)
timestamp ->
mapping {
hw -> mapping {
tv_nsec -> Uninitialized
tv_sec -> Uninitialized
}
if_index -> Uninitialized
kernel -> mapping {
tv_nsec -> Uninitialized
tv_sec -> Uninitialized
}
l2_length -> Uninitialized
tx_flags -> Uninitialized
}
} not leq Array: mapping {
addr_type -> Uninitialized
data -> {}
descriptor -> Uninitialized
if_index -> Uninitialized
length -> Uninitialized
local_addr ->
(If you see this, you are special!, Uninitialized)
remote_addr ->
(If you see this, you are special!, Uninitialized)
timestamp ->
mapping {
hw -> mapping {
tv_nsec ->
Uninitialized
tv_sec ->
Uninitialized
}
if_index -> Uninitialized
kernel -> mapping {
tv_nsec ->
Uninitialized
tv_sec ->
Uninitialized
}
l2_length -> Uninitialized
tx_flags -> Uninitialized
}
}
Using the current
master, 35 runs of the incremental analysis do not reach the fixpoint on chrony. This occurred with the regular incremental configuration. In all of the 35 runs, the unreached fixpoint is detected at the same code location withinchrony.In the experiments, it does not manifest in the runs where the incremental postsolver is active (with reluctant incremental analysis on or off).
Difference between rhs and computed solution.