[Eva] fixes traces domain for return statement

  - It seems not given by value to the domains

src/plugins/value/domains/traces/traces_domain.ml

@@ -493,35 +493,37 @@ module D = Domain_builder.Complete (Internal)
 
 let dummy_loc = Cil_datatype.Location.unknown
 
-let rec stmts_of_cfg cfg current acc =
+let rec stmts_of_cfg cfg current return_exp acc =
   match Graph.find current cfg with
-  | exception Not_found -> List.rev acc
+  | exception Not_found ->
+    let return_stmt = Cil.mkStmt (Cil_types.Return(return_exp,dummy_loc)) in
+    List.rev (return_stmt::acc)
   | [] -> assert false
   | [a] ->
     (match a with
      | Assign (n,lval,_typ,exp) ->
        let stmt = Cil.mkStmtOneInstr (Cil_types.Set(lval,exp,dummy_loc)) in
-       stmts_of_cfg cfg n (stmt::acc)
+       stmts_of_cfg cfg n return_exp (stmt::acc)
      | Assume (n,exp,b) ->
        let predicate = (Logic_utils.expr_to_predicate ~cast:true exp).Cil_types.ip_content in
        let predicate = if b then predicate else Logic_const.pnot predicate in
        let code_annot = Logic_const.new_code_annotation(Cil_types.AAssert([],predicate)) in
        let stmt = Cil.mkStmtOneInstr (Cil_types.Code_annot(code_annot,dummy_loc)) in
-       stmts_of_cfg cfg n (stmt::acc)
+       stmts_of_cfg cfg n return_exp (stmt::acc)
      | EnterScope (n,vs) ->
        let block = { Cil_types.battrs = [];
                      bscoping = true;
                      blocals = vs;
                      bstatics = [];
-                     bstmts = stmts_of_cfg cfg n [] } in
+                     bstmts = stmts_of_cfg cfg n return_exp [] } in
        let stmt = Cil.mkStmt (Cil_types.Block(block)) in
        List.rev (stmt::acc)
-     | LeaveScope (n,_) -> stmts_of_cfg cfg n acc
+     | LeaveScope (n,_) -> stmts_of_cfg cfg n return_exp acc
      | CallDeclared (n,kf,exps,lval) ->
        let call = Cil.new_exp ~loc:dummy_loc (Cil_types.Lval (Cil.var (Kernel_function.get_vi kf))) in
        let stmt = Cil.mkStmtOneInstr (Cil_types.Call(lval,call,exps,dummy_loc)) in
-       stmts_of_cfg cfg n (stmt::acc)
-     | Msg (n,_) -> stmts_of_cfg cfg n acc
+       stmts_of_cfg cfg n return_exp (stmt::acc)
+     | Msg (n,_) -> stmts_of_cfg cfg n return_exp acc
      | Top -> invalid_arg "top in the middle")
   | l ->
     let is_if = match l with
@@ -534,8 +536,8 @@ let rec stmts_of_cfg cfg current acc =
       match is_if with
       | None -> assert false (* todo *)
       | Some(exp,n1,n2) ->
-        let block1 = Cil.mkBlock (stmts_of_cfg cfg n1 []) in
-        let block2 = Cil.mkBlock (stmts_of_cfg cfg n2 []) in
+        let block1 = Cil.mkBlock (stmts_of_cfg cfg n1 return_exp []) in
+        let block2 = Cil.mkBlock (stmts_of_cfg cfg n2 return_exp []) in
         Cil.mkStmt (Cil_types.If(exp,block1,block2,dummy_loc)) in
     List.rev (stmt::acc)
 
@@ -543,7 +545,7 @@ let _ = Cil.stmt_of_instr_list
 
 let _ = File.from_filename
 
-let project_of_cfg s =
+let project_of_cfg vreturn s =
   let project = Project.create_by_copy ~selection:State_selection.empty ~last:true "Eva.Traces_domain" in
   let main = fst (Globals.entry_point ()) in
   let fundecls =
