diff --git a/src/kernel_services/ast_data/annotations.ml b/src/kernel_services/ast_data/annotations.ml
index cc6c5221d3e88a2f0f0cf893a453e9cc80869625..90690303633e5645a68168a2d13dcf4a7c9cab9c 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 c6b8e7d3f81dcf518e58918404d31c93da63d1af..1b7e315613ec5e5bd32073bb0b8eef9424d1218f 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.