diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index 0f1baeb7c2027fd32ee8f90aeb75ee9cc6f9145f..8fa75427624ba3f6f90a471807cdfd2575650a70 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -1849,8 +1849,8 @@ class cil_printer () = object (self)
let suppress =
not state.print_cil_input
&& not (Cil.msvcMode ())
- && (Cil.startsWith "box" an
- || Cil.startsWith "ccured" an
+ && (String.starts_with ~prefix:"box" an
+ || String.starts_with ~prefix:"ccured" an
|| an = "merger"
|| an = "cilnoremove")
in
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index dd9c80abda0b4c0838a65ba493617444d1d296c9..0cf772e7944d58bb83bb94ccac7d3f7d494f0f6b 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -1313,43 +1313,14 @@ let doVisit (vis: 'visitor)
let doVisitCil vis previsit startvisit children node =
doVisit vis vis#plain_copy_visitor previsit startvisit children node
-let rev_until i l =
- let rec aux acc =
- function
- [] -> acc
- | i'::_ when i' == i -> acc
- | i'::l -> aux (i'::acc) l
- in aux [] l
-
-(* mapNoCopy is like map but avoid copying the list if the function does not
- * change the elements. *)
-let mapNoCopy (f: 'a -> 'a) orig =
- let rec aux ((acc,has_changed) as res) l =
- match l with
- [] -> if has_changed then List.rev acc else orig
- | i :: resti ->
- let i' = f i in
- if has_changed then
- aux (i'::acc,true) resti
- else if i' != i then
- aux (i'::rev_until i orig,true) resti
- else
- aux res resti
- in aux ([],false) orig
+let mapNoCopy = Extlib.map_no_copy
+[@@alert deprecated "Use [Extlib.map_no_copy] instead"]
-let mapNoCopyList (f: 'a -> 'a list) orig =
- let rec aux ((acc,has_changed) as res) l =
- match l with
- [] -> if has_changed then List.rev acc else orig
- | i :: resti ->
- let l' = f i in
- if has_changed then
- aux (List.rev_append l' acc,true) resti
- else
- (match l' with
- [i'] when i' == i -> aux res resti
- | _ -> aux (List.rev_append l' (rev_until i orig), true) resti)
- in aux ([],false) orig
+let mapNoCopyList = Extlib.map_no_copy_list
+[@@alert deprecated "Use [Extlib.map_no_copy_list] instead"]
+
+let optMapNoCopy = Extlib.opt_map_no_copy
+[@@alert deprecated "Use [Extlib.opt_map_no_copy] instead."]
(* A visitor for lists *)
let doVisitList (vis: 'visit)
@@ -1373,7 +1344,7 @@ let doVisitList (vis: 'visit)
JustCopy | JustCopyPost _ -> only_copy_vis
| _ -> vis
in
- let nodespost = mapNoCopy (children vis) nodespre in
+ let nodespost = Extlib.map_no_copy (children vis) nodespre in
match action with
| DoChildrenPost f | ChangeDoChildrenPost (_, f) | JustCopyPost f ->
f nodespost
@@ -1382,12 +1353,6 @@ let doVisitList (vis: 'visit)
let doVisitListCil vis previsit startvisit children node =
doVisitList vis vis#plain_copy_visitor previsit startvisit children node
-let optMapNoCopy f o =
- match o with
- None -> o
- | Some x ->
- let x' = f x in if x' != x then Some x' else o
-
let debugVisit = false
let visitCilConst vis c =
@@ -1439,7 +1404,7 @@ and childrenTermNode vis tn =
let ci' =
doVisitCil vis id vis#vlogic_ctor_info_use alphabetabeta ci
in
- let args' = mapNoCopy vTerm args in
+ let args' = Extlib.map_no_copy vTerm args in
if ci' != ci || args != args' then TDataCons(ci',args') else tn
| TLval tl ->
let tl' = vTermLval tl in
@@ -1477,13 +1442,13 @@ and childrenTermNode vis tn =
| Tapp(li,labels,args) ->
let li' = vLogicInfo li in
let labels' =
- mapNoCopy (visitCilLogicLabel vis) labels in
+ Extlib.map_no_copy (visitCilLogicLabel vis) labels in
(*
Format.eprintf "Cil.children_term_node: li = %s(%d), li' = %s(%d)@."
li.l_var_info.lv_name li.l_var_info.lv_id
li'.l_var_info.lv_name li'.l_var_info.lv_id;
*)
- let args' = mapNoCopy vTerm args in
+ let args' = Extlib.map_no_copy vTerm args in
if li' != li || labels' != labels || args' != args then
Tapp(li',labels',args') else tn
| Tif(test,ttrue,tfalse) ->
@@ -1525,15 +1490,15 @@ and childrenTermNode vis tn =
| Ttype ty ->
let ty' = vTyp ty in if ty' != ty then Ttype ty' else tn
| Tunion locs ->
- let locs' = mapNoCopy (visitCilTerm vis) locs in
+ let locs' = Extlib.map_no_copy (visitCilTerm vis) locs in
if locs != locs' then Tunion(locs') else tn
| Tinter locs ->
- let locs' = mapNoCopy (visitCilTerm vis) locs in
+ let locs' = Extlib.map_no_copy (visitCilTerm vis) locs in
if locs != locs' then Tinter(locs') else tn
| Tcomprehension(lval,quant,pred) ->
let quant' = visitCilQuantifiers vis quant in
let lval' = visitCilTerm vis lval in
- let pred' = (optMapNoCopy (visitCilPredicate vis)) pred in
+ let pred' = (Extlib.opt_map_no_copy (visitCilPredicate vis)) pred in
if lval' != lval || quant' != quant || pred' != pred
then
Tcomprehension(lval',quant',pred')
@@ -1541,8 +1506,8 @@ and childrenTermNode vis tn =
tn
| Tempty_set -> tn
| Trange(low,high) ->
- let low' = optMapNoCopy (visitCilTerm vis) low in
- let high' = optMapNoCopy (visitCilTerm vis) high in
+ let low' = Extlib.opt_map_no_copy (visitCilTerm vis) low in
+ let high' = Extlib.opt_map_no_copy (visitCilTerm vis) high in
if low != low' || high != high' then Trange(low',high')
else tn
| Tlet(def,body) ->
@@ -1623,8 +1588,8 @@ and visitCilLogicInfo vis li =
and childrenLogicInfo vis li =
(* NB: underlying varinfo has been already visited. *)
- let lt = optMapNoCopy (visitCilLogicType vis) li.l_type in
- let lp = mapNoCopy (visitCilLogicVarDecl vis) li.l_profile in
+ let lt = Extlib.opt_map_no_copy (visitCilLogicType vis) li.l_type in
+ let lp = Extlib.map_no_copy (visitCilLogicVarDecl vis) li.l_profile in
li.l_type <- lt;
li.l_profile <- lp;
li.l_body <-
@@ -1632,14 +1597,14 @@ and childrenLogicInfo vis li =
match li.l_body with
| LBnone -> li.l_body
| LBreads ol ->
- let l = mapNoCopy (visitCilIdTerm vis) ol in
+ let l = Extlib.map_no_copy (visitCilIdTerm vis) ol in
if l != ol then LBreads l else li.l_body
| LBterm ot ->
let t = visitCilTerm vis ot in
if t != ot then LBterm t else li.l_body
| LBinductive inddef ->
let i =
- mapNoCopy
+ Extlib.map_no_copy
(fun (id,labs,tvars,p) ->
(id, labs, tvars, visitCilPredicate vis p))
inddef
@@ -1656,7 +1621,7 @@ and visitCilLogicTypeInfo vis lt =
vis#vlogic_type_info_decl childrenLogicTypeInfo lt
and childrenLogicTypeInfo vis lt =
- let def = optMapNoCopy (visitCilLogicTypeDef vis) lt.lt_def in
+ let def = Extlib.opt_map_no_copy (visitCilLogicTypeDef vis) lt.lt_def in
lt.lt_def <- def; lt
and visitCilLogicTypeDef vis def =
@@ -1665,7 +1630,7 @@ and visitCilLogicTypeDef vis def =
and childrenLogicTypeDef vis def =
match def with
| LTsum l ->
- let l' = mapNoCopy (visitCilLogicCtorInfoAddTable vis) l in
+ let l' = Extlib.map_no_copy (visitCilLogicCtorInfoAddTable vis) l in
if l != l' then LTsum l' else def
| LTsyn typ ->
let typ' = visitCilLogicType vis typ in
@@ -1688,7 +1653,7 @@ and childrenLogicCtorInfo vis ctor =
vis#vlogic_type_info_use alphabetabeta ctor.ctor_type
in
let ctor_params = ctor.ctor_params in
- let ctor_params' = mapNoCopy (visitCilLogicType vis) ctor_params in
+ let ctor_params' = Extlib.map_no_copy (visitCilLogicType vis) ctor_params in
if ctor_type != ctor.ctor_type || ctor_params != ctor_params' then
{ ctor with ctor_type = ctor_type; ctor_params = ctor_params' }
else ctor
@@ -1705,10 +1670,10 @@ and childrenLogicType vis ty =
| Ltype (s,l) ->
let s' = doVisitCil vis (Visitor_behavior.Get.logic_type_info vis#behavior)
vis#vlogic_type_info_use alphabetabeta s in
- let l' = mapNoCopy (visitCilLogicType vis) l in
+ let l' = Extlib.map_no_copy (visitCilLogicType vis) l in
if s' != s || l' != l then Ltype (s',l') else ty
| Larrow(args,rttyp) ->
- let args' = mapNoCopy(visitCilLogicType vis) args in
+ let args' = Extlib.map_no_copy (visitCilLogicType vis) args in
let rttyp' = visitCilLogicType vis rttyp in
if args' != args || rttyp' != rttyp then Larrow(args',rttyp') else ty
| Lvar _ -> ty
@@ -1724,7 +1689,7 @@ and visitCilLogicVarDecl vis lv =
and childrenLogicVarDecl vis lv =
lv.lv_type <- visitCilLogicType vis lv.lv_type;
lv.lv_origin <-
- optMapNoCopy (visitCilVarUse vis) lv.lv_origin;
+ Extlib.opt_map_no_copy (visitCilVarUse vis) lv.lv_origin;
lv
and visitCilLogicVarUse vis lv =
@@ -1760,11 +1725,11 @@ and visitCilLogicVarUse vis lv =
childrenLogicVarUse lv
and childrenLogicVarUse vis lv =
- lv.lv_origin <- optMapNoCopy (visitCilVarUse vis) lv.lv_origin; lv
+ lv.lv_origin <- Extlib.opt_map_no_copy (visitCilVarUse vis) lv.lv_origin; lv
and visitCilQuantifiers vis lv =
doVisitCil vis id vis#vquantifiers
- (fun vis l -> mapNoCopy (visitCilLogicVarDecl vis) l) lv
+ (fun vis l -> Extlib.map_no_copy (visitCilLogicVarDecl vis) l) lv
and visitCilIdPredicate vis ip =
doVisitCil
@@ -1803,8 +1768,8 @@ and childrenPredicateNode vis p =
Pfalse | Ptrue -> p
| Papp (pred,labels,args) ->
let pred' = vLogicInfo pred in
- let labels' = mapNoCopy (visitCilLogicLabel vis) labels in
- let args' = mapNoCopy vTerm args in
+ let labels' = Extlib.map_no_copy (visitCilLogicLabel vis) labels in
+ let args' = Extlib.map_no_copy vTerm args in
if pred' != pred || labels' != labels || args' != args then
Papp(pred',labels',args')
else p
@@ -1908,7 +1873,7 @@ and childrenPredicateNode vis p =
let t' = vTerm t in
if t' != t || s != s' then Pdangling (s',t') else p
| Pseparated seps ->
- let seps' = mapNoCopy vTerm seps in
+ let seps' = Extlib.map_no_copy vTerm seps in
if seps' != seps then Pseparated seps' else p
| Pfresh (s1,s2,t,n) ->
let s1' = visitCilLogicLabel vis s1 in
@@ -1939,7 +1904,7 @@ and visitCilFrees vis l =
and visitCilAllocates vis l =
doVisitCil vis id vis#vallocates childrenFreeAlloc l
and childrenFreeAlloc vis l =
- mapNoCopy (visitCilIdTerm vis) l
+ Extlib.map_no_copy (visitCilIdTerm vis) l
and visitCilAssigns vis a =
doVisitCil vis id vis#vassigns childrenAssigns a
@@ -1947,7 +1912,7 @@ and childrenAssigns vis a =
match a with
WritesAny -> a
| Writes l ->
- let l' = mapNoCopy (visitCilFrom vis) l in
+ let l' = Extlib.map_no_copy (visitCilFrom vis) l in
if l' != l then Writes l' else a
and visitCilFrom vis f =
@@ -1963,7 +1928,7 @@ and childrenDeps vis d =
match d with
FromAny -> d
| From l ->
- let l' = mapNoCopy (visitCilIdTerm vis) l in
+ let l' = Extlib.map_no_copy (visitCilIdTerm vis) l in
if l !=l' then From l' else d
and visitCilBehavior vis b =
@@ -1974,13 +1939,13 @@ and childrenBehavior vis b =
b.b_assumes <- visitCilPredicates vis b.b_assumes;
b.b_requires <- visitCilPredicates vis b.b_requires;
b.b_post_cond <-
- mapNoCopy
+ Extlib.map_no_copy
(function ((k,p) as pc) ->
let p' = visitCilIdPredicate vis p in if p != p' then (k,p') else pc)
b.b_post_cond;
b.b_assigns <- visitCilAssigns vis b.b_assigns;
b.b_allocation <- visitCilAllocation vis b.b_allocation ;
- b.b_extended <- mapNoCopy (visitCilExtended vis) b.b_extended;
+ b.b_extended <- Extlib.map_no_copy (visitCilExtended vis) b.b_extended;
b
and visitCilExtended vis orig =
@@ -1995,18 +1960,18 @@ and childrenCilExtended vis p =
match p with
| Ext_id _ -> p
| Ext_terms terms ->
- let terms' = mapNoCopy (visitCilTerm vis) terms in
+ let terms' = Extlib.map_no_copy (visitCilTerm vis) terms in
if terms == terms' then p else Ext_terms terms'
| Ext_preds preds ->
- let preds' = mapNoCopy (visitCilPredicate vis) preds in
+ let preds' = Extlib.map_no_copy (visitCilPredicate vis) preds in
if preds == preds' then p else Ext_preds preds'
| Ext_annot (id,annots) ->
- let annots' = mapNoCopy (visitCilExtended vis) annots in
+ let annots' = Extlib.map_no_copy (visitCilExtended vis) annots in
if annots == annots' then p else Ext_annot (id,annots')
-and visitCilPredicates vis ps = mapNoCopy (visitCilIdPredicate vis) ps
+and visitCilPredicates vis ps = Extlib.map_no_copy (visitCilIdPredicate vis) ps
-and visitCilBehaviors vis bs = mapNoCopy (visitCilBehavior vis) bs
+and visitCilBehaviors vis bs = Extlib.map_no_copy (visitCilBehavior vis) bs
and visitCilFunspec vis s =
doVisitCil vis (Visitor_behavior.cfunspec vis#behavior) vis#vspec childrenSpec s
@@ -2014,9 +1979,9 @@ and visitCilFunspec vis s =
and childrenSpec vis s =
s.spec_behavior <- visitCilBehaviors vis s.spec_behavior;
s.spec_variant <-
- optMapNoCopy (fun x -> (visitCilTerm vis (fst x), snd x)) s.spec_variant;
+ Extlib.opt_map_no_copy (fun x -> (visitCilTerm vis (fst x), snd x)) s.spec_variant;
s.spec_terminates <-
- optMapNoCopy (visitCilIdPredicate vis) s.spec_terminates;
+ Extlib.opt_map_no_copy (visitCilIdPredicate vis) s.spec_terminates;
(* nothing is done now for behaviors names, no need to visit complete and
disjoint behaviors clauses
*)
@@ -2117,9 +2082,9 @@ and childrenAnnotation vis a =
vis#get_filling_actions;
if mfi' != mfi then Dmodel_annot (mfi',loc) else a
| Dvolatile(tset,rvi,wvi,attr,loc) ->
- let tset' = mapNoCopy (visitCilIdTerm vis) tset in
- let rvi' = optMapNoCopy (visitCilVarUse vis) rvi in
- let wvi' = optMapNoCopy (visitCilVarUse vis) wvi in
+ let tset' = Extlib.map_no_copy (visitCilIdTerm vis) tset in
+ let rvi' = Extlib.opt_map_no_copy (visitCilVarUse vis) rvi in
+ let wvi' = Extlib.opt_map_no_copy (visitCilVarUse vis) wvi in
let attr' = visitCilAttributes vis attr in
if tset' != tset || rvi' != rvi || wvi' != wvi || attr' != attr then
Dvolatile(tset',rvi',wvi',attr',loc)
@@ -2128,7 +2093,7 @@ and childrenAnnotation vis a =
(*
Format.eprintf "cil.visitCilAnnotation on axiomatic %s@." id;
*)
- let l' = mapNoCopy (visitCilAnnotation vis) l in
+ let l' = Extlib.map_no_copy (visitCilAnnotation vis) l in
let attr' = visitCilAttributes vis attr in
if l' != l || attr != attr' then Daxiomatic(id,l',attr',loc) else a
| Dextended (e,attr,loc) ->
@@ -2307,7 +2272,7 @@ and childrenLocal_init vi (vis: cilVisitor) li =
if i != i' then AssignInit i' else li
| ConsInit(f,args, k) ->
let f' = visitCilVarUse vis f in
- let args' = mapNoCopy (visitCilExpr vis) args in
+ let args' = Extlib.map_no_copy (visitCilExpr vis) args in
if f' != f || args' != args then ConsInit(f',args',k) else li
and visitCilInstr (vis: cilVisitor) (i: instr) : instr list =
@@ -2330,11 +2295,11 @@ and childrenInstr (vis: cilVisitor) (i: instr) : instr =
let lv' = fLval lv in let e' = fExp e in
if lv' != lv || e' != e then Set(lv',e',l) else i
| Call(None,f,args,l) ->
- let f' = fExp f in let args' = mapNoCopy fExp args in
+ let f' = fExp f in let args' = Extlib.map_no_copy fExp args in
if f' != f || args' != args then Call(None,f',args',l) else i
| Call(Some lv,fn,args,l) ->
let lv' = fLval lv in let fn' = fExp fn in
- let args' = mapNoCopy fExp args in
+ let args' = Extlib.map_no_copy fExp args in
if lv' != lv || fn' != fn || args' != args
then Call(Some lv', fn', args', l) else i
@@ -2344,14 +2309,14 @@ and childrenInstr (vis: cilVisitor) (i: instr) : instr =
| Some ext ->
let asm_outputs_pre = ext.asm_outputs in
let asm_outputs =
- mapNoCopy
+ Extlib.map_no_copy
(fun ((id,s,lv) as pair) ->
let lv' = fLval lv in
if lv' != lv then (id,s,lv') else pair) asm_outputs_pre
in
let asm_inputs_pre = ext.asm_inputs in
let asm_inputs =
- mapNoCopy
+ Extlib.map_no_copy
(fun ((id,s,e) as pair) ->
let e' = fExp e in
if e' != e then (id,s,e') else pair) asm_inputs_pre
@@ -2400,14 +2365,14 @@ and childrenStmt (toPrepend: instr list ref) (vis:cilVisitor) (s:stmt): stmt =
let fExp e = (visitCilExpr vis e) in
let fBlock b = visitCilBlock vis b in
let fInst i = visitCilInstr vis i in
- let fLoopAnnot a = mapNoCopy (visitCilCodeAnnotation vis) a in
+ let fLoopAnnot a = Extlib.map_no_copy (visitCilCodeAnnotation vis) a in
(* Just change the statement kind *)
let skind' =
match s.skind with
Break _ | Continue _ | Return (None, _) -> s.skind
| UnspecifiedSequence seq ->
let seq' =
- mapNoCopy
+ Extlib.map_no_copy
(function (stmt,modified,writes,reads,calls) as orig->
let stmt' = visitCilStmt vis stmt in
(match stmt'.skind with
@@ -2417,12 +2382,12 @@ and childrenStmt (toPrepend: instr list ref) (vis:cilVisitor) (s:stmt): stmt =
to just copy the varinfo when using the copy visitor,
and not apply vvrbl, i.e. not using vis but generic_visitor ?
*)
- let modified' = mapNoCopy (visitCilLval vis) modified in
- let writes' = mapNoCopy (visitCilLval vis) writes in
- let reads' = mapNoCopy (visitCilLval vis) reads in
+ let modified' = Extlib.map_no_copy (visitCilLval vis) modified in
+ let writes' = Extlib.map_no_copy (visitCilLval vis) writes in
+ let reads' = Extlib.map_no_copy (visitCilLval vis) reads in
let calls' =
if Visitor_behavior.is_copy vis#behavior then
- (* we need new references anyway, no need for mapNoCopy *)
+ (* we need new references anyway, no need for Extlib.map_no_copy *)
List.map (fun x -> ref (Visitor_behavior.Memo.stmt vis#behavior !x)) calls
else calls
in
@@ -2459,7 +2424,7 @@ and childrenStmt (toPrepend: instr list ref) (vis:cilVisitor) (s:stmt): stmt =
let e' = fExp e in
toPrepend := vis#unqueueInstr (); (* insert these before the switch *)
let b' = fBlock b in
- let stmts' = mapNoCopy (Visitor_behavior.Get.stmt vis#behavior) stmts in
+ let stmts' = Extlib.map_no_copy (Visitor_behavior.Get.stmt vis#behavior) stmts in
(* the stmts in b should have cleaned up after themselves.*)
assertEmptyQueue vis;
if e' != e || b' != b || stmts' != stmts then
@@ -2478,7 +2443,7 @@ and childrenStmt (toPrepend: instr list ref) (vis:cilVisitor) (s:stmt): stmt =
let t' = visitCilType vis t in
if e != e' || t != t' then (e',t') else exc
in
- let e' = optMapNoCopy visit e in
+ let e' = Extlib.opt_map_no_copy visit e in
if e != e' then Throw (e,loc) else s.skind
| TryCatch (b,l,loc) ->
let b' = fBlock b in
@@ -2487,7 +2452,7 @@ and childrenStmt (toPrepend: instr list ref) (vis:cilVisitor) (s:stmt): stmt =
let b' = fBlock b in
if v != v' || b != b' then (v', b') else catch
in
- let l' = mapNoCopy visit l in
+ let l' = Extlib.map_no_copy visit l in
if b != b' || l != l' then TryCatch (b', l',loc) else s.skind
| TryFinally (b, h, l) ->
let b' = fBlock b in
@@ -2497,7 +2462,7 @@ and childrenStmt (toPrepend: instr list ref) (vis:cilVisitor) (s:stmt): stmt =
let b' = fBlock b in
assertEmptyQueue vis;
(* visit the instructions *)
- let il' = mapNoCopyList fInst il in
+ let il' = Extlib.map_no_copy_list fInst il in
(* Visit the expression *)
let e' = fExp e in
let il'' =
@@ -2523,7 +2488,7 @@ and childrenStmt (toPrepend: instr list ref) (vis:cilVisitor) (s:stmt): stmt =
if e' != e then Case (e', l) else lb
| lb -> lb
in
- mapNoCopy fLabel s.labels
+ Extlib.map_no_copy fLabel s.labels
in
if labels' != s.labels then s.labels <- labels';
s
@@ -2537,7 +2502,7 @@ and visitCilCatch_binder vis cb =
if v != v' || b != b' then (v', b') else conv
in
let v' = visitCilVarDecl vis v in
- let l' = mapNoCopy visit_one_conversion l in
+ let l' = Extlib.map_no_copy visit_one_conversion l in
if v != v' || l != l' then Catch_exn(v',l') else cb
| Catch_all -> cb
and visitCilBlock (vis: cilVisitor) (b: block) : block =
@@ -2560,11 +2525,11 @@ and childrenBlock (vis: cilVisitor) (b: block) : block =
that wish to create a local into the innermost scope can simply append
it to the current block.
*)
- let locals' = mapNoCopy (Visitor_behavior.Get.varinfo vis#behavior) b.blocals in
- let statics' = mapNoCopy (Visitor_behavior.Get.varinfo vis#behavior) b.bstatics in
+ let locals' = Extlib.map_no_copy (Visitor_behavior.Get.varinfo vis#behavior) b.blocals in
+ let statics' = Extlib.map_no_copy (Visitor_behavior.Get.varinfo vis#behavior) b.bstatics in
b.blocals <- locals';
b.bstatics <- statics';
- let stmts' = mapNoCopy fStmt b.bstmts in
+ let stmts' = Extlib.map_no_copy fStmt b.bstmts in
b.bstmts <- stmts';
flatten_transient_sub_blocks b
@@ -2605,7 +2570,7 @@ and childrenType (vis : cilVisitor) (t : typ) : typ =
let aa' = fAttr aa in
if at' != at || aa' != aa then (an,at',aa') else arg
in
- let argslist' = mapNoCopy visitArg argslist in
+ let argslist' = Extlib.map_no_copy visitArg argslist in
let a' = fAttr a in
if rettype' != rettype || argslist' != argslist || a' != a then
let args' = if argslist' == argslist then args else Some argslist' in
@@ -2641,7 +2606,7 @@ and childrenVarDecl (vis : cilVisitor) (v : varinfo) : varinfo =
in
let typ = visitCilType vis v.vtype in
v.vattr <- visitCilAttributes vis v.vattr;
- v.vlogic_var_assoc <- optMapNoCopy visit_orig_var_assoc v.vlogic_var_assoc;
+ v.vlogic_var_assoc <- Extlib.opt_map_no_copy visit_orig_var_assoc v.vlogic_var_assoc;
update_var_type v typ;
v
@@ -2650,7 +2615,7 @@ and visitCilVarUse vis v =
and visitCilAttributes (vis: cilVisitor) (al: attribute list) : attribute list=
let al' =
- mapNoCopyList
+ Extlib.map_no_copy_list
(doVisitListCil vis
id vis#vattr childrenAttribute) al in
if al' != al then
@@ -2662,7 +2627,7 @@ and childrenAttribute (vis: cilVisitor) (a: attribute) : attribute =
let fAttrP a = visitCilAttrParams vis a in
match a with
| Attr (n, args) ->
- let args' = mapNoCopy fAttrP args in
+ let args' = Extlib.map_no_copy fAttrP args in
if args' != args then Attr(n, args') else a
| AttrAnnot _ ->
a
@@ -2675,7 +2640,7 @@ and childrenAttrparam (vis: cilVisitor) (aa: attrparam) : attrparam =
match aa with
AInt _ | AStr _ -> aa
| ACons(n, args) ->
- let args' = mapNoCopy fAttrP args in
+ let args' = Extlib.map_no_copy fAttrP args in
if args' != args then ACons(n, args') else aa
| ASizeOf t ->
let t' = fTyp t in
@@ -2720,8 +2685,8 @@ and childrenAttrparam (vis: cilVisitor) (aa: attrparam) : attrparam =
let rec fix_succs_preds_block b block =
List.iter (fix_succs_preds b) block.bstmts
and fix_succs_preds b stmt =
- stmt.succs <- mapNoCopy (Visitor_behavior.Get.stmt b) stmt.succs;
- stmt.preds <- mapNoCopy (Visitor_behavior.Get.stmt b) stmt.preds;
+ stmt.succs <- Extlib.map_no_copy (Visitor_behavior.Get.stmt b) stmt.succs;
+ stmt.preds <- Extlib.map_no_copy (Visitor_behavior.Get.stmt b) stmt.preds;
match stmt.skind with
If(_,bthen,belse,_) ->
fix_succs_preds_block b bthen;
@@ -2731,8 +2696,8 @@ and fix_succs_preds b stmt =
stmt.skind <- Switch(e,cases,List.map (Visitor_behavior.Get.stmt b) stmts,l)
| Loop(annot,block,loc,stmt1,stmt2) ->
fix_succs_preds_block b block;
- let stmt1' = optMapNoCopy (Visitor_behavior.Get.stmt b) stmt1 in
- let stmt2' = optMapNoCopy (Visitor_behavior.Get.stmt b) stmt2 in
+ let stmt1' = Extlib.opt_map_no_copy (Visitor_behavior.Get.stmt b) stmt1 in
+ let stmt2' = Extlib.opt_map_no_copy (Visitor_behavior.Get.stmt b) stmt2 in
stmt.skind <- Loop(annot,block,loc,stmt1',stmt2')
| Block block -> fix_succs_preds_block b block
| TryFinally(block1,block2,_) ->
@@ -2778,9 +2743,9 @@ and childrenFunction (vis : cilVisitor) (f : fundec) : fundec =
end;
f.svar <- nv; (* hit the function name *)
(* visit the formals *)
- let newformals = mapNoCopy (visitCilVarDecl vis) f.sformals in
+ let newformals = Extlib.map_no_copy (visitCilVarDecl vis) f.sformals in
(* visit local declarations *)
- f.slocals <- mapNoCopy (visitCilVarDecl vis) f.slocals;
+ f.slocals <- Extlib.map_no_copy (visitCilVarDecl vis) f.slocals;
(* Make sure the type reflects the formals *)
let selection = State_selection.singleton FormalsDecl.self in
if Visitor_behavior.is_copy vis#behavior || newformals != f.sformals then begin
@@ -2809,7 +2774,7 @@ let visitCilFieldInfo vis f =
doVisitCil vis (Visitor_behavior.Memo.fieldinfo vis#behavior) vis#vfieldinfo childrenFieldInfo f
let childrenCompInfo vis comp =
- comp.cfields <- optMapNoCopy (mapNoCopy (visitCilFieldInfo vis)) comp.cfields;
+ comp.cfields <- Extlib.opt_map_no_copy (Extlib.map_no_copy (visitCilFieldInfo vis)) comp.cfields;
comp.cattr <- visitCilAttributes vis comp.cattr;
comp
@@ -2825,7 +2790,7 @@ let visitCilEnumItem vis e =
doVisitCil vis (Visitor_behavior.Memo.enumitem vis#behavior) vis#venumitem childrenEnumItem e
let childrenEnumInfo vis e =
- e.eitems <- mapNoCopy (visitCilEnumItem vis) e.eitems;
+ e.eitems <- Extlib.map_no_copy (visitCilEnumItem vis) e.eitems;
e.eattr <- visitCilAttributes vis e.eattr;
e
@@ -2865,7 +2830,7 @@ and childrenGlobal (vis: cilVisitor) (g: global) : global =
try Some (getFormalsDecl v) with Not_found -> None
in
let v' = visitCilVarDecl vis v in
- let form' = optMapNoCopy (mapNoCopy (visitCilVarDecl vis)) form in
+ let form' = Extlib.opt_map_no_copy (Extlib.map_no_copy (visitCilVarDecl vis)) form in
let spec' =
if is_empty_funspec spec then begin
if Visitor_behavior.is_copy vis#behavior then
@@ -2905,11 +2870,6 @@ and childrenGlobal (vis: cilVisitor) (g: global) : global =
if a' != a then GAnnot(a',l) else g
| GText _ | GAsm _ -> g
-(* sm: utility *)
-let startsWith prefix s =
- let prefixLen = String.length prefix in
- String.length s >= prefixLen && String.sub s 0 prefixLen = prefix
-
let bytesSizeOfInt (ik: ikind): int =
match ik with
| IChar | ISChar | IUChar | IBool -> 1
diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli
index e5a54e543c600d0ba69656229aa16b3632b7e56d..9bda2808e5339a19c7ec0f499a38aeca2ca40c29 100644
--- a/src/kernel_services/ast_queries/cil.mli
+++ b/src/kernel_services/ast_queries/cil.mli
@@ -2452,18 +2452,20 @@ val bitsOffset: typ -> offset -> int * int
this after you call {!Cil.initCIL}. *)
val fieldBitsOffset: fieldinfo -> int * int
-(** Like map but try not to make a copy of the list *)
+(** Like map but try not to make a copy of the list
+ @deprecated Frama-C+dev *)
val mapNoCopy: ('a -> 'a) -> 'a list -> 'a list
+[@@alert deprecated "Use [Extlib.map_no_copy] instead."]
-(** same as mapNoCopy for options*)
+(** same as mapNoCopy for options
+ @deprecated Frama-C+dev *)
val optMapNoCopy: ('a -> 'a) -> 'a option -> 'a option
+[@@alert deprecated "Use [Extlib.opt_map_no_copy] instead."]
-(** Like map but each call can return a list. Try not to make a copy of the
- list *)
+(** Like map but each call can return a list. Try not to make a copy of the list
+ @deprecated Frama-C+dev *)
val mapNoCopyList: ('a -> 'a list) -> 'a list -> 'a list
-
-(** sm: return true if the first is a prefix of the second string *)
-val startsWith: string -> string -> bool
+[@@alert deprecated "Use [Extlib.map_no_copy_list] instead."]
(* ************************************************************************* *)
(** {2 An Interpreter for constructing CIL constructs} *)
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index cb18e76893f995df9046975c33132ff4f1b9ca18..d21c6718d4c8ab09f8ac8d6880760d92094dce94 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -2268,7 +2268,7 @@ struct
method! vlogic_info_decl info =
match info.l_body with
| LBinductive l ->
- let l' = Cil.mapNoCopy self#treat_ind_case l in
+ let l' = Extlib.map_no_copy self#treat_ind_case l in
if l != l' then info.l_body <- LBinductive l';
SkipChildren
| _ -> DoChildren
diff --git a/src/kernel_services/visitors/cabsvisit.ml b/src/kernel_services/visitors/cabsvisit.ml
index d5a7fe9ae3d10bd455ccced764fec7f3d86270d7..ed9fa5846312b0493a04c8ec62d163c47e29c714 100644
--- a/src/kernel_services/visitors/cabsvisit.ml
+++ b/src/kernel_services/visitors/cabsvisit.ml
@@ -120,17 +120,17 @@ and childrenTypeSpecifier vis ts =
in
if n' != n || eo' != eo then (n', eo') else input
in
- let nel' = mapNoCopy doOneField nel in
+ let nel' = Extlib.map_no_copy doOneField nel in
if s' != s || nel' != nel then FIELD (s', nel') else input
| STATIC_ASSERT_FG _ -> input
in
match ts with
Tstruct (n, Some fg, extraAttrs) ->
(*(trace "sm" (dprintf "visiting struct %s\n" n));*)
- let fg' = mapNoCopy childrenFieldGroup fg in
+ let fg' = Extlib.map_no_copy childrenFieldGroup fg in
if fg' != fg then Tstruct( n, Some fg', extraAttrs) else ts
| Tunion (n, Some fg, extraAttrs) ->
- let fg' = mapNoCopy childrenFieldGroup fg in
+ let fg' = Extlib.map_no_copy childrenFieldGroup fg in
if fg' != fg then Tunion( n, Some fg', extraAttrs) else ts
| Tenum (n, Some ei, extraAttrs) ->
let doOneEnumItem ((s, e, loc) as ei) =
@@ -138,7 +138,7 @@ and childrenTypeSpecifier vis ts =
if e' != e then (s, e', loc) else ei
in
vis#vEnterScope ();
- let ei' = mapNoCopy doOneEnumItem ei in
+ let ei' = Extlib.map_no_copy doOneEnumItem ei in
vis#vExitScope();
if ei' != ei then Tenum( n, Some ei', extraAttrs) else ts
| TtypeofE e ->
@@ -167,7 +167,7 @@ and childrenSpecElem (vis: cabsVisitor) (se: spec_elem) : spec_elem =
and visitCabsSpecifier (vis: cabsVisitor) (s: specifier) : specifier =
doVisit vis vis#vspec childrenSpec s
-and childrenSpec vis s = mapNoCopy (childrenSpecElem vis) s
+and childrenSpec vis s = Extlib.map_no_copy (childrenSpecElem vis) s
and visitCabsDeclType vis (isfundef: bool) (dt: decl_type) : decl_type =
@@ -176,26 +176,26 @@ and childrenDeclType isfundef vis dt =
match dt with
JUSTBASE -> dt
| PARENTYPE (prea, dt1, posta) ->
- let prea' = mapNoCopyList (visitCabsAttribute vis) prea in
+ let prea' = Extlib.map_no_copy_list (visitCabsAttribute vis) prea in
let dt1' = visitCabsDeclType vis isfundef dt1 in
- let posta'= mapNoCopyList (visitCabsAttribute vis) posta in
+ let posta'= Extlib.map_no_copy_list (visitCabsAttribute vis) posta in
if prea' != prea || dt1' != dt1 || posta' != posta then
PARENTYPE (prea', dt1', posta') else dt
| ARRAY (dt1, al, e) ->
let dt1' = visitCabsDeclType vis isfundef dt1 in
- let al' = mapNoCopy (childrenAttribute vis) al in
+ let al' = Extlib.map_no_copy (childrenAttribute vis) al in
let e'= visitCabsExpression vis e in
if dt1' != dt1 || al' != al || e' != e then ARRAY(dt1', al', e') else dt
| PTR (al, dt1) ->
- let al' = mapNoCopy (childrenAttribute vis) al in
+ let al' = Extlib.map_no_copy (childrenAttribute vis) al in
let dt1' = visitCabsDeclType vis isfundef dt1 in
if al' != al || dt1' != dt1 then PTR(al', dt1') else dt
| PROTO (dt1, snl, gsnl, b) ->
(* Do not propagate isfundef further *)
let dt1' = visitCabsDeclType vis false dt1 in
let _ = vis#vEnterScope () in
- let snl' = mapNoCopy (childrenSingleName vis NVar) snl in
- let gsnl' = mapNoCopy (childrenSingleName vis NVar) gsnl in
+ let snl' = Extlib.map_no_copy (childrenSingleName vis NVar) snl in
+ let gsnl' = Extlib.map_no_copy (childrenSingleName vis NVar) gsnl in
(* Exit the scope only if not in a function definition *)
let _ = if not isfundef then vis#vExitScope () in
if dt1' != dt1 || snl' != snl || gsnl' != gsnl then
@@ -205,7 +205,7 @@ and childrenDeclType isfundef vis dt =
and childrenNameGroup vis (kind: nameKind) ((s, nl) as input) =
let s' = visitCabsSpecifier vis s in
- let nl' = mapNoCopy (visitCabsName vis kind s') nl in
+ let nl' = Extlib.map_no_copy (visitCabsName vis kind s') nl in
if s' != s || nl' != nl then (s', nl') else input
and visitCabsName vis (k: nameKind) (s: specifier)
@@ -214,7 +214,7 @@ and visitCabsName vis (k: nameKind) (s: specifier)
and childrenName (_s: specifier) (k: nameKind) vis (n: name) : name =
let (sn, dt, al, loc) = n in
let dt' = visitCabsDeclType vis (k = NFun) dt in
- let al' = mapNoCopy (childrenAttribute vis) al in
+ let al' = Extlib.map_no_copy (childrenAttribute vis) al in
if dt' != dt || al' != al then (sn, dt', al', loc) else n
and childrenInitName vis (s: specifier) (inn: init_name) : init_name =
@@ -243,7 +243,7 @@ and childrenDefinition vis d =
| DECDEF (spec,(s, inl), l) ->
let s' = visitCabsSpecifier vis s in
- let inl' = mapNoCopy (childrenInitName vis s') inl in
+ let inl' = Extlib.map_no_copy (childrenInitName vis s') inl in
if s' != s || inl' != inl then DECDEF (spec,(s', inl'), l) else d
| TYPEDEF (ng, l) ->
let ng' = childrenNameGroup vis NType ng in
@@ -259,7 +259,7 @@ and childrenDefinition vis d =
let e' = visitCabsExpression vis e in
if e' != e then STATIC_ASSERT (e', s, l) else d
| LINKAGE (n, l, dl) ->
- let dl' = mapNoCopyList (visitCabsDefinition vis) dl in
+ let dl' = Extlib.map_no_copy_list (visitCabsDefinition vis) dl in
if dl' != dl then LINKAGE (n, l, dl') else d
| GLOBANNOT _ -> d
@@ -268,8 +268,8 @@ and visitCabsBlock vis (b: block) : block =
and childrenBlock vis (b: block) : block =
let _ = vis#vEnterScope () in
- let battrs' = mapNoCopyList (visitCabsAttribute vis) b.battrs in
- let bstmts' = mapNoCopyList (visitCabsStatement vis) b.bstmts in
+ let battrs' = Extlib.map_no_copy_list (visitCabsAttribute vis) b.battrs in
+ let bstmts' = Extlib.map_no_copy_list (visitCabsStatement vis) b.bstmts in
let _ = vis#vExitScope () in
if battrs' != b.battrs || bstmts' != b.bstmts then
{ blabels = b.blabels; battrs = battrs'; bstmts = bstmts' }
@@ -373,8 +373,8 @@ and childrenStatement vis s =
let details' = match details with
| None -> details
| Some { aoutputs = outl; ainputs = inl; aclobbers = clobs; alabels = labels } ->
- let outl' = mapNoCopy childrenIdentStringExp outl in
- let inl' = mapNoCopy childrenIdentStringExp inl in
+ let outl' = Extlib.map_no_copy childrenIdentStringExp outl in
+ let inl' = Extlib.map_no_copy childrenIdentStringExp inl in
if outl' == outl && inl' == inl then
details
else
@@ -383,16 +383,16 @@ and childrenStatement vis s =
if details' != details then
{s with stmt_node = ASM (sl, b, details', l)} else s
| THROW (e,l) ->
- let e' = optMapNoCopy (visitCabsExpression vis) e in
+ let e' = Extlib.opt_map_no_copy (visitCabsExpression vis) e in
if e != e' then { s with stmt_node = THROW(e',l) } else s
| TRY_CATCH(t,l,loc) ->
let visit_one_catch (v,s as c) =
- let v' = optMapNoCopy (childrenSingleName vis NVar) v in
+ let v' = Extlib.opt_map_no_copy (childrenSingleName vis NVar) v in
let s' = vs loc s in
if v' != v || s' != s then (v,s) else c
in
let t' = vs loc t in
- let l' = mapNoCopy visit_one_catch l in
+ let l' = Extlib.map_no_copy visit_one_catch l in
if t' != t || l' != l then
{ s with stmt_node = TRY_CATCH(t',l',loc) }
else s
@@ -426,12 +426,12 @@ and childrenExpression vis e =
{ e with expr_node = CAST ((s', dt'), ie')} else e
| CALL (f, el, gl) ->
let f' = ve f in
- let el' = mapNoCopy ve el in
- let gl' = mapNoCopy ve gl in
+ let el' = Extlib.map_no_copy ve el in
+ let gl' = Extlib.map_no_copy ve gl in
if f' != f || el' != el then
{ e with expr_node = CALL (f', el',gl')} else e
| COMMA el ->
- let el' = mapNoCopy ve el in
+ let el' = Extlib.map_no_copy ve el in
if el' != el then { e with expr_node = COMMA (el') } else e
| CONSTANT _ -> e
| PAREN e1 ->
@@ -507,7 +507,7 @@ and childrenInitExpression vis ie =
let ie' = visitCabsInitExpression vis ie in
if iw' != iw || ie' != ie then (iw', ie') else input
in
- let il' = mapNoCopy childrenOne il in
+ let il' = Extlib.map_no_copy childrenOne il in
if il' != il then COMPOUND_INIT il' else ie
@@ -515,14 +515,14 @@ and visitCabsAttribute vis (a: attribute) : attribute list =
doVisitList vis vis#vattr childrenAttribute a
and childrenAttribute vis ((n, el) as input) =
- let el' = mapNoCopy (visitCabsExpression vis) el in
+ let el' = Extlib.map_no_copy (visitCabsExpression vis) el in
if el' != el then (n, el') else input
and visitCabsAttributes vis (al: attribute list) : attribute list =
- mapNoCopyList (visitCabsAttribute vis) al
+ Extlib.map_no_copy_list (visitCabsAttribute vis) al
let visitCabsFile (vis: cabsVisitor) ((fname, f): file) : file =
- (fname, mapNoCopyList (fun ((ghost,f) as glob) ->
+ (fname, Extlib.map_no_copy_list (fun ((ghost,f) as glob) ->
let f' = visitCabsDefinition vis f in
match f' with
[f'] when f == f' -> [glob]
diff --git a/src/kernel_services/visitors/visitor.ml b/src/kernel_services/visitors/visitor.ml
index 80a1138f6e890002fd0ef41e2604695ee1362dc6..163905a738ed53bf60cbbed5e42d58758148304b 100644
--- a/src/kernel_services/visitors/visitor.ml
+++ b/src/kernel_services/visitors/visitor.ml
@@ -481,14 +481,14 @@ class internal_generic_frama_c_visitor fundec queue current_kf behavior: frama_c
in
let change_do_children spec =
let new_behaviors =
- Cil.mapNoCopy self#vbehavior_annot spec.spec_behavior
+ Extlib.map_no_copy self#vbehavior_annot spec.spec_behavior
in
let new_terminates =
- Cil.optMapNoCopy (Cil.visitCilIdPredicate (self:>Cil.cilVisitor))
+ Extlib.opt_map_no_copy (Cil.visitCilIdPredicate (self:>Cil.cilVisitor))
spec.spec_terminates
in
let new_decreases =
- Cil.optMapNoCopy
+ Extlib.opt_map_no_copy
(fun (d,s as acc) ->
let d' = Cil.visitCilTerm (self:>Cil.cilVisitor) d in
if d != d' then (d',s) else acc)
diff --git a/src/libraries/stdlib/extlib.ml b/src/libraries/stdlib/extlib.ml
index 85e12b8b083124588bdaf97b3e18220890da9b29..1209a9b29632184700dec7183e990f55507f64a2 100644
--- a/src/libraries/stdlib/extlib.ml
+++ b/src/libraries/stdlib/extlib.ml
@@ -160,7 +160,6 @@ let subsets k l =
| [] -> assert false
in aux k l (List.length l)
-
let list_first_n n l =
let rec aux acc n = function
| h :: t when n > 0 -> aux (h :: acc) (n-1) t
@@ -190,6 +189,45 @@ let list_slice ?(first = 0) ?last l =
| None -> l
| Some n -> list_first_n (normalize n - first) l
+let rev_until i l =
+ let rec aux acc =
+ function
+ | [] -> acc
+ | i'::_ when i' == i -> acc
+ | i'::l -> aux (i'::acc) l
+ in aux [] l
+
+(* mapNoCopy is like map but avoid copying the list if the function does not
+ change the elements. *)
+let map_no_copy (f: 'a -> 'a) orig =
+ let rec aux ((acc,has_changed) as res) l =
+ match l with
+ | [] -> if has_changed then List.rev acc else orig
+ | i :: resti ->
+ let i' = f i in
+ if has_changed then
+ aux (i'::acc,true) resti
+ else if i' != i then
+ aux (i'::rev_until i orig,true) resti
+ else
+ aux res resti
+ in aux ([],false) orig
+
+(* Same than map_no_copy but [f] returns a list. *)
+let map_no_copy_list (f: 'a -> 'a list) orig =
+ let rec aux ((acc,has_changed) as res) l =
+ match l with
+ | [] -> if has_changed then List.rev acc else orig
+ | i :: resti ->
+ let l' = f i in
+ if has_changed then
+ aux (List.rev_append l' acc,true) resti
+ else
+ (match l' with
+ | [i'] when i' == i -> aux res resti
+ | _ -> aux (List.rev_append l' (rev_until i orig), true) resti)
+ in aux ([],false) orig
+
(* ************************************************************************* *)
(** {2 Options} *)
(* ************************************************************************* *)
@@ -216,6 +254,13 @@ let opt_map2 f x y = match x, y with
| None, _ | _, None -> None
| Some x, Some y -> Some (f x y)
+let opt_map_no_copy f o =
+ match o with
+ | None -> o
+ | Some x ->
+ let x' = f x in
+ if x' != x then Some x' else o
+
(* ************************************************************************* *)
(** {2 Performance} *)
(* ************************************************************************* *)
diff --git a/src/libraries/stdlib/extlib.mli b/src/libraries/stdlib/extlib.mli
index 26195f813742cab574d8a19f67c444f9287123f8..caaaa01103c8227386d9f84d83816032e37e0b5c 100644
--- a/src/libraries/stdlib/extlib.mli
+++ b/src/libraries/stdlib/extlib.mli
@@ -155,6 +155,14 @@ val list_slice: ?first:int -> ?last:int -> 'a list -> 'a list
and inverted ranges result in empty lists.
@since 18.0-Argon *)
+val map_no_copy: ('a -> 'a) -> 'a list -> 'a list
+(** Like map but try not to make a copy of the list
+ @since Frama-C+dev *)
+
+val map_no_copy_list: ('a -> 'a list) -> 'a list -> 'a list
+(** Like map but each call can return a list. Try not to make a copy of the list
+ @since Frama-C+dev *)
+
(* ************************************************************************* *)
(** {2 Options} *)
(* ************************************************************************* *)
@@ -189,6 +197,10 @@ val opt_map2: ('a -> 'b -> 'c) -> 'a option -> 'b option -> 'c option
[None].
@since 24.0-Chromium *)
+val opt_map_no_copy: ('a -> 'a) -> 'a option -> 'a option
+(** same as map_no_copy for options.
+ @since Frama-C+dev *)
+
(* ************************************************************************* *)
(** {2 Strings} *)
(* ************************************************************************* *)
diff --git a/tests/spec/Extend.ml b/tests/spec/Extend.ml
index 53e1e2b679a734a3b3e9c3dffe9a3a4f54173d08..240b3da0212a6f7168cebee620e334fdcc962b2d 100644
--- a/tests/spec/Extend.ml
+++ b/tests/spec/Extend.ml
@@ -47,7 +47,7 @@ let visit_bar vis ext =
match ext with
| Ext_id idx ->
let l = Bar_table.find idx in
- let l' = Cil.mapNoCopy (Cil.visitCilPredicate vis) l in
+ let l' = Extlib.map_no_copy (Cil.visitCilPredicate vis) l in
if Visitor_behavior.is_copy vis#behavior then begin
let idx' = Count.next () in
Queue.add (fun () -> Bar_table.add idx' l') vis#get_filling_actions;