Library compcertx.backend.ConstpropX
Require compcert.backend.Constprop.
Require ValueDomainX.
Import AST.
Import ValueDomainX.
Export Constprop.
Require ValueDomainX.
Import AST.
Import ValueDomainX.
Export Constprop.
Here we define per-function/module constant propagation, without any proof.
As said in ValueDomainX, we do not consider any optimization on
`const' global variables, so the read-only memory abstraction will
be empty.
Definition transf_function := transf_function rmtop.
Definition transf_fundef := transf_fundef rmtop.
Definition transf_program: RTL.program → RTL.program :=
transform_program transf_fundef.