LowerHil.Smodule Interpreter : AbstractInterpreter.Sval compute_post :
Interpreter.TransferFunctions.analysis_data ->
initial:domain ->
IR.Procdesc.t ->
domain optioncompute and return the postcondition for the given procedure starting from initial.