[e-acsl] \result

src/plugins/e-acsl/TODO

 à traiter avant la 1ère release:
 - quantifications sans exentension de syntaxe
-- \return
 
 ########
 # CODE #
 ########
 
+- mixed assumes and ensures
 - function contracts for functions only declared
   ==> le noyau génère un "assigns \nothing" pour ces fonctions...
   ce assign n'est de toute façon pas gérer
@@ -25,6 +25,7 @@
 # KNOWN BUGS #
 ##############
 - \at incorrect si StmtLabel faisant référence au stmt courant (voir test at.i)
+- incorrect d'utiliser un \old dans le post-state si pre-state == post-state
 
 #########
 # TESTS #

src/plugins/e-acsl/env.ml

@@ -148,13 +148,17 @@ let new_var ?(global=false) env t ty mk_stmts =
   let local_env, _ = top env in
   if global then
     (* do not use memoisation here: it is incorrect for terms corresponding to
-       impure expressions *)
+       impure expressions
+       [JS 2011/11/23] actually it is correct now since globals are only use for
+       \at *)
     do_new_var ~global env t ty mk_stmts  
   else
     try
       match t with
       | None -> raise No_term
-      | Some t -> Term.Map.find t local_env.mpz_tbl.new_exps, env
+      | Some t -> 
+	Options.feedback "memoized %a" Term.pretty t;
+	Term.Map.find t local_env.mpz_tbl.new_exps, env
     with Not_found | No_term -> 
       do_new_var ~global env t ty mk_stmts  
 

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.res.oracle

