Frama-C:
Plug-ins:
Libraries:

Frama-C API - Backwards

Parameters

Signature

val compute : Cil_types.stmt list -> unit

Fill in the T.stmtStartData, given a number of initial statements to start from (the sinks for the backwards data flow). All of the statements (not just the initial ones!) must have some entry in T.stmtStartData If you want to use bottom for the initial data, you should pass the complete list of statements to compute, so that everything is visited. find_stmts may be useful here.