diff --git a/src/kernel_services/ast_data/property.mli b/src/kernel_services/ast_data/property.mli index 6ed7d5ea8724286e5318045a67702d1177a3753c..d951fa1afb61b2990baece699c57ff35cc83b462 100644 --- a/src/kernel_services/ast_data/property.mli +++ b/src/kernel_services/ast_data/property.mli @@ -446,6 +446,9 @@ val ip_of_global_annotation_single: (**************************************************************************) val has_status: identified_property -> bool +(** Does the property has a logical status (which may be Never_tried)? + False for pragma, assumes clauses and some ACSL extensions. + @since Frama-C+dev *) val get_kinstr: identified_property -> kinstr val get_kf: identified_property -> kernel_function option