From 2271f156e142d363602a553c6dcbfc440b2ab3e0 Mon Sep 17 00:00:00 2001
From: Thibault Martin <thi.martin.pro@pm.me>
Date: Mon, 18 Mar 2024 12:13:27 +0100
Subject: [PATCH] Use new Current_loc mechanism to set loc locally
---
convert.ml | 190 ++++++++++++++++++++++--------------------------
convert_acsl.ml | 50 ++++++++-----
convert_env.ml | 2 +-
3 files changed, 118 insertions(+), 124 deletions(-)
diff --git a/convert.ml b/convert.ml
index 39a08595..50c629a2 100644
--- a/convert.ml
+++ b/convert.ml
@@ -420,6 +420,25 @@ let find_loc_list f l =
in
aux l
+let find_class_decl_loc = function
+ | CMethod (loc,_,_,_,_,_,_,_,_,_,_,_)
+ | CCompound (loc,_,_,_,_,_,_)
+ | CFieldDecl (loc,_,_,_,_)
+ | CTypedef (loc,_,_)
+ | CStaticConst (loc,_,_,_,_)
+ | CEnum (loc,_,_,_)
+ | Class_annot (loc,_) -> loc
+
+let find_loc_translation_unit_decl = function
+ | Function (_,_,loc,_,_,_,_,_,_,_,_,_,_)
+ | Compound(loc,_,_,_,_,_,_,_,_)
+ | GlobalVarDecl(loc,_,_,_,_,_)
+ | Typedef(loc,_,_,_,_)
+ | Namespace (loc,_,_)
+ | StaticConst (loc,_,_,_,_,_,_)
+ | EnumDecl(loc,_,_,_,_,_)
+ | GlobalAnnotation(loc,_) -> loc
+
let find_loc_stmt =
function
| Nop l -> l
@@ -654,8 +673,8 @@ let rec convert_base_type env spec decl typ does_remove_virtual =
let attrs = List.map cv_to_attr spec in
env,
(rt,
- (fun d ->
- rt_decl
+ (fun d ->
+ rt_decl
(PROTO (decl (protect_ptr_type attrs d), args,[],variadic))))
| LVReference (PFunctionPointer s)
| RVReference (PFunctionPointer s) ->
@@ -665,7 +684,7 @@ let rec convert_base_type env spec decl typ does_remove_virtual =
let attrs= List.map cv_to_attr spec in
env,
(rt,
- (fun d ->
+ (fun d ->
rt_decl (PROTO (decl (protect_ptr_type attrs d),args,[],variadic))))
| Pointer(PStandardMethodPointer _)
| LVReference (PStandardMethodPointer _)
@@ -1011,7 +1030,7 @@ and convert_expr_node ?(drop_temp=false) env aux e does_remove_virtual =
env (rt,decl JUSTBASE)
(mk_addrof env (mk_expr env (MEMBEROF(e, cname)))))
| RPKVirtualBasePointer(base_index, origin_type, noeffect) ->
- let derived_name,td =
+ let derived_name, td =
Convert_env.get_class_name_from_pointer
env origin_type.plain_type
in
@@ -1881,7 +1900,8 @@ and init_lambda_single_overload env aux lam_name lam_type ovl closures =
and convert_expr ?drop_temp env aux e =
let env = Convert_env.set_loc env e.eloc in
- convert_expr_node ?drop_temp env aux e.econtent
+ let loc = Convert_env.get_loc env in
+ Current_loc.with_loc loc (convert_expr_node ?drop_temp env aux) e.econtent
and convert_list_expr env aux l does_remove_virtual =
let env, aux, args =
@@ -2126,21 +2146,21 @@ and convert_init_statement env init does_remove_virtual =
let env = Convert_env.add_local_var env id_name typ.plain_type in
match init_val with
| None ->
- let init = (id_name, decl JUSTBASE,[],loc),NO_INIT in
- (env, aux, init::l, def, base)
+ let init = (id_name, decl JUSTBASE,[],loc),NO_INIT in
+ (env, aux, init::l, def, base)
| Some init ->
let var = Local { prequalification = []; decl_name = id_name } in
let env,aux',init, def' =
convert_initializer env typ var init does_remove_virtual
in
- let def = match def' with
- | None -> def
- | Some stmt -> stmt::def
- in
- let init = (id_name, decl JUSTBASE,attrs,loc),init in
- env, merge_aux aux' aux, init::l, def, base)
- init_declarator_list
- (env, empty_aux, [], [], None)
+ let def = match def' with
+ | None -> def
+ | Some stmt -> stmt::def
+ in
+ let init = (id_name, decl JUSTBASE,attrs,loc),init in
+ env, merge_aux aux' aux, init::l, def, base)
+ init_declarator_list
+ (env, empty_aux, [], [], None)
in
let l = List.rev l in
if l = [] then
@@ -2193,6 +2213,7 @@ and convert_incr_statement env incr does_remove_virtual =
env, mk_expr_l loc (GNU_BODY { blabels=[]; battrs=[]; bstmts = stmts })
and convert_statement env st does_remove_virtual =
+ let open Current_loc.Operators in
let rec add_temps tmps stmt =
match tmps with
| [] -> stmt
@@ -2221,55 +2242,45 @@ and convert_statement env st does_remove_virtual =
let block = List.fold_left (add_temp_update env) [] tmps in
make_block_stmt env (stmt::block)
in
+ let env = Convert_env.set_loc env (find_loc_stmt st) in
+ let cloc = Convert_env.get_loc env in
+ let<> UpdatedCurrentLoc = cloc in
let raw, env =
match st with
- | Nop l -> NOP (Cil_datatype.Location.of_lexing_loc l), env
- | Code_annot (l,annot) ->
- let env = Convert_env.set_loc env l in
- let cloc = Convert_env.get_loc env in
+ | Nop _ -> NOP (cloc), env
+ | Code_annot (_,annot) ->
let env, c_annot = Convert_acsl.convert_code_annot env annot in
CODE_ANNOT(c_annot,cloc), env
- | Return (l,Some e) ->
+ | Return (_,Some e) ->
let e = add_temporary (* env *) e in
let env, aux, e = convert_full_expr env e does_remove_virtual in
let e = convert_ref env (Convert_env.get_current_return_type env) e in
let aux = preserved_returned_object aux e in
- let stmt = RETURN(e,Cil_datatype.Location.of_lexing_loc l) in
+ let stmt = RETURN(e, cloc) in
let stmts = add_temps aux stmt in
stmts, env
- | Return(l, None) ->
- let cl = Cil_datatype.Location.of_lexing_loc l in
- RETURN({expr_loc = cl; expr_node = NOTHING},cl), env
- | Expression (loc,e) ->
- let env = Convert_env.set_loc env loc in
- let cloc = Cil_datatype.Location.of_lexing_loc loc in
+ | Return(_, None) ->
+ RETURN({expr_loc = cloc; expr_node = NOTHING},cloc), env
+ | Expression (_,e) ->
let env, aux, e =
convert_full_expr ~drop_temp:true env e does_remove_virtual
in
add_temps aux (COMPUTATION(e,cloc)), env
- | VirtualExpression (loc,e) ->
- let cloc = Cil_datatype.Location.of_lexing_loc loc in
+ | VirtualExpression (_,e) ->
if does_remove_virtual then NOP cloc, env
else
- let env = Convert_env.set_loc env loc in
let env, aux, e = convert_full_expr env e does_remove_virtual in
add_temps aux (COMPUTATION(e,cloc)), env
- | Ghost_block(loc,stmts) ->
+ | Ghost_block(_,stmts) ->
let old_ghost = Convert_env.is_ghost env in
- let env = Convert_env.set_loc env loc in
let env = Convert_env.set_ghost env true in
- let cloc = Cil_datatype.Location.of_lexing_loc loc in
let b, env = convert_block env stmts does_remove_virtual in
let env = Convert_env.set_ghost env old_ghost in
BLOCK(b,cloc,cloc), env
- | Block(loc,stmts) ->
- let env = Convert_env.set_loc env loc in
- let cloc = Cil_datatype.Location.of_lexing_loc loc in
+ | Block(_,stmts) ->
let b, env = convert_block env stmts does_remove_virtual in
BLOCK(b, cloc, cloc), env
- | Condition(loc,cond,true_action,false_action) ->
- let env = Convert_env.set_loc env loc in
- let cloc = Cil_datatype.Location.of_lexing_loc loc in
+ | Condition(_,cond,true_action,false_action) ->
let env, aux, cond = convert_condition env cond does_remove_virtual in
let true_action, env =
convert_statement env true_action does_remove_virtual
@@ -2278,18 +2289,12 @@ and convert_statement env st does_remove_virtual =
convert_statement env false_action does_remove_virtual
in
add_temps aux (IF(cond,true_action,false_action,cloc)), env
- | Label(loc,lab) ->
- let env = Convert_env.set_loc env loc in
- let cloc = Cil_datatype.Location.of_lexing_loc loc in
- let stmt = make_stmt env (NOP cloc) in
+ | Label(_,lab) ->
+ let stmt = make_stmt env (NOP (cloc)) in
LABEL(lab,stmt,cloc), env
- | Goto(loc,lab) ->
- let env = Convert_env.set_loc env loc in
- let cloc = Cil_datatype.Location.of_lexing_loc loc in
+ | Goto(_,lab) ->
GOTO(lab,cloc), env
- | Switch(loc,cond,cases) ->
- let env = Convert_env.set_loc env loc in
- let cloc = Cil_datatype.Location.of_lexing_loc loc in
+ | Switch(_,cond,cases) ->
let env, aux, cond = convert_condition env cond does_remove_virtual in
let cases_loc = find_loc_case_stmt_list cases in
let cases_loc = Cil_datatype.Location.of_lexing_loc cases_loc in
@@ -2300,9 +2305,7 @@ and convert_statement env st does_remove_virtual =
let cases = { blabels = []; battrs = []; bstmts = List.rev cases } in
let cases = make_stmt env (BLOCK(cases,cases_loc,cases_loc)) in
add_temps aux (SWITCH(cond,cases,cloc)), env
- | VarDecl (loc, name, typ, init) ->
- let env = Convert_env.set_loc env loc in
- let cloc = Cil_datatype.Location.of_lexing_loc loc in
+ | VarDecl (_, name, typ, init) ->
let env, (base, decl) = convert_specifiers env typ does_remove_virtual in
let qual_name = { prequalification = []; decl_name = name } in
let attrs = add_fc_destructor_attr env typ [] in
@@ -2347,11 +2350,9 @@ and convert_statement env st does_remove_virtual =
SEQUENCE (make_stmt env def, make_stmt env block, cloc)
in
stmt, env
- | Break l -> BREAK (Cil_datatype.Location.of_lexing_loc l), env
- | Continue l -> CONTINUE (Cil_datatype.Location.of_lexing_loc l), env
- | While (loc, cond, body, annot) ->
- let env = Convert_env.set_loc env loc in
- let cloc = Cil_datatype.Location.of_lexing_loc loc in
+ | Break _ -> BREAK (cloc), env
+ | Continue _ -> CONTINUE (cloc), env
+ | While (_, cond, body, annot) ->
let env, aux, cond = convert_full_expr env cond does_remove_virtual in
let body,env = convert_statement env body does_remove_virtual in
let body = add_temps_update aux body in
@@ -2359,9 +2360,7 @@ and convert_statement env st does_remove_virtual =
Convert_env.env_map Convert_acsl.convert_code_annot env annot
in
add_temps aux (WHILE(annot,cond,body,cloc)), env
- | DoWhile (loc, cond, body,annot) ->
- let env = Convert_env.set_loc env loc in
- let cloc = Cil_datatype.Location.of_lexing_loc loc in
+ | DoWhile (_, cond, body,annot) ->
let env, aux, cond = convert_full_expr env cond does_remove_virtual in
let body, env = convert_statement env body does_remove_virtual in
let body = add_temps_update aux body in
@@ -2369,9 +2368,7 @@ and convert_statement env st does_remove_virtual =
Convert_env.env_map Convert_acsl.convert_code_annot env annot
in
add_temps aux (DOWHILE(annot, cond, body, cloc)), env
- | For(loc, init, cond, incr, body,annot) ->
- let env = Convert_env.set_loc env loc in
- let cloc = Cil_datatype.Location.of_lexing_loc loc in
+ | For(_, init, cond, incr, body,annot) ->
let init, stmts, ienv =
convert_init_statement env init does_remove_virtual
in
@@ -2398,9 +2395,7 @@ and convert_statement env st does_remove_virtual =
make_block ienv (stmts @ block)
in
stmt, Convert_env.unscope ienv env
- | TryCatch (loc, t, c) ->
- let env = Convert_env.set_loc env loc in
- let cloc = Cil_datatype.Location.of_lexing_loc loc in
+ | TryCatch (_, t, c) ->
let t, env = convert_stmt_list env t does_remove_virtual in
let t = make_block_stmt env t in
let c, env =
@@ -2409,7 +2404,7 @@ and convert_statement env st does_remove_virtual =
in
let c = List.rev c in
TRY_CATCH(t,c,cloc), env
- | GccInlineAsm(loc, qual, instr, details) ->
+ | GccInlineAsm(_, qual, instr, details) ->
let qual = List.map (fun x -> cv_to_attr (convert_cv x)) qual in
let convert_asm_IO asm_io =
List.map
@@ -2425,7 +2420,6 @@ and convert_statement env st does_remove_virtual =
ainputs=convert_asm_IO i;
aclobbers=c; alabels=l }
in
- let cloc = Cil_datatype.Location.of_lexing_loc loc in
ASM(qual, instr, details, cloc), env
in
make_stmt env raw, env
@@ -2510,8 +2504,10 @@ let convert_enum_constants env ikind l =
List.map (convert_enum_constant env ikind) l
let convert_static_const env loc name ikind kind value does_remove_virtual =
+ let open Current_loc.Operators in
let env = Convert_env.set_loc env loc in
- let cloc = Cil_datatype.Location.of_lexing_loc loc in
+ let cloc = Convert_env.get_loc env in
+ let<> UpdatedCurrentLoc = cloc in
let qualified_name = Convert_env.qualify env name in
let name =
if Convert_env.is_extern_c env then name
@@ -3513,8 +3509,12 @@ let rec collect_class_components env body =
(* Note: the list of others global definition must be built in reverse
order, as it will be reverted by the callers. *)
and convert_class_component (env, implicits, types, fields, others) meth =
+ let open Current_loc.Operators in
+ let env = Convert_env.set_loc env (find_class_decl_loc meth) in
+ let cloc = Convert_env.get_loc env in
+ let<> UpdatedCurrentLoc = cloc in
match meth with
- | CMethod(loc,name,kind,return_type,all_args,variadic,body,implicit,tkind,
+ | CMethod(_,name,kind,return_type,all_args,variadic,body,implicit,tkind,
has_further_definition,_(*throws*),spec) ->
let qname = Convert_env.qualify env name in
let class_name =
@@ -3522,8 +3522,6 @@ and convert_class_component (env, implicits, types, fields, others) meth =
(Convert_env.class_name_from_qualifications
env qname.prequalification)
in
- let env = Convert_env.set_loc env loc in
- let cloc = Cil_datatype.Location.of_lexing_loc loc in
let env = add_special_member env qname kind return_type all_args in
let all_args = if implicit then add_arg_names all_args else all_args in
let args = remove_this_parameter kind all_args in
@@ -3592,12 +3590,11 @@ and convert_class_component (env, implicits, types, fields, others) meth =
FUNDEF(spec,(rt,name),cbody,cloc,cloc)
:: FUNDEF(spec,defname_bare,cbody_bare,cloc,cloc)
:: others))
- | CCompound(loc,name,kind,inherits,body,tkind,has_virtual) ->
- let new_env = Convert_env.set_loc env loc in
+ | CCompound(_,name,kind,inherits,body,tkind,has_virtual) ->
let is_extern_c = Convert_env.is_extern_c env in
- let qualified_name = Convert_env.qualify new_env name in
+ let qualified_name = Convert_env.qualify env name in
let new_env =
- make_class_env new_env (Declaration name) kind tkind is_extern_c
+ make_class_env env (Declaration name) kind tkind is_extern_c
in
let new_env,new_implicits,subtypes,subfields,subothers =
match body with
@@ -3633,9 +3630,7 @@ and convert_class_component (env, implicits, types, fields, others) meth =
::(List.append subtypes types))),
fields,
List.append subothers others
- | CFieldDecl(loc, name, typ, bf_info, is_mutable) ->
- let env = Convert_env.set_loc env loc in
- let cloc = Cil_datatype.Location.of_lexing_loc loc in
+ | CFieldDecl(_, name, typ, bf_info, is_mutable) ->
let env, (base,decl) = convert_specifiers env typ false in
(* We remove static qualifier to avoid confusion with the C's static. *)
let base =
@@ -3670,9 +3665,7 @@ and convert_class_component (env, implicits, types, fields, others) meth =
(FIELD(base,[(name,decl JUSTBASE,[],cloc),bf_length]), typ) ::fields,
others)
end
- | CTypedef (loc,name,typ) ->
- let env = Convert_env.set_loc env loc in
- let cloc = Cil_datatype.Location.of_lexing_loc loc in
+ | CTypedef (_,name,typ) ->
let qual_name = Convert_env.qualify env name in
let env = Convert_env.add_typedef env qual_name typ in
let name,_= Convert_env.typedef_normalize env qual_name TStandard in
@@ -3691,9 +3684,7 @@ and convert_class_component (env, implicits, types, fields, others) meth =
convert_static_const env loc name ikind ICLiteral value false
in
(env,implicits,types,fields,decl :: others)
- | CEnum(loc,name,ikind, body) ->
- let env = Convert_env.set_loc env loc in
- let cloc = Cil_datatype.Location.of_lexing_loc loc in
+ | CEnum(_,name,ikind, body) ->
let name, _ = Convert_env.typedef_normalize env
(Convert_env.qualify env name) TStandard in
let name = Mangling.mangle name TStandard None
@@ -3702,8 +3693,7 @@ and convert_class_component (env, implicits, types, fields, others) meth =
(env, implicits,
ONLYTYPEDEF([SpecType (Tenum(name,tags,[]))],cloc) :: types,
fields, others)
- | Class_annot(loc,annot) ->
- let env = Convert_env.set_loc env loc in
+ | Class_annot(_,annot) ->
let env, annot = Convert_acsl.convert_annot env annot in
(env,implicits,types,fields,GLOBANNOT [annot]:: others)
@@ -3816,15 +3806,18 @@ let is_frama_clang_array_init_name = function
(* NB: we should have a loc for the declaration itself
as well as for the body*)
let rec convert_global env glob =
+ let open Current_loc.Operators in
+ let env = Convert_env.set_loc env (find_loc_translation_unit_decl glob) in
+ let cloc = Convert_env.get_loc env in
+ let<> UpdatedCurrentLoc = cloc in
match glob with
- | GlobalAnnotation(loc,annot) ->
- let env = Convert_env.set_loc env loc in
+ | GlobalAnnotation(_,annot) ->
let env, annot = Convert_acsl.convert_annot env annot in
Convert_env.add_c_global env (GLOBANNOT [annot])
| Function (name, _, _, _, _, _, _, _, _, _, _, _, _)
when do_not_translate name
-> env
- | Function(name, kind, loc, return_type,all_args,
+ | Function(name, kind, _, return_type,all_args,
body, extern_c, ghost, variadic, tkind, has_further_definition,
_ (* throws *), spec) ->
let attrs =
@@ -3833,8 +3826,6 @@ let rec convert_global env glob =
else []
in
let all_args = constify_receiver kind all_args in
- let env = Convert_env.set_loc env loc in
- let cloc = Cil_datatype.Location.of_lexing_loc loc in
let benv = Convert_env.set_extern_c env extern_c in
let benv = Convert_env.set_ghost benv ghost in
let args = remove_this_parameter kind all_args in
@@ -3916,9 +3907,8 @@ let rec convert_global env glob =
let env = Convert_env.add_c_global env glob in
Convert_env.reset_func env
)
- | Compound(loc,name,kind,inherits,body,has_virtual,tc, is_extern_c,ghost) ->
+ | Compound(_,name,kind,inherits,body,has_virtual,tc, is_extern_c,ghost) ->
let old_ghost = Convert_env.is_ghost env in
- let env = Convert_env.set_loc env loc in
let env = Convert_env.set_extern_c env is_extern_c in
let env = Convert_env.set_ghost env ghost in
let qualified_name =
@@ -3935,9 +3925,7 @@ let rec convert_global env glob =
inherits;
let env = convert_class env name tc kind inherits body has_virtual in
Convert_env.set_ghost env old_ghost
- | GlobalVarDecl(loc,name,typ,init,is_extern_c, ghost) ->
- let env = Convert_env.set_loc env loc in
- let cloc = Cil_datatype.Location.of_lexing_loc loc in
+ | GlobalVarDecl(_,name,typ,init,is_extern_c, ghost) ->
let env = Convert_env.set_extern_c env is_extern_c in
let qualified_name = make_qualified_name env name in
let name =
@@ -3988,11 +3976,9 @@ let rec convert_global env glob =
Convert_env.set_ghost env old_ghost
(* Just don't pollute the C file with these types. *)
| Typedef(_,Declaration(t),_,_, _) when Cxx_utils.is_builtin_type t -> env
- | Typedef(loc,name,typ,is_extern_c_context, ghost) ->
+ | Typedef(_,name,typ,is_extern_c_context, ghost) ->
let old_ghost = Convert_env.is_ghost env in
let env = Convert_env.set_ghost env ghost in
- let env = Convert_env.set_loc env loc in
- let cloc = Cil_datatype.Location.of_lexing_loc loc in
let qual_name = make_qualified_name env name in
let env = Convert_env.add_typedef env qual_name typ in
let env =
@@ -4038,11 +4024,9 @@ let rec convert_global env glob =
let env = Convert_env.add_c_global env decl in
let env = Convert_env.set_ghost env old_ghost in
Convert_env.set_extern_c env old_extern_c
- | EnumDecl(loc,name,ikind, body,is_extern_c_context,ghost) ->
+ | EnumDecl(_,name,ikind, body,is_extern_c_context,ghost) ->
let old_ghost = Convert_env.is_ghost env in
- let env = Convert_env.set_loc env loc in
let env = Convert_env.set_ghost env ghost in
- let cloc = Cil_datatype.Location.of_lexing_loc loc in
let env = Convert_env.set_extern_c env is_extern_c_context in
let qualified_name = make_qualified_name env name in
let name =
diff --git a/convert_acsl.ml b/convert_acsl.ml
index c844ea36..5c8ed78b 100644
--- a/convert_acsl.ml
+++ b/convert_acsl.ml
@@ -23,6 +23,16 @@
open Intermediate_format
open Logic_ptree
+let find_loc_glob_annot = function
+ | Dfun_or_pred(loc,_)
+ | Daxiomatic(loc,_,_)
+ | Dtype (loc,_)
+ | Dlemma(loc,_,_,_,_,_)
+ | Dinvariant(loc,_)
+ | Dtype_annot(loc,_)
+ | Dmodel_annot(loc,_)
+ | Dvolatile(loc,_,_,_) -> loc
+
let convert_var env is_extern_c vi =
match vi.logic_var_lv_kind with
| LVGlobal | LVCGlobal ->
@@ -252,14 +262,16 @@ let rec plor ce1 ce2 =
| _ -> PLor (ce1, ce2)
let rec convert_logic_expr env e =
+ let open Current_loc.Operators in
let env = Convert_env.set_loc env e.loc in
let lexpr_loc = Convert_env.get_loc env in
+ let<> UpdatedCurrentLoc = lexpr_loc in
let env, lexpr_node = convert_logic_expr_node env e.node in
let anonymous = { lexpr_loc; lexpr_node } in
let res =
- List.fold_right
- (fun s res -> { lexpr_loc; lexpr_node = PLnamed(s,res) })
- e.names anonymous
+ List.fold_right
+ (fun s res -> { lexpr_loc; lexpr_node = PLnamed(s,res) })
+ e.names anonymous
in
env, res
and convert_logic_expr_node env = function
@@ -474,8 +486,10 @@ and path_of_offset env = function
env, PLpathIndex(i) :: path
and convert_pred_named env p =
+ let open Current_loc.Operators in
let env = Convert_env.set_loc env p.pred_loc in
let pred_loc = Convert_env.get_loc env in
+ let<> UpdatedCurrentLoc = pred_loc in
let env, cp = convert_pred env p.pred_content in
let cp =
List.fold_right
@@ -685,7 +699,7 @@ let convert_behavior env bhv =
let env, b_allocation = convert_allocation env bhv.alloc in
let env, b_extended = env_map convert_extended env bhv.extended in
env, { b_name; b_requires; b_assumes; b_post_cond;
- b_assigns; b_allocation; b_extended }
+ b_assigns; b_allocation; b_extended }
let convert_variant env v =
let env, body = convert_logic_expr env v.vbody in
@@ -773,10 +787,13 @@ let convert_code_annot env = function
env, APragma p
let rec convert_annot env annot =
+ let open Current_loc.Operators in
+ let env = Convert_env.set_loc env (find_loc_glob_annot annot) in
+ let loc = Convert_env.get_loc env in
+ let<> UpdatedCurrentLoc = loc in
let env, annot =
match annot with
- | Dfun_or_pred (loc,info) ->
- let env = Convert_env.set_loc env loc in
+ | Dfun_or_pred (_,info) ->
(* we don't necessarily need to mangle according to the signature,
as ACSL itself feature overloading. If we decide to have unique
names, we'll need to adapt mangling to accomodate for logic types.
@@ -830,8 +847,7 @@ let rec convert_annot env annot =
let env, body = Convert_env.env_map inductive_case env body in
env, LDinductive_def(name,labels,info.tparams,params,body)
)
- | Dvolatile(loc,mem,read,write) ->
- let env = Convert_env.set_loc env loc in
+ | Dvolatile(_,mem,read,write) ->
let env, mem = Convert_env.env_map convert_logic_expr env mem in
(* NB: should we have the real type of the arguments of the functions?*)
let mangle name signature =
@@ -840,12 +856,10 @@ let rec convert_annot env annot =
let read = Option.map (Fun.flip mangle None) read in
let write = Option.map (Fun.flip mangle None) write in
env, LDvolatile(mem,(read,write))
- | Daxiomatic(loc,s,annots) ->
- let env = Convert_env.set_loc env loc in
+ | Daxiomatic(_,s,annots) ->
let env, annots = Convert_env.env_map convert_annot env annots in
env, LDaxiomatic(s,annots)
- | Dtype(loc,lt_info) ->
- let env = Convert_env.set_loc env loc in
+ | Dtype(_,lt_info) ->
let name =
if lt_info.logic_type_info_is_extern_c then
lt_info.type_name.decl_name
@@ -859,14 +873,12 @@ let rec convert_annot env annot =
Convert_env.env_opt convert_logic_type_def env lt_info.definition
in
env, LDtype(name, lt_info.params, def)
- | Dlemma(loc,name,is_axiom,labs,params,body) ->
- let env = Convert_env.set_loc env loc in
+ | Dlemma(_,name,is_axiom,labs,params,body) ->
let labs = List.map convert_logic_label labs in
let kind = if is_axiom then Cil_types.Admit else Assert in
let env, body = convert_pred_tp env ~kind body in
env, LDlemma(name,labs,params,body)
- | Dinvariant(loc,body) ->
- let env = Convert_env.set_loc env loc in
+ | Dinvariant(_,body) ->
let name =
if body.li_extern_c then
body.li_name.decl_name
@@ -883,8 +895,7 @@ let rec convert_annot env annot =
Convert_env.fatal env "unexpected body for a global invariant"
in
env, LDinvariant(name, body)
- | Dtype_annot (loc, body) ->
- let env = Convert_env.set_loc env loc in
+ | Dtype_annot (_, body) ->
let inv_name =
if body.li_extern_c then
body.li_name.decl_name
@@ -909,8 +920,7 @@ let rec convert_annot env annot =
| _ -> Convert_env.fatal env "unexpected body for a type invariant"
in
env, LDtype_annot { inv_name; this_type; this_name; inv }
- | Dmodel_annot(loc,model) ->
- let env = Convert_env.set_loc env loc in
+ | Dmodel_annot(_,model) ->
let model_name = model.Intermediate_format.model_name in
let env, model_type = convert_logic_type env model.field_type in
let env, model_for_type = convert_logic_type env model.base_type in
diff --git a/convert_env.ml b/convert_env.ml
index a5251122..f215e185 100644
--- a/convert_env.ml
+++ b/convert_env.ml
@@ -160,7 +160,7 @@ let temp_name env s =
let set_loc env loc =
let loc = Cil_datatype.Location.of_lexing_loc loc in
- Current_loc.set loc; { env with location = loc }
+ { env with location = loc }
let get_loc env = env.location
--
GitLab