From 735ebf09e981491e2d474bc30c470254e10891d3 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Mon, 8 Feb 2021 14:54:51 +0100
Subject: [PATCH] [Kernel] avoid triggering warning 16
(unerasable-optional-argument)
---
src/kernel_internals/typing/cabs2cil.ml | 2 +-
src/kernel_services/analysis/logic_interp.ml | 4 ++--
src/kernel_services/ast_queries/logic_typing.ml | 6 +++---
src/kernel_services/ast_queries/logic_typing.mli | 4 ++--
src/plugins/aorai/data_for_aorai.ml | 2 +-
5 files changed, 9 insertions(+), 9 deletions(-)
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 4c70e7912aa..64bd16cb823 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 98cf45da1bd..7dedd4c4c7a 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 250e409acf6..b317c5daf7a 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 e1c613d9e29..109b45d7f1b 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 b1423f97bef..abc05400af3 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 =
--
GitLab