@@ -555,16 +557,20 @@ let project_of_cfg s =
     !l in
   let file = Project.on project (fun () ->
       let file = Ast.get () in
-      file.Cil_types.globals <-
-        List.map (fun v -> Cil_types.GVarDecl(v,dummy_loc)) s.globals;
+      (** main function *)
       let fundec = Cil.emptyFunctionFromVI (Kernel_function.get_vi main) in
       fundec.Cil_types.sformals <- s.main_formals;
-      let stmts = stmts_of_cfg s.graph s.start [] in
-      fundec.Cil_types.sbody <- Cil.mkBlock stmts;
-      (* Kernel_function.register_stmt *)
+      let stmts = Cil.mkBlock (stmts_of_cfg s.graph s.start vreturn []) in
+      (* Format.printf "@[<2>@[stmts:@] %a@]@." Printer.pp_block stmts; *)
+      fundec.Cil_types.sbody <- stmts;
+      file.Cil_types.globals <- Cil_types.GFun(fundec,dummy_loc) :: file.Cil_types.globals;
+      (* declared functions *)
       let fundecls = List.map (fun (fundecl,v) -> Cil_types.GFunDecl(fundecl,v,dummy_loc)) fundecls in
       file.Cil_types.globals <- fundecls @ file.Cil_types.globals;
-      file.Cil_types.globals <- Cil_types.GFun(fundec,dummy_loc) :: file.Cil_types.globals;
+      (* globals *)
+      file.Cil_types.globals <-
+        (List.map (fun v -> Cil_types.GVarDecl(v,dummy_loc)) s.globals)
+        @ file.Cil_types.globals;
       file
     ) () in
   ignore (Cil.refresh_visit project);
@@ -573,11 +579,15 @@ let project_of_cfg s =
 
 
 let print_last_traces () =
-  let state = D.Store.get_stmt_state (Kernel_function.find_return (fst (Globals.entry_point ())))  in
+  let return_stmt = Kernel_function.find_return (fst (Globals.entry_point ())) in
+  let return_exp = match return_stmt.Cil_types.skind with
+    | Cil_types.Return (oexp,_) -> oexp
+    | _ -> assert false in
+  let state = D.Store.get_stmt_state ~after:true return_stmt  in
   let header fmt = Format.fprintf fmt "Trace domains:" in
   let body = Bottom.pretty Traces.pretty in
   Value_parameters.printf ~dkey:Internal.log_category ~header " @[%a@]" body state;
-  Bottom.iter project_of_cfg state
+  Bottom.iter (project_of_cfg return_exp) state
 
 
 (*

tests/value/traces/oracle/test1.res.oracle

@@ -77,9 +77,9 @@ c -> 5 ])
     66 -> ([ LeaveScope: i -> 67 ])
     67 -> ([ Assign: g = tmp -> 70 ])
     68 -> ([ Assign: g = tmp -> 69 ])
-    69 -> ([ join -> 105 ])
-    70 -> ([ join -> 105 ]) ]}
- current: 105]
+    69 -> ([ join -> 107 ])
+    70 -> ([ join -> 107 ]) ]}
+ current: 107]
 [kernel] warning: no input file.
 [from] Computing for function main
 [from] Computing for function Frama_C_interval <-main
@@ -93,8 +93,82 @@ c -> 5 ])
 [from] Function main:
   Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
   g FROM Frama_C_entropy_source; g
+  \result FROM Frama_C_entropy_source; g
 [from] ====== END OF DEPENDENCIES ======
 [inout] Out (internal) for function main:
           Frama_C_entropy_source; g; c; tmp; i
 [inout] Inputs for function main:
           Frama_C_entropy_source; g
