Add conditional invariant context

README.md

@@ -76,6 +76,12 @@ function defined in `main.c`.
 
 The context is the situation in a target function in which the property must
 hold. It can be one of the following :
+- `\conditional_invariant` : the property `P` is guarantted to be verified at
+    the end of the target function *if* it is verified at the begining.
+- `\precond` : the property `P` is a precondition of the target function and is
+    must hold at each of its callsites.
+- `\postcond` : the property `P` hold at the end of the target function for
+    every initial state satisfying the preconditions of the function.
 - `\weak_invariant` : the property `P` is guaranteed to be verified at the
   beginning and end of the target function.
 - `\strong_invariant` : the property `P` must hold at every point of the target

meta_annotate.ml

@@ -186,22 +186,34 @@ class weak_inv_visitor flags full_table table (pre, post) = object (self)
       let pred_name = (Emitter.get_name ump.ump_emitter) :: pred'.pred_name in
       let pred'' = {pred' with pred_name} in
       let only_check = not ump.ump_assert in
-      let ip_requires = Logic_const.new_predicate ~only_check pred'' in
-      let ip_ensures = Logic_const.refresh_predicate ip_requires in
       let deps = ref [] in
       if pre then (
+        let ip_requires = Logic_const.new_predicate ~only_check pred'' in
         Annotations.add_requires ump.ump_emitter kf [ip_requires];
         let defb = Extlib.the (Cil.find_default_behavior (Annotations.funspec kf)) in
         let rips = Property.ip_of_requires kf Kglobal defb ip_requires :: !deps in
         let callsites_ip = get_callsites_ips kf rips in
         deps := rips @ callsites_ip @ !deps
       );
-      if post then (
-        Annotations.add_ensures ump.ump_emitter kf [(Normal, ip_ensures)];
+      let add_post ip =
+        Annotations.add_ensures ump.ump_emitter kf [(Normal, ip)];
         let defb = Extlib.the (Cil.find_default_behavior (Annotations.funspec kf)) in
-        let eip = Property.ip_of_ensures kf Kglobal defb (Normal, ip_ensures) in
+        let eip = Property.ip_of_ensures kf Kglobal defb (Normal, ip) in
         deps := eip :: !deps
-      );
+      in
+      begin match post with
+        | `None -> ()
+        | `Strict ->
+          let ip_ensures = Logic_const.new_predicate ~only_check pred'' in
+          add_post ip_ensures
+        | `Conditional ->
+          let pred' = Logic_const.pimplies (pred, pred) in
+          let pred'' = Meta_dispatch.name_mp_pred flags pred' ump.ump_counter in
+          let pred_name = (Emitter.get_name ump.ump_emitter) :: pred''.pred_name in
+          let pred''' = {pred'' with pred_name} in
+          let ip_ensures = Logic_const.new_predicate ~only_check pred''' in
+          add_post ip_ensures
+      end;
       Meta_dispatch.add_dependency ump !deps
     in
     (* Delay actual instanciation for correct numbering *)
@@ -506,7 +518,7 @@ let lvals_of_predicate pred =
  * maintain the invariant at the end
  *)
 class strong_inv_visitor flags all_mp table = object (self)
-  inherit weak_inv_visitor flags all_mp table (true, true)
+  inherit weak_inv_visitor flags all_mp table (true, `Strict)
   val mutable lenient = false
 
   (* Given a lval which is to be modified, check if its modification
@@ -598,7 +610,7 @@ let report all_mp tables =
 let annotate flags all_mp by_context =
   let get_vis table = function
     | Weak_invariant ->
-      (new weak_inv_visitor flags all_mp table (true, true) :> Visitor.frama_c_visitor)
+      (new weak_inv_visitor flags all_mp table (true, `Strict) :> Visitor.frama_c_visitor)
     | Calling ->
       (new calling_visitor flags all_mp table :> Visitor.frama_c_visitor)
     | Writing ->
@@ -608,9 +620,11 @@ let annotate flags all_mp by_context =
     | Strong_invariant ->
       (new strong_inv_visitor flags all_mp table :> Visitor.frama_c_visitor)
     | Precond ->
-      (new weak_inv_visitor flags all_mp table (true, false) :> Visitor.frama_c_visitor)
+      (new weak_inv_visitor flags all_mp table (true, `None) :> Visitor.frama_c_visitor)
     | Postcond ->
-      (new weak_inv_visitor flags all_mp table (false, true) :> Visitor.frama_c_visitor)
+      (new weak_inv_visitor flags all_mp table (false, `Strict) :> Visitor.frama_c_visitor)
+    | Conditional_invariant ->
+      (new weak_inv_visitor flags all_mp table (false, `Conditional) :> Visitor.frama_c_visitor)
   in
   List.iter (fun (ctx, table) ->
       let vis = get_vis table ctx in

meta_deduce.ml

@@ -217,6 +217,7 @@ let generate_mp prefix preds globals fmt (mp, tset) =
     (match mp.mp_context with
         | Weak_invariant -> "Weak invariant"
         | Strong_invariant -> "Strong invariant"
+        | Conditional_invariant -> "Conditional invariant"
         | Postcond -> "Postcond"
         | Precond -> "Precond"
         | Writing -> "Writing"

meta_dispatch.ml

@@ -102,7 +102,7 @@ let unpack_mp flags mp admit =
 let dispatch flags mps =
   let all_mp = Hashtbl.create 10 in
   let ctxts = [Weak_invariant; Strong_invariant; Writing; Reading; Calling;
-               Precond; Postcond] in
+               Precond; Postcond; Conditional_invariant] in
   let tables = List.map (fun ctx -> ctx, Str_Hashtbl.create 5) ctxts in
   List.iter (fun mp ->
       let table = List.assoc mp.mp_context tables in

meta_parse.ml

@@ -34,6 +34,7 @@ type context =
   | Reading
   | Postcond
   | Precond
+  | Conditional_invariant
 
 type target =
   | TgAll
@@ -76,7 +77,8 @@ let mp_contexts = [
   "\\calling";
   "\\reading";
   "\\postcond";
-  "\\precond"
+  "\\precond";
+  "\\conditional_invariant"
 ]
 let mp_metavariables = [
   "\\written";
@@ -387,6 +389,7 @@ let process_property tc loc = function
     let mp_context = match econtext.lexpr_node with
       | PLvar "\\weak_invariant" -> Weak_invariant
       | PLvar "\\strong_invariant" -> Strong_invariant
+      | PLvar "\\conditional_invariant" -> Conditional_invariant
       | PLvar "\\writing" -> Writing
       | PLvar "\\reading" -> Reading
       | PLvar "\\calling" -> Calling

meta_parse.mli

@@ -30,6 +30,7 @@ type context =
   | Reading
   | Postcond
   | Precond
+  | Conditional_invariant
 
 type target =
   | TgAll

tests/meta-wp/invariant.c

@@ -4,7 +4,7 @@
 
 #include <assert.h>
 
-unsigned A = 2;
+unsigned A = 2, B;
 
 //@ assigns \nothing;
 void requiresInv() {
@@ -14,9 +14,11 @@ void requiresInv() {
 void breaksInv() {
 	A += 1;
 }
+
 //@ assigns \nothing;
 void useless() {
 }
+
 //@ assigns A;
 void maintainsInv() {
 	if(A < 42)
@@ -24,8 +26,17 @@ void maintainsInv() {
 	else A -= 4;
 	useless();
 }
-//@ assigns A;
+
+//@ assigns B;
+void cond() {
+    if(B != 42){
+        B *= 2;
+    }
+}
+
+//@ assigns A, B;
 void main() {
+    cond();
 	maintainsInv();
 	requiresInv();
 
@@ -50,7 +61,13 @@ void main() {
 
 	meta \prop,
 			\name("invariant_2"),
-			\targets(\diff(\ALL, {main, useless})),
+			\targets(\diff(\ALL, {main, useless, cond})),
 			\context(\weak_invariant),
 		A % 2 == 0;
+
+    meta \prop,
+            \name(conditional),
+            \targets(cond),
+            \context(\conditional_invariant),
+        A == 42;
 */