From 9845f7777a2bcc1d4f445382fd7f6123140680bc Mon Sep 17 00:00:00 2001
From: Boris Yakobowski <boris.yakobowski@cea.fr>
Date: Sun, 7 Aug 2016 15:26:40 +0200
Subject: [PATCH] Adapt to trunk branch feature/virgile/filecheck-result
(removal of field return_stmt)
---
src/plugins/e-acsl/dup_functions.ml | 7 +++----
src/plugins/e-acsl/visit.ml | 2 +-
2 files changed, 4 insertions(+), 5 deletions(-)
diff --git a/src/plugins/e-acsl/dup_functions.ml b/src/plugins/e-acsl/dup_functions.ml
index c9c6d57ad0c..57741158f65 100644
--- a/src/plugins/e-acsl/dup_functions.ml
+++ b/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;
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index fa9e17d473c..03b1c827851 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/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
--
GitLab