+[value] Analyzing a complete application starting at main
+[value] Computing initial state
+[value] Initial state computed
+[value:initial-state] Values of globals at initialization
+  Frama_C_entropy_source ∈ [--..--]
+[value] using specification for function Frama_C_interval
+share/libc/__fc_builtin.h:52:[value] warning: function Frama_C_interval: precondition got status unknown.
+[value] done for function main
+[value] ====== VALUES COMPUTED ======
+[value:final-states] Values at end of function main:
+  Frama_C_entropy_source ∈ [--..--]
+  g ∈ {5; 45}
+  c ∈ [--..--]
+  __retres ∈ {5; 45}
+/* Generated by Frama-C */
+#include "__fc_builtin.h"
+int g;
+
+int main(int c)
+{
+  int __retres;
+  g = 42;
+  {
+    int tmp;
+    {
+      int \result<Frama_C_interval>;
+      \result<Frama_C_interval> = Frama_C_interval(0,1);
+      c = \result<Frama_C_interval>;
+      tmp = 0;
+      if (c) {
+        tmp = g;
+        {
+          i = 0;
+          /*@ assert i < 3; */ ;
+          tmp ++;
+          i ++;
+          /*@ assert i < 3; */ ;
+          tmp ++;
+          i ++;
+          /*@ assert i < 3; */ ;
+          tmp ++;
+          i ++;
+          /*@ assert ¬(i < 3); */ ;
+          g = tmp;
+          __retres = tmp;
+          goto return_label;
+        }
+      }
+      else {
+        tmp = 2;
+        {
+          i = 0;
+          /*@ assert i < 3; */ ;
+          tmp ++;
+          i ++;
+          /*@ assert i < 3; */ ;
+          tmp ++;
+          i ++;
+          /*@ assert i < 3; */ ;
+          tmp ++;
+          i ++;
+          /*@ assert ¬(i < 3); */ ;
+          g = tmp;
+          __retres = tmp;
+          goto return_label;
+        }
+      }
+      return_label: return __retres;
+    }
+  }
+}
+
+

tests/value/traces/oracle/test2.res.oracle

@@ -57,7 +57,7 @@ c -> 1 ])
     51 -> ([ finalize_call: loop -> 52 ])
     52 -> ([ Assign: tmp = \result<loop> -> 53 ])
     53 -> ([ LeaveScope: \result<loop> -> 54 ])
-    54 -> ([ join -> 122 ])
+    54 -> ([ join -> 124 ])
     55 -> ([ EnterScope: j -> 56 ])
     56 -> ([ Assign: j = tmp -> 57 ])
     57 -> ([ EnterScope: i -> 59 ])
@@ -85,8 +85,8 @@ c -> 1 ])
     116 -> ([ finalize_call: loop -> 117 ])
     117 -> ([ Assign: tmp = \result<loop> -> 118 ])
     118 -> ([ LeaveScope: \result<loop> -> 119 ])
-    119 -> ([ join -> 122 ]) ]}
- current: 122]
+    119 -> ([ join -> 124 ]) ]}
+ current: 124]
 [kernel] warning: no input file.
 [from] Computing for function loop
 [from] Done for function loop
@@ -97,7 +97,7 @@ c -> 1 ])
 [from] Function loop:
   \result FROM j
 [from] Function main:
-  NO EFFECTS
+  \result FROM c
 [from] ====== END OF DEPENDENCIES ======
 [inout] Out (internal) for function loop:
           j; i
@@ -107,9 +107,19 @@ c -> 1 ])
           tmp
 [inout] Inputs for function main:
           \nothing
+[value] Analyzing a complete application starting at main
+[value] Computing initial state
+[value] Initial state computed
+[value:initial-state] Values of globals at initialization
+  
+[value] done for function main
+[value] ====== VALUES COMPUTED ======
+[value:final-states] Values at end of function main:
+  __retres ∈ {4; 5}
 /* Generated by Frama-C */
-void main(int c)
+int main(int c)
 {
+  int __retres;
   {
     int tmp;
     tmp = 0;
@@ -134,6 +144,8 @@ void main(int c)
             int \result<loop>;
             \result<loop> = j;
             tmp = \result<loop>;
+            __retres = tmp;
+            goto return_label;
           }
         }
       }
