From b2925f8b403f419b8cc9b5f3fa5f3b2d02de6f30 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Thu, 12 May 2011 13:36:16 +0000
Subject: [PATCH] explicitely mark as unimplement function contracts + overload
vglob_aux instead of vglob
---
src/plugins/e-acsl/visit.ml | 18 +++++++++++++++++-
1 file changed, 17 insertions(+), 1 deletion(-)
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index 9791cc62cc0..75e89dd90a6 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -464,7 +464,7 @@ class e_acsl_visitor prj generate = object (self)
val mutable gen_vars = []
- method vglob g =
+ method vglob_aux g =
if !first_global then begin
first_global := false;
ChangeDoChildrenPost([ g ], fun l -> e_acsl_header () :: l)
@@ -475,6 +475,22 @@ class e_acsl_visitor prj generate = object (self)
BUT almost impossible without a main entry point *)
(* method vinit v off i = assert false *)
+ method vvdec vi =
+ try
+ let kf = Globals.Functions.get vi in
+ let spec = Kernel_function.get_spec kf in
+ if spec.spec_behavior <> [] then not_yet "behaviors clause of function";
+ if spec.spec_variant <> None then not_yet "variant clause of function";
+ if spec.spec_terminates <> None then
+ not_yet "terminates clause of function";
+ if spec.spec_complete_behaviors <> [] then
+ not_yet "complete behaviors of function";
+ if spec.spec_disjoint_behaviors <> [] then
+ not_yet "disjoint behaviors of function";
+ DoChildren
+ with Not_found ->
+ DoChildren
+
method vfundec f =
let add_gen_vars f = f.slocals <- gen_vars @ f.slocals; f in
ChangeDoChildrenPost(f, add_gen_vars)
--
GitLab