From 828cecef52f0c162f0aff5f16542dc58c4032dce Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr> Date: Wed, 13 Feb 2019 17:57:10 +0100 Subject: [PATCH] [kernel] Property: documents has_status. --- src/kernel_services/ast_data/property.mli | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/kernel_services/ast_data/property.mli b/src/kernel_services/ast_data/property.mli index 6ed7d5ea872..d951fa1afb6 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 -- GitLab