@@ -159,11 +171,13 @@ void main(int c)
             int \result<loop>;
             \result<loop> = j;
             tmp = \result<loop>;
+            __retres = tmp;
+            goto return_label;
           }
         }
       }
     }
-    return;
+    return_label: return __retres;
   }
 }
 

tests/value/traces/oracle/test3.res.oracle

+[kernel] Parsing tests/value/traces/test3.i (no preprocessing)
+[value] Analyzing a complete application starting at main
+[value] Computing initial state
+[value] Initial state computed
+[value:initial-state] Values of globals at initialization
+  g ∈ {0}
+[value] Recording results for main
+[value] done for function main
+[value] ====== VALUES COMPUTED ======
+[value:final-states] Values at end of function main:
+  g ∈ {4}
+  tmp ∈ {4}
+  __retres ∈ {5}
+[value:d-traces] Trace domains:
+ start: 0; globals = g; main_formals = c 
+ {[ 0 -> ([ initialize variable: g -> 1 ])
+    1 -> ([ initialize variable using type Main_Formal
+c -> 2 ])
+    2 -> ([ EnterScope: __retres -> 3 ])
+    3 -> ([ EnterScope: tmp -> 4 ])
+    4 -> ([ initialize variable: tmp -> 5 ])
+    5 -> ([ Assign: tmp = 4 -> 6 ])
+    6 -> ([ Assume: tmp true -> 7 ])
+    7 -> ([ Assign: g = tmp -> 8 ])
+    8 -> ([ Assign: __retres = g + 1 -> 9 ]) ]}
+ current: 9]
+[kernel] warning: no input file.
+[from] Computing for function main
+[from] Done for function main
+[from] ====== DEPENDENCIES COMPUTED ======
+       These dependencies hold at termination for the executions that terminate:
+[from] Function main:
+  g FROM \nothing
+  \result FROM \nothing
+[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function main:
+          g; tmp; __retres
+[inout] Inputs for function main:
+          g
+[value] Analyzing a complete application starting at main
+[value] Computing initial state
+[value] Initial state computed
+[value:initial-state] Values of globals at initialization
+  
+[value] done for function main
+[value] ====== VALUES COMPUTED ======
+[value:final-states] Values at end of function main:
+  g ∈ {4}

tests/value/traces/test1.c

 /* run.config
-   STDOPT: #"-eva-traces-domain -value-msg-key d-traces -slevel 10"
+   STDOPT: #"-eva-traces-domain -value-msg-key d-traces -slevel 10" +"-then-last -val -print"
 */
 
 #include "__fc_builtin.h"
 
 int g = 42;
 
-void main(int c){
+int main(int c){
   c = Frama_C_interval(0,1);
   int tmp;
   tmp = 0;
@@ -16,4 +16,5 @@ void main(int c){
     tmp ++;
   }
   g = tmp;
+  return tmp;
 }

tests/value/traces/test2.i

 /* run.config
-   STDOPT: #"-eva-traces-domain -value-msg-key d-traces -slevel 10" +"-then-last -check -print"
+   STDOPT: #"-eva-traces-domain -value-msg-key d-traces -slevel 10" +"-then-last -check -print -val"
 */
 
 
@@ -10,10 +10,11 @@ int loop(int j){
   return j;
 }
 
-void main(int c){
+int main(int c){
   int tmp;
   tmp = 0;
   if (c) tmp = 1;
   else tmp = 2;
   tmp = loop(tmp);
+  return tmp;
 }

tests/value/traces/test3.i

+/* run.config
+   STDOPT: #"-eva-traces-domain -value-msg-key d-traces -slevel 10" +"-then-last -val"
+*/
+
+int g;
+
+int main(int c){
+  int tmp = 4;
+  if(tmp){
+    g = tmp;
+  } else {
+    g = 1;
+  }
+  return g+1;
+}