From 07590938189c38ba5d7c6f6de4289b8f913f8b1f Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Wed, 23 Dec 2020 15:21:38 +0100
Subject: [PATCH] synchronize with frama-c/frama-c!3005
---
convert.ml | 40 ++++++++++++++++++++--------------------
convert_acsl.ml | 18 +++++++++---------
convert_link.ml | 2 +-
generate_spec.ml | 2 +-
reorder_defs.ml | 8 ++++----
5 files changed, 35 insertions(+), 35 deletions(-)
diff --git a/convert.ml b/convert.ml
index bde251ec..585825b3 100644
--- a/convert.ml
+++ b/convert.ml
@@ -44,7 +44,7 @@ let capture_name_type env =
let typ = if is_ref then Cxx_utils.obj_lvref typ else typ in (s, typ)
| Cap_this(is_ref) ->
let (name,tkind as cname) =
- Extlib.the (Convert_env.get_current_class env)
+ Option.get (Convert_env.get_current_class env)
in
let typ =
if is_ref then Cxx_utils.unqual_type (Struct (name, tkind))
@@ -674,13 +674,13 @@ let rec convert_base_type env spec decl typ does_remove_virtual =
env
(fun d ->
let dim =
- Extlib.may_map
- (fun e ->
- let _,_,ce =
- convert_expr env empty_aux e does_remove_virtual
- in
- ce.expr_node)
- ~dft:NOTHING
+ Option.fold
+ ~some:(fun e ->
+ let _,_,ce =
+ convert_expr env empty_aux e does_remove_virtual
+ in
+ ce.expr_node)
+ ~none:NOTHING
a.dimension
in
let exp =
@@ -2125,7 +2125,7 @@ and convert_init_statement env init does_remove_virtual =
let l = List.rev l in
if l = [] then
Convert_env.fatal env "Empty list of local variable declarations";
- let base = Extlib.the base in
+ let base = Option.get base in
let decl = DECDEF (None,(base,l),loc) in
match def with
| [] ->
@@ -2864,7 +2864,7 @@ let rec implicit_op_call op env most_derived (s, t) dst src =
and in another class that inherits from it).
*)
let op_class_name =
- Extlib.the
+ Option.get
(Convert_env.class_name_from_qualifications env opname.prequalification)
in
match op.get_op env most_derived op_class_name with
@@ -3358,7 +3358,7 @@ let is_assign_operator s = s = "operator="
let add_special_member env name kind rt args =
let (class_name, tc) =
- Extlib.the
+ Option.get
(Convert_env.class_name_from_qualifications env name.prequalification)
in
let signature args =
@@ -3448,7 +3448,7 @@ and convert_class_component (env, implicits, types, fields, others) meth =
has_further_definition,_(*throws*),spec) ->
let qname = Convert_env.qualify env name in
let class_name =
- Extlib.the
+ Option.get
(Convert_env.class_name_from_qualifications
env qname.prequalification)
in
@@ -3467,7 +3467,7 @@ and convert_class_component (env, implicits, types, fields, others) meth =
let signature = {result= return_type; parameter= args_sig; variadic } in
let signature = Convert_env.signature_normalize env signature in
let name = Mangling.mangle qname tkind (Some(kind,signature)) in
- let spec = Extlib.opt_map (convert_contract benv) spec in
+ let spec = Option.map (convert_contract benv) spec in
let extern_c = false in
let spec =
if has_further_definition
@@ -3544,7 +3544,7 @@ and convert_class_component (env, implicits, types, fields, others) meth =
in
let subothers = my_implicits @ subothers in
Class.add_class (qualified_name,tkind);
- Extlib.may
+ Option.iter
(List.iter (Class.add_inheritance_relation(qualified_name, tkind)))
inherits;
Convert_env.reset_current_class new_env,
@@ -3583,7 +3583,7 @@ and convert_class_component (env, implicits, types, fields, others) meth =
::others
end else begin
(* no need to mangle names: they can be shared by various structures *)
- let bf_length = Extlib.opt_map (convert_bitfield_info env) bf_info in
+ let bf_length = Option.map (convert_bitfield_info env) bf_info in
(env,implicits,
types,
(FIELD(base,[(name,decl JUSTBASE,[],cloc),bf_length]), typ) ::fields,
@@ -3617,7 +3617,7 @@ and convert_class_component (env, implicits, types, fields, others) meth =
(Convert_env.qualify env name) TStandard in
let name = Mangling.mangle name TStandard None
in
- let tags = Extlib.opt_map (convert_enum_constants env ikind) body in
+ let tags = Option.map (convert_enum_constants env ikind) body in
(env, implicits,
ONLYTYPEDEF([SpecType (Tenum(name,tags,[]))],cloc) :: types,
fields, others)
@@ -3671,7 +3671,7 @@ let rec convert_pod_field (cfields, typs, env) field =
SpecAttr (add_attr env Cil.frama_c_mutable []) :: base
else base
in
- let bf_length = Extlib.opt_map (convert_bitfield_info env) bf_info in
+ let bf_length = Option.map (convert_bitfield_info env) bf_info in
FIELD(base, [(name,decl JUSTBASE,[],cloc),bf_length])::cfields,
(name, typ) :: typs, env
| CCompound(_, name, kind, _, body, tn, _) ->
@@ -3827,7 +3827,7 @@ let rec convert_global env glob =
let signature = Convert_env.signature_normalize env signature in
Mangling.mangle qualified_name tkind (Some (kind, signature))
in
- let spec = Extlib.opt_map (convert_contract benv) spec in
+ let spec = Option.map (convert_contract benv) spec in
let implicit = false in
let spec =
if has_further_definition then spec
@@ -3902,7 +3902,7 @@ let rec convert_global env glob =
Convert_env.typedef_normalize env qualified_name tc
in
Class.add_class (qualified_name,tc);
- Extlib.may
+ Option.iter
(List.iter (Class.add_inheritance_relation(qualified_name,tc)))
inherits;
let env = convert_class env name tc kind inherits body has_virtual in
@@ -4025,7 +4025,7 @@ let rec convert_global env glob =
qualified_name TStandard in
Mangling.mangle qualified_name t None
in
- let tags = Extlib.opt_map (convert_enum_constants env ikind) body in
+ let tags = Option.map (convert_enum_constants env ikind) body in
let glob = ONLYTYPEDEF([SpecType (Tenum(name,tags,[]))],cloc) in
let env = Convert_env.add_c_global env glob in
let env = Convert_env.set_ghost env old_ghost in
diff --git a/convert_acsl.ml b/convert_acsl.ml
index 04267725..82c53f05 100644
--- a/convert_acsl.ml
+++ b/convert_acsl.ml
@@ -336,11 +336,11 @@ and convert_logic_expr_node env = function
| TComprehension (t,quants,pred) ->
let quants = List.map (convert_var_decl env) quants in
let t = convert_logic_expr env t in
- let pred = Extlib.opt_map (convert_pred_named env) pred in
+ let pred = Option.map (convert_pred_named env) pred in
PLcomprehension (t,quants,pred)
| TRange(l,h) ->
- let l = Extlib.opt_map (convert_logic_expr env) l in
- let h = Extlib.opt_map (convert_logic_expr env) h in
+ let l = Option.map (convert_logic_expr env) l in
+ let h = Option.map (convert_logic_expr env) h in
PLrange(l,h)
| TLet(info,t) ->
let body = convert_inner_body env info in
@@ -623,9 +623,9 @@ let convert_variant env v = convert_logic_expr env v.vbody, v.vname
let convert_function_contract env contract =
let spec_behavior = List.map (convert_behavior env) contract.behavior in
- let spec_variant = Extlib.opt_map (convert_variant env) contract.variant in
+ let spec_variant = Option.map (convert_variant env) contract.variant in
let spec_terminates =
- Extlib.opt_map (convert_pred_named env) contract.terminates
+ Option.map (convert_pred_named env) contract.terminates
in
let spec_complete_behaviors =
List.map (fun c -> c.behaviors) contract.complete_behaviors
@@ -698,7 +698,7 @@ let rec convert_annot env annot =
Mangling.mangle info_name t None
in
let labels = List.map convert_logic_label info.arg_labels in
- let rt = Extlib.opt_map (convert_logic_type env) info.returned_type in
+ let rt = Option.map (convert_logic_type env) info.returned_type in
let params = List.map (convert_logic_param env) info.profile in
(match info.fun_body,rt with
| LBnone, None ->
@@ -741,9 +741,9 @@ let rec convert_annot env annot =
let mangle name signature =
let name, t = Convert_env.typedef_normalize env name TStandard in
Mangling.mangle name t signature in
- let read = Extlib.opt_map (Extlib.swap mangle None)
+ let read = Option.map (Extlib.swap mangle None)
read in
- let write = Extlib.opt_map (Extlib.swap mangle None)
+ let write = Option.map (Extlib.swap mangle None)
write in
LDvolatile(mem,(read,write)), env
| Daxiomatic(loc,s,annots) ->
@@ -760,7 +760,7 @@ let rec convert_annot env annot =
env lt_info.type_name TStandard in
Mangling.mangle info_name t None
in
- let def = Extlib.opt_map (convert_logic_type_def env)
+ let def = Option.map (convert_logic_type_def env)
lt_info.definition in
LDtype(name, lt_info.params, def), env
| Dlemma(loc,name,is_axiom,labs,params,body) ->
diff --git a/convert_link.ml b/convert_link.ml
index 0c58a336..258d2005 100644
--- a/convert_link.ml
+++ b/convert_link.ml
@@ -131,7 +131,7 @@ class clean =
let c =
List.map
(fun (bind, body) ->
- add_subtypes (Extlib.the self#current_kf) bind, body)
+ add_subtypes (Option.get self#current_kf) bind, body)
c
in
s.skind <- TryCatch(t,c,l);
diff --git a/generate_spec.ml b/generate_spec.ml
index af83e29f..93f48b10 100644
--- a/generate_spec.ml
+++ b/generate_spec.ml
@@ -80,7 +80,7 @@ let add_separated_arg env acc arg =
match typ, Convert_env.current_struct_or_union env with
| (Struct (name,ts), (CClass | CStruct)) | Union (name,ts), CUnion
when Fclang_datatype.Qualified_name.equal
- (name,ts) (Extlib.the (Convert_env.get_current_class env))
+ (name,ts) (Option.get (Convert_env.get_current_class env))
->
let lexpr_loc = Cil_datatype.Location.of_lexing_loc arg.arg_loc in
let p =
diff --git a/reorder_defs.ml b/reorder_defs.ml
index cb31302c..b42541b7 100644
--- a/reorder_defs.ml
+++ b/reorder_defs.ml
@@ -291,7 +291,7 @@ end = struct
Frama_Clang_option.debug
~dkey "Need to move %a before %a"
print_node n print_node node;
- (false, Extlib.the n.glob, Some n))
+ (false, Option.get n.glob, Some n))
preds
in
add_dep res (defs @ wlist)
@@ -338,7 +338,7 @@ class compute_deps =
val mutable current_def = None
method private add_deps node =
- Dependencies.add_dependency node (Extlib.the current_def)
+ Dependencies.add_dependency node (Option.get current_def)
method! vtypespec = function
| Tstruct (s,_,_) ->
@@ -373,7 +373,7 @@ class compute_deps =
(match find_type_specifier l with
| Tenum(_, Some tags,_) ->
let process_tag (name,_,_) =
- Dependencies.set_symbol Id name false (Extlib.the current_def)
+ Dependencies.set_symbol Id name false (Option.get current_def)
in
List.iter process_tag tags
| Tstruct(_, Some l, _) | Tunion(_, Some l, _) ->
@@ -381,7 +381,7 @@ class compute_deps =
function
| FIELD(_,l) ->
let process_name ((n,_,_,_),_) =
- Dependencies.set_symbol Field n false (Extlib.the current_def)
+ Dependencies.set_symbol Field n false (Option.get current_def)
in
List.iter process_name l
| TYPE_ANNOT _ -> ()
--
GitLab