From 518863e3f23b6b326c8990cf4690cc08e8d8385d Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Tue, 19 Jan 2021 11:35:48 +0100
Subject: [PATCH] [kernel] Add function to add a spec to a function or
statement
---
src/kernel_services/ast_data/annotations.ml | 13 +++++++++++++
src/kernel_services/ast_data/annotations.mli | 8 ++++++++
2 files changed, 21 insertions(+)
diff --git a/src/kernel_services/ast_data/annotations.ml b/src/kernel_services/ast_data/annotations.ml
index cc6c5221d3e..90690303633 100644
--- a/src/kernel_services/ast_data/annotations.ml
+++ b/src/kernel_services/ast_data/annotations.ml
@@ -1001,6 +1001,19 @@ let add_disjoint e kf ?stmt ?active l =
Property_status.register (Property.ip_of_disjoint kf (kinstr stmt) active l)
end
+let add_spec ?register_children e kf ?stmt ?active spec =
+ add_behaviors ?register_children e kf ?stmt ?active spec.spec_behavior;
+ Option.iter (fun variant -> add_decreases e kf variant) spec.spec_variant;
+ Option.iter
+ (fun terminates -> add_terminates e kf ?stmt ?active terminates)
+ spec.spec_terminates;
+ List.iter
+ (fun complete -> add_complete e kf ?stmt ?active complete)
+ spec.spec_complete_behaviors;
+ List.iter
+ (fun disjoint -> add_disjoint e kf ?stmt ?active disjoint)
+ spec.spec_disjoint_behaviors
+
let extend_behavior
e kf ?stmt ?active ?(behavior=Cil.default_behavior_name) set_bhv =
(* Kernel.feedback "Function %a, behavior %s" Kf.pretty kf bhv_name;*)
diff --git a/src/kernel_services/ast_data/annotations.mli b/src/kernel_services/ast_data/annotations.mli
index c6b8e7d3f81..1b7e315613e 100644
--- a/src/kernel_services/ast_data/annotations.mli
+++ b/src/kernel_services/ast_data/annotations.mli
@@ -334,6 +334,14 @@ type 'a behavior_component_addition =
@since Aluminium-20160501
*)
+val add_spec: ?register_children:bool -> spec contract_component_addition
+(** Add new spec into the given contract.
+
+ [register_children] is directly given to the function [add_behaviors].
+
+ @since Frama-C+dev
+*)
+
val add_behaviors:
?register_children:bool -> funbehavior list contract_component_addition
(** Add new behaviors into the given contract.
--
GitLab