diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index b6660cac117df911653abe7845e0ba8ae15a8897..7ba8fa5f2a6c9d5a93c9bfb429456bfaac0b816b 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -480,8 +480,8 @@ let force_packed_attribute a =
let is_power_of_two i = i > 0 && i land (i-1) = 0
(* Computes the numeric value corresponding to an 'aligned' attribute:
- - if 'aligned' (without integer), then use the maximum machine alignment;
- - else, try to const-fold the expression to an integer value.
+ – if 'aligned' (without integer), then use the maximum machine alignment;
+ – else, try to const-fold the expression to an integer value.
Returns [Some n] in case of success, [None] otherwise.
Note that numeric values that are not powers of two are invalid and
also return [None]. *)
@@ -558,9 +558,9 @@ let process_pragmas_pack_align_comp_attributes ci cattrs =
match combine_aligned_attributes cattrs with
| None ->
(* No valid aligned attributes in this field.
- - if the composite type has a packed attribute, then add the
+ – if the composite type has a packed attribute, then add the
alignment given by the pack pragma;
- - otherwise, no alignment attribute is necessary.
+ – otherwise, no alignment attribute is necessary.
Drop existing "aligned" attributes, if there are invalid ones. *)
if Cil.hasAttribute "packed" cattrs then (dropAttribute "aligned" cattrs)
else begin
@@ -607,9 +607,9 @@ let process_pragmas_pack_align_field_attributes fi fattrs cattr =
match combine_aligned_attributes fattrs with
| None ->
(* No valid aligned attributes in this field.
- - if the composite type has a packed attribute, nothing needs to be
- done (the composite will have the "packed" attribute anyway);
- - otherwise, align on min(n,sizeof(fi.ftyp)).
+ – if the composite type has a packed attribute, nothing needs to be
+ done (the composite will have the "packed" attribute anyway);
+ – otherwise, align on min(n,sizeof(fi.ftyp)).
Drop existing "aligned" attributes, if there are invalid ones. *)
if Cil.hasAttribute "packed" cattr then (dropAttribute "aligned" fattrs)
else begin
@@ -2089,9 +2089,9 @@ struct
method private push: 'a.bool->'a->'a visitAction =
fun flag x ->
- Stack.push flag unspecified_stack;
- ChangeDoChildrenPost
- (x,fun x -> ignore(Stack.pop unspecified_stack); x)
+ Stack.push flag unspecified_stack;
+ ChangeDoChildrenPost
+ (x,fun x -> ignore(Stack.pop unspecified_stack); x)
method! vblock b =
@@ -4541,10 +4541,10 @@ let rec doSpecList ghost (suggestedAnonName: string)
constant's type is the smallest type (but at least int) that
will hold the value, with a preference for unsigned types.
The underlying type EI of the enum is picked as follows:
- - let T be the smallest integer type that holds all the enum's
- values; T is signed if any enum value is negative, unsigned otherwise
- - if the enum is packed or sizeof(T) >= sizeof(int), then EI = T
- - otherwise EI = int if T is signed and unsigned int otherwise
+ – let T be the smallest integer type that holds all the enum's
+ values; T is signed if any enum value is negative, unsigned otherwise
+ – if the enum is packed or sizeof(T) >= sizeof(int), then EI = T
+ – otherwise EI = int if T is signed and unsigned int otherwise
Note that these rules make the enum unsigned if possible *)
let updateEnum i : ikind =
if Integer.lt i !smallest then
@@ -5163,8 +5163,8 @@ and isVariableSizedArray ghost (dt: A.decl_type)
ARRAY (JUSTBASE, al, lo) when lo.expr_node != A.NOTHING ->
(* Checks whether the expression is an integer constant expression,
that is:
- - it contains no side-effect
- - it can be evaluated at compile-time
+ – it contains no side-effect
+ – it can be evaluated at compile-time
Note that we should not pass true as asconst argument for doExp,
since we are precisely trying to determine whether the expression
is a constant or not.
@@ -7787,22 +7787,22 @@ and doInitializer local_env (vi: varinfo) (inite: A.init_expression)
(* Consume some initializers. This is used by both global and local variables
initialization.
- - local_env is the current environment
- - asconst is used to indicate that expressions must be compile-time constant
+ – local_env is the current environment
+ – asconst is used to indicate that expressions must be compile-time constant
(i.e. we are in a global initializer)
- - add_implicit_ensures is a callback to add an ensures clause to contracts
+ – add_implicit_ensures is a callback to add an ensures clause to contracts
above current initialized part when it is partially initialized.
Does nothing initially. Useful only for initialization of locals
- - preinit corresponds to the initializers seen previously (for globals)
- - so contains the information about the current subobject currently being
+ – preinit corresponds to the initializers seen previously (for globals)
+ – so contains the information about the current subobject currently being
initialized
- - acc is the chunk corresponding to initializations seen previously
+ – acc is the chunk corresponding to initializations seen previously
(for locals)
- - initl is the current list of initializers to be processed
+ – initl is the current list of initializers to be processed
doInit returns a triple:
- - chunk performing initialization
- - preinit corresponding to the complete initialization
- - the list of unused initializers if any (should be empty most of the time)
+ – chunk performing initialization
+ – preinit corresponding to the complete initialization
+ – the list of unused initializers if any (should be empty most of the time)
*)
and doInit local_env asconst add_implicit_ensures preinit so acc initl =
let ghost = local_env.is_ghost in
diff --git a/src/kernel_services/abstract_interp/fc_float.ml b/src/kernel_services/abstract_interp/fc_float.ml
index 5f0b009bab1c3cdb1c011874d63fa65be598d4e5..c2f40659e5ae95f00fde9ace64b2c4a71fcd7325 100644
--- a/src/kernel_services/abstract_interp/fc_float.ml
+++ b/src/kernel_services/abstract_interp/fc_float.ml
@@ -212,7 +212,7 @@ let fmod round = binary mod_float round
let generate single double =
fun round prec ->
- round >>% fun () -> if is_single prec then single else double
+ round >>% fun () -> if is_single prec then single else double
let exp round = generate Floating_point.expf exp round
let log round = generate Floating_point.logf log round
diff --git a/src/kernel_services/ast_data/globals.ml b/src/kernel_services/ast_data/globals.ml
index ea4fd7b4489a40eeaf7afa641264772846a1f439..19de3c8145f979ff755a05e5762064d9fdb0cb3e 100644
--- a/src/kernel_services/ast_data/globals.ml
+++ b/src/kernel_services/ast_data/globals.ml
@@ -410,11 +410,11 @@ module Functions = struct
let o = object
method fold: 'a. (kernel_function -> 'a -> 'a) -> 'a -> 'a =
fun f acc ->
- fold
- (fun kf acc -> match kf.fundec with
- | Definition _ -> if is_definition then f kf acc else acc
- | Declaration _ -> if is_definition then acc else f kf acc)
- acc
+ fold
+ (fun kf acc -> match kf.fundec with
+ | Definition _ -> if is_definition then f kf acc else acc
+ | Declaration _ -> if is_definition then acc else f kf acc)
+ acc
method mem kf =
State.mem (get_vi kf) &&
(is_definition = Ast_info.Function.is_definition kf.fundec)
@@ -431,11 +431,11 @@ module Functions = struct
let o = object
method fold: 'a. (fundec -> 'a -> 'a) -> 'a -> 'a =
fun f acc ->
- fold
- (fun kf acc -> match kf.fundec with
- | Definition(fundec, _) -> f fundec acc
- | Declaration _ -> acc)
- acc
+ fold
+ (fun kf acc -> match kf.fundec with
+ | Definition(fundec, _) -> f fundec acc
+ | Declaration _ -> acc)
+ acc
method mem f = State.mem f.svar
end in
Parameter_category.create "functions" Cil_datatype.Fundec.ty
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index b0b3d4041b92d074c9ff3986214f04f9fb1fb291..adc133983a5b15ff4fa3ea4afa4266fd2d5e5b23 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -516,20 +516,20 @@ class cil_printer () = object (self)
method without_annot:
'a. (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a -> unit =
fun f fmt x ->
- let tmp = logic_printer_enabled in
- logic_printer_enabled <- false;
- let finally () = logic_printer_enabled <- tmp in
- Extlib.try_finally ~finally (f fmt) x;
+ let tmp = logic_printer_enabled in
+ logic_printer_enabled <- false;
+ let finally () = logic_printer_enabled <- tmp in
+ Extlib.try_finally ~finally (f fmt) x;
val mutable force_brace = false
method force_brace:
'a. (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a -> unit =
fun f fmt x ->
- let tmp = force_brace in
- force_brace <- true;
- let finally () = force_brace <- tmp in
- Extlib.try_finally ~finally f fmt x;
+ let tmp = force_brace in
+ force_brace <- true;
+ let finally () = force_brace <- tmp in
+ Extlib.try_finally ~finally f fmt x;
val current_stmt = Stack.create ()
diff --git a/src/kernel_services/ast_queries/filecheck.ml b/src/kernel_services/ast_queries/filecheck.ml
index 7567114270ced0f34a899a6fd4cfeaf3417651fb..7f9fb6810d409045fa5db13cd6df8e8acc8ff5ae 100644
--- a/src/kernel_services/ast_queries/filecheck.ml
+++ b/src/kernel_services/ast_queries/filecheck.ml
@@ -732,15 +732,15 @@ module Base_checker = struct
method private check_ei: 'a. enumitem -> 'a Cil.visitAction =
fun ei ->
- try
- let ei' = Enumitem.Hashtbl.find known_enumitems ei in
- if ei != ei' then
- check_abort "enumitem %s is not shared between declaration and use"
- ei.einame;
- Cil.DoChildren
- with Not_found ->
- check_abort "enumitem %s is used but not declared"
- ei.einame
+ try
+ let ei' = Enumitem.Hashtbl.find known_enumitems ei in
+ if ei != ei' then
+ check_abort "enumitem %s is not shared between declaration and use"
+ ei.einame;
+ Cil.DoChildren
+ with Not_found ->
+ check_abort "enumitem %s is used but not declared"
+ ei.einame
(* can't use vlogic_label, as it also visits the declared labels in
Tapp and Papp. *)
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index a0e404dd1c1e4b9dbb93575eed84077c85fd176d..c255a3c6a8709e28d1f43d2d8fe42947ebae5fcc 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -2992,80 +2992,80 @@ struct
and type_relation:
'a. _ -> _ -> (_ -> _ -> _ -> _ -> 'a) -> _ -> _ -> _ -> 'a =
fun ctxt env f t1 op t2 ->
- let loc1 = t1.lexpr_loc in
- let loc2 = t2.lexpr_loc in
- let loc = loc_join t1.lexpr_loc t2.lexpr_loc in
- let t1 = ctxt.type_term ctxt env t1 in
- let ty1 = t1.term_type in
- let t2 = ctxt.type_term ctxt env t2 in
- let ty2 = t2.term_type in
- let rel = match op with
- | Eq -> "eq"
- | Neq -> "ne"
- | Le -> "le"
- | Lt -> "lt"
- | Ge -> "ge"
- | Gt -> "gt"
+ let loc1 = t1.lexpr_loc in
+ let loc2 = t2.lexpr_loc in
+ let loc = loc_join t1.lexpr_loc t2.lexpr_loc in
+ let t1 = ctxt.type_term ctxt env t1 in
+ let ty1 = t1.term_type in
+ let t2 = ctxt.type_term ctxt env t2 in
+ let ty2 = t2.term_type in
+ let rel = match op with
+ | Eq -> "eq"
+ | Neq -> "ne"
+ | Le -> "le"
+ | Lt -> "lt"
+ | Ge -> "ge"
+ | Gt -> "gt"
+ in
+ let conditional_conversion t1 t2 =
+ let env,t,ty1,ty2 =
+ conditional_conversion loc env (Some rel) t1 t2
in
- let conditional_conversion t1 t2 =
- let env,t,ty1,ty2 =
- conditional_conversion loc env (Some rel) t1 t2
- in
- let t1 = { t1 with term_type = instantiate env t1.term_type } in
- let _,t1 =
- implicit_conversion ~overloaded:false loc1 t1 t1.term_type ty1
+ let t1 = { t1 with term_type = instantiate env t1.term_type } in
+ let _,t1 =
+ implicit_conversion ~overloaded:false loc1 t1 t1.term_type ty1
+ in
+ let t2 = { t2 with term_type = instantiate env t2.term_type } in
+ let _,t2 =
+ implicit_conversion ~overloaded:false loc2 t2 t2.term_type ty2
+ in
+ f loc op (mk_cast t1 t) (mk_cast t2 t)
+ in
+ begin match op with
+ | _ when plain_arithmetic_type ty1 && plain_arithmetic_type ty2 ->
+ conditional_conversion t1 t2
+ | Eq | Neq when isLogicPointer t1 && isLogicNull t2 ->
+ let t1 = mk_logic_pointer_or_StartOf t1 in
+ let t2 =
+ (* in case of a set, we perform two conversions: first from
+ integer to pointer, then from pointer to set of pointer. *)
+ if is_set_type t1.term_type then
+ mk_cast t2 (type_of_set_elem t1.term_type)
+ else t2
in
- let t2 = { t2 with term_type = instantiate env t2.term_type } in
- let _,t2 =
- implicit_conversion ~overloaded:false loc2 t2 t2.term_type ty2
+ f loc op t1 (mk_cast t2 t1.term_type)
+ | Eq | Neq when isLogicPointer t2 && isLogicNull t1 ->
+ let t2 = mk_logic_pointer_or_StartOf t2 in
+ let t1 =
+ if is_set_type t2.term_type then
+ mk_cast t1 (type_of_set_elem t2.term_type)
+ else t1
in
- f loc op (mk_cast t1 t) (mk_cast t2 t)
- in
- begin match op with
- | _ when plain_arithmetic_type ty1 && plain_arithmetic_type ty2 ->
- conditional_conversion t1 t2
- | Eq | Neq when isLogicPointer t1 && isLogicNull t2 ->
- let t1 = mk_logic_pointer_or_StartOf t1 in
- let t2 =
- (* in case of a set, we perform two conversions: first from
- integer to pointer, then from pointer to set of pointer. *)
- if is_set_type t1.term_type then
- mk_cast t2 (type_of_set_elem t1.term_type)
- else t2
- in
- f loc op t1 (mk_cast t2 t1.term_type)
- | Eq | Neq when isLogicPointer t2 && isLogicNull t1 ->
- let t2 = mk_logic_pointer_or_StartOf t2 in
- let t1 =
- if is_set_type t2.term_type then
- mk_cast t1 (type_of_set_elem t2.term_type)
- else t1
- in
- f loc op (mk_cast t1 t2.term_type) t2
- | Eq | Neq when isLogicArrayType ty1 && isLogicArrayType ty2 ->
- if is_same_logic_array_type ty1 ty2 then f loc op t1 t2
- else
- ctxt.error loc "comparison of incompatible types %a and %a"
- Cil_printer.pp_logic_type ty1 Cil_printer.pp_logic_type ty2
- | _ when isLogicPointer t1 && isLogicPointer t2 ->
- let t1 = mk_logic_pointer_or_StartOf t1 in
- let t2 = mk_logic_pointer_or_StartOf t2 in
- if is_same_logic_ptr_type ty1 ty2 ||
- ((op = Eq || op = Neq) &&
- (isLogicVoidPointerType t1.term_type ||
- isLogicVoidPointerType t2.term_type))
- then f loc op t1 t2
- else if (op=Eq || op = Neq) then conditional_conversion t1 t2
- else
- ctxt.error loc "comparison of incompatible types: %a and %a"
- Cil_printer.pp_logic_type t1.term_type
- Cil_printer.pp_logic_type t2.term_type
- | Eq | Neq -> conditional_conversion t1 t2
- | _ ->
+ f loc op (mk_cast t1 t2.term_type) t2
+ | Eq | Neq when isLogicArrayType ty1 && isLogicArrayType ty2 ->
+ if is_same_logic_array_type ty1 ty2 then f loc op t1 t2
+ else
+ ctxt.error loc "comparison of incompatible types %a and %a"
+ Cil_printer.pp_logic_type ty1 Cil_printer.pp_logic_type ty2
+ | _ when isLogicPointer t1 && isLogicPointer t2 ->
+ let t1 = mk_logic_pointer_or_StartOf t1 in
+ let t2 = mk_logic_pointer_or_StartOf t2 in
+ if is_same_logic_ptr_type ty1 ty2 ||
+ ((op = Eq || op = Neq) &&
+ (isLogicVoidPointerType t1.term_type ||
+ isLogicVoidPointerType t2.term_type))
+ then f loc op t1 t2
+ else if (op=Eq || op = Neq) then conditional_conversion t1 t2
+ else
ctxt.error loc "comparison of incompatible types: %a and %a"
Cil_printer.pp_logic_type t1.term_type
Cil_printer.pp_logic_type t2.term_type
- end
+ | Eq | Neq -> conditional_conversion t1 t2
+ | _ ->
+ ctxt.error loc "comparison of incompatible types: %a and %a"
+ Cil_printer.pp_logic_type t1.term_type
+ Cil_printer.pp_logic_type t2.term_type
+ end
and term_lval f t =
let check_lval t =
diff --git a/src/kernel_services/ast_transformations/inline.ml b/src/kernel_services/ast_transformations/inline.ml
index 600438e672790705bcb21a8956246d3539ef92a7..ba10dc8a509fc72d0374b2fde358059e8f63ae8a 100644
--- a/src/kernel_services/ast_transformations/inline.ml
+++ b/src/kernel_services/ast_transformations/inline.ml
@@ -51,13 +51,13 @@ module RemoveInlined =
let inline_parameter_category = object
method fold: 'a. (kernel_function -> 'a -> 'a) -> 'a -> 'a =
fun f acc ->
- Globals.Functions.fold
- (fun kf acc ->
- let vi = Kernel_function.get_vi kf in
- match kf.fundec with
- | Definition _ -> if vi.vinline then f kf acc else acc
- | Declaration _ -> acc)
- acc
+ Globals.Functions.fold
+ (fun kf acc ->
+ let vi = Kernel_function.get_vi kf in
+ match kf.fundec with
+ | Definition _ -> if vi.vinline then f kf acc else acc
+ | Declaration _ -> acc)
+ acc
method mem kf =
Kernel_function.is_definition kf && (Kernel_function.get_vi kf).vinline
end
diff --git a/src/libraries/utils/filepath.mli b/src/libraries/utils/filepath.mli
index 74eef31bbdbb8d6f2ff340258beffeef3539cd65..6d278f4407c85314f82d60ada84c31b7adb4b83b 100644
--- a/src/libraries/utils/filepath.mli
+++ b/src/libraries/utils/filepath.mli
@@ -36,6 +36,7 @@
unlike [realpath];
- non-existing directories in [realpath] may lead to ENOTDIR errors,
but [normalize] may accept them.
+
@modify Aluminium-20160501 optional base_name. *)
val normalize: ?base_name:string -> string -> string
@@ -59,8 +60,8 @@ val is_relative: ?base_name:string -> string -> bool
current working directory; also, symbolic names are resolved,
i.e. the result may be prefixed by known aliases (e.g. FRAMAC_SHARE).
See {!add_symbolic_dir} for more details.
- Therefore, the result of this function may not designate a valid name
- in the filesystem.
+ Therefore, the result of this function may not designate a valid name
+ in the filesystem.
@since Neon-20140301
@deprecated since 18.0-Argon
@@ -109,9 +110,9 @@ module Normalized: sig
current working directory; also, symbolic names are resolved,
i.e. the result may be prefixed by known aliases (e.g. FRAMAC_SHARE).
See {!add_symbolic_dir} for more details.
- Therefore, the result of this function may not designate a valid name
- in the filesystem and must ONLY be used to pretty-print information;
- it must NEVER to be converted back to a filepath later.
+ Therefore, the result of this function may not designate a valid name
+ in the filesystem and must ONLY be used to pretty-print information;
+ it must NEVER to be converted back to a filepath later.
*)
val pretty: Format.formatter -> t -> unit
diff --git a/src/libraries/utils/hptmap_sig.mli b/src/libraries/utils/hptmap_sig.mli
index a22d6fa4b3f341420ec27abcda56d9ade100a36c..3fdc7a3eb082e3d848e9b2ef81e695e286b3cc22 100644
--- a/src/libraries/utils/hptmap_sig.mli
+++ b/src/libraries/utils/hptmap_sig.mli
@@ -61,8 +61,8 @@ module type S = sig
except for the key [k] which is:
- removed from the map if [f o] = None
- bound to v' if [f o] = Some v'
- where [o] is (Some v) if [k] is bound to [v] in [m], or None if [k]
- is not bound in [m]. *)
+ where [o] is (Some v) if [k] is bound to [v] in [m], or None if [k]
+ is not bound in [m]. *)
val find : key -> t -> v
val find_check_missing: key -> t -> v
@@ -141,9 +141,9 @@ module type S = sig
- Absorbing returns the empty tree;
- (Traversing f) applies the function [f] to each binding of the remaining
subtree [t] (see [map']).
- The results of the function may be cached, depending on [cache]. If a cache
- is used, then the merge functions must be pure.
- *)
+
+ The results of the function may be cached, depending on [cache]. If a
+ cache is used, then the merge functions must be pure. *)
val generic_join :
cache:cache_type ->
diff --git a/src/plugins/gui/design.ml b/src/plugins/gui/design.ml
index 287a5d8e0b01a50e36a5dd37f0f4ea3ba4d3209f..4cf526308c22f254727310396baed427c6e28708 100644
--- a/src/plugins/gui/design.ml
+++ b/src/plugins/gui/design.ml
@@ -1298,18 +1298,18 @@ class main_window () : main_window_extension_points =
method private push_info_buffer :
'a. ?buffer:Buffer.t -> ('a, Format.formatter, unit) format -> 'a =
fun ?buffer fmt ->
- let b = match buffer with
- | None -> Buffer.create 80
- | Some b -> b
- in
- let bfmt = Format.formatter_of_buffer b in
- Format.kfprintf
- (function fmt ->
- Format.pp_print_flush fmt ();
- let content = Buffer.contents b in
- ignore (status_context#push content))
- bfmt
- fmt
+ let b = match buffer with
+ | None -> Buffer.create 80
+ | Some b -> b
+ in
+ let bfmt = Format.formatter_of_buffer b in
+ Format.kfprintf
+ (function fmt ->
+ Format.pp_print_flush fmt ();
+ let content = Buffer.contents b in
+ ignore (status_context#push content))
+ bfmt
+ fmt
method push_info fmt = self#push_info_buffer fmt
diff --git a/src/plugins/gui/wutil.ml b/src/plugins/gui/wutil.ml
index 7836b767e86b0f7c75531b592d0589318e1915bd..3804040a2b60035e42ab64795802f0486e055b30 100644
--- a/src/plugins/gui/wutil.ml
+++ b/src/plugins/gui/wutil.ml
@@ -169,9 +169,9 @@ class ['a] signal =
method set_enabled e = enabled <- e
method lock : (unit -> unit) -> unit =
fun f ->
- if not lock then
- try lock <- true ; f () ; lock <- false
- with err -> lock <- false ; raise err
+ if not lock then
+ try lock <- true ; f () ; lock <- false
+ with err -> lock <- false ; raise err
end
class ['a] selector default =
diff --git a/src/plugins/qed/logic.ml b/src/plugins/qed/logic.ml
index 4f1a82c6759eb17ad4812cec64dc1d0096a5fbfd..b9d0ee14b1e19d06d027192e4f0cdf1048abf1fe 100644
--- a/src/plugins/qed/logic.ml
+++ b/src/plugins/qed/logic.ml
@@ -519,9 +519,9 @@ sig
order of definition: each trailing terms only depend on heading ones.
The traversal is controlled by two optional arguments:
- - [shared] those terms are not traversed (considered as atomic, default to none)
- - [shareable] those terms ([is_simple] excepted) that can be shared (default to all)
- - [subterms] those sub-terms a term to be considered during
+ - [shared] those terms are not traversed (considered as atomic, default to none)
+ - [shareable] those terms ([is_simple] excepted) that can be shared (default to all)
+ - [subterms] those sub-terms a term to be considered during
traversal ([lc_iter] by default)
*)
diff --git a/src/plugins/rte/visit.ml b/src/plugins/rte/visit.ml
index a5e8ad38578f28365e4d918436372992d73386f9..f8e123d52089317afb287a36c3f50da7dcaedb11 100644
--- a/src/plugins/rte/visit.ml
+++ b/src/plugins/rte/visit.ml
@@ -108,15 +108,15 @@ class annot_visitor kf flags on_alarm = object (self)
method private generate_assertion: 'a. 'a Rte.alarm_gen -> 'a -> unit =
fun fgen ->
- let curr_stmt = self#current_stmt in
- let on_alarm ~invalid a =
- match curr_stmt with
- | None -> Options.warning ~current:true
- "Alarm generated outside any statement:@ %a"
- Alarms.pretty a
- | Some stmt -> on_alarm stmt ~invalid a
- in
- fgen ~remove_trivial:flags.Flags.remove_trivial ~on_alarm
+ let curr_stmt = self#current_stmt in
+ let on_alarm ~invalid a =
+ match curr_stmt with
+ | None -> Options.warning ~current:true
+ "Alarm generated outside any statement:@ %a"
+ Alarms.pretty a
+ | Some stmt -> on_alarm stmt ~invalid a
+ in
+ fgen ~remove_trivial:flags.Flags.remove_trivial ~on_alarm
(* Do not visit variable declarations, as no alarm should be emitted here,
and there is no statement to emit an alarm anyway ([generate_assertion]
diff --git a/src/plugins/server/data.mli b/src/plugins/server/data.mli
index 8c12a9465e4098629c4a1afd215439e31a481ef8..3e10ece5cbfb35d8753129d85d094c118919bab0 100644
--- a/src/plugins/server/data.mli
+++ b/src/plugins/server/data.mli
@@ -40,9 +40,9 @@ end
(** Datatype registration.
Name and page must be consistent with each other:
- - The name must be lowercase, dash-separated list of identifiers
- - Protocol data must start with ["<server>-*"]
- - Plugin data must start with ["<plugin>-*"]
+ - The name must be lowercase, dash-separated list of identifiers
+ - Protocol data must start with ["<server>-*"]
+ - Plugin data must start with ["<plugin>-*"]
*)
module type Info =
sig
diff --git a/src/plugins/server/request.mli b/src/plugins/server/request.mli
index c855405cb85088b1d88e60660a5a6e86e268493e..51d2ac92caf569f6a3e67ac342231468eee638ec 100644
--- a/src/plugins/server/request.mli
+++ b/src/plugins/server/request.mli
@@ -49,12 +49,12 @@ type 'b output = (module Output with type t = 'b)
(** Register a simple request of type [(a -> b)].
Name, page and kind must be consistent with each others:
- - No publication on [`Protocol] pages
- - Kernel requests shall starts with ["Kernel.*"]
- - Plugin requests shall starts with ["<Plugin>.*"]
- - SET requests must contain ["set"] (case insensitive)
- - GET requests must contain ["get"] or ["print"] (case insensitive)
- - EXEC requests must contain ["exec"] or ["compute"] (case insensitive)
+ - No publication on [`Protocol] pages
+ - Kernel requests shall starts with ["Kernel.*"]
+ - Plugin requests shall starts with ["<Plugin>.*"]
+ - SET requests must contain ["set"] (case insensitive)
+ - GET requests must contain ["get"] or ["print"] (case insensitive)
+ - EXEC requests must contain ["exec"] or ["compute"] (case insensitive)
*)
val register :
diff --git a/src/plugins/value/domains/abstract_domain.mli b/src/plugins/value/domains/abstract_domain.mli
index 4c77a1475887504958c8884cd540d0bdf5697822..1b8ed544fad1662faaae03fbbf7678e2b27b818b 100644
--- a/src/plugins/value/domains/abstract_domain.mli
+++ b/src/plugins/value/domains/abstract_domain.mli
@@ -128,8 +128,8 @@ module type Queries = sig
of [exp]. [Alarmset.all] is always a sound over-approximation of these
alarms.
- a value for the expression, which can be:
- - `Bottom if its evaluation is infeasible;
- - `Value (v, o) where [v] is an over-approximation of the abstract
+ – `Bottom if its evaluation is infeasible;
+ – `Value (v, o) where [v] is an over-approximation of the abstract
value of the expression [exp], and [o] is the origin of the value. *)
(** Query function for compound expressions:
@@ -232,7 +232,7 @@ module type Transfer = sig
- [stmt] is the statement of the call site;
- [call] represents the function call and its arguments.
- [pre] and [post] are the states before and at the end of the call
- respectively. *)
+ respectively. *)
val finalize_call:
stmt -> (location, value) call -> pre:state -> post:state -> state or_bottom
@@ -384,8 +384,8 @@ module type S = sig
(** [initialize_variable lval loc ~initialized init_value state] initializes
the value of the location [loc] of lvalue [lval] in [state] with:
- - bits 0 if init_value = Zero;
- - any bits if init_value = Top.
+ – bits 0 if init_value = Zero;
+ – any bits if init_value = Top.
The boolean initialized is true if the location is initialized, and false
if the location may be not initialized. *)
val initialize_variable:
diff --git a/src/plugins/value/domains/cvalue/builtins_malloc.ml b/src/plugins/value/domains/cvalue/builtins_malloc.ml
index b696a031f3ceb94b2b0dc803d4a12e2ebe6fbee8..f85c0c466ee462a48d0fb8bbd14878a4890e4a62 100644
--- a/src/plugins/value/domains/cvalue/builtins_malloc.ml
+++ b/src/plugins/value/domains/cvalue/builtins_malloc.ml
@@ -54,9 +54,9 @@ let () = Ast.add_monotonic_state Dynamic_Alloc_Bases.self
(* Remove some parts of the callstack:
- Remove the bottom of the call tree until we get to the call site
- of the call to the first malloc function. The idea is that each of
- these call site correspond to a different use of a malloc function,
- so it is interesting to keep their bases separated. *)
+ of the call to the first malloc function. The idea is that each of
+ these call site correspond to a different use of a malloc function,
+ so it is interesting to keep their bases separated. *)
let call_stack_no_wrappers () =
let stack = Value_util.call_stack () in
assert (stack != []);
diff --git a/src/plugins/value/domains/equality/equality.ml b/src/plugins/value/domains/equality/equality.ml
index 278404749c6349fd2f5ac17cbc0a3cf21da46c44..3aebc0c885bd3c2cbaa08d8aed9ccc8549a6ac0b 100644
--- a/src/plugins/value/domains/equality/equality.ml
+++ b/src/plugins/value/domains/equality/equality.ml
@@ -70,8 +70,8 @@ module Set = struct
from each lvalue or expression to:
- the equality in which it is involved;
- for a lvalue [lv], the set of expressions that contain [lv] in the map.
- This last information is needed when removing a lvalue, to remove or
- replace all expressions containing this lvalue. *)
+ This last information is needed when removing a lvalue, to remove or
+ replace all expressions containing this lvalue. *)
module Data = struct
(* For a lvalue [lv], the first set gathers the expressions that depends on
diff --git a/src/plugins/value/engine/evaluation.ml b/src/plugins/value/engine/evaluation.ml
index b56d00620330f489f0e440f296aa0e575f5b6465..699f57b6e2443d8cbf912d37c306f30ddd3df2ba 100644
--- a/src/plugins/value/engine/evaluation.ml
+++ b/src/plugins/value/engine/evaluation.ml
@@ -52,8 +52,8 @@ open Eval
fuel than before, if needed. *)
(* Reductions may happen in the forward evaluation when:
- - a domain returns a value more precise than the one internally computed;
- - alarms are emitted by an operation on values. In particular, locations
+ – a domain returns a value more precise than the one internally computed;
+ – alarms are emitted by an operation on values. In particular, locations
are reduced to their valid part for a read or write operation.
These reductions are propagated to the sub-expressions by a backward
evaluation, after the forward evaluation has finished.
diff --git a/src/plugins/value/engine/evaluation.mli b/src/plugins/value/engine/evaluation.mli
index f7febc17e4242c9d2b6f01189995ec86afcdfecc..b112178c2ac9cb2e021359f162731a2af1b9c2a3 100644
--- a/src/plugins/value/engine/evaluation.mli
+++ b/src/plugins/value/engine/evaluation.mli
@@ -46,6 +46,7 @@ module type S = sig
or `Value (valuation, value), where [value] is the numeric value computed
for the expression [expr], and [valuation] contains all the intermediate
results of the evaluation.
+
The [valuation] argument is a cache of already computed expressions.
It is empty by default.
The [reduction] argument allows deactivating the backward reduction
diff --git a/src/plugins/value/engine/partition.mli b/src/plugins/value/engine/partition.mli
index 1a48bf6e154c36c54bd8cee64fba21cea2a7f1f7..2a5177c756849b8abeb1bebb32e939066a11374f 100644
--- a/src/plugins/value/engine/partition.mli
+++ b/src/plugins/value/engine/partition.mli
@@ -127,10 +127,10 @@ type action =
| Restrict of Cil_types.exp * Integer.t list
(** [Restrict (exp, list)] restricts the rationing according to the evaluation
of the expression [exp]:
- - for each integer [i] in [list], states in which [exp] evaluates exactly
+ – for each integer [i] in [list], states in which [exp] evaluates exactly
to the singleton [i] receive the same unique stamp, and will thus be
joined together but kept separate from other states;
- - all other states are joined together.
+ – all other states are joined together.
Previous rationing is erased and replaced by this new stamping.
Implementation of the option -eva-split-return. *)
| Split of Cil_types.exp * split_kind * split_monitor
diff --git a/src/plugins/value/engine/subdivided_evaluation.ml b/src/plugins/value/engine/subdivided_evaluation.ml
index 3d0e928ef9f2da8cd8a22afc259eef4c4c6a90e3..965a8ca09342731b082c8da5f775ca3712178641 100644
--- a/src/plugins/value/engine/subdivided_evaluation.ml
+++ b/src/plugins/value/engine/subdivided_evaluation.ml
@@ -265,9 +265,9 @@ module Hypotheses = struct
let rec fold : type l. ('a -> 'b -> 'b) -> ('a, l) llist -> 'b -> 'b =
fun f list acc ->
- match list with
- | Nil -> acc
- | Cons (x, tl) -> fold f tl (f x acc)
+ match list with
+ | Nil -> acc
+ | Cons (x, tl) -> fold f tl (f x acc)
let rec fold2:
type l. ('a -> 'b -> 'c -> 'c) -> ('a, l) llist -> ('b, l) llist -> 'c -> 'c
@@ -298,19 +298,19 @@ module Hypotheses = struct
(* Pointwise comparison of two lists of subvalues. *)
let rec compare_subvalues: type l. l subvalues -> l subvalues -> int =
fun hyp1 hyp2 ->
- match hyp1, hyp2 with
- | Nil, Nil -> 0
- | Cons (v1, tail1), Cons (v2, tail2) ->
- let n = Cvalue.V.compare v1 v2 in
- if n = 0 then compare_subvalues tail1 tail2 else n
+ match hyp1, hyp2 with
+ | Nil, Nil -> 0
+ | Cons (v1, tail1), Cons (v2, tail2) ->
+ let n = Cvalue.V.compare v1 v2 in
+ if n = 0 then compare_subvalues tail1 tail2 else n
(* Pointwise join of two lists of subvalues. *)
let rec join_subvalues: type l. l subvalues -> l subvalues -> l subvalues =
fun l1 l2 ->
- match l1, l2 with
- | Nil, Nil -> Nil
- | Cons (x1, tl1), Cons (x2, tl2) ->
- Cons (Cvalue.V.join x1 x2, join_subvalues tl1 tl2)
+ match l1, l2 with
+ | Nil, Nil -> Nil
+ | Cons (x1, tl1), Cons (x2, tl2) ->
+ Cons (Cvalue.V.join x1 x2, join_subvalues tl1 tl2)
(* Extract the extremum of each subvalue of a list. Returns a list of lists
of values (one for each combination of extremum of the initial values). *)
diff --git a/src/plugins/value/engine/transfer_specification.ml b/src/plugins/value/engine/transfer_specification.ml
index e15091974e5c8cdc7de19f10e67d858ec9a6babc..b3be9e6f908aa569bd360e6f002cde811ecc29a5 100644
--- a/src/plugins/value/engine/transfer_specification.ml
+++ b/src/plugins/value/engine/transfer_specification.ml
@@ -465,12 +465,12 @@ module Make
(* Sound over-approximations of the effects of a function can be computed
through its specification in three different ways:
- - the default behavior is always an over-approximation of the function
+ – the default behavior is always an over-approximation of the function
effects, but can be very imprecise. We use it only if the two other ways
are inapplicable (both are strictly more precise).
- - any behavior whose assumes clause is true in the current state is also a
+ – any behavior whose assumes clause is true in the current state is also a
sound approximation of the function effects applied to this state.
- - the union of any complete set of behaviors is an over-approximation of
+ – the union of any complete set of behaviors is an over-approximation of
the function effects.
To obtain the highest precision, the states resulting from the
interpretation of any true behavior and of any complete set should be
diff --git a/src/plugins/value/engine/transfer_stmt.ml b/src/plugins/value/engine/transfer_stmt.ml
index 514e4ea789c0db62b5c02857c3417d66e9128ee5..24d5ca59ab6a103270a9c0a266cdc8499f7c24f6 100644
--- a/src/plugins/value/engine/transfer_stmt.ml
+++ b/src/plugins/value/engine/transfer_stmt.ml
@@ -361,9 +361,9 @@ module Make (Abstract: Abstractions.Eva) = struct
(* At the end of a call, this function gathers the arguments whose value can
be reduced at the call site. These are the arguments such that:
- - the formal has not been written during the call, but its value has been
+ – the formal has not been written during the call, but its value has been
reduced;
- - no variable of the concrete argument has been written during the call
+ – no variable of the concrete argument has been written during the call
(thus the concrete argument is still equal to the formal).
[state] is the state at the return statement of the called function;
it is used to evaluate the formals; their values are then compared to the
diff --git a/src/plugins/value/legacy/eval_op.ml b/src/plugins/value/legacy/eval_op.ml
index 207409c22900ce3e4105492ac3a6af47da41b382..03b3185c5769643921278386c05c1da5c31775e6 100644
--- a/src/plugins/value/legacy/eval_op.ml
+++ b/src/plugins/value/legacy/eval_op.ml
@@ -103,9 +103,9 @@ let reduce_by_initialized_defined f loc state =
(* il and ih are the bounds of the interval to reduce.
We change the initialized flags in the following cases:
- either we overwrite entire values, or the partly overwritten
- value is at the beginning or at the end of the subrange
+ value is at the beginning or at the end of the subrange
- or we do not lose information on misaligned or partial values:
- the result is a singleton *)
+ the result is a singleton *)
if V_Or_Uninitialized.(cardinal_zero_or_one v' || is_isotropic v') ||
((Int.equal offl il || Int.equal (Int.e_rem ll modu) abs_shift) &&
(Int.equal offh ih ||
diff --git a/src/plugins/value/legacy/eval_terms.ml b/src/plugins/value/legacy/eval_terms.ml
index ce9a20a55a312fa437321e4c9a52affec6a9aa2e..35f3c5c6ac8f1294f13ae513e625884ac38f6d30 100644
--- a/src/plugins/value/legacy/eval_terms.ml
+++ b/src/plugins/value/legacy/eval_terms.ml
@@ -1198,26 +1198,26 @@ and eval_tlval ~alarm_mode env t =
and eval_tif : 'a. (alarm_mode:_ -> _ -> _ -> 'a eval_result) -> ('a -> 'a -> 'a) -> ('a -> 'a -> 'a) -> alarm_mode:_ -> _ -> _ -> _ -> _ -> 'a eval_result =
fun eval join meet ~alarm_mode env tcond ttrue tfalse ->
- let r = eval_term ~alarm_mode env tcond in
- let ctrue = Cvalue.V.contains_non_zero r.eover
- and cfalse = Cvalue.V.contains_zero r.eover in
- match ctrue, cfalse with
- | true, true ->
- let vtrue = eval ~alarm_mode env ttrue in
- let vfalse = eval ~alarm_mode env tfalse in
- if not (same_etype vtrue.etype vfalse.etype) then
- Value_parameters.failure ~current:true
- "Incoherent types in conditional: %a vs. %a. \
- Please report"
- Printer.pp_typ vtrue.etype Printer.pp_typ vfalse.etype;
- let eover = join vtrue.eover vfalse.eover in
- let eunder = meet vtrue.eunder vfalse.eunder in
- { etype = vtrue.etype;
- ldeps = join_logic_deps vtrue.ldeps vfalse.ldeps;
- eunder; eover }
- | true, false -> eval ~alarm_mode env ttrue
- | false, true -> eval ~alarm_mode env tfalse
- | false, false -> assert false (* a logic alarm would have been raised*)
+ let r = eval_term ~alarm_mode env tcond in
+ let ctrue = Cvalue.V.contains_non_zero r.eover
+ and cfalse = Cvalue.V.contains_zero r.eover in
+ match ctrue, cfalse with
+ | true, true ->
+ let vtrue = eval ~alarm_mode env ttrue in
+ let vfalse = eval ~alarm_mode env tfalse in
+ if not (same_etype vtrue.etype vfalse.etype) then
+ Value_parameters.failure ~current:true
+ "Incoherent types in conditional: %a vs. %a. \
+ Please report"
+ Printer.pp_typ vtrue.etype Printer.pp_typ vfalse.etype;
+ let eover = join vtrue.eover vfalse.eover in
+ let eunder = meet vtrue.eunder vfalse.eunder in
+ { etype = vtrue.etype;
+ ldeps = join_logic_deps vtrue.ldeps vfalse.ldeps;
+ eunder; eover }
+ | true, false -> eval ~alarm_mode env ttrue
+ | false, true -> eval ~alarm_mode env tfalse
+ | false, false -> assert false (* a logic alarm would have been raised*)
(* if you add something here, update known_logic_funs above also *)
and eval_known_logic_function ~alarm_mode env li labels args =
diff --git a/src/plugins/value/utils/eval_typ.mli b/src/plugins/value/utils/eval_typ.mli
index ed2cdd50fecc1b0df0244d3ea86bad8db0d38fe3..35c9ed3578a9bd9c9ca8165bced3039d8eeca83e 100644
--- a/src/plugins/value/utils/eval_typ.mli
+++ b/src/plugins/value/utils/eval_typ.mli
@@ -34,7 +34,7 @@ val sizeof_lval_typ: typ -> Int_Base.t
(** [offsetmap_matches_type t o] returns true if either:
- [o] contains a single scalar binding, of the expected scalar type [t]
- (float or integer)
+ (float or integer)
- [o] contains multiple bindings, pointers, etc.
- [t] is not a scalar type. *)
val offsetmap_matches_type: typ -> Cvalue.V_Offsetmap.t -> bool
diff --git a/src/plugins/value/values/numerors/numerors_float.ml b/src/plugins/value/values/numerors/numerors_float.ml
index 9100f86425bfa2d17ac047aea38a3f655111af64..0dd24be71dba8e3b6e1bf62cb1beff96d5cba442 100644
--- a/src/plugins/value/values/numerors/numerors_float.ml
+++ b/src/plugins/value/values/numerors/numerors_float.ml
@@ -83,8 +83,8 @@ let unary_mpfrf f =
calling the binary function f on two inputs of type t *)
let binary_mpfrf f =
fun ?(rnd = Rounding.Near) ?(prec = P.Real) x y ->
- prec >>- fun () ->
- f (change_prec prec x) (change_prec prec y) (rounding rnd)
+ prec >>- fun () ->
+ f (change_prec prec x) (change_prec prec y) (rounding rnd)
(*-----------------------------------------------------------------------------
@@ -196,7 +196,7 @@ let div = binary_mpfrf Mpfrf.div
let pow = binary_mpfrf Mpfrf.pow
let pow_int =
fun ?(rnd = Rounding.Near) ?(prec = P.Real) x n ->
- prec >>- fun () -> Mpfrf.pow_int (change_prec prec x) n (rounding rnd)
+ prec >>- fun () -> Mpfrf.pow_int (change_prec prec x) n (rounding rnd)
(*-----------------------------------------------------------------------------
diff --git a/src/plugins/wp/Auto.ml b/src/plugins/wp/Auto.ml
index 86d62474d957176721e555f38477e58f3346b108..eafe23bd7bae4684b87673ef80e6e94e983cdde6 100644
--- a/src/plugins/wp/Auto.ml
+++ b/src/plugins/wp/Auto.ml
@@ -57,20 +57,20 @@ let t_cut ?(by="") (p : F.pred) (pi : Tactical.process) (hs,g) =
let t_case (p : F.pred) (a : Tactical.process) (b : Tactical.process) =
fun (hs,g) ->
- List.append
- (a (hs,F.p_imply p g))
- (b (hs,F.p_imply (F.p_not p) g))
+ List.append
+ (a (hs,F.p_imply p g))
+ (b (hs,F.p_imply (F.p_not p) g))
let t_cases ?(complete = "complete") (dps : (pred * Tactical.process) list) =
fun (hs,g) ->
- let pool = ref [] in
- List.iter
- (fun (p,pi) ->
- List.iter
- (fun u -> pool := u :: !pool)
- (pi (hs , p_imply p g))
- ) dps ;
- ( complete , (hs , p_any fst dps) ) :: List.rev !pool
+ let pool = ref [] in
+ List.iter
+ (fun (p,pi) ->
+ List.iter
+ (fun u -> pool := u :: !pool)
+ (pi (hs , p_imply p g))
+ ) dps ;
+ ( complete , (hs , p_any fst dps) ) :: List.rev !pool
let t_range e a b ~upper ~lower ~range s =
if (not (a <= b)) then raise (Invalid_argument "Wp.Auto.t_range") ;
diff --git a/src/plugins/wp/CfgCompiler.ml b/src/plugins/wp/CfgCompiler.ml
index f270951710659edcae6417637815e41af5da9dce..9b2eea8e009c153a13631e8b88cea6b3d0f4ef9c 100644
--- a/src/plugins/wp/CfgCompiler.ml
+++ b/src/plugins/wp/CfgCompiler.ml
@@ -333,16 +333,16 @@ struct
let succs : type a b. (a,b) env -> Node.t -> Node.t list =
fun cfg n ->
- match Node.Map.find n cfg.succs with
- | exception Not_found -> []
- | Goto n2 | Effect(_,n2) | Havoc(_,n2)
- | Branch(_,Some n2,None)
- | Branch(_,None,Some n2) -> [n2]
- | Binding (_,n2) -> [n2]
- | Branch(_,Some n1,Some n2) -> [n1;n2]
- | Branch(_,None,None) -> []
- | Either l -> l
- | Implies l -> List.map snd l
+ match Node.Map.find n cfg.succs with
+ | exception Not_found -> []
+ | Goto n2 | Effect(_,n2) | Havoc(_,n2)
+ | Branch(_,Some n2,None)
+ | Branch(_,None,Some n2) -> [n2]
+ | Binding (_,n2) -> [n2]
+ | Branch(_,Some n1,Some n2) -> [n1;n2]
+ | Branch(_,None,None) -> []
+ | Either l -> l
+ | Implies l -> List.map snd l
let pretty_edge : type a. Format.formatter -> (_,a) edge -> unit = fun fmt edge ->
match edge with
@@ -366,42 +366,42 @@ struct
let pretty_env : type a. Format.formatter -> (_,a) env -> unit =
fun fmt env ->
- Context.bind Lang.F.context_pp (Lang.F.env Lang.F.Vars.empty) (fun () ->
- Format.fprintf fmt
- "@[<v>@[<3>@[succs:@]@ %a@]@,@[<3>@[datas:@]@ %a@]@,@[<3>@[assumes:@]@ %a@]@]@."
- (Pretty_utils.pp_iter2 ~between:"->@," ~sep:",@ " Node.Map.iter Node.pp pretty_edge) env.succs
- (Pretty_utils.pp_iter2 ~between:"->@," ~sep:",@ " Node.Map.iter Node.pp
- (Pretty_utils.pp_iter Bag.iter pretty_data)) env.datas
- (Pretty_utils.pp_iter ~sep:",@ " Bag.iter P.pretty) env.assumes
- ) ()
+ Context.bind Lang.F.context_pp (Lang.F.env Lang.F.Vars.empty) (fun () ->
+ Format.fprintf fmt
+ "@[<v>@[<3>@[succs:@]@ %a@]@,@[<3>@[datas:@]@ %a@]@,@[<3>@[assumes:@]@ %a@]@]@."
+ (Pretty_utils.pp_iter2 ~between:"->@," ~sep:",@ " Node.Map.iter Node.pp pretty_edge) env.succs
+ (Pretty_utils.pp_iter2 ~between:"->@," ~sep:",@ " Node.Map.iter Node.pp
+ (Pretty_utils.pp_iter Bag.iter pretty_data)) env.datas
+ (Pretty_utils.pp_iter ~sep:",@ " Bag.iter P.pretty) env.assumes
+ ) ()
let dump_edge : type a. node -> Format.formatter -> (_, a) edge -> unit =
fun n fmt edge ->
- let pp_edge ?(label="") n' =
- Format.fprintf fmt " %a -> %a [ label=\"%s\" ] ;@." Node.pp n Node.pp n' label
- in
- begin match edge with
- | Goto n1 -> pp_edge n1
- | Branch (_, n1, n2)->
- Extlib.may pp_edge n1;
- Extlib.may pp_edge n2
- | Either ns -> List.iter pp_edge ns
- | Implies ns -> List.iter (fun (_,a) -> pp_edge a) ns
- | Effect (e, n') ->
- pp_edge ~label:(Format.asprintf "%a" E.pretty e) n'
- | Havoc (_, n') -> pp_edge ~label:"havoc" n'
- | Binding (_,n') -> pp_edge ~label:"binding" n'
- end
+ let pp_edge ?(label="") n' =
+ Format.fprintf fmt " %a -> %a [ label=\"%s\" ] ;@." Node.pp n Node.pp n' label
+ in
+ begin match edge with
+ | Goto n1 -> pp_edge n1
+ | Branch (_, n1, n2)->
+ Extlib.may pp_edge n1;
+ Extlib.may pp_edge n2
+ | Either ns -> List.iter pp_edge ns
+ | Implies ns -> List.iter (fun (_,a) -> pp_edge a) ns
+ | Effect (e, n') ->
+ pp_edge ~label:(Format.asprintf "%a" E.pretty e) n'
+ | Havoc (_, n') -> pp_edge ~label:"havoc" n'
+ | Binding (_,n') -> pp_edge ~label:"binding" n'
+ end
let dump_node : data Bag.t -> Format.formatter -> node -> unit =
fun datas fmt n ->
- Format.fprintf fmt " %a [ label=\"%a\n%a\" ] ;@."
- Node.pp n Node.pp n (Pretty_utils.pp_iter ~sep:"\n" Bag.iter pretty_data) datas
+ Format.fprintf fmt " %a [ label=\"%a\n%a\" ] ;@."
+ Node.pp n Node.pp n (Pretty_utils.pp_iter ~sep:"\n" Bag.iter pretty_data) datas
let dump_succ : type a. (_, a) env -> Format.formatter -> node -> (_, a) edge -> unit =
fun env fmt n e ->
- let datas = try Node.Map.find n env.datas with Not_found -> Bag.empty in
- Format.fprintf fmt "%a\n%a@\n" (dump_node datas) n (dump_edge n) e
+ let datas = try Node.Map.find n env.datas with Not_found -> Bag.empty in
+ Format.fprintf fmt "%a\n%a@\n" (dump_node datas) n (dump_edge n) e
let dump_assume : Format.formatter -> P.t -> unit =
let count = ref 0 in
@@ -420,72 +420,72 @@ struct
let output_dot : type a b. out_channel -> ?checks:_ -> (a,b) env -> unit =
fun cout ?(checks=Bag.empty) env ->
- let count = let c = ref max_int in fun () -> decr c; !c in
- let module E = struct
- type t = Graph.Graphviz.DotAttributes.edge list
- let default = []
- let compare x y = assert (x == y); 0
- end
- in
- let module V = struct
- type t =
- | Node of Node.t
- | Assume of int * Lang.F.pred
- | Check of int * Lang.F.pred
- (* todo better saner comparison *)
- let tag = function | Node i -> Node.tag i | Assume (i,_) -> i | Check (i,_) -> i
- let pp fmt = function | Node i -> Node.pp fmt i | Assume (i,_) -> Format.fprintf fmt "ass%i" i
- | Check (i,_) -> Format.fprintf fmt "chk%i" i
- let equal x y = (tag x) = (tag y)
- let compare x y = Transitioning.Stdlib.compare (tag x) (tag y)
- let hash x = tag x
- end in
- let module G = Graph.Imperative.Digraph.ConcreteBidirectionalLabeled (V)(E) in
- let module Dot = Graph.Graphviz.Dot(struct
- let graph_attributes _g = [`Fontname "fixed"]
- let default_vertex_attributes _g = (* [`Shape `Point] *) [`Shape `Circle]
- let vertex_name v = Format.asprintf "cp%a" V.pp v
- let vertex_attributes = function
- | V.Node n -> [`Label (escape "%a" Node.pp n)]
- | V.Assume (_,p) -> [`Style `Dashed; `Label (escape "%a" Lang.F.pp_pred p)]
- | V.Check (_,p) -> [`Style `Dotted; `Label (escape "%a" Lang.F.pp_pred p)]
- let get_subgraph _ = None
- let default_edge_attributes _g = []
- let edge_attributes ((_,e,_):G.E.t) : Graph.Graphviz.DotAttributes.edge list = e
- include G
- end) in
- let g = G.create () in
- let add_edge n1 l n2 = G.add_edge_e g (V.Node n1,l,V.Node n2) in
- let add_edges : type a b. Node.t -> (a,b) edge -> unit = fun n1 -> function
- | Goto n2 -> add_edge n1 [] n2
- | Branch((_,c),n2,n2') ->
- let aux s = function
- | None -> ()
- | Some n -> add_edge n1 [`Label (escape "%s%a" s Lang.F.pp_pred c)] n
- in
- aux "" n2; aux "!" n2'
- | Either l -> List.iter (add_edge n1 []) l
- | Implies l ->
- List.iter (fun (c,n) -> add_edge n1 [`Label (escape "%a" Lang.F.pp_pred (C.get c))] n) l
- | Effect ((_,e),n2) ->
- add_edge n1 [`Label (escape "%a" Lang.F.pp_pred e)] n2
- | Havoc (_,n2) -> add_edge n1 [`Label (escape "havoc")] n2
- | Binding (_,n2) -> add_edge n1 [`Label (escape "binding")] n2
- in
- Node.Map.iter add_edges env.succs;
- (** assumes *)
- Bag.iter (fun (m,p) ->
- let n1 = V.Assume(count (), p) in
- let assume_label = [`Style `Dashed ] in
- Node.Map.iter (fun n2 _ -> G.add_edge_e g (n1,assume_label,V.Node n2)) m
- ) env.assumes;
- (** checks *)
- Bag.iter (fun (m,p) ->
- let n1 = V.Check(count (), p) in
- let label = [`Style `Dotted ] in
- Node.Map.iter (fun n2 _ -> G.add_edge_e g (V.Node n2,label,n1)) m
- ) checks;
- Dot.output_graph cout g
+ let count = let c = ref max_int in fun () -> decr c; !c in
+ let module E = struct
+ type t = Graph.Graphviz.DotAttributes.edge list
+ let default = []
+ let compare x y = assert (x == y); 0
+ end
+ in
+ let module V = struct
+ type t =
+ | Node of Node.t
+ | Assume of int * Lang.F.pred
+ | Check of int * Lang.F.pred
+ (* todo better saner comparison *)
+ let tag = function | Node i -> Node.tag i | Assume (i,_) -> i | Check (i,_) -> i
+ let pp fmt = function | Node i -> Node.pp fmt i | Assume (i,_) -> Format.fprintf fmt "ass%i" i
+ | Check (i,_) -> Format.fprintf fmt "chk%i" i
+ let equal x y = (tag x) = (tag y)
+ let compare x y = Transitioning.Stdlib.compare (tag x) (tag y)
+ let hash x = tag x
+ end in
+ let module G = Graph.Imperative.Digraph.ConcreteBidirectionalLabeled (V)(E) in
+ let module Dot = Graph.Graphviz.Dot(struct
+ let graph_attributes _g = [`Fontname "fixed"]
+ let default_vertex_attributes _g = (* [`Shape `Point] *) [`Shape `Circle]
+ let vertex_name v = Format.asprintf "cp%a" V.pp v
+ let vertex_attributes = function
+ | V.Node n -> [`Label (escape "%a" Node.pp n)]
+ | V.Assume (_,p) -> [`Style `Dashed; `Label (escape "%a" Lang.F.pp_pred p)]
+ | V.Check (_,p) -> [`Style `Dotted; `Label (escape "%a" Lang.F.pp_pred p)]
+ let get_subgraph _ = None
+ let default_edge_attributes _g = []
+ let edge_attributes ((_,e,_):G.E.t) : Graph.Graphviz.DotAttributes.edge list = e
+ include G
+ end) in
+ let g = G.create () in
+ let add_edge n1 l n2 = G.add_edge_e g (V.Node n1,l,V.Node n2) in
+ let add_edges : type a b. Node.t -> (a,b) edge -> unit = fun n1 -> function
+ | Goto n2 -> add_edge n1 [] n2
+ | Branch((_,c),n2,n2') ->
+ let aux s = function
+ | None -> ()
+ | Some n -> add_edge n1 [`Label (escape "%s%a" s Lang.F.pp_pred c)] n
+ in
+ aux "" n2; aux "!" n2'
+ | Either l -> List.iter (add_edge n1 []) l
+ | Implies l ->
+ List.iter (fun (c,n) -> add_edge n1 [`Label (escape "%a" Lang.F.pp_pred (C.get c))] n) l
+ | Effect ((_,e),n2) ->
+ add_edge n1 [`Label (escape "%a" Lang.F.pp_pred e)] n2
+ | Havoc (_,n2) -> add_edge n1 [`Label (escape "havoc")] n2
+ | Binding (_,n2) -> add_edge n1 [`Label (escape "binding")] n2
+ in
+ Node.Map.iter add_edges env.succs;
+ (** assumes *)
+ Bag.iter (fun (m,p) ->
+ let n1 = V.Assume(count (), p) in
+ let assume_label = [`Style `Dashed ] in
+ Node.Map.iter (fun n2 _ -> G.add_edge_e g (n1,assume_label,V.Node n2)) m
+ ) env.assumes;
+ (** checks *)
+ Bag.iter (fun (m,p) ->
+ let n1 = V.Check(count (), p) in
+ let label = [`Style `Dotted ] in
+ Node.Map.iter (fun n2 _ -> G.add_edge_e g (V.Node n2,label,n1)) m
+ ) checks;
+ Dot.output_graph cout g
let dump_env : type a. name:string -> (_, a) env -> unit = fun ~name env ->
let file = (Filename.get_temp_dir_name ()) ^ "/cfg_" ^ name in
@@ -596,37 +596,37 @@ struct
(** return None when post is not accessible from this node *)
let rec effects : type a. (_,a) env -> node -> node -> S.domain option =
fun env post node ->
- if node = post
- then Some S.empty
- else
- match Node.Map.find node env.succs with
- | exception Not_found -> None
- | Goto (node2) ->
- effects env post node2
- | Branch (_, node2, node3) ->
- union_opt_or S.union
- (option_bind ~f:(effects env post) node2)
- (option_bind ~f:(effects env post) node3)
- | Either (l) ->
- (List.fold_left
- (fun acc node2 -> union_opt_or S.union
- acc (effects env post node2))
- None l)
- | Implies (l) ->
- (List.fold_left
- (fun acc (_,node2) -> union_opt_or S.union
- acc (effects env post node2))
- None l)
- | Effect (effect , node2) ->
- add_only_if_alive S.union
- (E.writes effect)
- (effects env post node2)
- | Havoc (m, node2) ->
- union_opt_and S.union
- (effects env m.post m.pre)
- (effects env post node2)
- | Binding (_,node2) ->
- effects env post node2
+ if node = post
+ then Some S.empty
+ else
+ match Node.Map.find node env.succs with
+ | exception Not_found -> None
+ | Goto (node2) ->
+ effects env post node2
+ | Branch (_, node2, node3) ->
+ union_opt_or S.union
+ (option_bind ~f:(effects env post) node2)
+ (option_bind ~f:(effects env post) node3)
+ | Either (l) ->
+ (List.fold_left
+ (fun acc node2 -> union_opt_or S.union
+ acc (effects env post node2))
+ None l)
+ | Implies (l) ->
+ (List.fold_left
+ (fun acc (_,node2) -> union_opt_or S.union
+ acc (effects env post node2))
+ None l)
+ | Effect (effect , node2) ->
+ add_only_if_alive S.union
+ (E.writes effect)
+ (effects env post node2)
+ | Havoc (m, node2) ->
+ union_opt_and S.union
+ (effects env m.post m.pre)
+ (effects env post node2)
+ | Binding (_,node2) ->
+ effects env post node2
(** restrict a cfg to the nodes accessible from the pre post given,
and compute havoc effect *)
@@ -1369,85 +1369,85 @@ struct
let compile : ?name:string -> ?mode:mode -> node -> Node.Set.t -> S.domain Node.Map.t ->
cfg -> F.pred Node.Map.t * S.t Node.Map.t * Conditions.sequence =
fun ?(name="cfg") ?(mode=`Bool_Forward) pre posts user_reads env ->
+ if Wp_parameters.has_dkey dkey then
+ Format.printf "@[0) pre:%a post:%a@]@."
+ Node.pp pre (Pretty_utils.pp_iter ~sep:"@ " Node.Set.iter Node.pp) posts;
+ if Wp_parameters.has_dkey dkey then
+ Format.printf "@[1) %a@]@." pretty_env env;
+ (** restrict environment to useful node and compute havoc effects *)
+ let env = restrict env pre posts in
+ if Wp_parameters.has_dkey dkey then
+ Format.printf "@[2) %a@]@." pretty_env env;
+ if Node.Map.is_empty env.succs then
+ Node.Map.empty,Node.Map.empty,
+ Conditions.sequence [Conditions.step (Conditions.Have(F.p_false))]
+ else
+ (** Simplify *)
+ let subst,env =
+ if true
+ then remove_dumb_gotos env
+ else Node.Map.empty, env
+ in
+ let pre = find_def ~def:pre pre subst in
+ (** Substitute in user_reads *)
+ let user_reads =
+ Node.Map.fold
+ (fun n n' acc ->
+ match Node.Map.find n user_reads with
+ | exception Not_found -> acc
+ | domain ->
+ let domain' =
+ try
+ S.union (Node.Map.find n' acc) domain
+ with Not_found -> domain
+ in
+ Node.Map.add n' domain' acc)
+ subst user_reads
+ in
+ (** For each node what must be read for assumes *)
+ let reads =
+ Bag.fold_left (fun acc e ->
+ Node.Map.union
+ (fun _ -> S.union) acc
+ (P.reads e))
+ user_reads env.assumes in
+ (** compute sigmas and relocate them *)
+ let env, sigmas = domains env reads pre in
if Wp_parameters.has_dkey dkey then
- Format.printf "@[0) pre:%a post:%a@]@."
- Node.pp pre (Pretty_utils.pp_iter ~sep:"@ " Node.Set.iter Node.pp) posts;
- if Wp_parameters.has_dkey dkey then
- Format.printf "@[1) %a@]@." pretty_env env;
- (** restrict environment to useful node and compute havoc effects *)
- let env = restrict env pre posts in
- if Wp_parameters.has_dkey dkey then
- Format.printf "@[2) %a@]@." pretty_env env;
- if Node.Map.is_empty env.succs then
- Node.Map.empty,Node.Map.empty,
- Conditions.sequence [Conditions.step (Conditions.Have(F.p_false))]
- else
- (** Simplify *)
- let subst,env =
- if true
- then remove_dumb_gotos env
- else Node.Map.empty, env
- in
- let pre = find_def ~def:pre pre subst in
- (** Substitute in user_reads *)
- let user_reads =
- Node.Map.fold
- (fun n n' acc ->
- match Node.Map.find n user_reads with
- | exception Not_found -> acc
- | domain ->
- let domain' =
- try
- S.union (Node.Map.find n' acc) domain
- with Not_found -> domain
- in
- Node.Map.add n' domain' acc)
- subst user_reads
- in
- (** For each node what must be read for assumes *)
- let reads =
- Bag.fold_left (fun acc e ->
- Node.Map.union
- (fun _ -> S.union) acc
- (P.reads e))
- user_reads env.assumes in
- (** compute sigmas and relocate them *)
- let env, sigmas = domains env reads pre in
- if Wp_parameters.has_dkey dkey then
- Format.printf "@[3) %a@]@." pretty_env env;
- if Wp_parameters.has_dkey dumpkey then
- dump_env ~name env;
- let f, preds =
- match mode with
- | `Tree ->
- (** Add a unique post node *)
- let final_node = node () in
- let env =
- Node.Set.fold (fun p cfg ->
- let s = {pre=S.create();post=S.create()} in
- let e = s,Lang.F.p_true in
- let goto = effect p e final_node in
- concat goto cfg
- ) posts env
- in
- To_tree.to_sequence_tree pre posts env
- | (`Bool_Backward | `Bool_Forward) as mode ->
- to_sequence_bool ~mode pre posts env in
- let predssigmas =
- Node.Map.merge
- (fun _ p s -> Some (Extlib.opt_conv F.p_false p, Extlib.opt_conv (S.create ()) s))
- preds sigmas in
- (** readd simplified nodes *)
- let predssigmas =
- Node.Map.fold (fun n n' acc -> Node.Map.add n (Node.Map.find n' predssigmas) acc )
- subst predssigmas
- in
- let preds =
- Node.Map.map(fun _ (x,_) -> x) predssigmas
- in
- let sigmas =
- Node.Map.map(fun _ (_,x) -> x) predssigmas
- in
- preds,sigmas,f
+ Format.printf "@[3) %a@]@." pretty_env env;
+ if Wp_parameters.has_dkey dumpkey then
+ dump_env ~name env;
+ let f, preds =
+ match mode with
+ | `Tree ->
+ (** Add a unique post node *)
+ let final_node = node () in
+ let env =
+ Node.Set.fold (fun p cfg ->
+ let s = {pre=S.create();post=S.create()} in
+ let e = s,Lang.F.p_true in
+ let goto = effect p e final_node in
+ concat goto cfg
+ ) posts env
+ in
+ To_tree.to_sequence_tree pre posts env
+ | (`Bool_Backward | `Bool_Forward) as mode ->
+ to_sequence_bool ~mode pre posts env in
+ let predssigmas =
+ Node.Map.merge
+ (fun _ p s -> Some (Extlib.opt_conv F.p_false p, Extlib.opt_conv (S.create ()) s))
+ preds sigmas in
+ (** readd simplified nodes *)
+ let predssigmas =
+ Node.Map.fold (fun n n' acc -> Node.Map.add n (Node.Map.find n' predssigmas) acc )
+ subst predssigmas
+ in
+ let preds =
+ Node.Map.map(fun _ (x,_) -> x) predssigmas
+ in
+ let sigmas =
+ Node.Map.map(fun _ (_,x) -> x) predssigmas
+ in
+ preds,sigmas,f
end
diff --git a/src/plugins/wp/Filtering.ml b/src/plugins/wp/Filtering.ml
index adf5bbd31779b2ab6a62b9f9f1ffcfd97ce8d63f..09db94091f3affe53151ca1e5936934ca18359b4 100644
--- a/src/plugins/wp/Filtering.ml
+++ b/src/plugins/wp/Filtering.ml
@@ -29,8 +29,8 @@ open Lang
open Lang.F
(* Inductive Properties:
- - filter ~polarity:true p ==> p
- - p ==> filter ~polarity:false p
+ - filter ~polarity:true p ==> p
+ - p ==> filter ~polarity:false p
*)
let rec filter ~polarity f p =
match F.p_expr p with
diff --git a/src/plugins/wp/Filtering.mli b/src/plugins/wp/Filtering.mli
index 7a0944c37bc7ff689e70e5703a565121d655e275..a84a1baa1e3cc1a0e64c3b1639dd57dd6627ca87 100644
--- a/src/plugins/wp/Filtering.mli
+++ b/src/plugins/wp/Filtering.mli
@@ -29,12 +29,12 @@ open Lang
(**
Erase parts of a predicate that do not satisfies the condition.
The erased parts are replaced by:
- - [true] when [~polarity:false] (for hypotheses)
- - [false] when [~polarity:true] (for goals)
+ - [true] when [~polarity:false] (for hypotheses)
+ - [false] when [~polarity:true] (for goals)
Hence, we have:
- - [filter ~polarity:true f p ==> p]
- - [p ==> filter ~polarity:false f p]
+ - [filter ~polarity:true f p ==> p]
+ - [p ==> filter ~polarity:false f p]
See [theory/filtering.why] for proofs.
*)
diff --git a/src/plugins/wp/GuiTactic.ml b/src/plugins/wp/GuiTactic.ml
index 34caa9678c84ef3a4f2440bd10486eb258b1d350..d5e58431b2aa38feee1a0bb8259d1af17cc4f092 100644
--- a/src/plugins/wp/GuiTactic.ml
+++ b/src/plugins/wp/GuiTactic.ml
@@ -408,10 +408,10 @@ class tactic
?range:bool -> ?vmin:int -> ?vmax:int ->
?filter:(Lang.F.term -> bool) -> 'a field -> unit =
fun ?enabled ?title ?tooltip ?range ?vmin ?vmax ?filter field ->
- let id = Tactical.ident field in
- List.iter (fun (fd : wfield) ->
- fd#update ?enabled ?title ?tooltip ?range ?vmin ?vmax ?filter id
- ) wfields
+ let id = Tactical.ident field in
+ List.iter (fun (fd : wfield) ->
+ fd#update ?enabled ?title ?tooltip ?range ?vmin ?vmax ?filter id
+ ) wfields
(* -------------------------------------------------------------------------- *)
(* --- Widget Behavior --- *)
diff --git a/src/plugins/wp/ProofScript.ml b/src/plugins/wp/ProofScript.ml
index 6649d349e675155a87176d1a248a5943af7414fe..35a027f61a35a1e10590516cd76d315596172eed 100644
--- a/src/plugins/wp/ProofScript.ml
+++ b/src/plugins/wp/ProofScript.ml
@@ -445,13 +445,13 @@ class console ~pool ~title =
?range:bool -> ?vmin:int -> ?vmax:int ->
?filter:(Lang.F.term -> bool) -> 'a field -> unit =
fun ?enabled ?title ?tooltip ?range ?vmin ?vmax ?filter field ->
- ignore enabled ;
- ignore title ;
- ignore tooltip ;
- ignore field ;
- ignore vmin ; ignore vmax ;
- ignore range ; ignore filter ;
- ()
+ ignore enabled ;
+ ignore title ;
+ ignore tooltip ;
+ ignore field ;
+ ignore vmin ; ignore vmax ;
+ ignore range ; ignore filter ;
+ ()
val mutable errors = false
method has_error = errors
diff --git a/src/plugins/wp/Sigs.ml b/src/plugins/wp/Sigs.ml
index 1960d594da337b6b0a086059468f287018542da8..43db54a110aea9a9706f602940bc2a49e035b56d 100644
--- a/src/plugins/wp/Sigs.ml
+++ b/src/plugins/wp/Sigs.ml
@@ -326,9 +326,9 @@ sig
shall be performed, otherwise return [Mvalue].
Recognized [Cil] patterns:
- - [Mvar x,[Mindex 0]] is rendered as [*x] when [x] has a pointer type
- - [Mmem p,[Mfield f;...]] is rendered as [p->f...] like in Cil
- - [Mmem p,[Mindex k;...]] is rendered as [p[k]...] to catch Cil [Mem(AddPI(p,k)),...] *)
+ - [Mvar x,[Mindex 0]] is rendered as [*x] when [x] has a pointer type
+ - [Mmem p,[Mfield f;...]] is rendered as [p->f...] like in Cil
+ - [Mmem p,[Mindex k;...]] is rendered as [p[k]...] to catch Cil [Mem(AddPI(p,k)),...] *)
val lookup : state -> term -> mval
(** Try to interpret a sequence of states into updates.
diff --git a/src/plugins/wp/Tactical.mli b/src/plugins/wp/Tactical.mli
index c135567fe9fe67191b949604a845248dc0b9f962..80ce4eb29c52fe910501e8f8a9cd871591e5ea09 100644
--- a/src/plugins/wp/Tactical.mli
+++ b/src/plugins/wp/Tactical.mli
@@ -133,9 +133,9 @@ val search :
find:(string -> 'a) ->
unit -> 'a named option field * parameter
(** Search field.
- - [browse s n] is the lookup function, used in the GUI only.
+ - [browse s n] is the lookup function, used in the GUI only.
Shall returns at most [n] results applying to selection [s].
- - [find n] is used at script replay, and shall retrieve the
+ - [find n] is used at script replay, and shall retrieve the
selected item's [id] later on. *)
type 'a formatter = ('a,Format.formatter,unit) format -> 'a
diff --git a/src/plugins/wp/cfgWP.ml b/src/plugins/wp/cfgWP.ml
index 5f50a2b765e08572d52e8dae984122823859ea63..5c9f650ca85e03c7b8c934b4b2c13b37a3255002 100644
--- a/src/plugins/wp/cfgWP.ml
+++ b/src/plugins/wp/cfgWP.ml
@@ -339,13 +339,13 @@ struct
let merge_all_vcs : vc Splitter.t Gmap.t list -> vc Splitter.t Gmap.t =
fun cases ->
- let targets = List.fold_left
- (fun goals vcs -> Gset.union goals (Gmap.domain vcs))
- Gset.empty cases in
- let goal g vcs = try Gmap.find g vcs with Not_found -> Splitter.empty in
- Gset.mapping
- (fun g -> Splitter.merge_all merge_vcs (List.map (goal g) cases))
- targets
+ let targets = List.fold_left
+ (fun goals vcs -> Gset.union goals (Gmap.domain vcs))
+ Gset.empty cases in
+ let goal g vcs = try Gmap.find g vcs with Not_found -> Splitter.empty in
+ Gset.mapping
+ (fun g -> Splitter.merge_all merge_vcs (List.map (goal g) cases))
+ targets
(* -------------------------------------------------------------------------- *)
(* --- Merge for Calculus --- *)
diff --git a/src/plugins/wp/wpStrategy.ml b/src/plugins/wp/wpStrategy.ml
index 250b33fb3df18a539a465aed423a2473ceb190c1..f87b744a61755072dfc906ed4e3e2cd282fb4c1e 100644
--- a/src/plugins/wp/wpStrategy.ml
+++ b/src/plugins/wp/wpStrategy.ml
@@ -35,12 +35,12 @@ type annot_kind =
but not an hypothesis (see Aboth): A /\ ...*)
| Aboth of bool
(* annotation can be used as both hypothesis and goal :
- - with true : considered as both : A /\ A=>..
- - with false : we just want to use it as hyp right now. *)
+ - with true : considered as both : A /\ A=>..
+ - with false : we just want to use it as hyp right now. *)
| AcutB of bool
(* annotation is use as a cut :
- - with true (A is also a goal) -> A (+ proof obligation A => ...)
- - with false (A is an hyp only) -> True (+ proof obligation A => ...) *)
+ - with true (A is also a goal) -> A (+ proof obligation A => ...)
+ - with false (A is an hyp only) -> True (+ proof obligation A => ...) *)
| AcallHyp of kernel_function
(* annotation is a called function property to consider as an Hyp.
* The pre are not here but in AcallPre since they can also