From 2f1c5a532eb326fceb243b4cde69ba6243d37fe7 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu, 3 Oct 2019 18:07:03 +0200
Subject: [PATCH] [Kernel] CabsVisit does not erase ghost parameters anymore
---
src/kernel_services/visitors/cabsvisit.ml | 7 +++++--
1 file changed, 5 insertions(+), 2 deletions(-)
diff --git a/src/kernel_services/visitors/cabsvisit.ml b/src/kernel_services/visitors/cabsvisit.ml
index 84bd662c1cc..2237d0abe0a 100644
--- a/src/kernel_services/visitors/cabsvisit.ml
+++ b/src/kernel_services/visitors/cabsvisit.ml
@@ -193,14 +193,17 @@ and childrenDeclType isfundef vis dt =
let al' = mapNoCopy (childrenAttribute vis) al in
let dt1' = visitCabsDeclType vis isfundef dt1 in
if al' != al || dt1' != dt1 then PTR(al', dt1') else dt
- | PROTO (dt1, snl,_, b) ->
+ | PROTO (dt1, snl, gsnl, b) ->
(* Do not propagate isfundef further *)
let dt1' = visitCabsDeclType vis false dt1 in
let _ = vis#vEnterScope () in
let snl' = mapNoCopy (childrenSingleName vis NVar) snl in
+ let gsnl' = mapNoCopy (childrenSingleName vis NVar) gsnl in
(* Exit the scope only if not in a function definition *)
let _ = if not isfundef then vis#vExitScope () in
- if dt1' != dt1 || snl' != snl then PROTO(dt1', snl',[] , b) else dt
+ if dt1' != dt1 || snl' != snl || gsnl' != gsnl then
+ PROTO(dt1', snl', gsnl' , b)
+ else dt
and childrenNameGroup vis (kind: nameKind) ((s, nl) as input) =
--
GitLab