Skip to content
Snippets Groups Projects
Commit 03c5d654 authored by Valentin Perrelle's avatar Valentin Perrelle
Browse files

[Kernel] Fix a typo in functions name

parent d23b1281
No related branches found
No related tags found
No related merge requests found
......@@ -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 =
......
......@@ -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. *)
......
......@@ -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
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment