diff --git a/src/kernel_services/analysis/logic_deps.ml b/src/kernel_services/analysis/logic_deps.ml index fb860df288dfeb6809e7017254ba02053dcf4e3f..5f1598f76e7117cf8a83634ba2d44af5187cda47 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 daa77f213739efd79b793f54a430ceda36e90fb7..2a25e71b12cf111e880689779b9111fbf4299c00 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 879a9dfac0b8525294c062c438686e54982bc76c..da0865896fa1318201e1e18505b146cd79d5f947 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