From 93575d83908d502f3386f9aca17d79f518a25791 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 5 May 2022 09:26:30 +0200
Subject: [PATCH] [kernel] Ast_diff: fixes the check of goto targets by
function.
---
src/kernel_services/ast_queries/ast_diff.ml | 4 ++++
1 file changed, 4 insertions(+)
diff --git a/src/kernel_services/ast_queries/ast_diff.ml b/src/kernel_services/ast_queries/ast_diff.ml
index 3abd04b4dc0..c7551b0733b 100644
--- a/src/kernel_services/ast_queries/ast_diff.ml
+++ b/src/kernel_services/ast_queries/ast_diff.ml
@@ -1258,6 +1258,10 @@ and is_same_binder b b' env =
and formals mapping to have been put in the local env
*)
and is_same_fundec f f' env: body_correspondance =
+ (* The goto_targets field of [env] accumulates visited goto targets to be
+ verified after the function body. If the given environment is not empty,
+ resets this field for this function. *)
+ let env = { env with goto_targets = [] } in
let res, env =
is_same_block f.sbody f'.sbody env &&>
check_goto_targets
--
GitLab