module Cvalue_specification: sig .. end
sig
end
Compute the validity status for from in pre_state, assuming the entire clause is assigns asgn \from from. The inferred dependencies are found_froms, while asgn evaluates to assigns_zone.
from
pre_state
assigns asgn \from from
found_froms
asgn
assigns_zone