From 03c5d6548751164c6a9ba13dc4102dc7070bcf45 Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Fri, 21 Oct 2022 13:20:43 +0200
Subject: [PATCH] [Kernel] Fix a typo in functions name
---
src/kernel_services/analysis/logic_deps.ml | 4 ++--
src/kernel_services/analysis/logic_deps.mli | 4 ++--
src/plugins/pdg/annot.ml | 6 +++---
3 files changed, 7 insertions(+), 7 deletions(-)
diff --git a/src/kernel_services/analysis/logic_deps.ml b/src/kernel_services/analysis/logic_deps.ml
index fb860df288d..5f1598f76e7 100644
--- a/src/kernel_services/analysis/logic_deps.ml
+++ b/src/kernel_services/analysis/logic_deps.ml
@@ -47,10 +47,10 @@ type t = {before:bool ; ki:stmt ; zone:Locations.Zone.t}
type zone_info = (t list) option
type decl = {var: Varinfo.Set.t ; lbl: Logic_label.Set.t}
-let mk_ctx_func_contrat ?before kf =
+let mk_ctx_func_contract ?before kf =
{ before; site=FunctionContract; kf }
-let mk_ctx_stmt_contrat ?before kf stmt =
+let mk_ctx_stmt_contract ?before kf stmt =
{ before; site=StatementContract stmt; kf }
let mk_ctx_stmt_annot kf stmt =
diff --git a/src/kernel_services/analysis/logic_deps.mli b/src/kernel_services/analysis/logic_deps.mli
index daa77f21373..2a25e71b12c 100644
--- a/src/kernel_services/analysis/logic_deps.mli
+++ b/src/kernel_services/analysis/logic_deps.mli
@@ -26,11 +26,11 @@ val compute_term_deps: (stmt -> term -> Locations.Zone.t option) ref
type ctx
-val mk_ctx_func_contrat: ?before:bool -> kernel_function -> ctx
+val mk_ctx_func_contract: ?before:bool -> kernel_function -> ctx
(** To build an interpretation context relative to function
contracts. *)
-val mk_ctx_stmt_contrat: ?before:bool -> kernel_function -> stmt -> ctx
+val mk_ctx_stmt_contract: ?before:bool -> kernel_function -> stmt -> ctx
(** To build an interpretation context relative to statement
contracts. *)
diff --git a/src/plugins/pdg/annot.ml b/src/plugins/pdg/annot.ml
index 879a9dfac0b..da0865896fa 100644
--- a/src/plugins/pdg/annot.ml
+++ b/src/plugins/pdg/annot.ml
@@ -76,13 +76,13 @@ let find_nodes_for_function_contract pdg f_interpret =
let find_fun_precond_nodes (pdg:PdgTypes.Pdg.t) p =
let f_interpret kf =
- let f_ctx = Logic_deps.mk_ctx_func_contrat ~before:true kf in
+ let f_ctx = Logic_deps.mk_ctx_func_contract ~before:true kf in
Logic_deps.from_pred p f_ctx
in find_nodes_for_function_contract pdg f_interpret
let find_fun_postcond_nodes pdg p =
let f_interpret kf =
- let f_ctx = Logic_deps.mk_ctx_func_contrat ~before:false kf in
+ let f_ctx = Logic_deps.mk_ctx_func_contract ~before:false kf in
Logic_deps.from_pred p f_ctx
in let nodes,deps = find_nodes_for_function_contract pdg f_interpret
in let nodes =
@@ -97,7 +97,7 @@ let find_fun_postcond_nodes pdg p =
let find_fun_variant_nodes pdg t =
let f_interpret kf =
- let f_ctx = Logic_deps.mk_ctx_func_contrat ~before:true kf in
+ let f_ctx = Logic_deps.mk_ctx_func_contract ~before:true kf in
Logic_deps.from_term t f_ctx
in find_nodes_for_function_contract pdg f_interpret
--
GitLab