diff --git a/share/Makefile.common b/share/Makefile.common
index f40ab0f72e2cb0a24bd4f9df4af2f67a95901b5c..71baa15ec6b673b680f33f18a344585aea18d45b 100644
--- a/share/Makefile.common
+++ b/share/Makefile.common
@@ -88,7 +88,7 @@ ifeq ($(DEVELOPMENT),yes)
# - 67 (unused module parameter in functor signature): naming all parameters
# in functor signatures is a common practice that seems harmless. Warning 60
# ensures that named functor parameters are indeed used in the implementation.
-WARNINGS ?= -w +a-4-6-9-40-41-42-44-45-48-50-67
+WARNINGS ?= -w +a-4-9-40-41-42-44-45-48-50-67
# - 3 (deprecated feature) cannot always be avoided for OCaml stdlib when
# supporting several OCaml versions
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 3b2e601d3e9c442cae2a372fe53fa3ea888a3332..f95f729713d002d77ec6f8db6bc18bdf3fdf2016 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -992,7 +992,8 @@ let alphaTable : location Alpha.alphaTable = H.create 307
* foo" or "union bar" *)
let fresh_global lookupname =
- fst (Alpha.newAlphaName alphaTable None lookupname (CurrentLoc.get ()))
+ fst (Alpha.newAlphaName ~alphaTable ~undolist:None ~lookupname
+ ~data:(CurrentLoc.get ()))
(* To keep different name scopes different, we add prefixes to names
* specifying the kind of name: the kind can be one of "" for variables or
@@ -1335,7 +1336,7 @@ let findCompType ghost kind name attr =
* struct already or because we want to create a version with different
* attributes *)
if kind = "enum" then
- let enum, isnew = createEnumInfo name name in
+ let enum, isnew = createEnumInfo name ~norig:name in
if isnew then
cabsPushGlobal (GEnumTagDecl (enum, CurrentLoc.get ()));
TEnum (enum, attr)
@@ -1420,11 +1421,11 @@ let rec is_boolean_result e =
(* Like Cil.mkCastT, but it calls typeForInsertedCast *)
let makeCastT ~(e: exp) ~(oldt: typ) ~(newt: typ) =
if need_cast oldt newt then
- Cil.mkCastT oldt (!typeForInsertedCast e oldt newt) e
+ Cil.mkCastT ~oldt ~newt:(!typeForInsertedCast e oldt newt) e
else e
let makeCast ~(e: exp) ~(newt: typ) =
- makeCastT e (typeOf e) newt
+ makeCastT ~e ~oldt:(typeOf e) ~newt
let is_scalar_type t =
match unrollType t with
@@ -2439,7 +2440,8 @@ class registerLabelsVisitor = object
let currentLoc = convLoc (Cabshelper.get_statementloc s) in
(match s.stmt_node with
| Cabs.LABEL (lbl,_,_) ->
- Alpha.registerAlphaName alphaTable (kindPlusName "label" lbl) currentLoc
+ Alpha.registerAlphaName ~alphaTable
+ ~lookupname:(kindPlusName "label" lbl) ~data:currentLoc
| _ -> ());
DoChildren
end
@@ -2934,7 +2936,7 @@ let rec castTo ?context ?(fromsource=false)
else
nt,
Cil.mkCastT
- ot nt'
+ ~oldt:ot ~newt:nt'
(constFold true
(new_exp ~loc:e.eloc
(BinOp(Ne,e,Cil.integer ~loc:e.eloc 0,intType))))
@@ -5115,9 +5117,9 @@ and doType (ghost:bool) isFuncArg
| Cabs.JUSTBASE -> bt, acc
| Cabs.PARENTYPE (a1, d, a2) ->
let a1' = doAttributes ghost a1 in
- let a1n, a1f, a1t = partitionAttributes AttrType a1' in
+ let a1n, a1f, a1t = partitionAttributes ~default:AttrType a1' in
let a2' = doAttributes ghost a2 in
- let a2n, a2f, a2t = partitionAttributes nameortype a2' in
+ let a2n, a2f, a2t = partitionAttributes ~default:nameortype a2' in
(*Format.printf "doType: @[a1n=%a@\na1f=%a@\na1t=%a@\na2n=%a@\na2f=%a@\na2t=%a@]@\n" d_attrlist a1n d_attrlist a1f d_attrlist a1t d_attrlist a2n d_attrlist a2f d_attrlist a2t;*)
let bt' = cabsTypeAddAttributes a1t bt in
(* log "bt' = %a@." d_type bt';*)
@@ -5164,7 +5166,7 @@ and doType (ghost:bool) isFuncArg
| Cabs.PTR (al, d) ->
let al' = doAttributes ghost al in
- let an, af, at = partitionAttributes AttrType al' in
+ let an, af, at = partitionAttributes ~default:AttrType al' in
(* Now recurse *)
let restyp, nattr = doDeclType (TPtr(bt, at)) acc d in
(* See if we can do anything with function type attributes *)
@@ -5466,7 +5468,7 @@ and makeCompType ghost (isstruct: bool)
let n', _ = newAlphaName ghost true kind n in
(* Create the self cell for use in fields and forward references. Or maybe
* one exists already from a forward reference *)
- let comp, _ = createCompInfo isstruct n' norig in
+ let comp, _ = createCompInfo isstruct n' ~norig in
let rec fold f acc = function
| [] -> acc
| [x] -> f ~last:true acc x
@@ -5955,8 +5957,8 @@ and doExp local_env
addOffsetLval (Index(e2'', NoOffset)) array
| _ -> (* Turn into *(e1 + e2) *)
mkMem
- (new_exp ~loc:e1''.eloc (BinOp(PlusPI, e1'', e2'', t1)))
- NoOffset
+ ~addr:(new_exp ~loc:e1''.eloc (BinOp(PlusPI, e1'', e2'', t1)))
+ ~off:NoOffset
in
(* Do some optimization of StartOf *)
let reads =
@@ -5981,7 +5983,7 @@ and doExp local_env
"Expecting a pointer type in *. Got %a."
Cil_printer.pp_typ t
in
- let res = mkMem e' NoOffset in
+ let res = mkMem ~addr:e' ~off:NoOffset in
let reads =
if Lval.Set.mem res local_env.authorized_reads
then r
@@ -6044,7 +6046,7 @@ and doExp local_env
"expecting a struct with field %s. Found %a. t1 is %a"
str Cil_printer.pp_typ x Cil_printer.pp_typ t'
in
- let lv' = mkMem e' field_offset in
+ let lv' = mkMem ~addr:e' ~off:field_offset in
let field_type = typeOfLval lv' in
let reads =
if Lval.Set.mem lv' local_env.authorized_reads
@@ -6266,7 +6268,9 @@ and doExp local_env
in
if isIntegralType t then
let tres = integralPromotion t in
- let e'' = new_exp ~loc (UnOp(Neg, makeCastT e' t tres, tres)) in
+ let e'' =
+ new_exp ~loc (UnOp(Neg, makeCastT ~e:e' ~oldt:t ~newt:tres, tres))
+ in
finishExp r se e'' tres
else
if isArithmeticType t then
@@ -6280,7 +6284,9 @@ and doExp local_env
in
if isIntegralType t then
let tres = integralPromotion t in
- let e'' = new_exp ~loc (UnOp(BNot, makeCastT e' t tres, tres)) in
+ let e'' =
+ new_exp ~loc (UnOp(BNot, makeCastT ~e:e' ~oldt:t ~newt:tres, tres))
+ in
finishExp r se e'' tres
else
Kernel.fatal ~current:true "Unary ~ on a non-integral type"
@@ -6759,7 +6765,7 @@ and doExp local_env
| AddrOf lv -> new_exp ~loc:f'.eloc (Lval(lv))
| _ ->
new_exp ~loc:f'.eloc
- (Lval (mkMem f' NoOffset))
+ (Lval (mkMem ~addr:f' ~off:NoOffset))
in
(rt,at,isvar, f'',[])
| x ->
@@ -7674,7 +7680,7 @@ and doExp local_env
end
in
finishExp [] (unspecified_chunk empty)
- (makeCast (integer ~loc addrval) voidPtrType) voidPtrType
+ (makeCast ~e:(integer ~loc addrval) ~newt:voidPtrType) voidPtrType
end
| Cabs.EXPR_PATTERN _ -> abort_context "EXPR_PATTERN in cabs2cil input"
@@ -7765,14 +7771,18 @@ and doBinOp loc (bop: binop) (e1: exp) (t1: typ) (e2: exp) (t2: typ) =
(* Keep the operator since it is arithmetic *)
tres,
optConstFoldBinOp loc false bop
- (makeCastT e1 t1 tres) (makeCastT e2 t2 tres) tres
+ (makeCastT ~e:e1 ~oldt:t1 ~newt:tres)
+ (makeCastT ~e:e2 ~oldt:t2 ~newt:tres)
+ tres
in
let doArithmeticComp () =
let tres = arithmeticConversion t1 t2 in
(* Keep the operator since it is arithmetic *)
intType,
optConstFoldBinOp loc false bop
- (makeCastT e1 t1 tres) (makeCastT e2 t2 tres) intType
+ (makeCastT ~e:e1 ~oldt:t1 ~newt:tres)
+ (makeCastT ~e:e2 ~oldt:t2 ~newt:tres)
+ intType
in
let doIntegralArithmetic () =
let tres = unrollType (arithmeticConversion t1 t2) in
@@ -7780,7 +7790,9 @@ and doBinOp loc (bop: binop) (e1: exp) (t1: typ) (e2: exp) (t2: typ) =
| TInt _ ->
tres,
optConstFoldBinOp loc false bop
- (makeCastT e1 t1 tres) (makeCastT e2 t2 tres) tres
+ (makeCastT ~e:e1 ~oldt:t1 ~newt:tres)
+ (makeCastT ~e:e2 ~oldt:t2 ~newt:tres)
+ tres
| _ ->
Kernel.fatal ~current:true "%a operator on non-integer type %a"
Cil_printer.pp_binop bop Cil_printer.pp_typ tres
@@ -7796,7 +7808,8 @@ and doBinOp loc (bop: binop) (e1: exp) (t1: typ) (e2: exp) (t2: typ) =
arguments with incompatible types to a common type *)
let e1', e2' =
if not (areCompatibleTypes t1p t2p) then
- makeCastT e1 t1 Cil.voidPtrType, makeCastT e2 t2 Cil.voidPtrType
+ makeCastT ~e:e1 ~oldt:t1 ~newt:Cil.voidPtrType,
+ makeCastT ~e:e2 ~oldt:t2 ~newt:Cil.voidPtrType
else e1, e2
in
intType,
@@ -7808,7 +7821,7 @@ and doBinOp loc (bop: binop) (e1: exp) (t1: typ) (e2: exp) (t2: typ) =
{ e1 with enode = AddrOf (addOffsetLval (Index (e2,NoOffset)) lv) }
| _ ->
optConstFoldBinOp loc false PlusPI e1
- (makeCastT e2 t2 (integralPromotion t2)) t1
+ (makeCastT ~e:e2 ~oldt:t2 ~newt:(integralPromotion t2)) t1
in
match bop with
| (Mult|Div) -> doArithmetic ()
@@ -7823,7 +7836,9 @@ and doBinOp loc (bop: binop) (e1: exp) (t1: typ) (e2: exp) (t2: typ) =
let t2' = integralPromotion t2 in
t1',
optConstFoldBinOp loc false bop
- (makeCastT e1 t1 t1') (makeCastT e2 t2 t2') t1'
+ (makeCastT ~e:e1 ~oldt:t1 ~newt:t1')
+ (makeCastT ~e:e2 ~oldt:t2 ~newt:t2')
+ t1'
| (PlusA|MinusA)
when isArithmeticType t1 && isArithmeticType t2 -> doArithmetic ()
| (Eq|Ne|Lt|Le|Ge|Gt)
@@ -7836,7 +7851,7 @@ and doBinOp loc (bop: binop) (e1: exp) (t1: typ) (e2: exp) (t2: typ) =
| MinusA when isPointerType t1 && isIntegralType t2 ->
t1,
optConstFoldBinOp loc false MinusPI e1
- (makeCastT e2 t2 (integralPromotion t2)) t1
+ (makeCastT ~e:e2 ~oldt:t2 ~newt:(integralPromotion t2)) t1
| MinusA when isPointerType t1 && isPointerType t2 ->
if areCompatibleTypes (* C99 6.5.6:3 *)
(Cil.type_remove_qualifier_attributes_deep t1)
@@ -7849,9 +7864,9 @@ and doBinOp loc (bop: binop) (e1: exp) (t1: typ) (e2: exp) (t2: typ) =
(* Two special cases for comparisons with the NULL pointer. We are a bit
more permissive. *)
| (Le|Lt|Ge|Gt|Eq|Ne) when isPointerType t1 && isZero e2 ->
- pointerComparison e1 t1 (makeCast e2 t1) t1
+ pointerComparison e1 t1 (makeCast ~e:e2 ~newt:t1) t1
| (Le|Lt|Ge|Gt|Eq|Ne) when isPointerType t2 && isZero e1 ->
- pointerComparison (makeCast e1 t2) t2 e2 t2
+ pointerComparison (makeCast ~e:e1 ~newt:t2) t2 e2 t2
| (Le|Lt|Ge|Gt|Eq|Ne) when isPointerType t1 && isPointerType t2 ->
pointerComparison e1 t1 e2 t2
@@ -8119,7 +8134,8 @@ and doInitializer local_env (vi: varinfo) (inite: Cabs.init_expression)
Kernel.debug ~dkey:Kernel.dkey_typing_init
"Collecting the initializer for %s@\n" vi.vname;
let (init, typ'', reads) =
- collectInitializer Cil_datatype.Lval.Set.empty preinit typ' typ'
+ collectInitializer Cil_datatype.Lval.Set.empty preinit typ'
+ ~parenttype:typ'
in
Kernel.debug ~dkey:Kernel.dkey_typing_init
"Finished the initializer for %s@\n init=%a@\n typ=%a@\n acc=%a@\n"
@@ -8493,7 +8509,7 @@ and doInit local_env asconst add_implicit_ensures preinit so acc initl =
asconst oneinit (AExp(Some so.soTyp))
in
let r = Cil_datatype.Lval.Set.of_list r in
- let init_expr = makeCastT oneinit' t' so.soTyp in
+ let init_expr = makeCastT ~e:oneinit' ~oldt:t' ~newt:so.soTyp in
let preinit' = setOneInit preinit so.soOff (SinglePre (init_expr, r)) in
(* Move on *)
advanceSubobj so;
@@ -9052,7 +9068,7 @@ and createLocal ghost ((_, sto, _, _) as specs)
in
let setlen = se0 +++
(mkStmtOneInstr ~ghost ~valid_sid
- (Set(var savelen, makeCast len savelen.vtype,
+ (Set(var savelen, makeCast ~e:len ~newt:savelen.vtype,
CurrentLoc.get ())),
[],[],[])
in
@@ -9082,7 +9098,8 @@ and createLocal ghost ((_, sto, _, _) as specs)
(Local_init
(vi,AssignInit
(SingleInit
- (makeCast (new_exp ~loc (Lval(var tmp))) vi.vtype)),
+ (makeCast ~e:(new_exp ~loc (Lval(var tmp)))
+ ~newt:vi.vtype)),
CurrentLoc.get ())),
[],[var vi],[var tmp])
end
@@ -9514,7 +9531,8 @@ and doDecl local_env (isglobal: bool) : Cabs.definition -> chunk = function
defaultChunk ~ghost
loc
(i2c (mkStmtOneInstr ~ghost:local_env.is_ghost ~valid_sid
- (Set ((Mem (makeCast (integer ~loc 0) intPtrType),
+ (Set ((Mem (makeCast ~e:(integer ~loc 0)
+ ~newt:intPtrType),
NoOffset),
integer ~loc 0, loc)),[],[],[]))
in
@@ -9602,7 +9620,7 @@ and doDecl local_env (isglobal: bool) : Cabs.definition -> chunk = function
match unrollType !currentReturnType with
| TVoid _ -> [], None
| (TInt _ | TEnum _ | TFloat _ | TPtr _) as rt ->
- let res = Some (makeCastT (zero ~loc) intType rt) in
+ let res = Some (makeCastT ~e:(zero ~loc) ~oldt:intType ~newt:rt) in
if !currentFunctionFDEC.svar.vname = "main" then
[],res
else begin
@@ -9616,8 +9634,12 @@ and doDecl local_env (isglobal: bool) : Cabs.definition -> chunk = function
(* 0 is not an admissible value for the return type.
On the other hand, *( T* )0 is. We're not supposed
to get there anyway. *)
- let null_ptr = makeCastT (zero ~loc) intType (TPtr(rt,[])) in
- let res = Some (new_exp ~loc (Lval (mkMem null_ptr NoOffset))) in
+ let null_ptr =
+ makeCastT ~e:(zero ~loc) ~oldt:intType ~newt:(TPtr(rt,[]))
+ in
+ let res =
+ Some (new_exp ~loc (Lval (mkMem ~addr:null_ptr ~off:NoOffset)))
+ in
Kernel.warning ~current:true ~wkey:Kernel.wkey_cert_msc_37
"Body of function %s falls-through. \
Adding a return statement"
@@ -9735,7 +9757,7 @@ and doTypedef ghost ((specs, nl): Cabs.name_group) =
which are invalid)
- redefinition via a typedef of a struct/union/enum IS allowed;
- other types are allowed. *)
- if declared_in_current_scope ghost n then
+ if declared_in_current_scope ~ghost n then
begin
match newTyp' with (* do NOT unroll type here,
redefinitions of typedefs are ok *)
@@ -9762,7 +9784,7 @@ and doTypedef ghost ((specs, nl): Cabs.name_group) =
if not (Kernel.C11.get ()) then error_c11_redefinition ()
end
end
- else if declared_in_current_scope ghost n then
+ else if declared_in_current_scope ~ghost n then
Kernel.error ~current:true
"redefinition of type '%s' in the same scope with incompatible type.@ \
Previous declaration was at %a" n Cil_datatype.Location.pretty oldloc;
@@ -10201,7 +10223,7 @@ and doStatement local_env (s : Cabs.statement) : chunk =
| Some (switchv, switch) -> (* We have already generated this one *)
(se
@@ (i2c(mkStmtOneInstr ~ghost ~valid_sid
- (Set (var switchv, makeCast e' intType, loc')),
+ (Set (var switchv, makeCast ~e:e' ~newt:intType, loc')),
[],[],[]), ghost))
@@ (s2c(mkStmt ~ghost ~valid_sid (Goto (ref switch, loc'))), ghost)
@@ -10232,7 +10254,8 @@ and doStatement local_env (s : Cabs.statement) : chunk =
(se @@
(i2c
(mkStmtOneInstr ~ghost ~valid_sid
- (Set (var switchv, makeCast e' intType, loc')),[],[],[]),
+ (Set (var switchv, makeCast ~e:e' ~newt:intType, loc')),
+ [],[],[]),
ghost))
@@ (s2c switch, ghost)
end
diff --git a/src/kernel_internals/typing/cfg.ml b/src/kernel_internals/typing/cfg.ml
index d0e7b4da779fb0548edf2fe50b0306a557970e7f..52b5692146f96e28507e53d81facbadb6e43ed79 100644
--- a/src/kernel_internals/typing/cfg.ml
+++ b/src/kernel_internals/typing/cfg.ml
@@ -347,7 +347,8 @@ let computeFileCFG (f : file) =
let labelAlphaTable : unit Alpha.alphaTable = Hashtbl.create 11
let freshLabel (base:string) =
- fst (Alpha.newAlphaName labelAlphaTable None base ())
+ fst (Alpha.newAlphaName ~alphaTable:labelAlphaTable ~undolist:None
+ ~lookupname:base ~data:())
let xform_switch_block ?(keepSwitch=false) b =
@@ -743,7 +744,8 @@ class registerLabelsVisitor : cilVisitor = object
List.iter
(function
| Label (name,_,_) ->
- Alpha.registerAlphaName labelAlphaTable name ()
+ Alpha.registerAlphaName ~alphaTable:labelAlphaTable
+ ~lookupname:name ~data:()
| _ -> ())
labels;
DoChildren
diff --git a/src/kernel_internals/typing/frontc.ml b/src/kernel_internals/typing/frontc.ml
index aac0b990d40dc4f934c4418475d6b7263979f9da..39eddfdf6bb1d4e99d717ede65b854b55ac3fdd8 100644
--- a/src/kernel_internals/typing/frontc.ml
+++ b/src/kernel_internals/typing/frontc.ml
@@ -49,7 +49,7 @@ let parse_to_cabs (path : Datatype.Filepath.t) =
try
Kernel.feedback ~level:2 "Parsing %a" Datatype.Filepath.pretty path;
Errorloc.clear_errors () ;
- let lexbuf = Clexer.init (path :> string) in
+ let lexbuf = Clexer.init ~filename:(path :> string) in
let cabs = Cparser.file Clexer.initial lexbuf in
(* Cprint.print_defs cabs;*)
Clexer.finish ();
diff --git a/src/kernel_internals/typing/infer_annotations.ml b/src/kernel_internals/typing/infer_annotations.ml
index ff645dc9217b6381ee05c0873037489f8fd54691..b6f2e39f836b07024ebfa3d7c0ebc93b4c31c370 100644
--- a/src/kernel_internals/typing/infer_annotations.ml
+++ b/src/kernel_internals/typing/infer_annotations.ml
@@ -26,7 +26,7 @@ open Logic_const
let emitter =
Emitter.create "Inferred annotations"
- [Emitter.Funspec; Emitter.Property_status] [] []
+ [Emitter.Funspec; Emitter.Property_status] ~correctness:[] ~tuning:[]
let assigns_from_prototype kf =
let vi = Kernel_function.get_vi kf in
@@ -164,7 +164,9 @@ let is_frama_c_builtin name =
(* Put an 'Unknown' status on all 'assigns' and 'from' clauses that we
generate. *)
let emit_unknown_status_on_assigns kf bhv assigns =
- let emit ip = Property_status.emit emitter [] ip Property_status.Dont_know in
+ let emit ip =
+ Property_status.emit emitter ~hyps:[] ip Property_status.Dont_know
+ in
let pptopt =
Property.ip_of_assigns
kf Kglobal (Property.Id_contract (Datatype.String.Set.empty,bhv)) assigns
diff --git a/src/kernel_internals/typing/mergecil.ml b/src/kernel_internals/typing/mergecil.ml
index 112319715aa4d6806ad5c797a47db2603f6d8779..0433964f1c79d790f916be819ed326584cfb16b0 100644
--- a/src/kernel_internals/typing/mergecil.ml
+++ b/src/kernel_internals/typing/mergecil.ml
@@ -618,7 +618,8 @@ module EnumMerging =
(e2.ename <-
fst
(Alpha.newAlphaName
- aeAlpha None e2.ename Cil_datatype.Location.unknown);
+ ~alphaTable:aeAlpha ~undolist:None ~lookupname:e2.ename
+ ~data:Cil_datatype.Location.unknown);
Kernel.debug ~dkey:Kernel.dkey_linker
"new anonymous name %s" e2.ename;
false))))
@@ -1391,9 +1392,12 @@ let update_compinfo ci =
| Some (loc,_) -> loc
| None -> Cil_datatype.Location.unknown
in
- Alpha.registerAlphaName sAlpha ci.cname loc;
+ Alpha.registerAlphaName ~alphaTable:sAlpha ~lookupname:ci.cname ~data:loc;
let orig_name = if ci.corig_name = "" then ci.cname else ci.corig_name in
- let n, _ = Alpha.newAlphaName sAlpha None orig_name loc in
+ let n, _ =
+ Alpha.newAlphaName ~alphaTable:sAlpha ~undolist:None
+ ~lookupname:orig_name ~data:loc
+ in
let oldnode = PlainMerging.find true node in
if oldnode == node then begin
let node =
@@ -1429,8 +1433,11 @@ let rec update_type_repr t =
| Some (loc,_) -> loc
| None -> Cil_datatype.Location.unknown
in
- Alpha.registerAlphaName vtAlpha ti.tname loc;
- let n,_ = Alpha.newAlphaName vtAlpha None ti.torig_name loc in
+ Alpha.registerAlphaName ~alphaTable:vtAlpha ~lookupname:ti.tname ~data:loc;
+ let n,_ =
+ Alpha.newAlphaName ~alphaTable:vtAlpha ~undolist:None
+ ~lookupname:ti.torig_name ~data:loc
+ in
let oldnode = PlainMerging.find true node in
if oldnode == node then begin
let node =
@@ -1670,7 +1677,8 @@ let oneFilePass1 (f:file) : unit =
* with the same name have been encountered before and we merge those types
* *)
let matchVarinfo (vi: varinfo) (loc, _ as l) =
- ignore (Alpha.registerAlphaName vtAlpha vi.vname (CurrentLoc.get ()));
+ ignore (Alpha.registerAlphaName ~alphaTable:vtAlpha
+ ~lookupname:vi.vname ~data:(CurrentLoc.get ()));
(* Make a node for it and put it in vEq *)
let vinode =
PlainMerging.mkSelfNode vEq vSyn !currentFidx vi.vname vi (Some l)
@@ -1841,7 +1849,8 @@ let oneFilePass1 (f:file) : unit =
let orig_name =
if ei.eorig_name = "" then ei.ename else ei.eorig_name
in
- ignore (Alpha.newAlphaName aeAlpha None orig_name l);
+ ignore (Alpha.newAlphaName ~alphaTable:aeAlpha ~undolist:None
+ ~lookupname:orig_name ~data:l);
ei.ereferenced <- false;
ignore
(EnumMerging.getNode eEq eSyn !currentFidx ei ei
@@ -2636,7 +2645,8 @@ let oneFilePass2 (f: file) =
(* Maybe it is static. Rename it then *)
if vi.vstorage = Static then begin
let newName, _ =
- Alpha.newAlphaName vtAlpha None vi.vname (CurrentLoc.get ())
+ Alpha.newAlphaName ~alphaTable:vtAlpha ~undolist:None
+ ~lookupname:vi.vname ~data:(CurrentLoc.get ())
in
let formals_decl =
try Some (Cil.getFormalsDecl vi)
@@ -2985,7 +2995,8 @@ let oneFilePass2 (f: file) =
if ci.corig_name = "" then ci.cname else ci.corig_name
in
let newname, _ =
- Alpha.newAlphaName sAlpha None orig_name (CurrentLoc.get ())
+ Alpha.newAlphaName ~alphaTable:sAlpha ~undolist:None
+ ~lookupname:orig_name ~data:(CurrentLoc.get ())
in
ci.cname <- newname;
ci.creferenced <- true;
@@ -3014,7 +3025,8 @@ let oneFilePass2 (f: file) =
if ei.eorig_name = "" then ei.ename else ei.eorig_name
in
let newname, _ =
- Alpha.newAlphaName eAlpha None orig_name (CurrentLoc.get ())
+ Alpha.newAlphaName ~alphaTable:eAlpha ~undolist:None
+ ~lookupname:orig_name ~data:(CurrentLoc.get ())
in
ei.ename <- newname;
ei.ereferenced <- true;
@@ -3023,7 +3035,8 @@ let oneFilePass2 (f: file) =
List.iter
(fun item ->
let newname,_ =
- Alpha.newAlphaName vtAlpha None item.eiorig_name item.eiloc
+ Alpha.newAlphaName ~alphaTable:vtAlpha ~undolist:None
+ ~lookupname:item.eiorig_name ~data:item.eiloc
in
item.einame <- newname)
ei.eitems;
@@ -3067,7 +3080,8 @@ let oneFilePass2 (f: file) =
with
None -> (* We must rename it and keep it *)
let newname, _ =
- Alpha.newAlphaName vtAlpha None ti.torig_name (CurrentLoc.get ())
+ Alpha.newAlphaName ~alphaTable:vtAlpha ~undolist:None
+ ~lookupname:ti.torig_name ~data:(CurrentLoc.get ())
in
ti.tname <- newname;
ti.treferenced <- true;
diff --git a/src/kernel_services/abstract_interp/base.ml b/src/kernel_services/abstract_interp/base.ml
index 3db4b30bf6075ec87febe9b07a1e6bde9ac942ce..2ebe0f3efa129c9d60576ec84dd1b4d5d105eb40 100644
--- a/src/kernel_services/abstract_interp/base.ml
+++ b/src/kernel_services/abstract_interp/base.ml
@@ -298,7 +298,9 @@ let offset_for_validity ~bitfield access base =
let max = last_valid_offset base max access in
if bitfield
then Ival.inject_range (Some min) (Some max)
- else Ival.inject_interval (Some min) (Some max) Int.zero Int.eight
+ else
+ Ival.inject_interval ~min:(Some min) ~max:(Some max) ~rem:Int.zero
+ ~modu:Int.eight
| Variable variable_v ->
let maxv = last_valid_offset base variable_v.max_alloc access in
Ival.inject_range (Some Int.zero) (Some maxv)
diff --git a/src/kernel_services/abstract_interp/int_interval.ml b/src/kernel_services/abstract_interp/int_interval.ml
index 8e11b3268456afa56a83c22156ea25dbfa6be7c1..9d72418a04c039447427c931d35c7881e5f5ff35 100644
--- a/src/kernel_services/abstract_interp/int_interval.ml
+++ b/src/kernel_services/abstract_interp/int_interval.ml
@@ -308,7 +308,7 @@ let compute_first_common mn1 mn2 r modu =
| Some m1, Some m2 -> Int.max m1 m2
| None, None -> assert false (* already tested above *)
in
- Some (Int.round_up_to_r m r modu)
+ Some (Int.round_up_to_r ~min:m ~r ~modu)
let compute_last_common mx1 mx2 r modu =
if mx1 = None && mx2 = None
@@ -320,7 +320,7 @@ let compute_last_common mx1 mx2 r modu =
| Some m1, Some m2 -> Int.min m1 m2
| None, None -> assert false (* already tested above *)
in
- Some (Int.round_down_to_r m r modu)
+ Some (Int.round_down_to_r ~max:m ~r ~modu)
let meet t1 t2 =
try
diff --git a/src/kernel_services/abstract_interp/int_val.ml b/src/kernel_services/abstract_interp/int_val.ml
index efd496e5dc49aae5caf2c5faa374abbf63dd1498..5cade9d5c4948b35ff016ea83e86dfbed557a055 100644
--- a/src/kernel_services/abstract_interp/int_val.ml
+++ b/src/kernel_services/abstract_interp/int_val.ml
@@ -961,13 +961,13 @@ struct
| None ->
(* We could do better here, as one of the bound may be finite. However,
this case should occur rarely or not at all. *)
- inject_interval None None r modu
+ inject_interval ~min:None ~max:None ~rem:r ~modu
| Some size ->
try compute_small_set ~size v1 v2 r modu
with Do_not_fit_small_sets ->
let min = compute_bound ~size v1 v2 true
and max = compute_bound ~size v1 v2 false in
- inject_interval (Some min) (Some max) r modu
+ inject_interval ~min:(Some min) ~max:(Some max) ~rem:r ~modu
end
let bitwise_or = let module M = BitwiseOperator (Or) in M.bitwise_forward
diff --git a/src/kernel_services/abstract_interp/offsetmap.ml b/src/kernel_services/abstract_interp/offsetmap.ml
index ffcf90297deebfe2d2f58afbf1015da8292e4521..db8459dee24109936a077c3b1bfdcea2f098387b 100644
--- a/src/kernel_services/abstract_interp/offsetmap.ml
+++ b/src/kernel_services/abstract_interp/offsetmap.ml
@@ -1138,7 +1138,7 @@ module Make (V : module type of Offsetmap_lattice_with_isotropy) = struct
let f_aux_merge_generic merge_v abs_min abs_max rem1 modu1 v1 rem2 modu2 v2 =
if Rel.equal rem1 rem2 && modu1 =~ modu2
then
- rem1, modu1, V.anisotropic_cast modu1 (merge_v modu1 v1 v2)
+ rem1, modu1, V.anisotropic_cast ~size:modu1 (merge_v modu1 v1 v2)
(* Format.printf "f_aux_merge: [%a, %a]@.(%a %a %a)@.(%a %a %a)@."
pretty_int abs_min pretty_int abs_max pretty_int rem1 pretty_int
modu1 V.pretty v1 pretty_int rem2 pretty_int modu2 V.pretty v2 ; *)
@@ -1196,7 +1196,7 @@ module Make (V : module type of Offsetmap_lattice_with_isotropy) = struct
[narrow {0} {1,2}] on the first bit is {0}, but the intersection
of the two sets is bottom. *)
let f_aux_merge_join merge_v abs_min abs_max rem1 modu1 v1 rem2 modu2 v2 =
- let joined size v1 v2 = V.anisotropic_cast size (merge_v size v1 v2) in
+ let joined size v1 v2 = V.anisotropic_cast ~size (merge_v size v1 v2) in
if V.is_isotropic v2 then
rem1, modu1, joined modu1 v1 v2
else if V.is_isotropic v1 then
@@ -1585,13 +1585,13 @@ module Make (V : module type of Offsetmap_lattice_with_isotropy) = struct
| Node (max, offl, subl, offr, subr, rem, m, v, _) ->
let new_offl = offl +~ curr_off in
if offset <~ curr_off then
- keep_below offset new_offl subl
+ keep_below ~offset new_offl subl
else if offset =~ curr_off then
new_offl, subl
else
let sup = curr_off +~ max in
if offset >~ sup then
- let new_offr, new_subr = keep_below offset (curr_off +~ offr) subr in
+ let new_offr, new_subr = keep_below ~offset (curr_off +~ offr) subr in
curr_off,
nNode max offl subl (new_offr -~ curr_off) new_subr rem m v
else
@@ -1614,7 +1614,7 @@ module Make (V : module type of Offsetmap_lattice_with_isotropy) = struct
(* This node should be forgotten,
let's look at the right subtree
*)
- keep_above offset new_offr subr
+ keep_above ~offset new_offr subr
else if offset =~ abs_max then
(* we are at the limit,
the right subtree is the answer
@@ -1624,7 +1624,7 @@ module Make (V : module type of Offsetmap_lattice_with_isotropy) = struct
if offset <~ curr_off then
(* we want to keep this node and part of its left subtree *)
let new_offl, new_subl =
- keep_above offset (curr_off +~ offl) subl
+ keep_above ~offset (curr_off +~ offl) subl
in
curr_off,
nNode max (new_offl -~ curr_off) new_subl offr subr rem m v
@@ -1638,8 +1638,8 @@ module Make (V : module type of Offsetmap_lattice_with_isotropy) = struct
let update_itv_with_rem ~exact ~offset ~abs_max ~size ~rem v curr_off tree =
if Int.(equal size zero) then curr_off, tree else
- let off1, t1 = keep_above abs_max curr_off tree in
- let off2, t2 = keep_below offset curr_off tree in
+ let off1, t1 = keep_above ~offset:abs_max curr_off tree in
+ let off2, t2 = keep_below ~offset curr_off tree in
if exact then
let off_add, t_add =
add_node ~min:offset ~max:abs_max rem size v off1 t1
@@ -2301,11 +2301,11 @@ module Int_Intervals_Map = struct
let shrink_itv co m ~prev_min ~new_min ~prev_max ~new_max : itvs =
let co, m as i =
if new_max <~ prev_max then
- keep_below (succ new_max) co m
+ keep_below ~offset:(succ new_max) co m
else co, m
in
if new_min >~ prev_min then
- keep_above (pred new_min) co m
+ keep_above ~offset:(pred new_min) co m
else i
(* Resize size [m] to size [new_min..new_max], by enlarging or shrinking
@@ -2316,13 +2316,13 @@ module Int_Intervals_Map = struct
else if new_max >~ prev_max then
add_itv ~min:(succ prev_max) ~max:new_max false co m
else (* new_max <~ prev_max *)
- keep_below (succ new_max) co m
+ keep_below ~offset:(succ new_max) co m
in
if new_min =~ prev_min then i
else if new_min <~ prev_min then
add_itv ~min:new_min ~max:(pred prev_min) false co m
else (* new_min >~ prev_min *)
- keep_above (pred new_min) co m
+ keep_above ~offset:(pred new_min) co m
(* normalizes a non-empty offsetmap [m], by removing an eventual rightmost
diff --git a/src/kernel_services/analysis/bit_utils.ml b/src/kernel_services/analysis/bit_utils.ml
index f01b2efec142c1435af8114dccbfe2e42a7309e6..56ab046111f2fe406891dac7d23a67e0bd9db79b 100644
--- a/src/kernel_services/analysis/bit_utils.ml
+++ b/src/kernel_services/analysis/bit_utils.ml
@@ -538,7 +538,7 @@ let rec find_offset typ ~offset om =
let rem = Integer.e_rem offset size_elt in
if offset_match_cell om size_elt then
(* [size] covers at most one cell; we continue in the relevant one *)
- let off, typ = find_offset typ_elt rem om in
+ let off, typ = find_offset typ_elt ~offset:rem om in
Index (exp_start, off), typ
else begin
match om with
@@ -571,7 +571,7 @@ let rec find_offset typ ~offset om =
find_field q
else
let off, typ =
- find_offset fi.ftype (Integer.sub offset off_fi) om
+ find_offset fi.ftype ~offset:(Integer.sub offset off_fi) om
in
Field (fi, off), typ
with NoMatchingOffset when not ci.cstruct ->
diff --git a/src/kernel_services/analysis/dataflow2.ml b/src/kernel_services/analysis/dataflow2.ml
index dfa2c2d3e673865e79113869889552c260cfa121..c9739cb909c96afa02b8342eef94d56f63cfce3f 100644
--- a/src/kernel_services/analysis/dataflow2.ml
+++ b/src/kernel_services/analysis/dataflow2.ml
@@ -416,7 +416,7 @@ module Forwards(T : ForwardsTransfer) = struct
when Integer.equal z Integer.zero ->
new_exp ~loc:exp_sw.eloc (UnOp(LNot,exp_sw,intType))
| _ ->
- Cil.new_exp exp_case.eloc
+ Cil.new_exp ~loc:exp_case.eloc
(BinOp (Eq, exp_sw, exp_case, Cil.intType))
in
let branch_case, branch_not_case = T.doGuard s exp before in
diff --git a/src/kernel_services/analysis/dataflows.ml b/src/kernel_services/analysis/dataflows.ml
index d6abaf94d53ab3a29ac3040d0cb57b158587d3e9..1ae975c0352cc53e856f98ed8f0be6e746173f9c 100644
--- a/src/kernel_services/analysis/dataflows.ml
+++ b/src/kernel_services/analysis/dataflows.ml
@@ -625,7 +625,7 @@ let transfer_switch_from_guard transfer_guard stmt state =
| Const (CInt64 (z,_,_))
when Integer.equal z Integer.zero ->
Cil.new_exp ~loc:cond.eloc (UnOp(LNot,cond,Cil.intType))
- | _ -> Cil.new_exp exp_case.eloc
+ | _ -> Cil.new_exp ~loc:exp_case.eloc
(BinOp (Eq, cond, exp_case, Cil.intType))
in
let (true_state, false_state) =
diff --git a/src/kernel_services/analysis/destructors.ml b/src/kernel_services/analysis/destructors.ml
index b03bdaa56e7cd620e467f3cdf8cc713743e6e9e7..d27181f230926989f942bf38515ef529205c361f 100644
--- a/src/kernel_services/analysis/destructors.ml
+++ b/src/kernel_services/analysis/destructors.ml
@@ -32,7 +32,8 @@ let add_destructor (_, l as acc) var =
let e =
match Globals.Functions.get_params kf with
| vi :: _ ->
- if Cil.need_cast (Cil.typeOf e) vi.vtype then Cil.mkCast vi.vtype e
+ if Cil.need_cast (Cil.typeOf e) vi.vtype then
+ Cil.mkCast ~newt:vi.vtype e
else e
| [] ->
Kernel.fatal
diff --git a/src/kernel_services/analysis/interpreted_automata.ml b/src/kernel_services/analysis/interpreted_automata.ml
index 0e57179344d60d3acdff202f9b6d6a9a340a1c09..229593bd7ebaa39b9523d8bb3390b92805f69887 100644
--- a/src/kernel_services/analysis/interpreted_automata.ml
+++ b/src/kernel_services/analysis/interpreted_automata.ml
@@ -422,7 +422,7 @@ let build_automaton ~annotations kf =
(* Guards for edges of the switch *)
let build_guard exp2 kind =
let enode = BinOp (Eq,exp1,exp2,Cil.intType) in
- Guard (Cil.new_exp exp2.eloc enode, kind, stmt)
+ Guard (Cil.new_exp ~loc:exp2.eloc enode, kind, stmt)
in
(* First build the automaton for the block *)
let block_control = {
diff --git a/src/kernel_services/analysis/logic_interp.ml b/src/kernel_services/analysis/logic_interp.ml
index 3baff8798d3e357741aa88fc504628de6cd454ae..5555fed2ae94bb0428063720e2f46be67422ea7c 100644
--- a/src/kernel_services/analysis/logic_interp.ml
+++ b/src/kernel_services/analysis/logic_interp.ml
@@ -312,7 +312,7 @@ and loc_to_exp ~result {term_node = lnode ; term_type = ltype; term_loc = loc} =
Logic_utils.is_same_type
(Logic_typing.type_of_set_elem set) t.term_type ->
loc_to_exp ~result t
- | Tnull -> [ Cil.mkCast (TPtr(TVoid [], [])) (Cil.zero ~loc) ]
+ | Tnull -> [ Cil.mkCast ~newt:(TPtr(TVoid [], [])) (Cil.zero ~loc) ]
(* additional constructs *)
| Tapp _ | Tlambda _ | Trange _ | Tlet _
@@ -787,7 +787,7 @@ struct
dependencies of [*p]. *)
if is_same_label current_label lbl then (
let typ = Logic_typing.type_of_pointed t.term_type in
- let tlv = Cil.mkTermMem t TNoOffset in
+ let tlv = Cil.mkTermMem ~addr:t ~off:TNoOffset in
let tlv' = Logic_const.term (TLval tlv) typ in
self#do_term_lval tlv';
DoChildren
@@ -818,7 +818,7 @@ struct
(function Base.CLogic_Var _ -> false | _ -> true)
z
in
- add_result current_before current_stmt z
+ add_result ~before:current_before current_stmt z
with Db.From.Not_lval ->
raise (NYI "[logic_interp] dependencies of a term lval")
diff --git a/src/kernel_services/ast_data/alarms.ml b/src/kernel_services/ast_data/alarms.ml
index 18add97e069152e48a79387c584924766683ea5d..ce0c8902d6ff10d013c553f57e394948600fe0bd 100644
--- a/src/kernel_services/ast_data/alarms.ml
+++ b/src/kernel_services/ast_data/alarms.ml
@@ -260,7 +260,7 @@ module D =
Printer.pp_exp e1
(match e2 with None -> ">=" | Some _ -> "<")
Printer.pp_exp
- (match e2 with None -> Cil.zero e1.eloc | Some e -> e)
+ (match e2 with None -> Cil.zero ~loc:e1.eloc | Some e -> e)
| Invalid_pointer e ->
Format.fprintf fmt "Invalid_pointer(@[%a@])" Exp.pretty e
| Invalid_shift(e, n) ->
@@ -270,7 +270,7 @@ module D =
| Pointer_comparison(e1, e2) ->
Format.fprintf fmt "Pointer_comparison(@[%a@],@ @[%a@])"
Printer.pp_exp
- (match e1 with None -> Cil.zero e2.eloc | Some e -> e)
+ (match e1 with None -> Cil.zero ~loc:e2.eloc | Some e -> e)
Printer.pp_exp e2
| Differing_blocks (e1, e2) ->
Format.fprintf fmt "Differing_blocks(@[%a@],@ @[%a@])"
@@ -557,11 +557,11 @@ let create_predicate ?(loc=Location.unknown) alarm =
let here = Logic_const.here_label in
let typ = Ctype Cil.charPtrType in
let t1 =
- Logic_const.term ~loc:(best_loc loc e1.eloc) (Tbase_addr(here, t1)) typ
+ Logic_const.term ~loc:(best_loc ~loc e1.eloc) (Tbase_addr(here, t1)) typ
in
let t2 = Logic_utils.expr_to_term e2 in
let t2 =
- Logic_const.term ~loc:(best_loc loc e2.eloc) (Tbase_addr(here, t2)) typ
+ Logic_const.term ~loc:(best_loc ~loc e2.eloc) (Tbase_addr(here, t2)) typ
in
Logic_const.prel ~loc (Req, t1, t2)
@@ -648,7 +648,7 @@ let create_predicate ?(loc=Location.unknown) alarm =
| TPtr (TFun (ret, None, var, attrs), _), Some args ->
let ltyps = List.map (fun arg -> "", Cil.typeOf arg, []) args in
let typ = TFun (ret, Some ltyps, var, attrs) in
- Cil.mkCast (TPtr (typ, [])) e
+ Cil.mkCast ~newt:(TPtr (typ, [])) e
| t', _ ->
Kernel.fatal
"Trying to emit a Function_pointer alarm over expression %a \
diff --git a/src/kernel_services/ast_data/annotations.ml b/src/kernel_services/ast_data/annotations.ml
index 5afa6b0fce1921ad604a4af8911a5e583fbacbcf..57dce2e0e7cd042148e25e344d7a95afb8b2e641 100644
--- a/src/kernel_services/ast_data/annotations.ml
+++ b/src/kernel_services/ast_data/annotations.ml
@@ -123,7 +123,7 @@ let () =
Ast.add_linked_state funspec_state;
Funspecs.add_hook_on_remove
(fun _ kf spec ->
- let ppts = Property.ip_of_spec kf Kglobal [] spec in
+ let ppts = Property.ip_of_spec kf Kglobal ~active:[] spec in
List.iter Property_status.remove ppts)
module Code_annots =
@@ -431,7 +431,8 @@ let pre_register_funspec ?tbl ?(emitter=Emitter.end_user) ?(force=false) kf =
(fun e spec -> Format.printf "Register for function %a, Emitter %a, spec %a@." Kf.pretty kf Emitter.Usable_emitter.pretty e Cil_printer.pp_funspec spec)
tbl;
*)
- List.iter Property_status.register (Property.ip_of_spec kf Kglobal [] spec)
+ List.iter Property_status.register
+ (Property.ip_of_spec kf Kglobal ~active:[] spec)
end
let register_funspec ?emitter ?force kf =
@@ -890,7 +891,7 @@ let add_behaviors ?(register_children=true) e kf ?stmt ?active bhvs =
let b' = Cil.mk_behavior ~name:bhv.b_name () in
merge_behavior b' bhv;
merge_behavior b' (List.find (is_same_behavior bhv) bhvs);
- let ip = Property.ip_of_behavior kf ki active bhv in
+ let ip = Property.ip_of_behavior kf ki ~active bhv in
Property_status.remove ip;
(* mergeable clauses, i.e. assigns, from, and allocates may have changed.
Thus, if register_children is true, we need to update
@@ -899,20 +900,20 @@ let add_behaviors ?(register_children=true) e kf ?stmt ?active bhvs =
add the additional ip, nothing will be removed.
*)
if register_children then begin
- let ip = Property.ip_from_of_behavior kf ki active bhv in
+ let ip = Property.ip_from_of_behavior kf ki ~active bhv in
List.iter Property_status.remove ip;
- let ip = Property.ip_assigns_of_behavior kf ki active bhv in
+ let ip = Property.ip_assigns_of_behavior kf ki ~active bhv in
Option.iter Property_status.remove ip;
- let ip = Property.ip_allocation_of_behavior kf ki active bhv in
+ let ip = Property.ip_allocation_of_behavior kf ki ~active bhv in
Option.iter Property_status.remove ip;
- let ip = Property.ip_from_of_behavior kf ki active b' in
+ let ip = Property.ip_from_of_behavior kf ki ~active b' in
List.iter Property_status.register ip;
- let ip = Property.ip_assigns_of_behavior kf ki active b' in
+ let ip = Property.ip_assigns_of_behavior kf ki ~active b' in
Option.iter Property_status.register ip;
- let ip = Property.ip_allocation_of_behavior kf ki active b' in
+ let ip = Property.ip_allocation_of_behavior kf ki ~active b' in
Option.iter Property_status.register ip;
end;
- let ip = Property.ip_of_behavior kf ki active b' in
+ let ip = Property.ip_of_behavior kf ki ~active b' in
Property_status.register ip;
end)
full_spec.spec_behavior;
@@ -929,7 +930,7 @@ let add_behaviors ?(register_children=true) e kf ?stmt ?active bhvs =
when List.exists (is_same_behavior bhv) full_spec.spec_behavior
-> ()
| _ -> Property_status.register ip)
- (Property.ip_all_of_behavior kf ki active bhv))
+ (Property.ip_all_of_behavior kf ki ~active bhv))
bhvs
end
@@ -976,7 +977,7 @@ let add_complete e kf ?stmt ?active l =
emit_spec.spec_complete_behaviors <- l :: emit_spec.spec_complete_behaviors;
let active = match active with None -> [] | Some l -> l in
Property_status.register
- (Property.ip_of_complete kf (kinstr stmt) active l)
+ (Property.ip_of_complete kf (kinstr stmt) ~active l)
end
let add_disjoint e kf ?stmt ?active l =
@@ -991,7 +992,7 @@ let add_disjoint e kf ?stmt ?active l =
List.iter (check_bhv_name full_spec) l;
emit_spec.spec_disjoint_behaviors <- l :: emit_spec.spec_disjoint_behaviors;
let active = match active with None -> [] | Some l -> l in
- Property_status.register (Property.ip_of_disjoint kf (kinstr stmt) active l)
+ Property_status.register (Property.ip_of_disjoint kf (kinstr stmt) ~active l)
end
let add_spec ?register_children e kf ?stmt ?active spec =
@@ -1024,10 +1025,10 @@ let extend_behavior
let b = List.find has_same_name full_spec.spec_behavior in
let b' = List.find has_same_name emit_spec.spec_behavior in
let active = match active with None -> [] | Some l -> l in
- let ip = Property.ip_of_behavior kf (kinstr stmt) active b in
+ let ip = Property.ip_of_behavior kf (kinstr stmt) ~active b in
Property_status.remove ip;
set_bhv b b';
- let ip = Property.ip_of_behavior kf (kinstr stmt) active b in
+ let ip = Property.ip_of_behavior kf (kinstr stmt) ~active b in
Property_status.register ip
let add_requires e kf ?stmt ?active ?behavior l =
@@ -1108,14 +1109,14 @@ let add_assigns ~keep_empty e kf ?stmt ?active ?behavior a =
(* All assigns of a same behavior share the property.
Thus must remove the previous property before adding the new one *)
List.iter Property_status.remove
- (Property.ip_from_of_behavior kf ki active full_bhv);
+ (Property.ip_from_of_behavior kf ki ~active full_bhv);
Option.iter Property_status.remove
- (Property.ip_assigns_of_behavior kf ki active full_bhv);
- full_bhv.b_assigns <- merge_assigns keep_empty full_bhv.b_assigns a;
+ (Property.ip_assigns_of_behavior kf ki ~active full_bhv);
+ full_bhv.b_assigns <- merge_assigns ~keep_empty full_bhv.b_assigns a;
Option.iter Property_status.register
- (Property.ip_assigns_of_behavior kf ki active full_bhv);
+ (Property.ip_assigns_of_behavior kf ki ~active full_bhv);
List.iter Property_status.register
- (Property.ip_from_of_behavior kf ki active full_bhv);
+ (Property.ip_from_of_behavior kf ki ~active full_bhv);
)
in
let old_spec = get_full_spec kf ?stmt ?behavior:active () in
@@ -1136,11 +1137,11 @@ let add_allocates ~keep_empty e kf ?stmt ?active ?behavior a =
merge_allocation ~keep_empty e_bhv.b_allocation a;
let active = match active with None -> [] | Some l -> l in
Option.iter Property_status.remove
- (Property.ip_allocation_of_behavior kf ki active full_bhv);
+ (Property.ip_allocation_of_behavior kf ki ~active full_bhv);
full_bhv.b_allocation <-
merge_allocation ~keep_empty full_bhv.b_allocation a;
Option.iter Property_status.register
- (Property.ip_allocation_of_behavior kf ki active full_bhv);
+ (Property.ip_allocation_of_behavior kf ki ~active full_bhv);
in
let old_spec = get_full_spec kf ?stmt ?behavior:active () in
let bhv = get_spec_behavior old_spec behavior in
@@ -1515,7 +1516,7 @@ let remove_behavior ?(force=false) e kf bhv =
(* Kernel.feedback "Removing behavior %s@." bhv.b_name; *)
(* Kernel.feedback "New spec is %a@." Cil_printer.pp_funspec spec; *)
List.iter Property_status.remove
- (Property.ip_all_of_behavior kf Kglobal [] bhv)
+ (Property.ip_all_of_behavior kf Kglobal ~active:[] bhv)
in
remove_in_funspec e kf set_spec
@@ -1544,14 +1545,14 @@ let remove_complete e kf l =
spec.spec_complete_behaviors <- filterq l spec.spec_complete_behaviors
in
remove_in_funspec e kf set_spec;
- Property_status.remove (Property.ip_of_complete kf Kglobal [] l)
+ Property_status.remove (Property.ip_of_complete kf Kglobal ~active:[] l)
let remove_disjoint e kf l =
let set_spec spec _tbl =
spec.spec_disjoint_behaviors <- filterq l spec.spec_disjoint_behaviors
in
remove_in_funspec e kf set_spec;
- Property_status.remove (Property.ip_of_disjoint kf Kglobal [] l)
+ Property_status.remove (Property.ip_of_disjoint kf Kglobal ~active:[] l)
let remove_requires e kf p =
let set_spec spec _tbl =
diff --git a/src/kernel_services/ast_data/property.ml b/src/kernel_services/ast_data/property.ml
index 82bf32e58fd85b336d2dbc9b7faadc3e196f88f4..16f4828980bb0c648de24f4539b7978aa5735cfb 100644
--- a/src/kernel_services/ast_data/property.ml
+++ b/src/kernel_services/ast_data/property.ml
@@ -1568,7 +1568,7 @@ let ip_from_of_code_annot kf st ca = match ca.annot_content with
let ip_post_cond_of_behavior kf st ~active b =
ip_ensures_of_behavior kf st b
@ (Option.to_list (ip_assigns_of_behavior kf st ~active b))
- @ ip_from_of_behavior kf st active b
+ @ ip_from_of_behavior kf st ~active b
@ (Option.to_list (ip_allocation_of_behavior kf st ~active b))
let ip_of_behavior ib_kf ib_kinstr ~active ib_bhv =
@@ -1629,8 +1629,8 @@ let ip_post_cond_of_spec kf st ~active s =
let ip_of_spec kf st ~active s =
List.concat (List.map (ip_all_of_behavior kf st ~active) s.spec_behavior)
- @ ip_complete_of_spec kf st active s
- @ ip_disjoint_of_spec kf st active s
+ @ ip_complete_of_spec kf st ~active s
+ @ ip_disjoint_of_spec kf st ~active s
@ (Option.to_list (ip_terminates_of_spec kf st s))
@ (Option.to_list (ip_decreases_of_spec kf st s))
@@ -1645,7 +1645,7 @@ let ip_of_code_annot kf stmt ca =
let ki = Kstmt stmt in
match ca.annot_content with
| AAssert _ | AInvariant _ -> [ IPCodeAnnot {ica_kf=kf; ica_stmt=stmt; ica_ca=ca} ]
- | AStmtSpec (active,s) -> ip_of_spec kf ki active s
+ | AStmtSpec (active,s) -> ip_of_spec kf ki ~active s
| AVariant t ->
[ IPDecrease {id_kf=kf;id_kinstr=ki;id_ca=Some ca; id_variant=t}]
| AAllocation _ ->
diff --git a/src/kernel_services/ast_data/property_status.ml b/src/kernel_services/ast_data/property_status.ml
index 4287fa14d5735d40b90af7a03ee46a92c3a8e0eb..552171036e72d27253e46c4999b8122a5dd54f35 100644
--- a/src/kernel_services/ast_data/property_status.ml
+++ b/src/kernel_services/ast_data/property_status.ml
@@ -371,7 +371,9 @@ let property_kind = function
| IPBehavior {ib_kf; ib_kinstr; ib_active; ib_bhv} ->
(* logical consequence of its postconditions *)
let active = Datatype.String.Set.elements ib_active in
- let post = Property.ip_post_cond_of_behavior ib_kf ib_kinstr active ib_bhv in
+ let post =
+ Property.ip_post_cond_of_behavior ib_kf ib_kinstr ~active ib_bhv
+ in
Consequence post
| IPReachable {ir_kf; ir_kinstr; ir_program_point} ->
begin
diff --git a/src/kernel_services/ast_data/statuses_by_call.ml b/src/kernel_services/ast_data/statuses_by_call.ml
index c9509e533d0dd5d7ebfe33780f2d1988800e1486..5e9870e4bafe0a0b3693bfea0134b75790d2cdb1 100644
--- a/src/kernel_services/ast_data/statuses_by_call.ml
+++ b/src/kernel_services/ast_data/statuses_by_call.ml
@@ -170,7 +170,7 @@ let transpose_pred_at_callsite ~formals ~concretes id_pred =
let pred = Logic_const.pred_of_id_pred id_pred in
try
let arguments = associate [] ~formals ~concretes in
- let visitor :> Cil.cilVisitor = replacement_visitor arguments in
+ let visitor :> Cil.cilVisitor = replacement_visitor ~arguments in
let new_pred = Cil.visitCilPredicateNode visitor pred.pred_content in
let p_unnamed = Logic_const.unamed ~loc:pred.pred_loc new_pred in
let p_named = { p_unnamed with pred_name = pred.pred_name } in
diff --git a/src/kernel_services/ast_printing/printer_tag.ml b/src/kernel_services/ast_printing/printer_tag.ml
index d3b8032bb8c9f462943d0a156b32fdefe7cd7498..8e8af849c19b2f0cce75ef37fe5db241f190d00d 100644
--- a/src/kernel_services/ast_printing/printer_tag.ml
+++ b/src/kernel_services/ast_printing/printer_tag.ml
@@ -682,7 +682,7 @@ struct
(Property.ip_of_behavior
(Option.get self#current_kf)
self#current_kinstr
- active_behaviors b))
+ ~active:active_behaviors b))
super#behavior b
method! decreases fmt t =
@@ -705,7 +705,7 @@ struct
(Property.ip_of_complete
(Option.get self#current_kf)
self#current_kinstr
- active_behaviors
+ ~active:active_behaviors
t))
super#complete_behaviors t
@@ -715,7 +715,7 @@ struct
(Property.ip_of_disjoint
(Option.get self#current_kf)
self#current_kinstr
- active_behaviors
+ ~active:active_behaviors
t))
super#disjoint_behaviors t
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 448ed28deb36f956227fcc2b88e65bbbb31c9ec8..bdf9ad830c3992722787f154cb9b959a18e87840 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -242,7 +242,7 @@ let pp_attributes_ref = Extlib.mk_fun "Cil.pp_attributes_ref"
let default_behavior_name = "default!"
let is_default_mk_behavior ~name ~assumes = name = default_behavior_name && assumes =[]
-let is_default_behavior b = is_default_mk_behavior b.b_name b.b_assumes
+let is_default_behavior b = is_default_mk_behavior ~name:b.b_name ~assumes:b.b_assumes
let find_default_behavior spec =
try
@@ -5593,7 +5593,7 @@ let mkAddrOf ~loc ((_b, _off) as lval) : exp =
(* array *)
| _ -> new_exp ~loc (AddrOf lval)
-let mkAddrOfVi vi = mkAddrOf vi.vdecl (var vi)
+let mkAddrOfVi vi = mkAddrOf ~loc:vi.vdecl (var vi)
let mkAddrOrStartOf ~loc (lv: lval) : exp =
match unrollTypeSkel (typeOfLval lv) with
@@ -5874,8 +5874,8 @@ let mkBinOp ~loc op e1 e2 =
let machdep = false in
let make_expr common_type res_type =
constFoldBinOp ~loc machdep op
- (mkCastT t1 common_type e1)
- (mkCastT t2 common_type e2)
+ (mkCastT ~oldt:t1 ~newt:common_type e1)
+ (mkCastT ~oldt:t2 ~newt:common_type e2)
res_type
in
let doArithmetic () =
@@ -5931,14 +5931,14 @@ let mkBinOp ~loc op e1 e2 =
let t1' = integralPromotion t1 in
let t2' = integralPromotion t2 in
constFoldBinOp ~loc machdep op
- (mkCastT t1 t1' e1) (mkCastT t2 t2' e2) t1'
+ (mkCastT ~oldt:t1 ~newt:t1' e1) (mkCastT ~oldt:t2 ~newt:t2' e2) t1'
| (PlusA|MinusA)
when isArithmeticType t1 && isArithmeticType t2 -> doArithmetic ()
| (PlusPI|MinusPI) when isPointerType t1 && isIntegralType t2 ->
constFoldBinOp ~loc machdep op e1 e2 t1
| MinusPP when isPointerType t1 && isPointerType t2 ->
(* NB: Same as cabs2cil. Check if this is really what the standard says*)
- constFoldBinOp ~loc machdep op e1 (mkCastT t2 t1 e2) intType
+ constFoldBinOp ~loc machdep op e1 (mkCastT ~oldt:t2 ~newt:t1 e2) intType
| (Eq|Ne|Lt|Le|Ge|Gt)
when isArithmeticType t1 && isArithmeticType t2 ->
doArithmeticComp ()
@@ -6106,7 +6106,7 @@ let rec makeZeroInit ~loc (t: typ) : init =
| TPtr _ as t ->
SingleInit(
- if theMachine.insertImplicitCasts then mkCast t (zero ~loc)
+ if theMachine.insertImplicitCasts then mkCast ~newt:t (zero ~loc)
else zero ~loc)
| x -> Kernel.fatal ~current:true "Cannot initialize type: %a" !pp_typ_ref x
@@ -6290,7 +6290,8 @@ let uniqueVarNames (f: file) : unit =
(* Here if this is the first time we define a name *)
Hashtbl.add globalNames vi.vname vi.vid;
(* And register it *)
- Alpha.registerAlphaName gAlphaTable vi.vname (CurrentLoc.get ())
+ Alpha.registerAlphaName ~alphaTable:gAlphaTable
+ ~lookupname:vi.vname ~data:(CurrentLoc.get ())
end)
| _ -> ());
@@ -6334,7 +6335,7 @@ let uniqueVarNames (f: file) : unit =
(* Fix the type again *)
setFormals fdec fdec.sformals;
(* Undo the changes to the global table *)
- Alpha.undoAlphaChanges gAlphaTable !undolist;
+ Alpha.undoAlphaChanges ~alphaTable:gAlphaTable ~undolist:!undolist;
()
end
| _ -> ());
diff --git a/src/kernel_services/ast_queries/file.ml b/src/kernel_services/ast_queries/file.ml
index c3cace34893b20ffbcdc21cb9041c3499c5abcf1..3a4dd2b55f0ae4241e37da8f1a8808144683a28b 100644
--- a/src/kernel_services/ast_queries/file.ml
+++ b/src/kernel_services/ast_queries/file.ml
@@ -759,7 +759,9 @@ let add_annotation kf st a =
| AStmtSpec
([],
({ spec_behavior = [ { b_name = "Frama_C_implicit_init" } as bhv]})) ->
- let props = Property.ip_post_cond_of_behavior kf (Kstmt st) [] bhv in
+ let props =
+ Property.ip_post_cond_of_behavior kf (Kstmt st) ~active:[] bhv
+ in
List.iter (fun p -> Implicit_annotations.add p []) props
| _ -> ()
@@ -1220,7 +1222,7 @@ let fill_built_ins () =
Cil_builtins.init_builtins ();
end else begin
Kernel.debug "Machine is not computed, initialize everything";
- Cil.initCIL (Logic_builtin.init()) (get_machdep ());
+ Cil.initCIL ~initLogicBuiltins:(Logic_builtin.init()) (get_machdep ());
end;
(* Fill logic tables with builtins *)
Logic_env.Builtins.apply ();
@@ -1633,7 +1635,7 @@ let reorder_ast () = reorder_custom_ast (Ast.get())
(* Fill logic tables with builtins *)
let init_cil () =
- Cil.initCIL (Logic_builtin.init()) (get_machdep ());
+ Cil.initCIL ~initLogicBuiltins:(Logic_builtin.init()) (get_machdep ());
Logic_env.Builtins.apply ();
Logic_env.prepare_tables ()
diff --git a/src/kernel_services/ast_transformations/inline.ml b/src/kernel_services/ast_transformations/inline.ml
index c4d70589e7d2ece6eb332abbf9cb94b54060d082..abc07955e5d3b7f347d06c660023c18f3aad4ff4 100644
--- a/src/kernel_services/ast_transformations/inline.ml
+++ b/src/kernel_services/ast_transformations/inline.ml
@@ -251,7 +251,7 @@ let inliner functions_to_inline = object (self)
r.vdefined <- false;
Cil.update_var_type
r (Cil.typeRemoveAttributes ["const"] r.vtype);
- false, None, (Cil.mkAddrOf loc (Cil.var r)) :: args
+ false, None, (Cil.mkAddrOf ~loc (Cil.var r)) :: args
| Some _, _ ->
Kernel.fatal "Attempt to initialize an inexistent varinfo"
in
diff --git a/src/plugins/aorai/aorai_utils.ml b/src/plugins/aorai/aorai_utils.ml
index c48bc00ff4efd4552ff5bdff6c72ef144c57154b..2c3075fad5b7684070d0d6dfff77441ea291ff0f 100644
--- a/src/plugins/aorai/aorai_utils.ml
+++ b/src/plugins/aorai/aorai_utils.ml
@@ -397,27 +397,27 @@ let rec term_to_exp t res =
let loc = t.term_loc in
match t.term_node with
| TConst (Integer (value,repr)) -> Cil.kinteger64 ~loc ?repr value
- | TConst (LStr str) -> new_exp loc (Const (CStr str))
- | TConst (LWStr l) -> new_exp loc (Const (CWStr l))
- | TConst (LChr c) -> new_exp loc (Const (CChr c))
+ | TConst (LStr str) -> new_exp ~loc (Const (CStr str))
+ | TConst (LWStr l) -> new_exp ~loc (Const (CWStr l))
+ | TConst (LChr c) -> new_exp ~loc (Const (CChr c))
| TConst (LReal l_real) ->
(* r_nearest is by definition in double precision. *)
- new_exp loc (Const (CReal (l_real.r_nearest, FDouble, None)))
- | TConst (LEnum e) -> new_exp loc (Const (CEnum e))
- | TLval tlval -> new_exp loc (Lval (tlval_to_lval tlval res))
- | TSizeOf ty -> new_exp loc (SizeOf ty)
- | TSizeOfE t -> new_exp loc (SizeOfE(term_to_exp t res))
- | TSizeOfStr s -> new_exp loc (SizeOfStr s)
- | TAlignOf ty -> new_exp loc (AlignOf ty)
- | TAlignOfE t -> new_exp loc (AlignOfE (term_to_exp t res))
+ new_exp ~loc (Const (CReal (l_real.r_nearest, FDouble, None)))
+ | TConst (LEnum e) -> new_exp ~loc (Const (CEnum e))
+ | TLval tlval -> new_exp ~loc (Lval (tlval_to_lval tlval res))
+ | TSizeOf ty -> new_exp ~loc (SizeOf ty)
+ | TSizeOfE t -> new_exp ~loc (SizeOfE(term_to_exp t res))
+ | TSizeOfStr s -> new_exp ~loc (SizeOfStr s)
+ | TAlignOf ty -> new_exp ~loc (AlignOf ty)
+ | TAlignOfE t -> new_exp ~loc (AlignOfE (term_to_exp t res))
| TUnOp (unop, t) ->
- new_exp loc (UnOp (unop, term_to_exp t res, Cil.intType))
+ new_exp ~loc (UnOp (unop, term_to_exp t res, Cil.intType))
| TBinOp (binop, t1, t2)->
- new_exp loc
+ new_exp ~loc
(BinOp(binop, term_to_exp t1 res, term_to_exp t2 res, Cil.intType))
- | TCastE (ty, t) -> new_exp loc (CastE (ty, term_to_exp t res))
- | TAddrOf tlval -> new_exp loc (AddrOf (tlval_to_lval tlval res))
- | TStartOf tlval -> new_exp loc (StartOf (tlval_to_lval tlval res))
+ | TCastE (ty, t) -> new_exp ~loc (CastE (ty, term_to_exp t res))
+ | TAddrOf tlval -> new_exp ~loc (AddrOf (tlval_to_lval tlval res))
+ | TStartOf tlval -> new_exp ~loc (StartOf (tlval_to_lval tlval res))
| TLogic_coerce (_,t) -> term_to_exp t res
| _ ->
Aorai_option.fatal
@@ -441,7 +441,7 @@ and tlval_to_lval (tlhost, toffset) res =
end
in
(Var v_info, t_to_loffset toffset)
- |TMem t -> mkMem (term_to_exp t res) (t_to_loffset toffset)
+ |TMem t -> mkMem ~addr:(term_to_exp t res) ~off:(t_to_loffset toffset)
|TResult _ ->
(match res with
| Some res -> Var res, t_to_loffset toffset
@@ -576,7 +576,7 @@ let crosscond_to_exp generated_kf curr_f curr_status loc cond res =
let stmts2, vars2, defs2, e2 = expnode_convert c2 in
stmts1 @ stmts2, vars1 @ vars2,
Cil_datatype.Varinfo.Set.union defs1 defs2,
- Cil.mkBinOp loc LOr e1 e2
+ Cil.mkBinOp ~loc LOr e1 e2
| Some i when Integer.is_zero i -> expnode_convert c2
| Some _ -> [], [], Cil_datatype.Varinfo.Set.empty,e1)
| TAnd (c1, c2) ->
@@ -586,7 +586,7 @@ let crosscond_to_exp generated_kf curr_f curr_status loc cond res =
let stmts2, vars2, defs2, e2 = expnode_convert c2 in
stmts1 @ stmts2, vars1 @vars2,
Cil_datatype.Varinfo.Set.union defs1 defs2,
- Cil.mkBinOp loc LAnd e1 e2
+ Cil.mkBinOp ~loc LAnd e1 e2
| Some i when Integer.is_zero i ->
[], [], Cil_datatype.Varinfo.Set.empty, e1
| Some _ -> expnode_convert c2)
@@ -594,32 +594,32 @@ let crosscond_to_exp generated_kf curr_f curr_status loc cond res =
let stmts1, vars1, defs1, e1 = expnode_convert c1 in
(match Cil.isInteger e1 with
| None ->
- stmts1, vars1, defs1, Cil.new_exp loc (UnOp(LNot, e1,Cil.intType))
+ stmts1, vars1, defs1, Cil.new_exp ~loc (UnOp(LNot, e1,Cil.intType))
| Some i when Integer.is_zero i ->
- [], [], Cil_datatype.Varinfo.Set.empty, Cil.one loc
- | Some _ -> [], [], Cil_datatype.Varinfo.Set.empty, Cil.zero loc)
+ [], [], Cil_datatype.Varinfo.Set.empty, Cil.one ~loc
+ | Some _ -> [], [], Cil_datatype.Varinfo.Set.empty, Cil.zero ~loc)
| TCall (f,None) ->
if check_current_event f Promelaast.Call then
- [], [], Cil_datatype.Varinfo.Set.empty, Cil.one loc
+ [], [], Cil_datatype.Varinfo.Set.empty, Cil.one ~loc
else
- [], [], Cil_datatype.Varinfo.Set.empty, Cil.zero loc
+ [], [], Cil_datatype.Varinfo.Set.empty, Cil.zero ~loc
| TCall (f, Some bhv) ->
if check_current_event f Promelaast.Call then begin
let res, stmt, new_kf = mk_behavior_call generated_kf f bhv in
[ stmt ], [res], new_kf, Cil.evar res
end else
- [], [], Cil_datatype.Varinfo.Set.empty, Cil.zero loc
+ [], [], Cil_datatype.Varinfo.Set.empty, Cil.zero ~loc
| TReturn f ->
if check_current_event f Promelaast.Return then
- [], [], Cil_datatype.Varinfo.Set.empty, Cil.one loc
+ [], [], Cil_datatype.Varinfo.Set.empty, Cil.one ~loc
else
- [], [], Cil_datatype.Varinfo.Set.empty, Cil.zero loc
- | TTrue -> [], [], Cil_datatype.Varinfo.Set.empty, Cil.one loc
- | TFalse -> [], [], Cil_datatype.Varinfo.Set.empty, Cil.zero loc
+ [], [], Cil_datatype.Varinfo.Set.empty, Cil.zero ~loc
+ | TTrue -> [], [], Cil_datatype.Varinfo.Set.empty, Cil.one ~loc
+ | TFalse -> [], [], Cil_datatype.Varinfo.Set.empty, Cil.zero ~loc
| TRel(rel,t1,t2) ->
[], [], Cil_datatype.Varinfo.Set.empty,
Cil.mkBinOp
- loc (rel_convert rel) (term_to_exp t1 res) (term_to_exp t2 res)
+ ~loc (rel_convert rel) (term_to_exp t1 res) (term_to_exp t2 res)
in
expnode_convert cond
@@ -774,7 +774,7 @@ let int2enumstate nums =
let enum = find_enum nums in
Logic_const.term (TConst (LEnum enum)) (Ctype (TEnum (enum.eihost,[])))
-let int2enumstate_exp loc nums = new_exp loc (Const (CEnum (find_enum nums)))
+let int2enumstate_exp loc nums = new_exp ~loc (Const (CEnum (find_enum nums)))
(** Given an lval term 'host' and an integer value 'off', it returns a lval term host[off]. *)
let mk_offseted_array_states_as_enum host off =
@@ -821,7 +821,7 @@ let is_state_pred state =
Logic_const.tvar (Data_for_aorai.get_state_logic_var state))
let is_state_non_det_stmt (_,copy) loc =
- mkStmtOneInstr ~ghost:true (Set (Cil.var copy, Cil.one loc, loc))
+ mkStmtOneInstr ~ghost:true (Set (Cil.var copy, Cil.one ~loc, loc))
let is_state_det_stmt state loc =
let var = Data_for_aorai.get_varinfo curState in
@@ -833,12 +833,12 @@ let is_state_exp state loc =
if Aorai_option.Deterministic.get ()
then
Cil.mkBinOp
- loc Eq
+ ~loc Eq
(int2enumstate_exp loc state.nums)
(Cil.evar ~loc (Data_for_aorai.get_varinfo curState))
else
Cil.mkBinOp
- loc Eq (Cil.evar (Data_for_aorai.get_state_var state)) (Cil.one loc)
+ ~loc Eq (Cil.evar (Data_for_aorai.get_state_var state)) (Cil.one ~loc)
let is_out_of_state_pred state =
if Aorai_option.Deterministic.get () then
@@ -864,12 +864,12 @@ let is_out_of_state_exp state loc =
if Aorai_option.Deterministic.get ()
then
Cil.mkBinOp
- loc Ne
+ ~loc Ne
(int2enumstate_exp loc state.nums)
(evar ~loc (Data_for_aorai.get_varinfo curState))
else
Cil.mkBinOp
- loc Eq
+ ~loc Eq
(Cil.evar (Data_for_aorai.get_state_var state))
(mk_int_exp 0)
@@ -1944,17 +1944,17 @@ let act_convert loc act res =
function
| Counter_init t_lval ->
Cil.mkStmtOneInstr
- ~ghost:true (Set (tlval_to_lval t_lval res, Cil.one loc, loc))
+ ~ghost:true (Set (tlval_to_lval t_lval res, Cil.one ~loc, loc))
| Counter_incr t_lval ->
let my_lval = tlval_to_lval t_lval res in
Cil.mkStmtOneInstr ~ghost:true
(Set
(my_lval,
(Cil.mkBinOp
- loc
+ ~loc
PlusA
- (Cil.new_exp loc (Lval my_lval))
- (Cil.one loc)),
+ (Cil.new_exp ~loc (Lval my_lval))
+ (Cil.one ~loc)),
loc))
| Copy_value (t_lval, t) ->
Cil.mkStmtOneInstr ~ghost:true
@@ -1971,11 +1971,11 @@ let mk_transitions_stmt generated_kf loc f st res trans =
let (tr_stmts, tr_vars, tr_funcs, exp) =
crosscond_to_exp generated_kf f st loc trans.cross res
in
- let cond = Cil.mkBinOp loc LAnd (is_state_exp trans.start loc) exp in
+ let cond = Cil.mkBinOp ~loc LAnd (is_state_exp trans.start loc) exp in
(tr_stmts @ aux_stmts,
tr_vars @ aux_vars,
Cil_datatype.Varinfo.Set.union tr_funcs new_funcs,
- Cil.mkBinOp loc LOr exp_from_trans cond,
+ Cil.mkBinOp ~loc LOr exp_from_trans cond,
(Cil.copy_exp cond, act_convert loc trans.actions res)
:: stmt_from_action))
trans
@@ -2150,12 +2150,12 @@ let auto_func_block generated_kf loc f st status res =
(* First statement : what is the current status : called or return ? *)
equalsStmt
(Cil.var (Data_for_aorai.get_varinfo Data_for_aorai.curOpStatus))
- (Cil.new_exp loc (Const (Data_for_aorai.op_status_to_cenum st))) loc;
+ (Cil.new_exp ~loc (Const (Data_for_aorai.op_status_to_cenum st))) loc;
(* Second statement : what is the current operation,
i.e. which function ? *)
equalsStmt
(Cil.var (Data_for_aorai.get_varinfo Data_for_aorai.curOp))
- (Cil.new_exp loc
+ (Cil.new_exp ~loc
(Const (Data_for_aorai.func_to_cenum (Kernel_function.get_name f))))
loc
]
diff --git a/src/plugins/constant_propagation/api.ml b/src/plugins/constant_propagation/api.ml
index 546a99f3100d4c05a6c437898202fa996fb7958a..58e6e1fad7e4643ee0c661f0671d35671cf417c4 100644
--- a/src/plugins/constant_propagation/api.ml
+++ b/src/plugins/constant_propagation/api.ml
@@ -93,7 +93,7 @@ class propagate project fnames ~cast_intro = object(self)
else
oldt, newt
in
- let exp = Cil.mkCastT oldt newt e in
+ let exp = Cil.mkCastT ~oldt ~newt e in
if cast_intro then
exp
else match exp.enode with
@@ -274,7 +274,9 @@ class propagate project fnames ~cast_intro = object(self)
they will disappear when the l-value is dereferenced. *)
match self#propagated exp_mem ~ignore_const_cast:true with
| Some exp_mem' ->
- let lv = Cil.new_exp expr.eloc (Lval (Cil.mkMem exp_mem' off)) in
+ let lv =
+ Cil.new_exp ~loc:expr.eloc (Lval (Cil.mkMem ~addr:exp_mem' ~off))
+ in
Cil.ChangeDoChildrenPost (lv, fun x -> x)
| None -> Cil.DoChildren
end
@@ -317,9 +319,9 @@ class propagate project fnames ~cast_intro = object(self)
Cil.DoChildrenPost add_decls
method! vlval lv =
- let simplify (host,offs as lv) = match host with
- | Mem e -> Cil.mkMem e offs (* canonize in case the propagation
- simplified [lv] *)
+ let simplify (host,off as lv) = match host with
+ | Mem e -> Cil.mkMem ~addr:e ~off (* canonize in case the propagation
+ simplified [lv] *)
| Var _ -> lv
in
Cil.ChangeDoChildrenPost(lv, simplify)
@@ -356,7 +358,7 @@ let journalized_get =
let fresh_project =
FC_file.create_project_from_visitor
(PropagationParameters.Project_name.get ())
- (fun prj -> new propagate prj fnames cast_intro)
+ (fun prj -> new propagate prj fnames ~cast_intro)
in
let ctx = Parameter_state.get_selection_context () in
let ctx = State_selection.diff ctx selection_command_line_option in
@@ -382,7 +384,7 @@ let compute () =
PropagationParameters.feedback "beginning constant propagation";
let fnames = PropagationParameters.SemanticConstFold.get () in
let cast_intro = PropagationParameters.CastIntro.get () in
- let propagated = get fnames cast_intro in
+ let propagated = get fnames ~cast_intro in
if PropagationParameters.SemanticConstFolding.get () then
FC_file.pretty_ast ~prj:propagated ();
let project_name = Project.get_unique_name propagated in
diff --git a/src/plugins/e-acsl/src/code_generator/global_observer.ml b/src/plugins/e-acsl/src/code_generator/global_observer.ml
index 3ba52a52f12062bc633f7acb3023649c05211cf7..49f351fd678bac63d9e41680498de74dda3650fc 100644
--- a/src/plugins/e-acsl/src/code_generator/global_observer.ml
+++ b/src/plugins/e-acsl/src/code_generator/global_observer.ml
@@ -134,8 +134,8 @@ let mk_init_function () =
Literal_strings.fold
(fun s vi stmts ->
let loc = Location.unknown in
- let e = Cil.new_exp ~loc:loc (Const (CStr s)) in
- let str_size = Cil.new_exp loc (SizeOfStr s) in
+ let e = Cil.new_exp ~loc (Const (CStr s)) in
+ let str_size = Cil.new_exp ~loc (SizeOfStr s) in
Smart_stmt.assigns ~loc ~result:(Cil.var vi) e
:: Smart_stmt.store_stmt ~str_size vi
:: Smart_stmt.full_init_stmt vi
diff --git a/src/plugins/e-acsl/src/code_generator/injector.ml b/src/plugins/e-acsl/src/code_generator/injector.ml
index 50b878a67e9cb41875b9e1cd9c5750d5e3906bdb..ad0d79d1acb046c529fe59081b3b58a08db959f8 100644
--- a/src/plugins/e-acsl/src/code_generator/injector.ml
+++ b/src/plugins/e-acsl/src/code_generator/injector.ml
@@ -175,7 +175,7 @@ let inject_in_instr env kf stmt = function
let caller, args =
match caller.enode with
| Lval (Var fvi, _) ->
- let fvi, args = rename_caller loc fvi args in
+ let fvi, args = rename_caller ~loc fvi args in
Cil.evar fvi, args
| _ -> caller, args
in
@@ -813,10 +813,10 @@ let inject_mtracking_handler main =
(* some non-standard arguments. *)
nulls
in
- let ptr_size = Cil.sizeOf loc Cil.voidPtrType in
+ let ptr_size = Cil.sizeOf ~loc Cil.voidPtrType in
let args = args @ [ ptr_size ] in
- let init = Smart_stmt.rtl_call loc "memory_init" args in
- let clean = Smart_stmt.rtl_call loc "memory_clean" [] in
+ let init = Smart_stmt.rtl_call ~loc "memory_init" args in
+ let clean = Smart_stmt.rtl_call ~loc "memory_clean" [] in
surround_function_with fundec init (Some clean)
in
Option.iter handle_main main
diff --git a/src/plugins/e-acsl/src/code_generator/loops.ml b/src/plugins/e-acsl/src/code_generator/loops.ml
index 44d5e8fdc770257ba1368a413631d1b127aafd78..11e6b986d0181c534b48c3d2678bf083342b967b 100644
--- a/src/plugins/e-acsl/src/code_generator/loops.ml
+++ b/src/plugins/e-acsl/src/code_generator/loops.ml
@@ -386,7 +386,7 @@ let rec mk_nested_loops ~loc mk_innermost_block kf env lscope_vars =
(* Even though p is considered a RTE, it was generated while
typing the loop, and was already typed at this moment. Thus
there is no need to type it again *)
- !predicate_to_exp_ref adata kf (Env.push env) p
+ !predicate_to_exp_ref ~adata kf (Env.push env) p
in
let stmt, env =
Assert.runtime_check
diff --git a/src/plugins/e-acsl/src/code_generator/smart_exp.ml b/src/plugins/e-acsl/src/code_generator/smart_exp.ml
index 0f341c105c7cb17e90c07cd61142c5f8203ab643..11bbe595da24af5eaa69e95251fe8aecc803d33b 100644
--- a/src/plugins/e-acsl/src/code_generator/smart_exp.ml
+++ b/src/plugins/e-acsl/src/code_generator/smart_exp.ml
@@ -69,7 +69,7 @@ let lnot ~loc e =
Cil.zero ~loc
let null ~loc =
- Cil.mkCast (TPtr (TVoid [], [])) (Cil.zero ~loc)
+ Cil.mkCast ~newt:(TPtr (TVoid [], [])) (Cil.zero ~loc)
(*
Local Variables:
diff --git a/src/plugins/e-acsl/src/code_generator/smart_stmt.ml b/src/plugins/e-acsl/src/code_generator/smart_stmt.ml
index e76366fa4ce2ca8d087bd63fb7b84d4b05fa98cb..62bb1853203f0e5e80832473b35528d2b085bf9f 100644
--- a/src/plugins/e-acsl/src/code_generator/smart_stmt.ml
+++ b/src/plugins/e-acsl/src/code_generator/smart_stmt.ml
@@ -168,7 +168,7 @@ let initialize ~loc (host, offset as lv) = match host, offset with
let typ = Cil.typeOfLval lv in
rtl_call ~loc
"initialize"
- [ Cil.mkAddrOf ~loc lv; Cil.new_exp loc (SizeOf typ) ]
+ [ Cil.mkAddrOf ~loc lv; Cil.new_exp ~loc (SizeOf typ) ]
let named_store_stmt name ?str_size vi =
let ty = Cil.unrollType vi.vtype in
diff --git a/src/plugins/e-acsl/src/code_generator/translate_predicates.ml b/src/plugins/e-acsl/src/code_generator/translate_predicates.ml
index bbfd3a767701130246363136fa348942176a641b..571e1a983880730b8473a7b59070d02760975a82 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_predicates.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate_predicates.ml
@@ -121,7 +121,7 @@ let rec predicate_content_to_exp ~adata ?(inplace=false) ?name kf env p =
None
e1
res2
- (Cil.zero loc, env3))
+ (Cil.zero ~loc, env3))
)
env)
| Por(p1, p2) ->
@@ -145,7 +145,7 @@ let rec predicate_content_to_exp ~adata ?(inplace=false) ?name kf env p =
kf
None
e1
- (Cil.one loc, env')
+ (Cil.one ~loc, env')
res2)
)
env)
@@ -238,7 +238,7 @@ let rec predicate_content_to_exp ~adata ?(inplace=false) ?name kf env p =
let p = { p with pred_name = name :: p.pred_name } in
let tp = Logic_const.toplevel_predicate ~kind:Assert p in
let annot = Logic_const.new_code_annotation (AAssert ([],tp)) in
- Typing.preprocess_rte (Env.Local_vars.get env) annot;
+ Typing.preprocess_rte ~lenv:(Env.Local_vars.get env) annot;
!translate_rte_annots_ref
Printer.pp_code_annotation
annot
diff --git a/src/plugins/e-acsl/src/code_generator/translate_terms.ml b/src/plugins/e-acsl/src/code_generator/translate_terms.ml
index b9ace500b655ca11fbdac5f02eb7ba040be7d369..c5530b377bcb98a94b65380f4b4fd4d31e3c8b48 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_terms.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate_terms.ml
@@ -121,8 +121,8 @@ let affect_binop ~loc var_as_varinfo var_as_exp binop exp_type exp1 exp2 =
else if Gmp_types.Q.is_t exp_type then
Error.not_yet "rational in affect_binop"
else
- Smart_stmt.assigns loc
- (Cil.var var_as_varinfo)
+ Smart_stmt.assigns ~loc
+ ~result:(Cil.var var_as_varinfo)
(Cil.mkBinOp ~loc binop exp1 exp2 )
let rec thost_to_host kf env th = match th with
@@ -203,7 +203,7 @@ and extended_quantifier_to_exp ~adata ~loc kf env t t_min t_max lambda name =
let lbd_stmt,env =
Env.pop_and_get env
(Gmp.affect ~loc (Cil.var lbd_as_varinfo) lbd_as_exp e_lbd)
- false Env.Middle
+ ~global_clear:false Env.Middle
in
(* statement construction *)
(* cond = k > e_max; or cond = __gmpz_cmp(k,e_max) *)
@@ -653,7 +653,7 @@ and context_insensitive_term_to_exp ~adata ?(inplace=false) kf env t =
Extlib.nest
adata
(Translate_utils.conditional_to_exp
- ~name:"or" ~loc kf (Some t) e1 (Cil.one loc, env') res2)
+ ~name:"or" ~loc kf (Some t) e1 (Cil.one ~loc, env') res2)
)
env)
in
@@ -674,7 +674,7 @@ and context_insensitive_term_to_exp ~adata ?(inplace=false) kf env t =
Extlib.nest
adata
(Translate_utils.conditional_to_exp
- ~name:"and" ~loc kf (Some t) e1 res2 (Cil.zero loc, env3))
+ ~name:"and" ~loc kf (Some t) e1 res2 (Cil.zero ~loc, env3))
)
env)
in
diff --git a/src/plugins/e-acsl/src/code_generator/typed_number.ml b/src/plugins/e-acsl/src/code_generator/typed_number.ml
index 879b90b89d5bca36abebf57b1da22faf82951ca3..389ee6cfd6c263e7d8a7e22fead7b3ba28af770d 100644
--- a/src/plugins/e-acsl/src/code_generator/typed_number.ml
+++ b/src/plugins/e-acsl/src/code_generator/typed_number.ml
@@ -67,7 +67,7 @@ let add_cast ~loc ?name env kf ctx strnum t_opt e =
only non integral value that can be seen as an integer, while the
type system infers that it is C-representable (see
tests/runtime/null.i) *)
- Cil.mkCast Cil.longType e (* \null *)
+ Cil.mkCast ~newt:Cil.longType e (* \null *)
else
e
in
diff --git a/src/plugins/from/callwise.ml b/src/plugins/from/callwise.ml
index d1777d344888060b813b5c79818334fe0bbd1261..3c7d13ec481e04eaccd7de8149e7bbeeaf616699 100644
--- a/src/plugins/from/callwise.ml
+++ b/src/plugins/from/callwise.ml
@@ -171,7 +171,7 @@ let record_for_individual_froms (call_stack, value_res) =
| { value_initial_state } :: _ -> value_initial_state
in
if From_parameters.VerifyAssigns.get () then
- !Db.Value.verify_assigns_froms cur_kf pre_state froms;
+ !Db.Value.verify_assigns_froms cur_kf ~pre:pre_state froms;
(match value_res with
| Value_types.NormalStore (_, memexec_counter) ->
MemExec.replace memexec_counter froms
diff --git a/src/plugins/gui/design.ml b/src/plugins/gui/design.ml
index 402b9459e3b4cbff8128ce19e8ac3f05e7aca4c8..b84c78b521a758476eb3fa02d6364fc0a5b58700 100644
--- a/src/plugins/gui/design.ml
+++ b/src/plugins/gui/design.ml
@@ -697,7 +697,7 @@ struct
let iter = source#get_iter_at_char offset in
let mark = iter#set_line_offset 0 in
let category = category validity in
- source#remove_source_marks mark mark () ;
+ source#remove_source_marks ~start:mark ~stop:mark () ;
ignore (source#create_source_mark ~category mark) ;
Hashtbl.replace tooltip_marks iter#line (long_category validity);
match call_site with
@@ -882,7 +882,7 @@ class main_window () : main_window_extension_points =
(* status bar (at bottom) *)
(* toplevel_vbox->bottom_hbox-> *statusbar *)
let statusbar = GMisc.statusbar ~packing:bottom_hbox#add () in
- let status_context = statusbar#new_context "messages" in
+ let status_context = statusbar#new_context ~name:"messages" in
(* progress bar (at bottom) *)
(* toplevel_vbox->bottom_hbox-> [statusbar;*progress_bar] *)
@@ -992,7 +992,9 @@ class main_window () : main_window_extension_points =
let (xbuf, ybuf) = source_viewer#window_to_buffer_coords
~tag:`WIDGET ~x:(int_of_float x) ~y:(int_of_float y)
in
- let iterpos = source_viewer#get_iter_at_location xbuf ybuf in
+ let iterpos =
+ source_viewer#get_iter_at_location ~x:xbuf ~y:ybuf
+ in
let line = iterpos#line in
if Hashtbl.mem Feedback.tooltip_marks line then begin
let text = Hashtbl.find Feedback.tooltip_marks line in
@@ -1093,17 +1095,18 @@ class main_window () : main_window_extension_points =
in
expander#set_label_widget (label_hb#coerce);
ignore (expander#connect#activate
- (fun () -> (* Save expansion of panels*)
- Configuration.set key_config
- (Configuration.ConfBool (not expander#expanded))));
+ ~callback:(fun () -> (* Save expansion of panels*)
+ Configuration.set key_config
+ (Configuration.ConfBool (not expander#expanded))));
let frame = GBin.frame ~packing:expander#add () in
frame#add widget;
(* Drag stuff *)
expander#drag#source_set ~modi:[`BUTTON1] ~actions:[`MOVE] targets;
ignore (expander#drag#connect#beginning
- (fun _ -> dragged_frame:=Some (frame,text)));
- ignore (expander#drag#connect#ending (fun _ -> dragged_frame:=None));
+ ~callback:(fun _ -> dragged_frame:=Some (frame,text)));
+ ignore (expander#drag#connect#ending
+ ~callback:(fun _ -> dragged_frame:=None));
(* Refreshers *)
Option.iter
@@ -1120,31 +1123,31 @@ class main_window () : main_window_extension_points =
let dropper (widget:GObj.widget) =
widget#drag#dest_set ~flags:[`ALL] ~actions:[`MOVE] targets;
ignore (widget#drag#connect#drop
- (fun drag_context ~x:_ ~y:_ ~time:_ ->
- match !dragged_frame with
- | None (* Not dropping a panel *) -> true
- | Some (frame,title) ->
- (*Format.printf "Hello %d %d %ld@." x y time;*)
- let w = drag_context#source_widget in
- let new_w =
- GWindow.window ~position:`MOUSE ~title ~show:true () in
- let b = GPack.vbox ~packing:new_w#add () in
- frame#misc#reparent b#coerce;
- ignore (new_w#connect#destroy
- (fun () ->
- frame#misc#reparent w;
- w#misc#show ()));
- w#misc#hide ();
- true));
+ ~callback:(fun drag_context ~x:_ ~y:_ ~time:_ ->
+ match !dragged_frame with
+ | None (* Not dropping a panel *) -> true
+ | Some (frame,title) ->
+ (*Format.printf "Hello %d %d %ld@." x y time;*)
+ let w = drag_context#source_widget in
+ let new_w =
+ GWindow.window ~position:`MOUSE ~title ~show:true () in
+ let b = GPack.vbox ~packing:new_w#add () in
+ frame#misc#reparent b#coerce;
+ ignore (new_w#connect#destroy
+ ~callback:(fun () ->
+ frame#misc#reparent w;
+ w#misc#show ()));
+ w#misc#hide ();
+ true));
ignore (widget#drag#connect#motion
- (fun drag_context ~x:_ ~y:_ ~time ->
- (*Format.printf "Motion %d %d %ld@." x y time;*)
- drag_context#status ~time (Some `MOVE);
- true));
+ ~callback:(fun drag_context ~x:_ ~y:_ ~time ->
+ (*Format.printf "Motion %d %d %ld@." x y time;*)
+ drag_context#status ~time (Some `MOVE);
+ true));
ignore (widget#drag#connect#leave
- (fun drag_context ~time ->
- (*Format.printf "Motion %d %d %ld@." x y time;*)
- drag_context#status ~time (Some `MOVE)));
+ ~callback:(fun drag_context ~time ->
+ (*Format.printf "Motion %d %d %ld@." x y time;*)
+ drag_context#status ~time (Some `MOVE)));
in
dropper main_window#coerce;
dropper source_viewer#coerce;
@@ -1206,7 +1209,7 @@ class main_window () : main_window_extension_points =
iter#line iter#line_offset
;
ignore (self#source_viewer#backward_display_line_start iter);
- self#source_viewer#buffer#place_cursor iter;
+ self#source_viewer#buffer#place_cursor ~where:iter;
ignore (self#source_viewer#scroll_to_mark
~use_align:true ~yalign:0.5 ~xalign:0. `INSERT);
let adj = source_viewer_scroll#hadjustment in
@@ -1338,11 +1341,11 @@ class main_window () : main_window_extension_points =
Format.kfprintf
(function _ ->
ignore (w#event#connect#leave_notify
- (fun _ -> self#pop_info ();true));
+ ~callback:(fun _ -> self#pop_info ();true));
ignore (w#event#connect#enter_notify
- (fun _ ->
- Format.pp_print_flush bfmt ();
- self#push_info_buffer ~buffer "" ;false)))
+ ~callback:(fun _ ->
+ Format.pp_print_flush bfmt ();
+ self#push_info_buffer ~buffer "" ;false)))
bfmt
fmt
@@ -1421,7 +1424,7 @@ class main_window () : main_window_extension_points =
in
match found_iters with
| Some (i1,i2) ->
- buffer#place_cursor i1;
+ buffer#place_cursor ~where:i1;
buffer#select_range i1 i2;
ignore (scroll_to_iter i1
~use_align:false
@@ -1541,7 +1544,9 @@ class main_window () : main_window_extension_points =
let (xbuf, ybuf) = source_viewer#window_to_buffer_coords
~tag:`WIDGET ~x:(int_of_float x) ~y:(int_of_float y)
in
- let iterpos = source_viewer#get_iter_at_location xbuf ybuf in
+ let iterpos =
+ source_viewer#get_iter_at_location ~x:xbuf ~y:ybuf
+ in
let line = iterpos#line in
try
let stmt = Hashtbl.find Feedback.call_sites line in
@@ -1659,26 +1664,26 @@ class main_window () : main_window_extension_points =
(* Set the relative position for all paned whenever the main window is
resized *)
ignore (main_window#misc#connect#size_allocate
- (fun ({Gtk.width=w;Gtk.height=h} as rect) ->
- Configuration.set "window_width" (Configuration.ConfInt w);
- Configuration.set "window_height" (Configuration.ConfInt h);
-
- if main_window_metrics.Gtk.width <> w
- || main_window_metrics.Gtk.height <> h then
- begin
- place_paned hb_sources
- (Configuration.find_float ~default:0.5 "hb_sources");
- place_paned vb_message_sources
- (Configuration.find_float ~default:0.71
- "vb_message_sources");
- place_paned filetree_panel_vpaned
- (Configuration.find_float ~default:0.5
- "filetree_panel_vpaned");
- place_paned toplevel_hpaned
- (Configuration.find_float ~default:0.18
- "toplevel_hpaned");
- end;
- main_window_metrics <- rect));
+ ~callback:(fun ({Gtk.width=w;Gtk.height=h} as rect) ->
+ Configuration.set "window_width" (Configuration.ConfInt w);
+ Configuration.set "window_height" (Configuration.ConfInt h);
+
+ if main_window_metrics.Gtk.width <> w
+ || main_window_metrics.Gtk.height <> h then
+ begin
+ place_paned hb_sources
+ (Configuration.find_float ~default:0.5 "hb_sources");
+ place_paned vb_message_sources
+ (Configuration.find_float ~default:0.71
+ "vb_message_sources");
+ place_paned filetree_panel_vpaned
+ (Configuration.find_float ~default:0.5
+ "filetree_panel_vpaned");
+ place_paned toplevel_hpaned
+ (Configuration.find_float ~default:0.18
+ "toplevel_hpaned");
+ end;
+ main_window_metrics <- rect));
file_tree <- Some (Filetree.make file_tree_view);
self#file_tree#add_select_function (filetree_selector self#toplevel);
diff --git a/src/plugins/gui/file_manager.ml b/src/plugins/gui/file_manager.ml
index 60e776f88f0f81ba2619d394abdeb8f99f529cff..d0b7e8b624783a92a35cf798b0dc5d9164c46a50 100644
--- a/src/plugins/gui/file_manager.ml
+++ b/src/plugins/gui/file_manager.ml
@@ -225,8 +225,8 @@ let preferences (host_window: Design.main_window_extension_points) =
Gui_parameters.debug "canceled, preferences not saved";
dialog#destroy ()
in
- ignore (wb_ok#connect#clicked f_ok);
- ignore (wb_cancel#connect#clicked f_cancel);
+ ignore (wb_ok#connect#clicked ~callback:f_ok);
+ ignore (wb_cancel#connect#clicked ~callback:f_cancel);
(* the enter key is linked to the ok action *)
(* the escape key is linked to the cancel action *)
dialog#misc#grab_focus ();
@@ -247,9 +247,9 @@ let insert (host_window: Design.main_window_extension_points) =
~icon:`REFRESH ~label:"Reparse"
~tooltip:"Reparse source files, and replay analyses"
(Menu_manager.Unit_callback (fun () -> reparse host_window));
- Menu_manager.toolmenubar `REVERT_TO_SAVED "Load session"
+ Menu_manager.toolmenubar ~icon:`REVERT_TO_SAVED ~label:"Load session"
(Menu_manager.Unit_callback (fun () -> load_file host_window));
- Menu_manager.toolmenubar `SAVE "Save session"
+ Menu_manager.toolmenubar ~icon:`SAVE ~label:"Save session"
(Menu_manager.Unit_callback (fun () -> save_file host_window));
Menu_manager.menubar ~icon:`SAVE_AS "Save session as"
(Menu_manager.Unit_callback (fun () -> save_file_as host_window));
diff --git a/src/plugins/gui/filetree.ml b/src/plugins/gui/filetree.ml
index 1358a33b520284acd4380ee4b4c147b7303fad95..f1b9ad235814e23a7bdc2bc9eb134dc46538f4ae 100644
--- a/src/plugins/gui/filetree.ml
+++ b/src/plugins/gui/filetree.ml
@@ -975,7 +975,7 @@ let make (tree_view:GTree.view) =
let () = match get_column_header_button column with
| None ->
(* Should not happen, but who knowns? *)
- ignore (column#connect#clicked pop_menu)
+ ignore (column#connect#clicked ~callback:pop_menu)
| Some button ->
(* Connect the menu to a right click. *)
let callback evt =
@@ -988,26 +988,26 @@ let make (tree_view:GTree.view) =
(* Changes the sort order when left-clicking on the column header. *)
let callback () = self#change_sort column MYTREE.Ascending; self#reset () in
- ignore (column#connect#clicked callback);
+ ignore (column#connect#clicked ~callback:callback);
(* Sets the sort_kind to the initial sort. *)
sort_kind <- `ASCENDING, column#get_oid;
ignore (MenusHide.mi_set_callback
- mhide_functions key_hide_functions self#reset_internal);
+ mhide_functions ~key:key_hide_functions self#reset_internal);
ignore (MenusHide.mi_set_callback
- mhide_variables key_hide_variables self#reset_internal);
+ mhide_variables ~key:key_hide_variables self#reset_internal);
ignore (MenusHide.mi_set_callback
- mhide_stdlib key_hide_stdlib self#reset_internal);
+ mhide_stdlib ~key:key_hide_stdlib self#reset_internal);
ignore (MenusHide.mi_set_callback
- mhide_defined key_hide_defined self#reset_internal);
+ mhide_defined ~key:key_hide_defined self#reset_internal);
ignore (MenusHide.mi_set_callback
- mhide_undefined key_hide_undefined self#reset_internal);
+ mhide_undefined ~key:key_hide_undefined self#reset_internal);
ignore (MenusHide.mi_set_callback
- mhide_builtins key_hide_builtins self#reset_internal);
+ mhide_builtins ~key:key_hide_builtins self#reset_internal);
ignore (MenusHide.mi_set_callback
- mhide_annotations key_hide_annotations self#reset_internal);
+ mhide_annotations ~key:key_hide_annotations self#reset_internal);
ignore (MenusHide.mi_set_callback
- mflat_mode key_flat_mode self#reset_internal);
+ mflat_mode ~key:key_flat_mode self#reset_internal);
menu#add (GMenu.separator_item () :> GMenu.menu_item);
tree_view#set_model (Some (init_model:>GTree.model));
diff --git a/src/plugins/gui/gtk_form.ml b/src/plugins/gui/gtk_form.ml
index 3af4a4bdfe89fb657d83940188a4ad9ed45fb954..23207f17b0a94bf2709bca7121ec962bd8da9546 100644
--- a/src/plugins/gui/gtk_form.ml
+++ b/src/plugins/gui/gtk_form.ml
@@ -81,7 +81,7 @@ let menu entries ?width ?tooltip ~packing get set demon =
try combo_box#set_active (lookup 0 (get ()) entries)
with Not_found -> ()
in
- ignore (combo_box#connect#changed callback) ;
+ ignore (combo_box#connect#changed ~callback) ;
Gtk_helper.do_tooltip ?tooltip combo_box ;
register demon update
diff --git a/src/plugins/gui/gtk_helper.ml b/src/plugins/gui/gtk_helper.ml
index 06ce6a12167605be6ea706f450aeca9bb3a70071..2a0af55e56de346fa6d647097b0276ba53232af8 100644
--- a/src/plugins/gui/gtk_helper.ml
+++ b/src/plugins/gui/gtk_helper.ml
@@ -495,7 +495,7 @@ let on_combo
let k = select 0 !result values in
if k >= 0 then combo_box#set_active k
in
- ignore (combo_box#connect#changed callback) ;
+ ignore (combo_box#connect#changed ~callback) ;
ignore (mk_label ~use_markup ~xalign:0. container label) ;
(fun () -> update ())
@@ -676,8 +676,8 @@ let input_widget ~parent ~widget ~event ~get_text ~bind_ok ~expand
retour := None;
window#destroy ()
in
- ignore (wb_ok#connect#clicked f_ok);
- ignore (wb_cancel#connect#clicked f_cancel);
+ ignore (wb_ok#connect#clicked ~callback:f_ok);
+ ignore (wb_cancel#connect#clicked ~callback:f_cancel);
(* the enter key is linked to the ok action *)
(* the escape key is linked to the cancel action *)
ignore (event#connect#key_press ~callback:
@@ -698,7 +698,7 @@ let input_widget ~parent ~widget ~event ~get_text ~bind_ok ~expand
let input_string ~parent ~title ?ok ?cancel ?(text="") message =
let we_chaine = GEdit.entry ~text () in
if text <> "" then
- we_chaine#select_region 0 (we_chaine#text_length);
+ we_chaine#select_region ~start:0 ~stop:(we_chaine#text_length);
input_widget ~parent ~widget:we_chaine#coerce ~event:we_chaine#event
~get_text:(fun () -> we_chaine#text) ~bind_ok:true
~expand: false
@@ -740,7 +740,7 @@ class error_manager ?reset (o_parent:GWindow.window_skel) : host =
~modal:true
()
in
- ignore (w#connect#response (fun _ -> w#destroy ()));
+ ignore (w#connect#response ~callback:(fun _ -> w#destroy ()));
ignore (w#run ());
if reset then f_reset ()
@@ -834,9 +834,9 @@ let make_text_page ?pos (notebook:GPack.notebook) title =
let flash_ref = ref flash in
let w = GText.view ~packing:sw#add () in
let _ = w#set_editable false in
- let _ = w#misc#connect#map (fun () -> !flash_ref false) in
- let _ = w#event#connect#focus_in (fun _ -> !flash_ref false; false) in
- let _ = w#buffer#connect#changed (fun () -> !flash_ref true)
+ let _ = w#misc#connect#map ~callback:(fun () -> !flash_ref false) in
+ let _ = w#event#connect#focus_in ~callback:(fun _ -> !flash_ref false; false) in
+ let _ = w#buffer#connect#changed ~callback:(fun () -> !flash_ref true)
in
let reparent_page (notebook:GPack.notebook) =
let flash, sw = make_tab_label notebook in
diff --git a/src/plugins/gui/launcher.ml b/src/plugins/gui/launcher.ml
index 4afc056925e0cb8f5ab3b494693ecad14368a12b..77354ccdba1bde29f31e94b640ac6611207f5228 100644
--- a/src/plugins/gui/launcher.ml
+++ b/src/plugins/gui/launcher.ml
@@ -263,9 +263,9 @@ let show ?height ?width ~(host:basic_main) () =
()
in
ignore (dialog#misc#connect#size_allocate
- (fun ({Gtk.width=w;Gtk.height=h}) ->
- Configuration.set "launcher_width" (Configuration.ConfInt w);
- Configuration.set "launcher_height" (Configuration.ConfInt h)));
+ ~callback:(fun ({Gtk.width=w;Gtk.height=h}) ->
+ Configuration.set "launcher_width" (Configuration.ConfInt w);
+ Configuration.set "launcher_height" (Configuration.ConfInt h)));
ignore
(GMisc.label
~text:"Customize parameters, then click on `Execute'"
@@ -280,12 +280,12 @@ let show ?height ?width ~(host:basic_main) () =
let cancel =
GButton.button ~label:"Close" ~stock:`CANCEL ~packing:buttons#pack ()
in
- ignore (cancel#connect#released dialog#destroy);
+ ignore (cancel#connect#released ~callback:dialog#destroy);
let button_run =
GButton.button
~label:"Configure analysis" ~stock:`EXECUTE ~packing:buttons#pack ()
in
- ignore (button_run#connect#released (run host dialog));
+ ignore (button_run#connect#released ~callback:(run host dialog));
let plugins = ref [] in
Plugin.iter_on_plugins
(fun p ->
diff --git a/src/plugins/gui/menu_manager.ml b/src/plugins/gui/menu_manager.ml
index 1ea516b767f60fc8f63bbaf5078faa9dedeeecad..e7a25f57ae1609c47061180c13123d6cc2d828cc 100644
--- a/src/plugins/gui/menu_manager.ml
+++ b/src/plugins/gui/menu_manager.ml
@@ -249,20 +249,21 @@ class menu_manager ?packing (_:Gtk_helper.host) =
let item = match stock_opt, callback with
| None, Unit_callback callback ->
let mi = GMenu.menu_item ~packing:!!menubar_packing ~label () in
- ignore (mi#connect#activate callback);
+ ignore (mi#connect#activate ~callback);
MStandard mi
| Some stock, Unit_callback callback ->
let image = (GMisc.image ~stock ~xalign:0. () :> GObj.widget) in
let text = label in
let packing = !!menubar_packing in
let mi = Gtk_helper.image_menu_item ~image ~text ~packing in
- ignore (mi#connect#activate callback);
+ ignore (mi#connect#activate ~callback);
MStandard mi
| _, Bool_callback (callback, active) ->
let mi = GMenu.check_menu_item
~packing:!!menubar_packing ~label ~active:(active ()) ()
in
- ignore (mi#connect#activate (fun () -> callback mi#active));
+ ignore (mi#connect#activate
+ ~callback:(fun () -> callback mi#active));
set_active_states <-
(fun () -> mi#set_active (active ())) :: set_active_states;
MCheck mi
diff --git a/src/plugins/gui/pretty_source.ml b/src/plugins/gui/pretty_source.ml
index 159758dd7d3dab7f325e7486207be2982f21a268..57097deb4f181bbd979a48adad0672636cade807 100644
--- a/src/plugins/gui/pretty_source.ml
+++ b/src/plugins/gui/pretty_source.ml
@@ -385,7 +385,7 @@ let display_source globals
~callback:(fun _ -> call_cc next_10)
()) ca *)
end;
- source#place_cursor source#start_iter;
+ source#place_cursor ~where:source#start_iter;
let last_shown_area =
Gtk_helper.make_tag source ~name:"last_shown_area"
[`BACKGROUND "light green"]
diff --git a/src/plugins/gui/property_navigator.ml b/src/plugins/gui/property_navigator.ml
index f13abe403ac4a21112d2539b1f2c86d47065ce50..0566095701dc9db9eb6c119ed6c131df250cf440 100644
--- a/src/plugins/gui/property_navigator.ml
+++ b/src/plugins/gui/property_navigator.ml
@@ -304,9 +304,9 @@ struct
let expanded =Gtk_helper.Configuration.find_bool ~default:true key_config in
let expander = GBin.expander ~expanded ~packing:box#pack () in
ignore (expander#connect#activate
- (fun () -> (* Save expansion of panels*)
- Gtk_helper.Configuration.set key_config
- (Gtk_helper.Configuration.ConfBool (not expander#expanded))));
+ ~callback:(fun () -> (* Save expansion of panels*)
+ Gtk_helper.Configuration.set key_config
+ (Gtk_helper.Configuration.ConfBool (not expander#expanded))));
let hb = GPack.vbox ~packing:expander#add () in
let markup = Printf.sprintf "<span font_weight=\"bold\">%s</span>" text in
let label = GMisc.label ~markup () in
@@ -515,8 +515,8 @@ let make_panel (main_ui:main_window_extension_points) =
reset_menu_button#misc#set_tooltip_text "Reconfigure filters according to presets";
reset_menu_button#add icon#coerce;
ignore (reset_menu_button#connect#clicked
- (fun () -> checks_menu#popup ~button:0
- ~time:(GtkMain.Main.get_current_event_time ())));
+ ~callback:(fun () -> checks_menu#popup ~button:0
+ ~time:(GtkMain.Main.get_current_event_time ())));
let sc_buttons =
GBin.scrolled_window ~vpolicy:`AUTOMATIC ~hpolicy:`NEVER ()
in
@@ -559,7 +559,7 @@ let make_panel (main_ui:main_window_extension_points) =
let format_graph ppf =
Consolidation_graph.dump (Consolidation_graph.get ip) ppf in
Dgraph_helper.graph_window_through_dot
- main_ui#main_window "Dependencies" format_graph
+ ~parent:main_ui#main_window ~title:"Dependencies" format_graph
| None -> ()));
view#selection#set_select_function
(fun path currently_selected ->
diff --git a/src/plugins/gui/wfile.ml b/src/plugins/gui/wfile.ml
index c58964822cc684b1dea04a7a9415c2ae07b1e03d..7c2151dbb2fab7409aadc1a3676be00eafcead3d 100644
--- a/src/plugins/gui/wfile.ml
+++ b/src/plugins/gui/wfile.ml
@@ -41,7 +41,7 @@ class dialog
initializer
begin
- ignore (dialog#event#connect#delete (fun _ -> true)) ;
+ ignore (dialog#event#connect#delete ~callback:(fun _ -> true)) ;
dialog#add_button "Cancel" `DELETE_EVENT ;
dialog#add_button select `SELECT ;
ignore (GMisc.label ~packing:(dialog#action_area#pack ~expand:true) ()) ;
@@ -102,7 +102,7 @@ class button ?kind ?title ?select ?tooltip ?parent () =
begin
button#add box#coerce ;
button#set_focus_on_click false ;
- ignore (button#connect#clicked self#select) ;
+ ignore (button#connect#clicked ~callback:self#select) ;
dialog#connect current#set ;
Wutil.set_tooltip button tooltip ;
current#connect
diff --git a/src/plugins/gui/widget.ml b/src/plugins/gui/widget.ml
index 38be3eeb0ecbc394421bb81736855b37d98db5d4..d5aa28abf66ff5e7916cbe37c44336f2898e8109 100644
--- a/src/plugins/gui/widget.ml
+++ b/src/plugins/gui/widget.ml
@@ -198,7 +198,7 @@ class button ?align ?icon ?label ?(border=true) ?tooltip () =
method! set_enabled e = s#set_enabled e ; b#set_enabled e
method default = button#grab_default
initializer
- ignore (button#connect#clicked self#fire)
+ ignore (button#connect#clicked ~callback:self#fire)
end
(* -------------------------------------------------------------------------- *)
@@ -216,7 +216,8 @@ class checkbox ~label ?tooltip () =
initializer
begin
set_tooltip button tooltip ;
- ignore (button#connect#clicked (fun () -> s#set button#active)) ;
+ ignore (button#connect#clicked
+ ~callback:(fun () -> s#set button#active)) ;
end
end
@@ -236,7 +237,7 @@ class toggle ?align ?icon ?label ?(border=true) ?tooltip () =
toggle_icon_warning := false ) ;
b#set_icon icn
initializer
- ignore (button#connect#clicked (fun () -> s#set button#active))
+ ignore (button#connect#clicked ~callback:(fun () -> s#set button#active))
end
class switch ?tooltip () =
@@ -253,7 +254,7 @@ class switch ?tooltip () =
begin
set_tooltip evt tooltip ;
ignore (evt#event#connect#button_release
- (fun _evt -> self#set (not s#get) ; false)) ;
+ ~callback:(fun _evt -> self#set (not s#get) ; false)) ;
end
end
@@ -274,7 +275,8 @@ class radio_group ~label ?tooltip () =
initializer
begin
set_tooltip button tooltip ;
- ignore (button#connect#clicked (fun () -> s#set button#active)) ;
+ ignore (button#connect#clicked
+ ~callback:(fun () -> s#set button#active)) ;
end
end
@@ -286,7 +288,8 @@ class toggle_group ?label ?icon ?tooltip () =
inherit! button_skel ?icon ?tooltip (button :> GButton.button_skel) as b
method! set_enabled e = s#set_enabled e ; b#set_enabled e
method! set a = s#set a ; button#set_relief (if a then `NORMAL else `NONE)
- initializer ignore (button#connect#clicked (fun () -> s#set (not s#get)))
+ initializer ignore (button#connect#clicked
+ ~callback:(fun () -> s#set (not s#get)))
end
class ['a] group (default : 'a) =
@@ -403,7 +406,7 @@ class ['a] menu ~default ?(options=[]) ?render ?items () =
end
initializer
- ignore (cmb#connect#notify_active self#clicked)
+ ignore (cmb#connect#notify_active ~callback:self#clicked)
end
diff --git a/src/plugins/gui/wpane.ml b/src/plugins/gui/wpane.ml
index a10bbbd0e5ebb8e3fcb4b33469b2e78570647e76..abad65ccd83d0a07247370b6790fc89daea5b4db 100644
--- a/src/plugins/gui/wpane.ml
+++ b/src/plugins/gui/wpane.ml
@@ -190,7 +190,7 @@ class ['a] notebook ?tabs ~default () =
method on_focus page f = select#connect (fun p -> f (page = p))
initializer
begin
- ignore (view#connect#switch_page self#switched) ;
+ ignore (view#connect#switch_page ~callback:self#switched) ;
Wutil.on tabs (fun p -> view#set_show_tabs true ; view#set_tab_pos p) ;
end
method coerce = view#coerce
@@ -284,7 +284,7 @@ class ['a] dialog ~title ~window ?(resize=false) () =
hclip#set_left_padding 24 ;
hclip#set_right_padding 24 ;
ignore (shell#event#connect#delete
- (fun _ -> self#select `CANCEL ; true)) ;
+ ~callback:(fun _ -> self#select `CANCEL ; true)) ;
(* returning [true] prevent the dialog from being destroyed *)
end
diff --git a/src/plugins/impact/compute_impact.ml b/src/plugins/impact/compute_impact.ml
index c2412a84cc92794fb76f8fe504adcae0328d5bc7..1744f0a3e7da3f56490a759d998ecd28957c7be2 100644
--- a/src/plugins/impact/compute_impact.ml
+++ b/src/plugins/impact/compute_impact.ml
@@ -246,7 +246,7 @@ let add_to_do_aux ~init wl kf pdg (pn, zone as n) =
(** Build the initial value of the [todo] field, from a list of initial nodes *)
let initial_to_do_list wl kf pdg nodes =
- List.iter (fun n -> add_to_do_aux true wl kf pdg n) nodes
+ List.iter (fun n -> add_to_do_aux ~init:true wl kf pdg n) nodes
(** Mark a new node as impacted, and simultaneously mark that it is equivalent
to nodes that are all initial nodes *)
@@ -434,7 +434,8 @@ let all_upward_callers wl kfs =
"Found call %a -> %a"
Kernel_function.pretty caller Kernel_function.pretty callee;
let nodes =
- lazy (Pdg_aux.all_call_out_nodes pdg_callee pdg_caller callsite)
+ lazy (Pdg_aux.all_call_out_nodes ~callee:pdg_callee ~caller:pdg_caller
+ callsite)
in
wl.upward_calls <-
KfKfCall.Map.add (caller, callee, callsite) nodes wl.upward_calls
diff --git a/src/plugins/impact/register_gui.ml b/src/plugins/impact/register_gui.ml
index 6c9657c1b3b10d536ba493ba6b7fa84fcfdf7523..7bab54731cca8a0cea1b44c18d227f15e00d86c8 100644
--- a/src/plugins/impact/register_gui.ml
+++ b/src/plugins/impact/register_gui.ml
@@ -145,7 +145,7 @@ let impact_highlighter buffer loc ~start ~stop =
if Enabled.get () then
let buffer = buffer#buffer in
let tag name color =
- let t = make_tag buffer name [`BACKGROUND color ] in
+ let t = make_tag buffer ~name [`BACKGROUND color ] in
apply_tag buffer t start stop
in
let hilight kf s =
diff --git a/src/plugins/inout/operational_inputs.ml b/src/plugins/inout/operational_inputs.ml
index 716bf523e0895fd1d5b3aca6fa31215a75724dca..a395988ec71f11fa143044ffb9ea436ba5af2492 100644
--- a/src/plugins/inout/operational_inputs.ml
+++ b/src/plugins/inout/operational_inputs.ml
@@ -144,7 +144,8 @@ let eval_assigns kf state assigns =
| From l ->
let aux acc { it_content = from } =
let _, loc, deps =
- !Db.Properties.Interp.loc_to_loc_under_over None state from in
+ !Db.Properties.Interp.loc_to_loc_under_over ~result:None state from
+ in
let acc = Zone.join (clean_deps deps) acc in
let z = enumerate_valid_bits Read loc in
Zone.join z acc
diff --git a/src/plugins/instantiate/basic_blocks.ml b/src/plugins/instantiate/basic_blocks.ml
index 1f5ffa62f3e5b7a52ee840b669722c6994c38ff3..391bc8393730f0dac9479b3ab9cf279456ebed39 100644
--- a/src/plugins/instantiate/basic_blocks.ml
+++ b/src/plugins/instantiate/basic_blocks.ml
@@ -45,7 +45,7 @@ let call_function lval vi args =
let typs = Cil.argsToList typs in
let gen_arg exp (_, typ, _) =
if Cil_datatype.Typ.equal vi.vtype typ then exp
- else Cil.mkCast typ exp
+ else Cil.mkCast ~newt:typ exp
in
let args = List.map2 gen_arg args typs in
Call(lval, (Cil.evar vi), args, loc)
diff --git a/src/plugins/instantiate/string/memset.ml b/src/plugins/instantiate/string/memset.ml
index 1893eccee5e79c448be12dc0c3b2e3acb7a8e521..b507191adc662529c4920dfea98bde3cb2a2e860 100644
--- a/src/plugins/instantiate/string/memset.ml
+++ b/src/plugins/instantiate/string/memset.ml
@@ -253,7 +253,7 @@ let retype_args (_t, e) args =
| Value_of t -> base_char_type t
| _ -> unexpected "trying to retype arguments on an ill-typed call"
in
- let v = Cil.mkCast base_type (Cil.stripCasts v) in
+ let v = Cil.mkCast ~newt:base_type (Cil.stripCasts v) in
[ ptr ; v ; n ]
| Some fv, [ ptr ; v ; n ] ->
let ptr = Cil.stripCasts ptr in
diff --git a/src/plugins/metrics/metrics_gui.ml b/src/plugins/metrics/metrics_gui.ml
index ffa5177eeac76688b38a700d9152cff965f53df5..b51ee8ad14930f28ee3f6ed7bee8d9db9372da9a 100644
--- a/src/plugins/metrics/metrics_gui.ml
+++ b/src/plugins/metrics/metrics_gui.ml
@@ -81,7 +81,7 @@ let init_panel (main_ui: Design.main_window_extension_points) =
let launch_button = GButton.button ~label:"Launch"
~packing:(up#pack) ()
in
- ignore(launch_button#connect#clicked (fun () ->
+ ignore(launch_button#connect#clicked ~callback:(fun () ->
let actions = (get_panel ()).actions in
let sopt = GEdit.text_combo_get_active choices in
match sopt with
diff --git a/src/plugins/metrics/register_gui.ml b/src/plugins/metrics/register_gui.ml
index 55d9fe2936cc6c7cb8566c60d7ac8d97cbee01af..43c78ef633fdb6c0af1f6cb20d6f5cb0f814cf28 100644
--- a/src/plugins/metrics/register_gui.ml
+++ b/src/plugins/metrics/register_gui.ml
@@ -294,7 +294,9 @@ module ValueCoverageGUI = struct
Varinfo.Set.diff metrics.syntactic metrics.semantic
in
let hilit color =
- let tag = make_tag buffer#buffer "metrics" [`BACKGROUND color] in
+ let tag =
+ make_tag buffer#buffer ~name:"metrics" [`BACKGROUND color]
+ in
apply_tag buffer#buffer tag start stop
in
let syn_hilit () = hilit "yellow"
diff --git a/src/plugins/occurrence/register_gui.ml b/src/plugins/occurrence/register_gui.ml
index 9c7cded8ae3a2e4ddbe42b704e3f260a7199c8e4..dca96b2801708b3d86462a2d10a3c4da18cca3a9 100644
--- a/src/plugins/occurrence/register_gui.ml
+++ b/src/plugins/occurrence/register_gui.ml
@@ -115,7 +115,7 @@ let occurrence_highlighter buffer loc ~start ~stop =
let result = filter_accesses result in
let buffer = buffer#buffer in
let highlight () =
- let tag = make_tag buffer "occurrence" [`BACKGROUND "yellow" ] in
+ let tag = make_tag buffer ~name:"occurrence" [`BACKGROUND "yellow" ] in
apply_tag buffer tag start stop
in
match loc with
diff --git a/src/plugins/pdg/build.ml b/src/plugins/pdg/build.ml
index f88749851b7a988b2749892be9332e7680a502f6..25aae34647763bf81d689a6121ff339dc3430c87 100644
--- a/src/plugins/pdg/build.ml
+++ b/src/plugins/pdg/build.ml
@@ -308,13 +308,13 @@ let create_lval_node pdg state key ~l_loc ~exact ~l_dpds ~l_decl =
let new_node = add_elem pdg key in
add_dpds pdg new_node Dpd.Addr state l_dpds;
add_decl_dpds pdg new_node Dpd.Addr l_decl;
- let new_state = Pdg_state.add_loc_node state exact l_loc new_node in
+ let new_state = Pdg_state.add_loc_node state ~exact l_loc new_node in
(new_node, new_state)
let add_from pdg state_before state lval (default, deps) =
let new_node = add_elem pdg (Key.out_from_key lval) in
let exact = (not default) in
- let state = Pdg_state.add_loc_node state exact lval new_node in
+ let state = Pdg_state.add_loc_node state ~exact lval new_node in
add_dpds pdg new_node Dpd.Data state_before deps;
state
@@ -327,7 +327,7 @@ let process_call_output pdg state_before_call state stmt out default from_out fc
let key = Key.call_output_key stmt out in
let new_node = create_call_output_node pdg state_before_call stmt
key from_out fct_dpds in
- let state = Pdg_state.add_loc_node state exact out new_node
+ let state = Pdg_state.add_loc_node state ~exact out new_node
in state
(** mix between process_call_output and process_asgn *)
@@ -340,7 +340,7 @@ let process_call_return pdg state_before_call state_with_inputs stmt
add_dpds pdg new_node Dpd.Addr state_before_call l_dpds;
add_decl_dpds pdg new_node Dpd.Addr l_decl;
let new_state =
- Pdg_state.add_loc_node state_before_call exact l_loc new_node in
+ Pdg_state.add_loc_node state_before_call ~exact l_loc new_node in
new_state
(** for skip statement : we want to add a node in the PDG in order to be able
@@ -473,7 +473,7 @@ let add_retres pdg state ret_stmt retres_loc_dpds retres_decls =
let retres = Locations.(enumerate_valid_bits Read retres_loc) in
add_dpds pdg return_node Dpd.Data state retres_loc_dpds;
add_decl_dpds pdg return_node Dpd.Data retres_decls;
- let new_state = Pdg_state.add_loc_node state true retres return_node in
+ let new_state = Pdg_state.add_loc_node state ~exact:true retres return_node in
create_fun_output_node pdg (Some new_state) retres;
new_state
@@ -843,7 +843,7 @@ module Computer
let join_and_is_included smaller larger =
pdg_debug "smaller (new): %a larger (old) %a" pretty smaller pretty larger;
- let is_new, new_state = Pdg_state.test_and_merge larger smaller in
+ let is_new, new_state = Pdg_state.test_and_merge ~old:larger smaller in
pdg_debug "new_state: %a is_new: %b" pretty new_state is_new;
(new_state, not is_new)
;;
@@ -947,7 +947,7 @@ let compute_pdg_for_f kf =
let init_state =
process_entry_point pdg f_stmts;
let formals = Kernel_function.get_formals kf in
- process_declarations pdg formals f_locals
+ process_declarations pdg ~formals ~locals:f_locals
in
let froms = match f_stmts with
| [] ->
diff --git a/src/plugins/pdg/ctrlDpds.ml b/src/plugins/pdg/ctrlDpds.ml
index 549de05a6a3d30bc0e27d65b74fbb201f24b897e..960f0db2193cb581f13d496613c16832018d65e5 100644
--- a/src/plugins/pdg/ctrlDpds.ml
+++ b/src/plugins/pdg/ctrlDpds.ml
@@ -128,7 +128,7 @@ end = struct
let rec process_stmts prev_list stmts = match stmts with
| [] -> prev_list
| s :: tail ->
- let s_last_stmts = process_stmt graph prev_list s in
+ let s_last_stmts = process_stmt graph ~prev_list ~stmt:s in
process_stmts s_last_stmts tail
in process_stmts [] blk.bstmts
diff --git a/src/plugins/pdg_types/pdgIndex.ml b/src/plugins/pdg_types/pdgIndex.ml
index 018db8c4ff5df08f056c6d0707467d53d00ca3e2..37d4b2f13828cb70435f68d66c29a3ffe78d8651 100644
--- a/src/plugins/pdg_types/pdgIndex.ml
+++ b/src/plugins/pdg_types/pdgIndex.ml
@@ -161,11 +161,11 @@ module Signature = struct
let add_info sgn key info ~replace =
match key with
- | In InCtrl -> add_in_ctrl sgn info replace
- | In (InNum n) -> add_input sgn n info replace
- | In (InImpl loc) -> add_impl_input sgn loc info replace
- | Out OutRet -> add_out_ret sgn info replace
- | Out (OutLoc k) -> add_output sgn k info replace
+ | In InCtrl -> add_in_ctrl sgn info ~replace
+ | In (InNum n) -> add_input sgn n info ~replace
+ | In (InImpl loc) -> add_impl_input sgn loc info ~replace
+ | Out OutRet -> add_out_ret sgn info ~replace
+ | Out (OutLoc k) -> add_output sgn k info ~replace
let find_input sgn n =
try
@@ -528,7 +528,7 @@ module FctIndex = struct
| _ -> assert false
let add_info_sig_call calls call k e replace =
- let new_sgn old = Signature.add_info old k e replace in
+ let new_sgn old = Signature.add_info old k e ~replace in
let rec add l = match l with
| [] -> [(call, (None, new_sgn Signature.empty))]
| ((call1, (e1, sgn1)) as c1) :: tl ->
@@ -579,7 +579,7 @@ module FctIndex = struct
let hfct = if replace then H.replace else H.add in
match key with
| Key.SigKey k ->
- idx.sgn <- Signature.add_info idx.sgn k e replace
+ idx.sgn <- Signature.add_info idx.sgn k e ~replace
| Key.CallStmt _ -> raise CallStatement (* see add_info_call *)
| Key.SigCallKey (call, k) ->
idx.calls <- add_info_sig_call idx.calls call k e replace
diff --git a/src/plugins/reduc/value2acsl.ml b/src/plugins/reduc/value2acsl.ml
index 310892eec2ba996b86b55c6b9c1243dd25cf145a..dd109f17674031cb0419b42e2e6b74bb14747d0f 100644
--- a/src/plugins/reduc/value2acsl.ml
+++ b/src/plugins/reduc/value2acsl.ml
@@ -116,16 +116,16 @@ let valid_to_predicate_opt ~loc t valid =
Some p
| Base.Unknown (_, _, _) -> None
| Base.Variable { Base.min_alloc = bmn } when Integer.(equal bmn minus_one) ->
- not_yet "Invalid Base.Variable above max_alloc";
+ not_yet ~what:"Invalid Base.Variable above max_alloc";
None
| Base.Variable { Base.min_alloc = bmn; Base.max_alloc = bmx } ->
- not_yet "Invalid Base.Variable above max_alloc";
+ not_yet ~what:"Invalid Base.Variable above max_alloc";
let tbmn = Cil.lconstant ~loc bmn in
let tbmx = Cil.lconstant ~loc bmx in
let p = Logic_const.pvalid_range ~loc (here_lbl, t, tbmn, tbmx) in
Some p
| Base.Invalid ->
- not_yet "Invalid Base";
+ not_yet ~what:"Invalid Base";
None
let base_to_predicate ~loc t (b: Base.t) =
diff --git a/src/plugins/security_slicing/register_gui.ml b/src/plugins/security_slicing/register_gui.ml
index db23ca9f70155577f2ee56cfae29ef1954fdb08b..8af85d491c13ccf280e0600f734419c2a7db15e5 100644
--- a/src/plugins/security_slicing/register_gui.ml
+++ b/src/plugins/security_slicing/register_gui.ml
@@ -47,15 +47,15 @@ let security_highlighter buffer loc ~start ~stop =
| PStmt (_,s) ->
let f = ForwardHighlighterState.get () in
if List.exists (fun k -> k.sid=s.sid) f then begin
- let tag = make_tag buffer"forward" [`BACKGROUND "orange" ] in
+ let tag = make_tag buffer ~name:"forward" [`BACKGROUND "orange" ] in
apply_tag buffer tag start stop end;
let i = IndirectBackwardHighlighterState.get () in
if List.exists (fun k -> k.sid=s.sid) i then begin
- let tag = make_tag buffer"indirect_backward" [`BACKGROUND "cyan" ] in
+ let tag = make_tag buffer ~name:"indirect_backward" [`BACKGROUND "cyan" ] in
apply_tag buffer tag start stop end;
let d = DirectHighlighterState.get () in
if List.exists (fun k -> k.sid=s.sid) d then begin
- let tag = make_tag buffer"direct" [`BACKGROUND "green" ] in
+ let tag = make_tag buffer ~name:"direct" [`BACKGROUND "green" ] in
apply_tag buffer tag start stop end
| PStmtStart _
| PExp _ | PVDecl _ | PTermLval _ | PLval _ | PGlobal _ | PIP _ -> ()
diff --git a/src/plugins/slicing/fct_slice.ml b/src/plugins/slicing/fct_slice.ml
index bcd4330616f84dbb87001b978dbde09babe5f750..b470412386a2539a15b5fd3c3b3fb857fa5de024 100644
--- a/src/plugins/slicing/fct_slice.ml
+++ b/src/plugins/slicing/fct_slice.ml
@@ -202,7 +202,7 @@ end = struct
end;
let _ff, call = call_id in
let new_call_info = to_call in
- PdgIndex.FctIndex.add_info_call ff_marks call new_call_info true
+ PdgIndex.FctIndex.add_info_call ff_marks call new_call_info ~replace:true
end
end
diff --git a/src/plugins/slicing/register.ml b/src/plugins/slicing/register.ml
index 3f6f79579a61dad3f1fcccb13c21c541c4552843..7490aa7e68f2ae929c43802469f9bfafa54878fe 100644
--- a/src/plugins/slicing/register.ml
+++ b/src/plugins/slicing/register.ml
@@ -40,7 +40,7 @@ let main () =
let kf_entry, _library = Globals.entry_point () in
SlicingParameters.warning "Adding an extra request on the entry point of function: %a." Kernel_function.pretty kf_entry;
let set = Api.Select.empty_selects in
- let set = Api.Select.select_func_calls_into set true kf_entry in
+ let set = Api.Select.select_func_calls_into set ~spare:true kf_entry in
Api.Request.add_persistent_selection set
end;
diff --git a/src/plugins/slicing/register_gui.ml b/src/plugins/slicing/register_gui.ml
index b0bf2f895d352ca073f47a5cad931041b7286134..8f9193ea1a7ea15efc07885167102194dd5a1910 100644
--- a/src/plugins/slicing/register_gui.ml
+++ b/src/plugins/slicing/register_gui.ml
@@ -542,8 +542,8 @@ let slicing_panel (main_ui:Design.main_window_extension_points) =
~packing:(table#attach ~left:0 ~top:1) () in
main_ui#help_message b "%s" msg_help_libraries ;
ignore (b#connect#toggled
- (fun () ->
- gui_set_slicing_undef_functions main_ui b#active));
+ ~callback:(fun () ->
+ gui_set_slicing_undef_functions main_ui b#active));
b
in
let level_refresh = Gtk_helper.on_int ~lower:0 ~upper:3
diff --git a/src/plugins/slicing/slicingMarks.ml b/src/plugins/slicing/slicingMarks.ml
index 79f55729c4b16a1210a0dcbd71a30f5246e35556..d32603122c23f6479a4139c1d7f4194016ba25ca 100644
--- a/src/plugins/slicing/slicingMarks.ml
+++ b/src/plugins/slicing/slicingMarks.ml
@@ -229,7 +229,7 @@ module MarkPair = struct
*)
let combine ma mb =
let combine_m ma mb =
- let is_new, mr = Mark.combine ma mb in
+ let is_new, mr = Mark.combine ~old:ma mb in
let m_to_prop = if is_new then mr else Mark.bottom in
mr, m_to_prop
in
diff --git a/src/plugins/slicing/slicingSelect.ml b/src/plugins/slicing/slicingSelect.ml
index 5dd5ffe77a88b254d2093e757904d20701d30afe..25b922ab7f417778765b40c4bc8eeb43efc48ae6 100644
--- a/src/plugins/slicing/slicingSelect.ml
+++ b/src/plugins/slicing/slicingSelect.ml
@@ -122,7 +122,7 @@ let select_stmt_zone kf ?(select=empty_db_select kf) stmt ~before loc mark =
try
let pdg = !Db.Pdg.get kf in
let nodes, undef =
- !Db.Pdg.find_location_nodes_at_stmt pdg stmt before loc in
+ !Db.Pdg.find_location_nodes_at_stmt pdg stmt ~before loc in
let sel = mk_select pdg sel nodes undef mark in
(fvar, sel)
with
diff --git a/src/plugins/sparecode/register.ml b/src/plugins/sparecode/register.ml
index f6f8b9cdb50eef488e2baef3ba68d4854c2ddfc9..f446712652869570f8f842ce390501f68b4e551d 100644
--- a/src/plugins/sparecode/register.ml
+++ b/src/plugins/sparecode/register.ml
@@ -113,7 +113,7 @@ let main () =
if Sparecode_params.Analysis.get () then begin
let select_annot = Sparecode_params.Annot.get () in
let select_slice_pragma = true in
- let new_proj = get select_annot select_slice_pragma in
+ let new_proj = get ~select_annot ~select_slice_pragma in
File.pretty_ast ~prj:new_proj ()
end
else if Sparecode_params.GlobDecl.get () then begin
diff --git a/src/plugins/studia/studia_gui.ml b/src/plugins/studia/studia_gui.ml
index 38628cc3b39acd192263c6cc68e564af0998e573..0abf647801ac257e643f8ca71ad62cb79623fbf5 100644
--- a/src/plugins/studia/studia_gui.ml
+++ b/src/plugins/studia/studia_gui.ml
@@ -270,10 +270,10 @@ let add_item (main_ui:Design.main_window_extension_points) ~uses_value menu name
ignore (item#connect#activate ~callback);
(* Needed for the menu in the Information panel. *)
ignore (item#event#connect#button_press
- (fun evt ->
- if GdkEvent.Button.button evt = 1
- then (callback (); true)
- else false))
+ ~callback:(fun evt ->
+ if GdkEvent.Button.button evt = 1
+ then (callback (); true)
+ else false))
let selector (popup_factory:GMenu.menu GMenu.factory)
(main_ui:Design.main_window_extension_points)
diff --git a/src/plugins/value/domains/cvalue/builtins_memory.ml b/src/plugins/value/domains/cvalue/builtins_memory.ml
index 94ede7e37f8f6621f3f2b3b721781006b90ddea0..78f408543e5c54f7ca237d7fb4d38ebe5200af2f 100644
--- a/src/plugins/value/domains/cvalue/builtins_memory.ml
+++ b/src/plugins/value/domains/cvalue/builtins_memory.ml
@@ -175,7 +175,10 @@ let frama_c_memcpy state actuals =
to be copied, we use a more precise method (see do_size below).
However, in all cases, those locations are used to compute the
read and written bits. *)
- let range = Ival.inject_interval (Some Int.zero) diff Int.zero char_bits in
+ let range =
+ Ival.inject_interval ~min:(Some Int.zero) ~max:diff
+ ~rem:Int.zero ~modu:char_bits
+ in
let size_char = Int_Base.inject char_bits in
let loc_src = make_loc (Location_Bits.shift range src) size_char in
let loc_dst = make_loc (Location_Bits.shift range dst) size_char in
@@ -550,7 +553,7 @@ let frama_c_memset_precise state dst v (exp_size, size) =
let offset_dst_bits = Int.mul offset_dst size_char in
let vi_dst = Base.to_varinfo base_dst in
let mo = Bit_utils.MatchSize size_bits in
- snd (Bit_utils.(find_offset vi_dst.vtype offset_dst_bits mo))
+ snd (Bit_utils.(find_offset vi_dst.vtype ~offset:offset_dst_bits mo))
in
let offsm = memset_typ_offsm typ v in
let dst_loc = Locations.loc_bytes_to_loc_bits dst in
diff --git a/src/plugins/value/domains/cvalue/cvalue_specification.ml b/src/plugins/value/domains/cvalue/cvalue_specification.ml
index acdcec85f51f4c0585c2a325e4072405084fa87c..4336ecdaf401a9f1eca74ec30d9b86e2c376df5c 100644
--- a/src/plugins/value/domains/cvalue/cvalue_specification.ml
+++ b/src/plugins/value/domains/cvalue/cvalue_specification.ml
@@ -34,7 +34,7 @@ let eval_assigns_from pre_state it =
Locations.Zone.bottom
else
try
- let eval_env = Eval_terms.env_assigns pre_state in
+ let eval_env = Eval_terms.env_assigns ~pre:pre_state in
let under, _ =
Eval_terms.eval_tlval_as_zone_under_over
~alarm_mode:Eval_terms.Ignore Locations.Read eval_env term
diff --git a/src/plugins/value/engine/evaluation.ml b/src/plugins/value/engine/evaluation.ml
index 2ec215954a1b392c5dcf92819b5be023f9b22783..aaef33f5418aaa61710b7e891c1916d054a622cb 100644
--- a/src/plugins/value/engine/evaluation.ml
+++ b/src/plugins/value/engine/evaluation.ml
@@ -1405,7 +1405,8 @@ module Make
let context = fast_eval_context state in
fst (eval_offset context ~reduce_valid_index:true typ_pointed remaining)
>>- fun (rem, _, _) ->
- Loc.backward_index typ_pointed v rem loc_offset >>- fun (v', rem') ->
+ Loc.backward_index typ_pointed ~index:v ~remaining:rem loc_offset >>-
+ fun (v', rem') ->
let reduced_v = if Value.is_included v v' then None else Some v' in
backward_eval fuel state exp reduced_v >>- fun _ ->
backward_offset fuel state typ_pointed remaining rem'
diff --git a/src/plugins/value/engine/subdivided_evaluation.ml b/src/plugins/value/engine/subdivided_evaluation.ml
index 7b4a86c43e50b81f85e7f6873ac486510c29390f..85f224d50c2a15140f137749dffe9691d9519cfc 100644
--- a/src/plugins/value/engine/subdivided_evaluation.ml
+++ b/src/plugins/value/engine/subdivided_evaluation.ml
@@ -241,7 +241,7 @@ let has_smaller_max_bound = compare_bound Ival.has_smaller_max_bound
let subdivide size cvalue =
try
let ival = Cvalue.V.project_ival cvalue in
- let ival1, ival2 = Ival.subdivide size ival in
+ let ival1, ival2 = Ival.subdivide ~size ival in
Cvalue.V.inject_ival ival1, Cvalue.V.inject_ival ival2
with Cvalue.V.Not_based_on_null -> assert false
diff --git a/src/plugins/value/engine/transfer_specification.ml b/src/plugins/value/engine/transfer_specification.ml
index 34ee085634c9a09253a35992aced84d4dcd8207f..5e7c9fe748d405df493353f325fd917ba656778d 100644
--- a/src/plugins/value/engine/transfer_specification.ml
+++ b/src/plugins/value/engine/transfer_specification.ml
@@ -238,7 +238,8 @@ module Make
let set_ploc = Location.set Main_locations.PLoc.key
let set_location loc = set_ploc (Main_locations.PLoc.make loc)
- let make_env state = Eval_terms.env_assigns (Domain.get_cvalue_or_top state)
+ let make_env state =
+ Eval_terms.env_assigns ~pre:(Domain.get_cvalue_or_top state)
(* Evaluates the location affected by an assigns, allocates, frees or \from
clause. Returns None if the clause cannot be interpreted. *)
diff --git a/src/plugins/value/gui_files/gui_callstacks_manager.ml b/src/plugins/value/gui_files/gui_callstacks_manager.ml
index efb1b7fc3a952749151e6e627e57946c74c0ed48..c395857193f414fcbda684681b6812909cabaf50 100644
--- a/src/plugins/value/gui_files/gui_callstacks_manager.ml
+++ b/src/plugins/value/gui_files/gui_callstacks_manager.ml
@@ -338,7 +338,7 @@ module Make (Input: Input) = struct
column#set_visible true
end;
in
- ignore (show#connect#activate callback_show_hide);
+ ignore (show#connect#activate ~callback:callback_show_hide);
(!!menu)#add (show :> GMenu.menu_item);
with Not_found -> ()
in
@@ -368,7 +368,7 @@ module Make (Input: Input) = struct
end
in
match get_column_header_button col with
- | None -> ignore (col#connect#clicked pop_menu) (* TODO: warn *)
+ | None -> ignore (col#connect#clicked ~callback:pop_menu) (* TODO: warn *)
| Some button ->
(* Connect the callback to a right-click *)
let callback evt =
@@ -547,12 +547,12 @@ module Make (Input: Input) = struct
) model.columns_type;
callback_remove_filters ();
in
- ignore (remove#connect#activate callback_remove);
+ ignore (remove#connect#activate ~callback:callback_remove);
if has_filters then begin
let txt_unfilter = "Remove filters on this column" in
let unfilter = GMenu.menu_item ~label:txt_unfilter () in
(!!menu)#add unfilter;
- ignore (unfilter#connect#activate callback_remove_filters);
+ ignore (unfilter#connect#activate ~callback:callback_remove_filters);
end;
in
let aux_expr_column (col: GTree.view_column) coltype txt tip =
@@ -606,7 +606,8 @@ module Make (Input: Input) = struct
if Option.is_some model.focused_rev_callstacks then begin
let unfocus = GMenu.menu_item ~label:"Unfocus callstack(s)" () in
(!!menu)#add unfocus;
- ignore (unfocus#connect#activate (callback_focus_unfocus None icon))
+ ignore (unfocus#connect#activate
+ ~callback:(callback_focus_unfocus None icon))
end;
in
(* Add 'Focus on all displayed callstacks' to menu *)
@@ -623,7 +624,7 @@ module Make (Input: Input) = struct
displayed callstacks" () in
(!!menu)#add focus_all;
ignore (focus_all#connect#activate
- (callback_focus_unfocus (Some callstacks) icon));
+ ~callback:(callback_focus_unfocus (Some callstacks) icon));
in
let tip_callstack = "Callstacks at which the selection was analyzed" in
let icon_callstack =
@@ -692,9 +693,9 @@ module Make (Input: Input) = struct
menu#add (GMenu.separator_item ());
menu#add equal;
menu#add different;
- ignore (copy#connect#activate callback_copy);
- ignore (equal#connect#activate (callback_only_except true));
- ignore (different#connect#activate (callback_only_except false));
+ ignore (copy#connect#activate ~callback:callback_copy);
+ ignore (equal#connect#activate ~callback:(callback_only_except true));
+ ignore (different#connect#activate ~callback:(callback_only_except false));
(* add menu items for variables present in the selected expression *)
let callback_display_var vi () =
Option.iter (fun loc ->
@@ -720,7 +721,8 @@ module Make (Input: Input) = struct
Printer.pp_varinfo vi in
let varmenuitem = GMenu.menu_item ~label () in
menu#add varmenuitem;
- ignore (varmenuitem#connect#activate (callback_display_var vi));
+ ignore (varmenuitem#connect#activate
+ ~callback:(callback_display_var vi));
) vars_to_display;
if nb_omitted > 0 then begin
let label =
@@ -790,7 +792,7 @@ module Make (Input: Input) = struct
let focus = GMenu.menu_item ~label:"Focus on this callstack"() in
(!!menu)#add focus;
ignore (focus#connect#activate
- (callback_focus_unfocus (Some [cs]) icon));
+ ~callback:(callback_focus_unfocus (Some [cs]) icon));
| GC_Filtered | GC_Consolidated -> ()
end;
add_focus_all_callstacks menu icon;
diff --git a/src/plugins/value/gui_files/gui_red.ml b/src/plugins/value/gui_files/gui_red.ml
index bb61b22553ce19d86af6018142ab5c767de138fb..d930bc028367175be99711d0e61ed6e44d1fad85 100644
--- a/src/plugins/value/gui_files/gui_red.ml
+++ b/src/plugins/value/gui_files/gui_red.ml
@@ -194,7 +194,7 @@ let make_panel (main_ui:main_window_extension_points) =
(* Fill the table when it is created. We are probably missing a call to
'reset' once the saved state is loaded through -load... *)
let (_:GtkSignal.id) =
- w.widget#coerce#misc#connect#after#realize (fun () -> fill w)
+ w.widget#coerce#misc#connect#after#realize ~callback:(fun () -> fill w)
in
(* Insert the page in the notebook, then return *)
let n =
diff --git a/src/plugins/value/gui_files/register_gui.ml b/src/plugins/value/gui_files/register_gui.ml
index 467c1cf77127cbfebacb0e1eef9829b1201d595a..fda18017f390f47ab0a3da7bd9929391f795de2a 100644
--- a/src/plugins/value/gui_files/register_gui.ml
+++ b/src/plugins/value/gui_files/register_gui.ml
@@ -142,10 +142,10 @@ let value_panel pack (main_ui:main_ui) =
in
let refresh () = precision_refresh (); slevel_refresh (); main_refresh() in
ignore (run_button#connect#pressed
- (fun () ->
- main_ui#protect ~cancelable:true
- (fun () -> refresh (); Analysis.compute (); main_ui#reset ());
- ));
+ ~callback:(fun () ->
+ main_ui#protect ~cancelable:true
+ (fun () -> refresh (); Analysis.compute (); main_ui#reset ());
+ ));
pack box;
"Eva", box#coerce, Some refresh
@@ -185,7 +185,8 @@ let active_highlighter buffer localizable ~start ~stop =
end
else
let dead_code_area =
- make_tag buffer "deadcode" [`BACKGROUND "tomato";`STYLE `ITALIC]
+ make_tag buffer ~name:"deadcode"
+ [`BACKGROUND "tomato";`STYLE `ITALIC]
in
apply_tag buffer dead_code_area start stop
end
diff --git a/src/plugins/value/legacy/eval_terms.ml b/src/plugins/value/legacy/eval_terms.ml
index fcde70a2619627f5755831a2d84a45899c6a178d..f67de28e246188d45b482be494873e72e6800d98 100644
--- a/src/plugins/value/legacy/eval_terms.ml
+++ b/src/plugins/value/legacy/eval_terms.ml
@@ -831,7 +831,7 @@ let eval_logic_charchr builtin env s c ldeps_s ldeps_c =
let eval_logic_memchr_off builtin env s c n =
let minus_one = Cvalue.V.inject_int Integer.minus_one in
let positive = Cvalue.V.inject_ival Ival.positive_integers in
- let pred_n = Cvalue.V.add_untyped Int_Base.one n.eover minus_one in
+ let pred_n = Cvalue.V.add_untyped ~factor:Int_Base.one n.eover minus_one in
let n_pos = Cvalue.V.narrow positive pred_n in
let eover =
if Cvalue.V.is_bottom n_pos then minus_one else
diff --git a/src/plugins/value/parameters.ml b/src/plugins/value/parameters.ml
index a42796de51ee8c5bc7181c0212a2aa59ec62672f..d09607a544dc82f0a5f7f3585eb2709ff97a6e25 100644
--- a/src/plugins/value/parameters.ml
+++ b/src/plugins/value/parameters.ml
@@ -162,7 +162,7 @@ let register_domain ~name ~descr =
create_domain_option name;
domains_ref := (name, descr) :: !domains_ref;
Cmdline.replace_option_help
- Domains.option_name "eva" domains (domains_help ())
+ Domains.option_name ~plugin:"eva" ~group:domains (domains_help ())
(* Checks that a domain has been registered. *)
let check_domain option_name domain =
@@ -276,7 +276,7 @@ module Numerors_Real_Size =
"Set <n> as the significand size of the MPFR representation \
of reals used by the numerors domain (defaults to 128)"
end)
-let () = Numerors_Real_Size.set_range 1 max_int
+let () = Numerors_Real_Size.set_range ~min:1 ~max:max_int
let () = add_precision_dep Numerors_Real_Size.parameter
let () = Parameter_customize.set_group domains
@@ -490,7 +490,7 @@ module AutomaticContextMaxDepth =
let help = "Use <n> as the depth of the default context for Eva. \
(defaults to 2)"
end)
-let () = AutomaticContextMaxDepth.set_range 0 max_int
+let () = AutomaticContextMaxDepth.set_range ~min:0 ~max:max_int
let () = add_correctness_dep AutomaticContextMaxDepth.parameter
let () = Parameter_customize.set_group initial_context
@@ -618,7 +618,7 @@ module SemanticUnrollingLevel =
The larger n, the more precise and expensive the analysis \
(defaults to 0)"
end)
-let () = SemanticUnrollingLevel.set_range 0 max_int
+let () = SemanticUnrollingLevel.set_range ~min:0 ~max:max_int
let () = add_precision_dep SemanticUnrollingLevel.parameter
let () = Parameter_customize.set_group precision_tuning
@@ -670,7 +670,7 @@ module MinLoopUnroll =
Can be overwritten on a case-by-case basis by loop unroll annotations."
end)
let () = add_precision_dep MinLoopUnroll.parameter
-let () = MinLoopUnroll.set_range 0 max_int
+let () = MinLoopUnroll.set_range ~min:0 ~max:max_int
let () = Parameter_customize.set_group precision_tuning
module AutoLoopUnroll =
@@ -684,7 +684,7 @@ module AutoLoopUnroll =
are completely unrolled."
end)
let () = add_precision_dep AutoLoopUnroll.parameter
-let () = AutoLoopUnroll.set_range 0 max_int
+let () = AutoLoopUnroll.set_range ~min:0 ~max:max_int
let () = Parameter_customize.set_group precision_tuning
module DefaultLoopUnroll =
@@ -698,7 +698,7 @@ module DefaultLoopUnroll =
not explicitly provide a limit."
end)
let () = add_precision_dep DefaultLoopUnroll.parameter
-let () = DefaultLoopUnroll.set_range 0 max_int
+let () = DefaultLoopUnroll.set_range ~min:0 ~max:max_int
let () = Parameter_customize.set_group precision_tuning
module HistoryPartitioning =
@@ -712,7 +712,7 @@ module HistoryPartitioning =
traces are also distinct. (A value of 0 deactivates this feature)"
end)
let () = add_precision_dep HistoryPartitioning.parameter
-let () = HistoryPartitioning.set_range 0 max_int
+let () = HistoryPartitioning.set_range ~min:0 ~max:max_int
let () = Parameter_customize.set_group precision_tuning
module ValuePartitioning =
@@ -739,7 +739,7 @@ module SplitLimit =
enumerating more than N cases"
end)
let () = add_precision_dep SplitLimit.parameter
-let () = SplitLimit.set_range 0 max_int
+let () = SplitLimit.set_range ~min:0 ~max:max_int
let () = Parameter_customize.set_group precision_tuning
module InterproceduralSplits =
@@ -826,7 +826,7 @@ module ILevel =
end)
let () = add_precision_dep ILevel.parameter
let () = ILevel.add_update_hook (fun _ i -> Int_set.set_small_cardinal i)
-let () = ILevel.set_range 2 max_int
+let () = ILevel.set_range ~min:2 ~max:max_int
let builtins = ref Datatype.String.Set.empty
let register_builtin name = builtins := Datatype.String.Set.add name !builtins
@@ -903,7 +903,7 @@ module LinearLevel =
appears multiple times, by splitting its value at most n times. \
Defaults to 0."
end)
-let () = LinearLevel.set_range 0 max_int
+let () = LinearLevel.set_range ~min:0 ~max:max_int
let () = add_precision_dep LinearLevel.parameter
let () = Parameter_customize.set_group precision_tuning
@@ -985,7 +985,7 @@ module ArrayPrecisionLevel =
Array accesses are precise as long as the interval for the \
index contains less than n values. (defaults to 200)"
end)
-let () = ArrayPrecisionLevel.set_range 0 max_int
+let () = ArrayPrecisionLevel.set_range ~min:0 ~max:max_int
let () = add_precision_dep ArrayPrecisionLevel.parameter
let () = ArrayPrecisionLevel.add_update_hook
(fun _ v -> Offsetmap.set_plevel v)
@@ -1092,7 +1092,7 @@ module StopAtNthAlarm =
let arg_name = "n"
let help = "Abort the analysis when the nth alarm is emitted."
end)
-let () = StopAtNthAlarm.set_range 0 max_int
+let () = StopAtNthAlarm.set_range ~min:0 ~max:max_int
(* -------------------------------------------------------------------------- *)
(* --- Ugliness required for correctness --- *)
@@ -1143,7 +1143,7 @@ module OracleDepth =
let default = 2
let arg_name = ""
end)
-let () = OracleDepth.set_range 0 max_int
+let () = OracleDepth.set_range ~min:0 ~max:max_int
let () = add_precision_dep OracleDepth.parameter
let () = Parameter_customize.set_group precision_tuning
@@ -1156,7 +1156,7 @@ module ReductionDepth =
let default = 4
let arg_name = ""
end)
-let () = ReductionDepth.set_range 0 max_int
+let () = ReductionDepth.set_range ~min:0 ~max:max_int
let () = add_precision_dep ReductionDepth.parameter
@@ -1220,7 +1220,7 @@ module MallocLevel =
let help = "Set to [m] the number of precise dynamic allocations \
besides the initial one, for each callstack (defaults to 0)"
end)
-let () = MallocLevel.set_range 0 max_int
+let () = MallocLevel.set_range ~min:0 ~max:max_int
let () = add_precision_dep MallocLevel.parameter
(* -------------------------------------------------------------------------- *)
@@ -1310,7 +1310,7 @@ module Precision =
from 0 (fastest but rather imprecise analysis) \
to 11 (accurate but potentially slow analysis)."
end)
-let () = Precision.set_range (-1) 11
+let () = Precision.set_range ~min:(-1) ~max:11
let () = add_precision_dep Precision.parameter
(* Sets a parameter [P] to [t], unless it has already been set by any other
diff --git a/src/plugins/value/register.ml b/src/plugins/value/register.ml
index 31e30531c845bf5f415d93ba3a835d98b78d2fa1..c57f8f46daae27c684ebb342d69dd314407365f0 100644
--- a/src/plugins/value/register.ml
+++ b/src/plugins/value/register.ml
@@ -67,7 +67,7 @@ let assigns_inputs_to_zone state assigns =
| Writes l -> List.fold_left treat_asgn Zone.bottom l
let assigns_outputs_aux ~eval ~bot ~top ~join state ~result assigns =
- let env = Eval_terms.env_post_f state state result () in
+ let env = Eval_terms.env_post_f ~pre:state ~post:state ~result () in
let treat_asgn acc ({it_content = out},_) =
if Logic_utils.is_result out && result = None
then acc
diff --git a/src/plugins/value/utils/eval_typ.ml b/src/plugins/value/utils/eval_typ.ml
index 3305dd9bf332ae8031533adec71f01c54956a77c..51facb7e4e7a70a71aaa631e5a56bfc20c946ae9 100644
--- a/src/plugins/value/utils/eval_typ.ml
+++ b/src/plugins/value/utils/eval_typ.ml
@@ -125,7 +125,7 @@ let compatible_functions typ_pointer ?args kfs =
let check_pointer (list, alarm) kf =
let typ = Kernel_function.get_type kf in
if Cil.isFunctionType typ then
- match is_compatible_function typ_pointer typ with
+ match is_compatible_function ~typ_pointed:typ_pointer ~typ_fun:typ with
| Compatible -> kf :: list, alarm
| Incompatible_but_accepted -> kf :: list, true
| Incompatible -> list, true
diff --git a/src/plugins/value/values/cvalue_backward.ml b/src/plugins/value/values/cvalue_backward.ml
index 6269187a45848c7e5da7c738261a26e42d661edb..1915751da68a9f234270d8c834e33a255f65a107 100644
--- a/src/plugins/value/values/cvalue_backward.ml
+++ b/src/plugins/value/values/cvalue_backward.ml
@@ -71,12 +71,13 @@ let backward_relation typ ~positive op =
(* res == v1 +/- v2 *)
let backward_add_int typ ~res_value ~v1 ~v2 pos =
(* v1 == res -/+ v2 *)
- let v1' = V.add_untyped Int_Base.(if pos then minus_one else one) res_value v2
+ let v1' =
+ V.add_untyped ~factor:Int_Base.(if pos then minus_one else one) res_value v2
(* +/- v2 == res - v1 *)
and v2' =
if pos
- then V.add_untyped Int_Base.minus_one res_value v1
- else V.add_untyped Int_Base.minus_one v1 res_value
+ then V.add_untyped ~factor:Int_Base.minus_one res_value v1
+ else V.add_untyped ~factor:Int_Base.minus_one v1 res_value
in
(* TODO: no need for reinterpret if no overflow. *)
Some (Cvalue_forward.reinterpret typ v1',
@@ -270,8 +271,8 @@ let backward_binop ~typ_res ~res_value ~typ_e1 v1 binop v2 =
| MinusPP, TInt _ ->
let factor = Bit_utils.osizeof_pointed typ_e1 in
- let v1 = V.add_untyped factor v2 res_value
- and v2 = V.add_untyped (Int_Base.neg factor) v1 res_value in
+ let v1 = V.add_untyped ~factor v2 res_value
+ and v2 = V.add_untyped ~factor:(Int_Base.neg factor) v1 res_value in
Some (v1, v2)
(* comparison operators *)
@@ -300,7 +301,7 @@ let backward_binop ~typ_res ~res_value ~typ_e1 v1 binop v2 =
(* the following equality only holds when v1 does not change sign, which
is why we split its range: v1 == (v1 / v2) * v2 + res *)
let v1' v1 res =
- V.add_untyped Int_Base.one res (V.mul (V.div v1 v2) v2)
+ V.add_untyped ~factor:Int_Base.one res (V.mul (V.div v1 v2) v2)
in
let ge = Abstract_interp.Comp.Ge and le = Abstract_interp.Comp.Le in
let v1_pos = V.backward_comp_int_left ge v1 V.singleton_zero in
@@ -318,7 +319,7 @@ let backward_binop ~typ_res ~res_value ~typ_e1 v1 binop v2 =
else
(* v2 = (v1 - res) / (v1 / v2) *)
V.div
- (V.add_untyped Int_Base.minus_one v1 res_value)
+ (V.add_untyped ~factor:Int_Base.minus_one v1 res_value)
(V.div v1 v2)
in
Some (v1', v2')
diff --git a/src/plugins/value/values/cvalue_forward.ml b/src/plugins/value/values/cvalue_forward.ml
index cfc6e7b31d90d7157a81e25736aac13f8d64b0e2..b1a91b8758b3ce1425776f7ae3cec963bcca1c49 100644
--- a/src/plugins/value/values/cvalue_forward.ml
+++ b/src/plugins/value/values/cvalue_forward.ml
@@ -359,7 +359,7 @@ let forward_minus_pp ~typ ev1 ev2 =
in
if not (Parameters.WarnPointerSubstraction.get ()) then
(* Generate garbled mix if the two pointers disagree on their base *)
- let minus_val = V.add_untyped Int_Base.minus_one ev1 ev2 in
+ let minus_val = V.add_untyped ~factor:Int_Base.minus_one ev1 ev2 in
try
V.inject_ival (conv (Cvalue.V.project_ival minus_val))
with Cvalue.V.Not_based_on_null ->
@@ -376,12 +376,12 @@ let forward_minus_pp ~typ ev1 ev2 =
The function must behave as if it was acting on unbounded integers *)
let forward_binop_int ~typ ev1 op ev2 =
match op with
- | PlusPI -> V.add_untyped (Bit_utils.osizeof_pointed typ) ev1 ev2
+ | PlusPI -> V.add_untyped ~factor:(Bit_utils.osizeof_pointed typ) ev1 ev2
| MinusPI ->
let int_base = Int_Base.neg (Bit_utils.osizeof_pointed typ) in
- V.add_untyped int_base ev1 ev2
- | PlusA -> V.add_untyped (Int_Base.one) ev1 ev2
- | MinusA -> V.add_untyped Int_Base.minus_one ev1 ev2
+ V.add_untyped ~factor:int_base ev1 ev2
+ | PlusA -> V.add_untyped ~factor:(Int_Base.one) ev1 ev2
+ | MinusA -> V.add_untyped ~factor:Int_Base.minus_one ev1 ev2
| MinusPP -> forward_minus_pp ~typ ev1 ev2
| Mod -> V.c_rem ev1 ev2
| Div -> V.div ev1 ev2
diff --git a/src/plugins/value/values/numerors/numerors_arithmetics.ml b/src/plugins/value/values/numerors/numerors_arithmetics.ml
index 9cc89818508e2d92bbaae8d80bb15542d67969a5..a725200e9f14ac35e69270799a002763bd2430b1 100644
--- a/src/plugins/value/values/numerors/numerors_arithmetics.ml
+++ b/src/plugins/value/values/numerors/numerors_arithmetics.ml
@@ -134,7 +134,8 @@ let two = F.of_int 2
let change_prec prec t =
let approx = I.change_prec prec t.approx in
if I.is_nan t.approx then
- { t with approx ; abs_err = I.top P.Real ; rel_err = I.top P.Real }
+ { t with approx ; abs_err = I.top ~prec:P.Real ;
+ rel_err = I.top ~prec:P.Real }
else
let epsilon = F.machine_epsilon prec in
let abs_err =
@@ -210,11 +211,11 @@ end = struct
let ufp = F.pow_int two (I.get_max_exponent itv) in
let t = F.mul ufp epsilon in
I.of_numerors_floats (F.neg t, t)
- | None -> I.zero P.Real
+ | None -> I.zero ~prec:P.Real
in
let delta_part = match delta_opt with
| Some delta -> I.of_numerors_floats (F.neg delta, delta)
- | None -> I.zero P.Real
+ | None -> I.zero ~prec:P.Real
in
let res = I.join epsilon_part delta_part in
if not (I.eq old_itv itv) then I.add_nan res else res
@@ -238,14 +239,14 @@ end = struct
in
let t = F.mul max_ufp epsilon in
I.of_numerors_floats (F.neg t, t)
- | None -> I.zero P.Real
+ | None -> I.zero ~prec:P.Real
in
let delta_part = match delta_opt with
| Some delta ->
let one = I.of_ints ~prec:P.Real (-1, 1) in
let r = I.div (I.of_numerors_floats (F.neg delta, delta)) itv in
non_bottom_narrow r one
- | None -> I.zero P.Real
+ | None -> I.zero ~prec:P.Real
in
let res = I.join epsilon_part delta_part in
if not (I.eq old_itv itv) then I.add_nan res else res
@@ -576,7 +577,7 @@ module Rel_Err : Arithmetic with
let sqrt v ~exact ~abs_err =
let p = I.prec v.approx in
let naive = I.div abs_err exact in
- let g = I.add (Elementary.rel p (I.sqrt v.approx)) one in
+ let g = I.add (Elementary.rel ~prec:p (I.sqrt v.approx)) one in
let err = I.sub (I.mul (I.sqrt (I.add v.rel_err one)) g) one in
narrow_errors naive err
diff --git a/src/plugins/value/values/numerors/numerors_interval.ml b/src/plugins/value/values/numerors/numerors_interval.ml
index 4af5e4e9bd86fa93b3dea1b93cdf5b472a99282d..ded1e62a5ae622753371d86bda765221ad9f8ca4 100644
--- a/src/plugins/value/values/numerors/numerors_interval.ml
+++ b/src/plugins/value/values/numerors/numerors_interval.ml
@@ -298,9 +298,9 @@ let monotonic ~prec (op : operator) a b =
let treat_nan x y =
nan := true ;
if F.is_inf x && not (F.eq b1 e1) then
- add @@ op ~prec (F.apply_sign x (F.of_int ~prec 1)) y ;
+ add @@ op ~prec (F.apply_sign ~src:x ~dst:(F.of_int ~prec 1)) y ;
if F.is_inf y && not (F.eq b2 e2) then
- add @@ op ~prec x (F.apply_sign y (F.of_int ~prec 1)) ;
+ add @@ op ~prec x (F.apply_sign ~src:y ~dst:(F.of_int ~prec 1)) ;
in
let op rnd x y =
let r = op ~rnd ~prec x y in
@@ -437,20 +437,20 @@ let backward_gt ?(prec = Precisions.Real) y x =
let finite_values ~prec = function
| NaN _ -> None
| I (x, y, _) ->
- let min = F.max (F.maximal_neg_float prec) x in
- let max = F.min (F.maximal_pos_float prec) y in
+ let min = F.max (F.maximal_neg_float ~prec) x in
+ let max = F.min (F.maximal_pos_float ~prec) y in
if max < min then None else Some (min, max)
let backward_op (op : operator) fnan ?(prec = Precisions.Real) value result () =
if contains_infinity result || (contains_nan value && contains_nan result)
- then `Value (top prec)
+ then `Value (top ~prec)
else
let reduced_for_nan =
if contains_nan result
then `Value (fnan value)
else `Bottom
and reduced_for_finite =
- match finite_values prec result, finite_values prec value with
+ match finite_values ~prec result, finite_values ~prec value with
| None, _ | _, None -> `Bottom
| Some (xres, yres), Some (xval, yval) ->
if Precisions.eq prec Precisions.Real then
diff --git a/src/plugins/value/values/numerors/numerors_value.ml b/src/plugins/value/values/numerors/numerors_value.ml
index 2efe4c08c46e03431beb220d3288289dd4a6f5d3..c90b9c1a67af2e72c05da6d7bed6f9b53c4f8e7c 100644
--- a/src/plugins/value/values/numerors/numerors_value.ml
+++ b/src/plugins/value/values/numerors/numerors_value.ml
@@ -163,10 +163,10 @@ let constant _ = function
let prec = Precisions.of_fkind fkind in
let exact =
match opt with
- | Some s -> I.of_strings Precisions.Real (s, s)
- | None -> I.of_floats Precisions.Real (r, r)
+ | Some s -> I.of_strings ~prec:Precisions.Real (s, s)
+ | None -> I.of_floats ~prec:Precisions.Real (r, r)
in
- let approx = I.of_floats_without_rounding prec (r, r) in
+ let approx = I.of_floats_without_rounding ~prec (r, r) in
let abs_err = I.sub approx exact in
let rel_err =
if I.is_zero exact then I.of_floats ~prec:P.Real (0.0, 0.0)
diff --git a/src/plugins/value_types/cvalue.ml b/src/plugins/value_types/cvalue.ml
index 3440bfa9bf199efb33dedb1733b13c27ef40d293..ba493d0e92be6e70a989450823c77722455bc0c5 100644
--- a/src/plugins/value_types/cvalue.ml
+++ b/src/plugins/value_types/cvalue.ml
@@ -192,7 +192,7 @@ module V = struct
let o, ok = conv_offset o in
if o = NoOffset then
let o' = match Cil.unrollType typ_base with
- | TArray _ -> Index (Cil.(zero Cil_builtins.builtinLoc), NoOffset)
+ | TArray _ -> Index (Cil.(zero ~loc:Cil_builtins.builtinLoc), NoOffset)
| TComp (ci, _) -> Field (List.hd (Option.get ci.cfields), NoOffset)
| _ -> raise Bit_utils.NoMatchingOffset
in o', ok
@@ -683,7 +683,7 @@ module V = struct
| Map m ->
let card =
M.fold (fun _ v card ->
- Int.add card (Ival.cardinal_estimate v size)
+ Int.add card (Ival.cardinal_estimate v ~size)
) m Int.zero
in
Int.min card (Int.two_power size)
diff --git a/src/plugins/wp/GuiNavigator.ml b/src/plugins/wp/GuiNavigator.ml
index 06ce124947dc8a45e37179a91d5d5cafed9cf9a7..e39380a3381dd45a5217b3267096eeeaf31fb888 100644
--- a/src/plugins/wp/GuiNavigator.ml
+++ b/src/plugins/wp/GuiNavigator.ml
@@ -509,7 +509,7 @@ let make (main : main_window_extension_points) =
panel#pack ~expand:false focusbar#coerce ;
panel#pack ~expand:true ~fill:true book#coerce ;
let tab_label = (GMisc.label ~text:"WP Goals" ())#coerce in
- ignore (panel#misc#connect#after#realize behavior#reload) ;
+ ignore (panel#misc#connect#after#realize ~callback:behavior#reload) ;
ignore (main#lower_notebook#append_page ~tab_label panel#coerce) ;
main#register_source_highlighter source#highlight ;
main#register_source_selector popup#register ;
diff --git a/src/plugins/wp/GuiPanel.ml b/src/plugins/wp/GuiPanel.ml
index 0752478bedb2e095a2cbca187e890f31b52a5457..b434fe801aff2d135842d18e398e55c50ea63c2b 100644
--- a/src/plugins/wp/GuiPanel.ml
+++ b/src/plugins/wp/GuiPanel.ml
@@ -278,7 +278,7 @@ let wp_panel
let cancel = GButton.button ~packing:(pbox#pack ~expand:false) ~stock:`STOP () in
cancel#misc#set_sensitive false ;
let server = ProverTask.server () in
- ignore (cancel#connect#released (fun () -> Task.cancel_all server)) ;
+ ignore (cancel#connect#released ~callback:(fun () -> Task.cancel_all server));
let inactive = (0,0) in
let state = ref inactive in
Task.on_server_activity server
diff --git a/src/plugins/wp/GuiSource.ml b/src/plugins/wp/GuiSource.ml
index d7705f05633d9e5f80273fbdef7f57a4117ef5a2..79bfa4eb70814131d7b24302f180cba755c1b54f 100644
--- a/src/plugins/wp/GuiSource.ml
+++ b/src/plugins/wp/GuiSource.ml
@@ -154,7 +154,7 @@ module PATH = Stmt.Set
module DEPS = Property.Set
let apply_tag name attr buffer start stop =
- let tg = Gtk_helper.make_tag buffer name attr in
+ let tg = Gtk_helper.make_tag buffer ~name attr in
Gtk_helper.apply_tag buffer tg start stop
let apply_goal = apply_tag "wp.goal" [`BACKGROUND "lightblue"]
diff --git a/src/plugins/wp/Lang.ml b/src/plugins/wp/Lang.ml
index 1767be3aff4aee53582f620a4620bd9afe79f842..52c49b7561c3b043368ee3305b791f4fb25a2d32 100644
--- a/src/plugins/wp/Lang.ml
+++ b/src/plugins/wp/Lang.ml
@@ -293,7 +293,7 @@ let mem_builtin_type ~name =
try ignore (find_builtin name) ; true
with Not_found -> false
-let is_builtin lt = mem_builtin_type lt.lt_name
+let is_builtin lt = mem_builtin_type ~name:lt.lt_name
let is_builtin_type ~name = function
| Data(Mtype m,_) ->
diff --git a/src/plugins/wp/LogicUsage.ml b/src/plugins/wp/LogicUsage.ml
index dda6a165c049aab746b410bb8e51ac6529125c30..f0adcba3d16e439c27a3156fffe50c62f1282f7f 100644
--- a/src/plugins/wp/LogicUsage.ml
+++ b/src/plugins/wp/LogicUsage.ml
@@ -370,7 +370,7 @@ class visitor =
| Daxiomatic _ ->
begin
let pf = database.proofcontext in
- let ax = axiomatic_of_global pf global in
+ let ax = axiomatic_of_global ~context:pf global in
register_axiomatic database ax ;
axiomatic <- Some ax ;
DoChildrenPost
@@ -404,7 +404,7 @@ class visitor =
(* --- LEMMAS --- *)
| Dlemma _ ->
- let lem = lemma_of_global database.proofcontext global in
+ let lem = lemma_of_global ~context:database.proofcontext global in
register_lemma database self#section lem ;
if Logic_utils.use_predicate lem.lem_predicate.tp_kind then
database.proofcontext <- lem :: database.proofcontext ;
diff --git a/src/plugins/wp/MemTyped.ml b/src/plugins/wp/MemTyped.ml
index c33350d38663a2a360243a6f1ec37251638865d9..50a414265a5c5538e3659b30fba7ca427a996905 100644
--- a/src/plugins/wp/MemTyped.ml
+++ b/src/plugins/wp/MemTyped.ml
@@ -809,26 +809,26 @@ struct
| Garbled , _ | _ , Garbled -> Mismatch
| Str(a,n) , Str(b,m) ->
begin
- match compare_slot a b with
+ match compare_slot ~dst:a ~src:b with
| Mismatch -> Mismatch
| Drem a'->
let w1 = a' @ decr_slot a n w1 in
let w2 = decr_slot b m w2 in
- compare w1 w2
+ compare ~dst:w1 ~src:w2
| Srem b' ->
let w1 = decr_slot a n w1 in
let w2 = b' @ decr_slot b m w2 in
- compare w1 w2
+ compare ~dst:w1 ~src:w2
| Equal ->
if n < m then
let w2 = Str(a,Int64.sub m n)::w2 in
- compare w1 w2
+ compare ~dst:w1 ~src:w2
else if n > m then
let w1 = Str(a,Int64.sub n m)::w1 in
- compare w1 w2
+ compare ~dst:w1 ~src:w2
else
(* n = m *)
- compare w1 w2
+ compare ~dst:w1 ~src:w2
end
| Arr(u,n) , Arr(v,m) ->
begin
@@ -837,21 +837,21 @@ struct
| Drem u' ->
let w1 = u' @ add_array u (Int64.pred n) w1 in
let w2 = add_array v (Int64.pred m) w2 in
- compare w1 w2
+ compare ~dst:w1 ~src:w2
| Srem v' ->
let w1 = add_array u (Int64.pred n) w1 in
let w2 = v' @ add_array v (Int64.pred m) w2 in
- compare w1 w2
+ compare ~dst:w1 ~src:w2
| Equal ->
if n < m then
let w2 = add_array v (Int64.sub m n) w2 in
- compare w1 w2
+ compare ~dst:w1 ~src:w2
else if n > m then
let w1 = add_array u (Int64.sub n m) w1 in
- compare w1 w2
+ compare ~dst:w1 ~src:w2
else
(* n = m *)
- compare w1 w2
+ compare ~dst:w1 ~src:w2
end
| Arr(u,n) , Str _ ->
compare ~dst:((layout u) @ add_array u (Int64.pred n) w1) ~src
@@ -914,7 +914,7 @@ struct
match compare ~dst:(layout dst) ~src with
| Equal | Srem _ -> true
| Mismatch -> false
- | Drem dst -> repeated dst src
+ | Drem dst -> repeated ~dst ~src
let rec pretty fmt = function
| C_pointer ty -> Format.fprintf fmt "%a*" pretty (Ctypes.object_of ty)
diff --git a/src/plugins/wp/ProofEngine.ml b/src/plugins/wp/ProofEngine.ml
index 45de09e0ba836a166a974191ded7a09165a5067a..84c3aa22696a3e6eb4d64eb5f05ad3bae353017e 100644
--- a/src/plugins/wp/ProofEngine.ml
+++ b/src/plugins/wp/ProofEngine.ml
@@ -382,7 +382,7 @@ let anchor tree ?node () =
| None ->
match tree.root with
| Some n -> n
- | None -> mk_root tree
+ | None -> mk_root ~tree
let commit fork =
List.iter (fun (_,wp) -> ignore (Wpo.resolve wp)) fork.Fork.goals ;
diff --git a/src/plugins/wp/ProverWhy3.ml b/src/plugins/wp/ProverWhy3.ml
index 15359c65d6a23326a91f9854ff65b0d826f45650..72fc49e17cb073adcb0e0303ee6af51aa3404b94 100644
--- a/src/plugins/wp/ProverWhy3.ml
+++ b/src/plugins/wp/ProverWhy3.ml
@@ -24,16 +24,16 @@ let dkey = Wp_parameters.register_category "prover"
let dkey_api = Wp_parameters.register_category "why3_api"
let option_file = LogicBuiltins.create_option
- (fun ~driver_dir x -> Filename.concat driver_dir x)
+ ~sanitizer:(fun ~driver_dir x -> Filename.concat driver_dir x)
"why3" "file"
let option_import = LogicBuiltins.create_option
- (fun ~driver_dir:_ x -> x)
+ ~sanitizer:(fun ~driver_dir:_ x -> x)
"why3" "import"
let option_qual =
LogicBuiltins.create_option
- (fun ~driver_dir:_ x -> x)
+ ~sanitizer:(fun ~driver_dir:_ x -> x)
"why3" "qualifier"
let why3_failure msg =
@@ -323,14 +323,14 @@ let rec of_trigger ~cnv t =
with Not_found -> why3_failure "Unbound variable %a" Lang.F.pp_var v
end
| Qed.Engine.TgGet(m,k) ->
- t_app ~cnv ~f:["map"] ~l:"Map" ~p:["get"] [of_trigger cnv m;of_trigger cnv k]
+ t_app ~cnv ~f:["map"] ~l:"Map" ~p:["get"] [of_trigger ~cnv m;of_trigger ~cnv k]
| TgSet(m,k,v) ->
- t_app ~cnv ~f:["map"] ~l:"Map" ~p:["set"] [of_trigger cnv m;of_trigger cnv k;of_trigger cnv v]
+ t_app ~cnv ~f:["map"] ~l:"Map" ~p:["set"] [of_trigger ~cnv m;of_trigger ~cnv k;of_trigger ~cnv v]
| TgFun (f,l) -> begin
match lfun_name f with
| F_call s ->
let ls = Why3.Theory.(ns_find_ls (get_namespace cnv.th) (cut_path s)) in
- Why3.Term.t_app_infer ls (List.map (fun e -> of_trigger cnv e) l)
+ Why3.Term.t_app_infer ls (List.map (fun e -> of_trigger ~cnv e) l)
| _ -> why3_failure "can not convert extented calls in triggers"
end
| TgProp (f,l) ->
@@ -338,7 +338,7 @@ let rec of_trigger ~cnv t =
match lfun_name f with
| F_call s ->
let ls = Why3.Theory.(ns_find_ls (get_namespace cnv.th) (cut_path s)) in
- Why3.Term.t_app_infer ls (List.map (fun e -> of_trigger cnv e) l)
+ Why3.Term.t_app_infer ls (List.map (fun e -> of_trigger ~cnv e) l)
| _ -> why3_failure "can not convert extented calls in triggers"
end
@@ -378,11 +378,11 @@ let rec of_term ~cnv expected t : Why3.Term.term =
coerce ~cnv sort expected $ Literal.const_float ~cnv t repr
| Times(z,t), Int, _ ->
coerce ~cnv sort expected $
- t_app ~cnv ~f:["int"] ~l:"Int" ~p:["infix *"] [Literal.const_int z; of_term cnv sort t]
+ t_app ~cnv ~f:["int"] ~l:"Int" ~p:["infix *"] [Literal.const_int z; of_term ~cnv sort t]
| Times(z,t), Real, _ ->
coerce ~cnv sort expected $
t_app ~cnv ~f:["real"] ~l:"Real" ~p:["infix *"]
- [Literal.const_real ~cnv (Q.of_bigint z); of_term cnv sort t]
+ [Literal.const_real ~cnv (Q.of_bigint z); of_term ~cnv sort t]
| Add l, Int, _ ->
coerce ~cnv sort expected $
t_app_fold ~f:["int"] ~l:"Int" ~p:["infix +"] ~cnv sort l
@@ -440,7 +440,7 @@ let rec of_term ~cnv expected t : Why3.Term.term =
t_app ~cnv ~f:["bool"] ~l:"Bool" ~p:["notb"] [of_term ~cnv expected e]
| Not e, _, Prop ->
let cnv = {cnv with polarity = Cvalues.negate cnv.polarity} in
- Why3.Term.t_not (of_term cnv expected e)
+ Why3.Term.t_not (of_term ~cnv expected e)
| Imply (l,e), _, _ ->
let e = (of_term ~cnv expected) e in
let cnv' = {cnv with polarity = Cvalues.negate cnv.polarity} in
@@ -455,10 +455,10 @@ let rec of_term ~cnv expected t : Why3.Term.term =
| Eq (a,b), _, Prop -> begin
match Lang.F.typeof a with
| Prop | Bool ->
- Why3.Term.t_iff (of_term cnv Prop a) (of_term cnv Prop b)
+ Why3.Term.t_iff (of_term ~cnv Prop a) (of_term ~cnv Prop b)
| tau ->
match List.find (fun spe -> spe.Lang.For_export.for_tau tau) !specific_equalities with
- | spe when cnv.polarity = `Positive -> of_term cnv expected (spe.mk_new_eq a b)
+ | spe when cnv.polarity = `Positive -> of_term ~cnv expected (spe.mk_new_eq a b)
| exception Not_found -> Why3.Term.t_equ (of_term' cnv a) (of_term' cnv b)
| _ -> Why3.Term.t_equ (of_term' cnv a) (of_term' cnv b)
end
@@ -466,11 +466,11 @@ let rec of_term ~cnv expected t : Why3.Term.term =
begin
match Lang.F.typeof a with
| Prop | Bool ->
- Why3.Term.t_not (Why3.Term.t_iff (of_term cnv Prop a) (of_term cnv Prop b))
+ Why3.Term.t_not (Why3.Term.t_iff (of_term ~cnv Prop a) (of_term ~cnv Prop b))
| tau ->
match List.find (fun spe -> spe.Lang.For_export.for_tau tau) !specific_equalities with
| spe when cnv.polarity = `Negative ->
- Why3.Term.t_not (of_term cnv expected (spe.mk_new_eq a b))
+ Why3.Term.t_not (of_term ~cnv expected (spe.mk_new_eq a b))
| exception Not_found -> Why3.Term.t_neq (of_term' cnv a) (of_term' cnv b)
| _ -> Why3.Term.t_neq (of_term' cnv a) (of_term' cnv b)
end
@@ -480,21 +480,21 @@ let rec of_term ~cnv expected t : Why3.Term.term =
t_app ~cnv ~f:(wp_why3_lib "qed") ~l:"Qed" ~p:["neqb"] [of_term' cnv a; of_term' cnv b]
| If(a,b,c), _, _ ->
let cnv' = {cnv with polarity = `NoPolarity} in
- Why3.Term.t_if (of_term cnv' Prop a) (of_term cnv expected b) (of_term cnv expected c)
+ Why3.Term.t_if (of_term ~cnv:cnv' Prop a) (of_term ~cnv expected b) (of_term ~cnv expected c)
| Aget(m,k), _, _ -> begin
coerce ~cnv sort expected $
let mtau = Lang.F.typeof m in
let ksort = match mtau with
| Array(ksort,_) -> ksort
| _ -> assert false (** absurd: by qed typing *)in
- t_app ~cnv ~f:["map"] ~l:"Map" ~p:["get"] [of_term cnv mtau m;of_term cnv ksort k]
+ t_app ~cnv ~f:["map"] ~l:"Map" ~p:["get"] [of_term ~cnv mtau m;of_term ~cnv ksort k]
end
| Aset(m,k,v), Array(ksort,vsort), _ ->
coerce ~cnv sort expected $
- t_app ~cnv ~f:["map"] ~l:"Map" ~p:["set"] [of_term cnv sort m;of_term cnv ksort k;of_term cnv vsort v]
+ t_app ~cnv ~f:["map"] ~l:"Map" ~p:["set"] [of_term ~cnv sort m;of_term ~cnv ksort k;of_term ~cnv vsort v]
| Acst(_,v), Array(_,vsort), _ ->
coerce ~cnv sort expected $
- t_app' ~cnv ~f:["map"] ~l:"Const" ~p:["const"] [of_term cnv vsort v] (of_tau cnv sort)
+ t_app' ~cnv ~f:["map"] ~l:"Const" ~p:["const"] [of_term ~cnv vsort v] (of_tau ~cnv sort)
(* Generic *)
| Fun (f,l), _, _ -> begin
let t_app ls l r =
@@ -509,10 +509,10 @@ let rec of_term ~cnv expected t : Why3.Term.term =
match find s, expected with
| ls, (Prop | Bool) ->
coerce ~cnv sort expected $
- t_app ls l (of_tau cnv sort)
+ t_app ls l (of_tau ~cnv sort)
| ls, _ ->
coerce ~cnv sort expected $
- t_app ls l (of_tau cnv sort)
+ t_app ls l (of_tau ~cnv sort)
| exception Not_found -> why3_failure "Can't find '%s' in why3 namespace" s
in
let apply_from_ns' s l =
@@ -524,7 +524,7 @@ let rec of_term ~cnv expected t : Why3.Term.term =
| Qed.Engine.F_left s, _ | Qed.Engine.F_assoc s, _ ->
let rec aux = function
| [] -> why3_failure "Empty application"
- | [a] -> of_term cnv expected a
+ | [a] -> of_term ~cnv expected a
| a::l ->
apply_from_ns s [of_term' cnv a; aux l] sort
in
@@ -532,7 +532,7 @@ let rec of_term ~cnv expected t : Why3.Term.term =
| Qed.Engine.F_right s, _ ->
let rec aux = function
| [] -> why3_failure "Empty application"
- | [a] -> of_term cnv expected a
+ | [a] -> of_term ~cnv expected a
| a::l ->
apply_from_ns s [aux l;of_term' cnv a] sort
in
@@ -568,7 +568,7 @@ let rec of_term ~cnv expected t : Why3.Term.term =
| Rget(a,f), _ , _ -> begin
let s = Lang.name_of_field f in
match Why3.Theory.(ns_find_ls (get_namespace cnv.th) (cut_path s)) with
- | ls -> Why3.Term.t_app ls [of_term' cnv a] (of_tau cnv expected)
+ | ls -> Why3.Term.t_app ls [of_term' cnv a] (of_tau ~cnv expected)
| exception Not_found -> why3_failure "Can't find '%s' in why3 namespace" s
end
| Rdef(l), Data(Comp (c, k),_) , _ -> begin
@@ -580,7 +580,7 @@ let rec of_term ~cnv expected t : Why3.Term.term =
match Why3.Theory.(ns_find_ls (get_namespace cnv.th) (cut_path s)) with
| ls ->
let l = List.map (fun (_,t) -> of_term' cnv t) l in
- Why3.Term.t_app ls l (of_tau cnv expected)
+ Why3.Term.t_app ls l (of_tau ~cnv expected)
| exception Not_found -> why3_failure "Can't find '%s' in why3 namespace" s
end
| (Rdef _, Data ((Mtype _|Mrecord (_, _)|Atype _), _), _)
@@ -620,7 +620,7 @@ and t_app_fold ~cnv ~f ~l ~p expected lt =
fold_map (of_term ~cnv expected) fold lt
and of_term' cnv t =
- of_term cnv (Lang.F.typeof t) t
+ of_term ~cnv (Lang.F.typeof t) t
and share cnv expected t =
let l = Lang.F.QED.shared ~shareable ~shared ~subterms [t] in
@@ -635,7 +635,7 @@ and share cnv expected t =
and mk_lets cnv l =
List.fold_left (fun (cnv,lets) e ->
let cnv' = {cnv with polarity = `NoPolarity} in
- let e' = of_term cnv' (Lang.F.typeof e) e in
+ let e' = of_term ~cnv:cnv' (Lang.F.typeof e) e in
match e'.t_ty with
| None -> ({cnv with subst = Lang.F.Tmap.add e e' cnv.subst},lets)
| Some ty ->
@@ -655,7 +655,7 @@ and successive_binders cnv q t =
| Bind((Forall|Exists) as q',tau,t) when q' = q ->
let x = Lang.F.fresh cnv.pool tau in
let x' = Why3.Ident.id_fresh (Lang.F.Tau.basename tau) in
- let x' = Why3.Term.create_vsymbol x' (Why3.Opt.get (of_tau cnv tau)) in
+ let x' = Why3.Term.create_vsymbol x' (Why3.Opt.get (of_tau ~cnv tau)) in
let cnv = {cnv with subst = Lang.F.Tmap.add (Lang.F.e_var x) (Why3.Term.t_var x') cnv.subst} in
let t = Lang.F.QED.e_unbind x t in
let why3_vars, t = successive_binders cnv q t in
@@ -679,7 +679,7 @@ let convert cnv expected t =
let mk_binders cnv l =
List.fold_left (fun (cnv,lets) v ->
- match of_tau cnv (Lang.F.tau_of_var v) with
+ match of_tau ~cnv (Lang.F.tau_of_var v) with
| None -> why3_failure "Quantification on prop"
| Some ty ->
let x = Why3.Ident.id_fresh (Lang.F.Var.basename v) in
@@ -753,7 +753,7 @@ class visitor (ctx:context) c =
let th = ctx.th in
let th = Why3.Theory.open_scope th name in
let th = Why3.Theory.use_export th thy in
- let th = Why3.Theory.close_scope th true in
+ let th = Why3.Theory.close_scope th ~import:true in
Wp_parameters.debug ~dkey:dkey_api "End on_cluster %s@." name;
ctx.th <- th
@@ -783,7 +783,7 @@ class visitor (ctx:context) c =
let th = ctx.th in
let th = Why3.Theory.open_scope th name in
let th = Why3.Theory.use_export th thy in
- let th = Why3.Theory.close_scope th import in
+ let th = Why3.Theory.close_scope th ~import in
ctx.th <- th
method on_library thy =
diff --git a/src/plugins/wp/RefUsage.ml b/src/plugins/wp/RefUsage.ml
index dadf93f8b177d82a12a3fd0ade153251e214b0e9..aba320386be55c760015f14251f26179ebe80ab6 100644
--- a/src/plugins/wp/RefUsage.ml
+++ b/src/plugins/wp/RefUsage.ml
@@ -205,7 +205,7 @@ let shift (m:model) (k:value) =
| Val_var x -> Val_shift(x,k)
| Val_comp(x,e) -> share ~old:e (fun k -> Val_comp(x,k)) (E.cup e k)
| Val_shift(x,e) -> share ~old:e (fun k -> Val_shift(x,k)) (E.cup e k)
- | E old -> share_vcup m old k
+ | E old -> share_vcup m ~old k
let field = function
| Val_var x -> Val_comp(x,E.bot)
diff --git a/src/plugins/wp/StmtSemantics.ml b/src/plugins/wp/StmtSemantics.ml
index e2f297f097dbb8a7aba069a751052e98bf3e4b62..bdef7e39bacdb888fdabdf020c480a06b5a45801 100644
--- a/src/plugins/wp/StmtSemantics.ml
+++ b/src/plugins/wp/StmtSemantics.ml
@@ -475,7 +475,7 @@ struct
parallel behavior env spec.spec_behavior
and assigns : env -> assigns -> paths = fun env a ->
- let frame, _, _ = mk_frame "assigns" env in
+ let frame, _, _ = mk_frame ~descr:"assigns" env in
let lenv = L.mk_env () in (* TODO: lenv for ghost code. *)
let here = Sigma.create () in
let authorized_region = L.in_frame frame
diff --git a/src/plugins/wp/TacSplit.ml b/src/plugins/wp/TacSplit.ml
index 0749a5532540e80d984f8d610ab565e425957e2b..eaec10793db2aabf68f18176b45409c9b24f681c 100644
--- a/src/plugins/wp/TacSplit.ml
+++ b/src/plugins/wp/TacSplit.ml
@@ -253,7 +253,7 @@ class split =
let cases = [ "Split" , F.p_bool p ] in
Applicable (Tactical.split cases)
| And es ->
- let nb_parts,parts = PartitionsQQ.get vars es in
+ let nb_parts,parts = PartitionsQQ.get ~vars es in
if nb_parts=1 then Not_applicable
else begin
feedback#set_title "Split (exists and)" ;
@@ -347,7 +347,7 @@ class split =
let cases = [ "Split (distrib forall and)" , When p ] in
Applicable (Tactical.replace ~at:step.id cases)
| Or es ->
- let nb_parts,parts = PartitionsQQ.get vars es in
+ let nb_parts,parts = PartitionsQQ.get ~vars es in
if nb_parts=1 then Not_applicable
else begin
feedback#set_title "Split (forall or)" ;
diff --git a/src/plugins/wp/Vlist.ml b/src/plugins/wp/Vlist.ml
index 876e5d09c2f807d7c0301cb3bb17ccd63ed8a7b3..e74e82bb738487d7f738212d27a6be8a6b166284 100644
--- a/src/plugins/wp/Vlist.ml
+++ b/src/plugins/wp/Vlist.ml
@@ -49,7 +49,7 @@ let l_repeat = E.(F_call "repeat")
(*--- Typechecking ---*)
let () = LogicBuiltins.add_type t_list ~library ~link:l_list ()
-let a_list = Lang.get_builtin_type t_list
+let a_list = Lang.get_builtin_type ~name:t_list
let vlist_get_tau = function
| None -> invalid_arg "a list operator without result type"
diff --git a/src/plugins/wp/WpTac.ml b/src/plugins/wp/WpTac.ml
index 72b21e10405352cb7426b1f42e5f753bbe572ff9..2b2e5dbd761caa3c90e149b86afeb49478d58c8d 100644
--- a/src/plugins/wp/WpTac.ml
+++ b/src/plugins/wp/WpTac.ml
@@ -346,7 +346,7 @@ let cnf_dnf ~pol ~depth e =
(cf@cxf),cnf
with | Absorbant -> [],[[]]
in
- let tool = tools pol in
+ let tool = tools ~pol in
let cNf = cnf_dnf ~depth ~pol e in
try
match cNf with
diff --git a/src/plugins/wp/wpPropId.ml b/src/plugins/wp/wpPropId.ml
index 03610465bb50266622bb32da622c35aee52afdc2..6cfe1a111264208d5a3c3c3d82608fccb3ef747a 100644
--- a/src/plugins/wp/wpPropId.ml
+++ b/src/plugins/wp/wpPropId.ml
@@ -149,9 +149,9 @@ let mk_fct_from_id kf kf_has_exit bhv tkind from =
mk_prop kind (Option.get id)
let mk_disj_bhv_id (kf,ki,active,disj) =
- mk_prop PKProp (Property.ip_of_disjoint kf ki active disj)
+ mk_prop PKProp (Property.ip_of_disjoint kf ki ~active disj)
let mk_compl_bhv_id (kf,ki,active,comp) =
- mk_prop PKProp (Property.ip_of_complete kf ki active comp)
+ mk_prop PKProp (Property.ip_of_complete kf ki ~active comp)
let mk_decrease_id kf s x =
mk_prop PKDecreases (Property.ip_of_decreases kf s x)
diff --git a/src/plugins/wp/wpReached.ml b/src/plugins/wp/wpReached.ml
index ba3d027febaa2f565ce1d09ea935fbd0f0305804..1069e9ef7a4757bb69778f0747839f80dbab700a 100644
--- a/src/plugins/wp/wpReached.ml
+++ b/src/plugins/wp/wpReached.ml
@@ -417,7 +417,7 @@ let set_unreachable pid =
| IPPredicate {ip_kind = PKAssumes _} -> []
| IPBehavior {ib_kf; ib_kinstr; ib_active; ib_bhv} ->
let active = Datatype.String.Set.elements ib_active in
- (ip_post_cond_of_behavior ib_kf ib_kinstr active ib_bhv) @
+ (ip_post_cond_of_behavior ib_kf ib_kinstr ~active ib_bhv) @
(ip_requires_of_behavior ib_kf ib_kinstr ib_bhv)
| IPExtended _ -> []
(* Extended clauses might concern anything. Don't validate them
diff --git a/src/plugins/wp/wpReport.ml b/src/plugins/wp/wpReport.ml
index fcfa0245131934d3a6844e6b2d7cf4171a39b2ba..bf3d4d0832752d07c36b59bbf04109e1b3a5f551 100644
--- a/src/plugins/wp/wpReport.ml
+++ b/src/plugins/wp/wpReport.ml
@@ -371,7 +371,7 @@ let add_goal (gs:fcstat) wpo =
let ds : dstats = get_section gs section in
let status,prop = Wpo.get_proof wpo in
let ps : pstats = get_property ds prop in
- add_results status [gs.global ; ds.dstats ; ps] wpo ;
+ add_results ~status [gs.global ; ds.dstats ; ps] wpo ;
let ok = (status = `Passed) in
add_cover gs.gcoverage ok prop ;
add_cover ds.dcoverage ok prop ;
@@ -553,10 +553,10 @@ let number ~config fmt k =
else Format.pp_print_int fmt k
let properties ~config fmt (s:coverage) = function
- | "" -> percent config fmt (Property.Set.cardinal s.proved) (Property.Set.cardinal s.covered)
- | "total" -> number config fmt (Property.Set.cardinal s.covered)
- | "valid" -> number config fmt (Property.Set.cardinal s.proved)
- | "failed" -> number config fmt (Property.Set.cardinal s.covered - Property.Set.cardinal s.proved)
+ | "" -> percent ~config fmt (Property.Set.cardinal s.proved) (Property.Set.cardinal s.covered)
+ | "total" -> number ~config fmt (Property.Set.cardinal s.covered)
+ | "valid" -> number ~config fmt (Property.Set.cardinal s.proved)
+ | "failed" -> number ~config fmt (Property.Set.cardinal s.covered - Property.Set.cardinal s.proved)
| _ -> raise Exit
@@ -576,10 +576,10 @@ let is_stat_name = function
let stat ~config fmt s = function
- | "success" -> percent config fmt s.valid s.total
- | "total" -> number config fmt s.total
- | "valid" | "" -> number config fmt s.valid
- | "failed" -> number config fmt (s.unsuccess + s.inconclusive)
+ | "success" -> percent ~config fmt s.valid s.total
+ | "total" -> number ~config fmt s.total
+ | "valid" | "" -> number ~config fmt s.valid
+ | "failed" -> number ~config fmt (s.unsuccess + s.inconclusive)
| "status" ->
let msg =
if s.inconclusive > 0 then config.status_inconclusive else
@@ -587,8 +587,8 @@ let stat ~config fmt s = function
if s.valid >= s.total then config.status_passed else
config.status_untried
in Format.pp_print_string fmt msg
- | "inconclusive" -> number config fmt s.inconclusive
- | "unsuccess" -> number config fmt s.unsuccess
+ | "inconclusive" -> number ~config fmt s.inconclusive
+ | "unsuccess" -> number ~config fmt s.unsuccess
| "time" ->
if s.time > 0.0 then
Rformat.pp_time_range ladder fmt s.time
@@ -623,7 +623,7 @@ let pcstats ~config fmt (s,c) cmd arg =
let env_toplevel ~config gstat fmt cmd arg =
try
- pcstats config fmt (gstat.global, gstat.gcoverage) cmd arg
+ pcstats ~config fmt (gstat.global, gstat.gcoverage) cmd arg
with Exit ->
if arg=""
then Wp_parameters.error ~once:true "Unknown toplevel-format '%%%s'" cmd
@@ -660,7 +660,7 @@ let env_section ~config ~name sstat fmt cmd arg =
| Fun kf -> config.function_prefix, ( Kernel_function.get_name kf)
in Format.fprintf fmt "%s%s" prefix name
| _ ->
- pcstats config fmt (ds.dstats, ds.dcoverage) cmd arg
+ pcstats ~config fmt (ds.dstats, ds.dcoverage) cmd arg
with Exit ->
if arg=""
then Wp_parameters.error ~once:true "Unknown section-format '%%%s'" cmd
@@ -692,7 +692,7 @@ let env_property ~config ~name pstat fmt cmd arg =
| "property" ->
Description.pp_local fmt p
| _ ->
- pstats config fmt stat cmd arg
+ pstats ~config fmt stat cmd arg
with Exit ->
if arg=""
then Wp_parameters.error ~once:true "Unknown property-format '%%%s'" cmd
diff --git a/src/plugins/wp/wpo.ml b/src/plugins/wp/wpo.ml
index 645c469a3810a6f05dbfb74cb22651f9788b073c..fbc6df714458fb2357f53853a004f26b9a58f82c 100644
--- a/src/plugins/wp/wpo.ml
+++ b/src/plugins/wp/wpo.ml
@@ -958,8 +958,8 @@ let _ignore =
WpoType.ty ProverType.ty
(Datatype.pair Datatype.string Datatype.string))
(fun w p ->
- (DISK.file_logout w.po_pid (get_model w) p,
- DISK.file_logerr w.po_pid (get_model w) p))
+ (DISK.file_logout ~pid:w.po_pid ~model:(get_model w) ~prover:p,
+ DISK.file_logerr ~pid:w.po_pid ~model:(get_model w) ~prover:p))
let pp_logfile fmt w prover =
let model = get_model w in
diff --git a/tests/journal/intra.ml b/tests/journal/intra.ml
index 7785c391999cf580cd9d92645b63f9a34d0f93b3..0962a71402273c161496fe0885c0c5879589ef9d 100644
--- a/tests/journal/intra.ml
+++ b/tests/journal/intra.ml
@@ -1 +1,4 @@
-let () = Db.Main.extend (fun _ -> ignore (Sparecode.Register.get true true))
+let () =
+ Db.Main.extend (fun _ ->
+ ignore (Sparecode.Register.get ~select_annot:true
+ ~select_slice_pragma:true))
diff --git a/tests/misc/add_assigns.ml b/tests/misc/add_assigns.ml
index 3b1412f0f1c2247bb67865aef6fbb01b48bdb825..7cf5569c55135d17e737453d3a6ac86bea968a46 100644
--- a/tests/misc/add_assigns.ml
+++ b/tests/misc/add_assigns.ml
@@ -26,7 +26,9 @@ let main () =
(fun b -> b.b_name = Cil.default_behavior_name)
(Annotations.behaviors kf)
in
- let ip = Option.get (Property.ip_assigns_of_behavior kf Kglobal [] bhv) in
+ let ip =
+ Option.get (Property.ip_assigns_of_behavior kf Kglobal ~active:[] bhv)
+ in
Property_status.(emit emitter ~hyps:[] ip True)
end
diff --git a/tests/slicing/libSelect.ml b/tests/slicing/libSelect.ml
index 309d09278480d329cc4ae0307e2169914d9d6231..6149a8dd0c1feb11cc3747e35108dd1cd5957491 100644
--- a/tests/slicing/libSelect.ml
+++ b/tests/slicing/libSelect.ml
@@ -83,7 +83,7 @@ let get_zones str_data (kinst, kf) =
let select_data_before_stmt str_data kinst kf =
let mark = Slicing.Api.Mark.make ~data:true ~addr:false ~ctrl:false in
let zone = get_zones str_data (kinst, kf) in
- Slicing.Api.Select.select_stmt_zone_internal kf kinst true zone mark
+ Slicing.Api.Select.select_stmt_zone_internal kf kinst ~before:true zone mark
(** build the selection for returned value of the function *)
@@ -94,7 +94,7 @@ let select_retres kf =
let zone = Locations.(enumerate_valid_bits Read loc) in
let mark = Slicing.Api.Mark.make ~data:true ~addr:false ~ctrl:false in
let before = false in
- Slicing.Api.Select.select_stmt_zone_internal kf ki before zone mark
+ Slicing.Api.Select.select_stmt_zone_internal kf ki ~before zone mark
with Db.Value.Void_Function -> raise No_return
;;
@@ -104,7 +104,7 @@ let select_data data kf =
let ki = Kernel_function.find_return kf in
let mark = Slicing.Api.Mark.make ~data:true ~addr:false ~ctrl:false in
let zone = get_zones data (ki, kf) in
- Slicing.Api.Select.select_stmt_zone_internal kf ki true zone mark
+ Slicing.Api.Select.select_stmt_zone_internal kf ki ~before:true zone mark
(* with Logic_interp.Error (_, str) -> raise (Unknown_data data) *)
with _ -> raise (Unknown_data data)
;;
diff --git a/tests/spec/Extend_recursive_preprocess.ml b/tests/spec/Extend_recursive_preprocess.ml
index f56767b5cc5aed48608d55bcb89e5c721472d175..51b53f09b821d9ff3544ab39ff265e6d30366235 100644
--- a/tests/spec/Extend_recursive_preprocess.ml
+++ b/tests/spec/Extend_recursive_preprocess.ml
@@ -13,10 +13,10 @@ let ext_typing_fooo _typing_context _loc l =
let ext_typing_block typing_context loc_here node =
match node.extended_node with
| Ext_lexpr (name,data) ->
- let status,kind = Logic_typing.get_typer name typing_context node.extended_loc data in
+ let status,kind = Logic_typing.get_typer name ~typing_context ~loc:node.extended_loc data in
Logic_const.new_acsl_extension name loc_here status kind
| Ext_extension (name, id, data) ->
- let status,kind = Logic_typing.get_typer_block name typing_context node.extended_loc (id,data) in
+ let status,kind = Logic_typing.get_typer_block name ~typing_context ~loc:node.extended_loc (id,data) in
Logic_const.new_acsl_extension name loc_here status kind
let ext_typing_foo typing_context loc (s,d) =
diff --git a/tests/spec/loop_assigns_generated.ml b/tests/spec/loop_assigns_generated.ml
index 7e9340737ab5ed66e19981bec6e1ba8d3d2b5de8..00739577e3d845c29c86de1d3c6658fa34b6365f 100644
--- a/tests/spec/loop_assigns_generated.ml
+++ b/tests/spec/loop_assigns_generated.ml
@@ -1,7 +1,7 @@
open Cil_types
-let e1 = Emitter.(create "emitter1" [ Code_annot ] [] [])
-let e2 = Emitter.(create "emitter2" [ Code_annot ] [] [])
+let e1 = Emitter.(create "emitter1" [ Code_annot ] ~correctness:[] ~tuning:[])
+let e2 = Emitter.(create "emitter2" [ Code_annot ] ~correctness:[] ~tuning:[])
let mk_assigns e v =
let lv = Cil.cvar_to_lvar v in