BCHPostconditionval read_xml_postcondition :
CHXmlDocument.xml_element_int ->
BCHLibTypes.bterm_t ->
BCHLibTypes.fts_parameter_t list ->
BCHLibTypes.xxpredicate_tread_xml_postcondition node thisf pars returns the postcondition predicate encoded in the xml node node for the function identified by thisf with parameters pars
val read_xml_postconditions :
CHXmlDocument.xml_element_int ->
BCHLibTypes.bterm_t ->
BCHLibTypes.fts_parameter_t list ->
BCHLibTypes.xxpredicate_t listread_xml_postconditions node thisf pars returns the list of postcondition predicates contained in the xml node node for the function identified by thisf with parameters pars
val read_xml_errorpostconditions :
CHXmlDocument.xml_element_int ->
BCHLibTypes.bterm_t ->
BCHLibTypes.fts_parameter_t list ->
BCHLibTypes.xxpredicate_t listread_xml_errorpostconditions node thisf pars returns the list of error-postcondition predicates contained in the xml node node for the function identified by thisf with parameters pars
val read_xml_shortcut_postconditions :
CHXmlDocument.xml_element_int ->
BCHLibTypes.bterm_t ->
BCHLibTypes.xxpredicate_t list * BCHLibTypes.xxpredicate_t listreturns a tuple of postconditions and error-postconditions read from a single xml node containing short-cut postconditions.