+[e-acsl] memoized \old(x)
+[e-acsl] memoized \old(x)
+[e-acsl] memoized \old(x)-\old(x)
+tests/e-acsl-runtime/result.i:7:[e-acsl] warning: missing guard for ensuring that the given integer is C-representable
+[e-acsl] memoized \result
+[e-acsl] memoized 0
+[value] Analyzing a complete application starting at main
+[value] Computing initial state
+[value] Initial state computed
+[value] Values of globals at initialization
+        Y ∈ {1}
+[value] computing for function f <- main.
+        Called from PROJECT_FILE.i:188.
+[value] computing for function mpz_init_set_si <- f <- main.
+        Called from PROJECT_FILE.i:143.
+PROJECT_FILE.i:33:[value] Function mpz_init_set_si: postcondition got status valid.
+[value] Done for function mpz_init_set_si
+[value] computing for function mpz_init <- f <- main.
+        Called from PROJECT_FILE.i:144.
+PROJECT_FILE.i:21:[value] Function mpz_init: postcondition got status valid.
+[value] Done for function mpz_init
+[value] computing for function mpz_sub <- f <- main.
+        Called from PROJECT_FILE.i:145.
+PROJECT_FILE.i:70:[value] Function mpz_sub: precondition got status valid.
+PROJECT_FILE.i:71:[value] Function mpz_sub: precondition got status valid.
+PROJECT_FILE.i:72:[value] Function mpz_sub: precondition got status valid.
+[value] Done for function mpz_sub
+[value] computing for function mpz_get_si <- f <- main.
+        Called from PROJECT_FILE.i:146.
+PROJECT_FILE.i:96:[value] Function mpz_get_si: precondition got status valid.
+[value] Done for function mpz_get_si
+[value] computing for function e_acsl_fail <- f <- main.
+        Called from PROJECT_FILE.i:148.
+[value] computing for function printf <- e_acsl_fail <- f <- main.
+        Called from PROJECT_FILE.i:129.
+[value] Done for function printf
+[value] computing for function exit <- e_acsl_fail <- f <- main.
+        Called from PROJECT_FILE.i:129.
+PROJECT_FILE.i:119:[value] Function exit: postcondition got status invalid.
+[value] Done for function exit
+[value] Recording results for e_acsl_fail
+[value] Done for function e_acsl_fail
+[value] computing for function mpz_clear <- f <- main.
+        Called from PROJECT_FILE.i:150.
+PROJECT_FILE.i:43:[value] Function mpz_clear: precondition got status valid.
+[value] Done for function mpz_clear
+[value] computing for function mpz_clear <- f <- main.
+        Called from PROJECT_FILE.i:151.
+[value] Done for function mpz_clear
+PROJECT_FILE.i:131:[value] Function f: postcondition got status valid.
+[value] Recording results for f
+[value] Done for function f
+[value] computing for function g <- main.
+        Called from PROJECT_FILE.i:189.
+PROJECT_FILE.i:158:[value] Function g: postcondition got status valid.
+[value] Recording results for g
+[value] Done for function g
+[value] computing for function h <- main.
+        Called from PROJECT_FILE.i:190.
+[value] computing for function mpz_init_set_si <- h <- main.
+        Called from PROJECT_FILE.i:174.
+[value] Done for function mpz_init_set_si
+[value] computing for function mpz_init_set_si <- h <- main.
+        Called from PROJECT_FILE.i:175.
+[value] Done for function mpz_init_set_si
+[value] computing for function mpz_cmp <- h <- main.
+        Called from PROJECT_FILE.i:176.
+PROJECT_FILE.i:49:[value] Function mpz_cmp: precondition got status valid.
+PROJECT_FILE.i:50:[value] Function mpz_cmp: precondition got status valid.
+[value] Done for function mpz_cmp
+[value] computing for function e_acsl_fail <- h <- main.
+        Called from PROJECT_FILE.i:177.
+[value] computing for function printf <- e_acsl_fail <- h <- main.
+        Called from PROJECT_FILE.i:129.
+[value] Done for function printf
+[value] computing for function exit <- e_acsl_fail <- h <- main.
+        Called from PROJECT_FILE.i:129.
+[value] Done for function exit
+[value] Recording results for e_acsl_fail
+[value] Done for function e_acsl_fail
+[value] computing for function mpz_clear <- h <- main.
+        Called from PROJECT_FILE.i:178.
+[value] Done for function mpz_clear
+[value] computing for function mpz_clear <- h <- main.
+        Called from PROJECT_FILE.i:179.
+[value] Done for function mpz_clear
+PROJECT_FILE.i:165:[value] Function h: postcondition got status valid.
+[value] Recording results for h
+[value] Done for function h
+[value] Recording results for main
+[value] done for function main
+[value] ====== VALUES COMPUTED ======
+[value] Values for function g:
+[value] Values for function e_acsl_fail:
+          NON TERMINATING FUNCTION
+[value] Values for function f:
+          x ∈ {0}
+          e_acsl_1 ∈ {1}
+          e_acsl_3 ∈ {1}
+[value] Values for function h:
+          __retres ∈ {0}
+[value] Values for function main:
+          __retres ∈ {0}
+/* Generated by Frama-C */
+struct __anonstruct___mpz_struct_1 {
+   int _mp_alloc ;
+   int _mp_size ;
+   unsigned long *_mp_d ;
+};
+typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
+typedef __mpz_struct mpz_t[1];
+/*@ ensures \valid(\old(x));
+    assigns *x;  */
+extern void mpz_init(__mpz_struct * /*[1]*/ x);
+/*@ ensures \valid(\old(z));
+    assigns *z;
+    assigns *z \from n;  */
+extern void mpz_init_set_si(__mpz_struct * /*[1]*/ z, long n);
+/*@ requires \valid(x);
+    assigns *x;  */
+extern void mpz_clear(__mpz_struct * /*[1]*/ x);
+/*@ requires \valid(z1);
+    requires \valid(z2);
+    assigns \nothing;  */
+extern int mpz_cmp(__mpz_struct const * /*[1]*/ z1,
+                   __mpz_struct const * /*[1]*/ z2);
+/*@ requires \valid(z1);
+    requires \valid(z2);
+    requires \valid(z3);
+    assigns *z1; 
+*/
+extern void mpz_sub(__mpz_struct * /*[1]*/ z1,
+                    __mpz_struct const * /*[1]*/ z2,
+                    __mpz_struct const * /*[1]*/ z3);
+/*@ requires \valid(z);
+    assigns \nothing;  */
+extern long mpz_get_si(__mpz_struct const * /*[1]*/ z);
+/*@ terminates \false;
+    ensures \false;
+    assigns \nothing;  */
+extern void exit(int status);
+/*@ assigns \nothing;  */
+extern int printf(char const * , ...);
+void e_acsl_fail(char *msg)
+{
+  printf("%s\n",msg);
+  exit(1);
+  return;
+}
+
+/*@ ensures \result ≡ (int)(\old(x)-\old(x));  */
+int f(int x)
+{
+  int e_acsl_1;
+  int e_acsl_3;
+  e_acsl_3 = x;
+  e_acsl_1 = x;
+  x = 0;
+  {
+    mpz_t e_acsl_2;
+    mpz_t e_acsl_4;
+    int e_acsl_5;
+    mpz_init_set_si((__mpz_struct *)(e_acsl_2),(long)e_acsl_1);
+    mpz_init((__mpz_struct *)(e_acsl_4));
+    mpz_sub((__mpz_struct *)(e_acsl_4),(__mpz_struct const *)(e_acsl_2),
+            (__mpz_struct const *)(e_acsl_2));
+    e_acsl_5 = (int)mpz_get_si((__mpz_struct const *)(e_acsl_4));
+    if (! (x == e_acsl_5)) {
+      e_acsl_fail((char *)"(\\result == (int)(\\old(x)-\\old(x)))");
+    }
+    mpz_clear((__mpz_struct *)(e_acsl_2));
+    mpz_clear((__mpz_struct *)(e_acsl_4));
+    return (x);
+  }
+  
+}
+
+int Y = 1;
+/*@ ensures \result ≡ Y;  */
+int g(int x)
+{
+  if (! (x == Y)) { e_acsl_fail((char *)"(\\result == Y)"); }
+  return (x);
+}
+
+/*@ ensures \result ≡ 0;  */
+int h(void)
+{
+  int __retres;
+  __retres = 0;
+  {
+    mpz_t e_acsl_1;
+    mpz_t e_acsl_2;
+    int e_acsl_3;
+    mpz_init_set_si((__mpz_struct *)(e_acsl_1),(long)__retres);
+    mpz_init_set_si((__mpz_struct *)(e_acsl_2),(long)0);
+    e_acsl_3 = mpz_cmp((__mpz_struct const *)(e_acsl_1),
+                       (__mpz_struct const *)(e_acsl_2));
+    if (! (e_acsl_3 == 0)) { e_acsl_fail((char *)"(\\result == 0)"); }
+    mpz_clear((__mpz_struct *)(e_acsl_1));
+    mpz_clear((__mpz_struct *)(e_acsl_2));
+    return (__retres);
+  }
+  
+}
+
+int main(void)
+{
+  int __retres;
+  f(1);
+  g(Y);
+  h();
+  __retres = 0;
+  return (__retres);
+}
+
+

