Merge branch 'feature/simplify_address_difference' into 'master'

Simplify simple address equality/difference

Closes #7

See merge request frama-c/meta!37

meta_simplify.ml

@@ -72,11 +72,24 @@ let neq_lval tl1 tl2 =
       not (Logic_utils.is_same_var l1 l2) || offset_neq of1 of2
     | _ -> false
 
-let term_lval_of_term t = match t.term_node with
+(* 
+   Assuming t is a term representing an address, 
+   returns the lval it is an address of
+*)
+let get_addressed_lval t = match t.term_node with
   | TAddrOf l -> l
   | TStartOf l -> l
   | _ -> (TMem t, TNoOffset)
 
+(*
+    If t is explicitely the address of an object,
+    returns that object.
+*)
+let get_addressed_var_opt t = match t.term_node with
+  | TAddrOf l -> Some l
+  | TStartOf l -> Some l
+  | _ -> None
+
 (* 
  * Simplifies \separated predicates to \true or \false when possible, and
  * propagates through common logic operators. Also simplifies equality and
@@ -89,14 +102,23 @@ class simplifier_visitor = object(_)
     | Pseparated [t1; t2] when Logic_utils.is_same_term t1 t2 ->
       Cil.ChangeTo Pfalse
     | Pseparated [t1; t2] ->
-      let l1 = term_lval_of_term t1 in
-      let l2 = term_lval_of_term t2 in
+      let l1 = get_addressed_lval t1 in
+      let l2 = get_addressed_lval t2 in
       if neq_lval l1 l2 then Cil.ChangeTo Ptrue
       else Cil.DoChildren
     | Prel (Rneq, t1, t2) when Logic_utils.is_same_term t1 t2 ->
       Cil.ChangeTo Pfalse
     | Prel (Req, t1, t2) when Logic_utils.is_same_term t1 t2 ->
       Cil.ChangeTo Ptrue
+    | Prel ((Req | Rneq) as rel, t1, t2)
+      when Option.is_some (get_addressed_var_opt t1)
+        && Option.is_some (get_addressed_var_opt t2) ->
+      let l1 = Option.get (get_addressed_var_opt t1) in
+      let l2 = Option.get (get_addressed_var_opt t2) in
+      if neq_lval l1 l2 then
+        if rel = Rneq then Cil.ChangeTo Ptrue
+        else Cil.ChangeTo Pfalse
+      else Cil.DoChildren
     | Pnot _ -> Cil.DoChildrenPost (function
         | Pnot t when Logic_utils.is_trivially_true t -> Pfalse
         | Pnot t when Logic_utils.is_trivially_false t -> Ptrue

tests/meta-wp/oracle/uncalled.res.oracle

@@ -6,13 +6,7 @@
 [wp] Running WP plugin...
 [wp] tests/meta-wp/uncalled.c:21: Warning: Missing 'calls' for default behavior
 [wp] Warning: Missing RTE guards
-[wp] tests/meta-wp/uncalled.c:21: Warning: 
-  Missing assigns clause (assigns 'everything' instead)
-[wp] 2 goals scheduled
-[wp] [Qed] Goal typed_main_assert_calling_1_meta : Valid
-[wp] [Qed] Goal typed_main_assert_calling_2_meta : Valid
-[wp] Proved goals:    2 / 2
-  Qed:             2
+[wp] Warning: No goal generated
 [eva] Analyzing a complete application starting at main
 [eva] Computing initial state
 [eva] Initial state computed
@@ -35,10 +29,7 @@
   ----------------------------------------------------------------------------
   0 alarms generated by the analysis.
   ----------------------------------------------------------------------------
-  Evaluation of the logical properties reached by the analysis:
-    Assertions        2 valid     0 unknown     0 invalid      2 total
-    Preconditions     0 valid     0 unknown     0 invalid      0 total
-  100% of the logical properties reached have been proven.
+  No logical properties have been reached by the analysis.
   ----------------------------------------------------------------------------
 /* Generated by Frama-C */
 void called(void)
@@ -63,8 +54,6 @@ void nowhere(void)
 
 void main(void)
 {
-  /*@ assert calling_1: meta: &called ≢ &uncalled; */
-  /*@ assert calling_2: meta: &called ≢ &nowhere; */
   called();
   void (*ptr)() = (void (*)())(& uncalled);
   ptr = (void (*)())(& pointed);

tests/meta/oracle/called_arg.res.oracle

@@ -16,7 +16,6 @@ void f(int x)
   /*@ assert p42_not_used_as_y: meta: (int)(1 + 1) ≢ 42; */
   /*@ assert p42_not_used_as_y_for_g2: meta: (int)(1 + 1) ≢ 42; */
   g2(1 + 1);
-  /*@ assert p42_not_used_as_y_for_g2: meta: ¬(&g3 ≡ &g2); */
   g3(x + 2);
   return;
 }