diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml index 4c70e7912aa6f3fc37ee63b1e160179b3874ed1b..64bd16cb8239e8272bed82fc0653977951537875 100644 --- a/src/kernel_internals/typing/cabs2cil.ml +++ b/src/kernel_internals/typing/cabs2cil.ml @@ -3923,7 +3923,7 @@ struct let anonCompFieldName = anonCompFieldName let conditionalConversion = logicConditionalConversion let find_macro _ = raise Not_found - let find_var ?label ~var = + let find_var ?label var = let find_from_curr_env test = (* logic has always access to the ghost variables. *) match Datatype.String.Hashtbl.find ghost_env var with diff --git a/src/kernel_services/analysis/logic_interp.ml b/src/kernel_services/analysis/logic_interp.ml index 98cf45da1bd0c70c4b39f8ff3fc5e3d6fc8b56f0..7dedd4c4c7adbd6fca8949d7c940a91decff2608 100644 --- a/src/kernel_services/analysis/logic_interp.ml +++ b/src/kernel_services/analysis/logic_interp.ml @@ -27,7 +27,7 @@ open Cil_datatype exception Error of Cil_types.location * string exception Unbound of string -let find_var kf kinstr ?label ~var = +let find_var kf kinstr ?label var = let vi = try let vi = Globals.Vars.find_from_astinfo var (VLocal kf) in @@ -89,7 +89,7 @@ end) = let find_macro _ = raise Not_found - let find_var ?label ~var = find_var X.kf X.kinstr ?label ~var + let find_var ?label var = find_var X.kf X.kinstr ?label var let find_enum_tag x = try diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml index 250e409acf6a0d98e05f474c6cea24cec0d44f40..b317c5daf7a72cf8413c5e366010e7b51aacaaad 100644 --- a/src/kernel_services/ast_queries/logic_typing.ml +++ b/src/kernel_services/ast_queries/logic_typing.ml @@ -488,7 +488,7 @@ type typing_context = { anonCompFieldName : string; conditionalConversion : typ -> typ -> typ; find_macro : string -> lexpr; - find_var : ?label:string -> var:string -> logic_var; + find_var : ?label:string -> string -> logic_var; find_enum_tag : string -> exp * typ; find_comp_field: compinfo -> string -> offset; find_type : type_namespace -> string -> typ; @@ -670,7 +670,7 @@ module Make val anonCompFieldName : string val conditionalConversion : typ -> typ -> typ val find_macro : string -> lexpr - val find_var : ?label:string -> var:string -> logic_var + val find_var : ?label:string -> string -> logic_var val find_enum_tag : string -> exp * typ val find_comp_field: compinfo -> string -> offset val find_type : type_namespace -> string -> typ @@ -2615,7 +2615,7 @@ struct with Not_found -> try let label = Lenv.string_of_current_label env in - let info = ctxt.find_var ?label ~var:x in + let info = ctxt.find_var ?label x in (match info.lv_origin with | Some lv -> check_current_label loc env; diff --git a/src/kernel_services/ast_queries/logic_typing.mli b/src/kernel_services/ast_queries/logic_typing.mli index e1c613d9e297cac4e1fdc8a18ab8a31489934bf3..109b45d7f1b47375d2ed4b23d9c505c1cfb7d036 100644 --- a/src/kernel_services/ast_queries/logic_typing.mli +++ b/src/kernel_services/ast_queries/logic_typing.mli @@ -97,7 +97,7 @@ type typing_context = { anonCompFieldName : string; conditionalConversion : typ -> typ -> typ; find_macro : string -> Logic_ptree.lexpr; - find_var : ?label:string -> var:string -> logic_var; + find_var : ?label:string -> string -> logic_var; (** the label argument is a C label (obeying the restrictions of which label can be present in a \at). If present, the scope for searching local C variables is the one of the statement with @@ -262,7 +262,7 @@ module Make val anonCompFieldName : string val conditionalConversion : typ -> typ -> typ val find_macro : string -> Logic_ptree.lexpr - val find_var : ?label:string -> var:string -> logic_var + val find_var : ?label:string -> string -> logic_var (** see corresponding field in {!Logic_typing.typing_context}. *) val find_enum_tag : string -> exp * typ val find_type : type_namespace -> string -> typ diff --git a/src/plugins/aorai/data_for_aorai.ml b/src/plugins/aorai/data_for_aorai.ml index b1423f97bef4baa66534e326e85340364dd9ef14..abc05400af319157f5bf72762e44972d831f463b 100644 --- a/src/plugins/aorai/data_for_aorai.ml +++ b/src/plugins/aorai/data_for_aorai.ml @@ -697,7 +697,7 @@ struct let conditionalConversion = Cabs2cil.logicConditionalConversion let is_loop () = false let find_macro _ = raise Not_found - let find_var ?label:_ ~var:_ = raise Not_found + let find_var ?label:_ _ = raise Not_found let find_enum_tag _ = raise Not_found (*let find_comp_type ~kind:_ _ = raise Not_found*) let find_comp_field info s =