src/plugins/e-acsl/tests/e-acsl-runtime/result.i

+/* run.config
+   COMMENT: \result
+   EXECNOW: LOG gen_result.c BIN gen_result.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/result.i -e-acsl-project p -e-acsl-include-headers -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_result.c > /dev/null && gcc -o ./tests/e-acsl-runtime/result/gen_result.out ./tests/e-acsl-runtime/result/gen_result.c -lgmp
+*/
+
+// && ./tests/e-acsl-runtime/result/gen_result.out
+/*@ ensures \result == (int)(x - x); */
+int f(int x) { 
+  x = 0; 
+  return x; }
+
+int Y = 1;
+
+// does not work since it is converted into \result == \old(x) and, 
+// in this particular case, the pre-state and the post-state are the same and 
+// it does not work yet (related to issue in at.i).
+// /*@ ensures \result == x; */ 
+/*@ ensures \result == Y; */
+int g(int x) { 
+  return x; 
+}
+
+/*@ ensures \result == 0; */
+int h() { return 0; }
+
+int main(void) {
+  f(1);
+  g(Y);
+  h();
+  return 0;
+}

src/plugins/e-acsl/visit.ml

@@ -145,7 +145,16 @@ let constant_to_exp ?(loc=Location.unknown) = function
 let rec thost_to_host env = function
   | TVar { lv_origin = Some v } -> Var v, env
   | TVar { lv_origin = None } -> Misc.not_yet "logic variable"
