Module Db.Constant_Propagation

module Constant_Propagation: sig .. end

Constant propagation plugin.


val get : (Cil_datatype.Fundec.Set.t -> cast_intro:bool -> Project.t) Pervasives.ref

Propagate constant into the functions given by name. note: the propagation is performed into all functions when the set is empty; and casts can be introduced when cast_intro is true.

val compute : (unit -> unit) Pervasives.ref

Propagate constant into the functions given by the parameters (in the same way that Db.Constant_Propagation.get. Then pretty print the resulting program.