CCHPostCondition
val record_postconditions : string -> CCHAnalysisTypes.c_environment_int -> CCHPreTypes.invariant_io_int -> unit