-  | TResult _typ -> Misc.not_yet "\\result"
+  | TResult _typ -> 
+    let vis = Env.get_visitor env in
+    let kf = Extlib.the vis#current_kf in
+    let stmt = 
+      try Kernel_function.find_return kf 
+      with Kernel_function.No_Statement -> assert false
+    in
+    (match stmt.skind with
+    | Return(Some { enode = Lval (lhost, NoOffset) }, _) -> lhost, env
+    | _ -> assert false)
   | TMem t ->
     let e, env = term_to_exp env (Ctype intType) t in
     Options.warning ~source:(fst e.eloc) ~once:true
@@ -307,7 +316,7 @@ and context_insensitive_term_to_exp env t =
        That is this variable which is the resulting expression. 
        ACSL typing rule ensures that the type of this variable is the same as
        the one of [e]. *)
-    let res, env =
+    let res, new_env =
       Env.new_var ~global:true env
 	(Some t) (typeOf e)
 	(fun lv' e' -> 
@@ -316,15 +325,16 @@ and context_insensitive_term_to_exp env t =
 	     initialize it. *)
 	  new_v := Some (lv', e'); [])
     in
-    let env_ref = ref env in
-    (* visitor modifying in place the labeled statement in order to store [e] in
-       the resulting variable at this location which is the only correct one. *)
+    let env_ref = ref new_env in
+      (* visitor modifying in place the labeled statement in order to store [e]
+	 in the resulting variable at this location which is the only correct
+	 one. *)
     let o = object 
       inherit Visitor.frama_c_inplace
       method vstmt_aux stmt = 
 	let new_lv, new_e = Extlib.the !new_v in
-	(* either a standard C affectation or an mpz one according to type of
-	   [e] *) 
+	  (* either a standard C affectation or an mpz one according to type of
+	     [e] *) 
 	let new_stmt =
 	  if Mpz.is_t (typeOf new_e) then
 	    Mpz.init_set new_e e
@@ -332,23 +342,21 @@ and context_insensitive_term_to_exp env t =
 	    mkStmtOneInstr ~valid_sid:true
 	      (Set((Var new_lv, NoOffset), e, Location.unknown))
 	in
-	assert (!env_ref == env);
-	(* generate the new block of code for the labeled statement and the
-	   corresponding environment *)
-	let block, env = 
-	  Env.pop_and_get env new_stmt ~global_clear:false Env.Middle
+	assert (!env_ref == new_env);
+	  (* generate the new block of code for the labeled statement and the
+	     corresponding environment *)
+	let block, new_env = 
+	  Env.pop_and_get new_env new_stmt ~global_clear:false Env.Middle
 	in
 	let pre = match label with
 	  | LogicLabel(_, s) when s = "Here" || s = "Post" -> true
 	  | StmtLabel _ | LogicLabel _ -> false
 	in
-	env_ref := Env.extend_stmt_in_place env stmt ~pre block;
-(*	Options.feedback "the new stmt is (sid %d): %a" stmt.sid 
-	  Stmt.pretty stmt;*)
+	env_ref := Env.extend_stmt_in_place new_env stmt ~pre block;
 	ChangeTo stmt
     end
     in
-    let bhv = (Env.get_visitor env)#behavior in
+    let bhv = (Env.get_visitor new_env)#behavior in
     let new_stmt = Visitor.visitFramacStmt o (get_stmt bhv stmt) in
     set_stmt bhv stmt new_stmt;
     res, !env_ref, false
@@ -379,11 +387,11 @@ and comparison_to_exp ?(loc=Location.unknown) ?e1 env bop t1 t2 t_opt =
   let ctx = match e1 with
     | None -> principal_type_from_term t1 t2 
     | Some(_, ctx) -> 
-(*      Options.feedback "principality oriented by %a" d_logic_type ctx;*)
+      (*      Options.feedback "principality oriented by %a" d_logic_type ctx;*)
       principal_type_from_term { t1 with term_type = ctx } t2
   in
-(*  Options.feedback "principal type of %a and %a is %a" 
-    d_term t1 d_term t2 d_logic_type ctx;*)
+  (*  Options.feedback "principal type of %a and %a is %a" 
+      d_term t1 d_term t2 d_logic_type ctx;*)
   let e1, env = match e1 with
     | None -> term_to_exp env ctx t1
     | Some(e1, ctx1) when Cil_datatype.Logic_type.equal ctx ctx1 -> e1, env