Merge branch 'feature/virgile/filecheck-result' into 'master'

Adapt to trunk branch  feature/virgile/filecheck-result

(removal of field return_stmt)

See merge request !71

src/plugins/e-acsl/dup_functions.ml

@@ -191,16 +191,15 @@ let dup_fundec loc spec bhv kf vi new_vi =
     sbody = body;
     smaxstmtid = None;
     sallstmts = [];
-    sspec = new_spec }, 
-  return
+    sspec = new_spec }
 
 let dup_global loc old_prj spec bhv kf vi new_vi = 
   let name = vi.vname in
   Options.feedback ~dkey ~level:2 "entering in function %s" name;
-  let fundec, return = dup_fundec loc spec bhv kf vi new_vi  in
+  let fundec = dup_fundec loc spec bhv kf vi new_vi  in
   let fct = Definition(fundec, loc) in
   let new_spec = fundec.sspec in
-  let new_kf = { fundec = fct; return_stmt = Some return; spec = new_spec } in
+  let new_kf = { fundec = fct; spec = new_spec } in
   Kernel_function.Hashtbl.add fct_tbl new_kf ();
   Globals.Functions.register new_kf;
   Globals.Functions.replace_by_definition new_spec fundec loc;

src/plugins/e-acsl/visit.ml

@@ -206,7 +206,7 @@ class e_acsl_visitor prj generate = object (self)
               (* Create and register [__e_acsl_globals_init] as kernel
                  function *)
               let kf =
-                { fundec = fct; return_stmt = Some return; spec = spec }
+                { fundec = fct; spec = spec }
               in
               Globals.Functions.register kf;
               Globals.Functions.replace_by_definition