From 24f77debbcc2e85d0d6992968f46525be1ede075 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Mon, 14 Jan 2019 16:05:38 +0100
Subject: [PATCH] [wp] linting files
---
src/plugins/wp/Cfloat.ml | 28 +++++------
src/plugins/wp/Letify.ml | 44 ++++++++---------
src/plugins/wp/MemTyped.ml | 38 +++++++--------
src/plugins/wp/Model.ml | 8 +--
src/plugins/wp/Plang.ml | 22 ++++-----
src/plugins/wp/ProverScript.ml | 68 +++++++++++++-------------
src/plugins/wp/StmtSemantics.ml | 86 ++++++++++++++++-----------------
src/plugins/wp/TacSplit.ml | 6 +--
src/plugins/wp/proof.ml | 4 +-
src/plugins/wp/proof.mli | 2 +-
src/plugins/wp/wpPropId.ml | 6 +--
11 files changed, 156 insertions(+), 156 deletions(-)
diff --git a/src/plugins/wp/Cfloat.ml b/src/plugins/wp/Cfloat.ml
index 7605e763426..a16ae09a683 100644
--- a/src/plugins/wp/Cfloat.ml
+++ b/src/plugins/wp/Cfloat.ml
@@ -73,17 +73,17 @@ let real = Str.regexp (mantissa ^ comma ^ exponent ^ "$")
let parse_literal v r =
try
- if Str.string_match real r 0 then
- let ma = Str.matched_group 1 r in
- let mb = try Str.matched_group 3 r with Not_found -> "" in
- let me = try Str.matched_group 6 r with Not_found -> "0" in
- let n = int_of_string me - String.length mb in
- let d n =
- let s = Bytes.make (succ n) '0' in
- Bytes.set s 0 '1' ; Q.of_string (Bytes.to_string s) in
- let m = Q.of_string (ma ^ mb) in
- if n < 0 then Q.div m (d (-n)) else
- if n > 0 then Q.mul m (d n) else m
+ if Str.string_match real r 0 then
+ let ma = Str.matched_group 1 r in
+ let mb = try Str.matched_group 3 r with Not_found -> "" in
+ let me = try Str.matched_group 6 r with Not_found -> "0" in
+ let n = int_of_string me - String.length mb in
+ let d n =
+ let s = Bytes.make (succ n) '0' in
+ Bytes.set s 0 '1' ; Q.of_string (Bytes.to_string s) in
+ let m = Q.of_string (ma ^ mb) in
+ if n < 0 then Q.div m (d (-n)) else
+ if n > 0 then Q.mul m (d n) else m
else Q.of_float v
with Failure _ ->
Warning.error ~source:"acsl" "Unexpected real literal %S" r
@@ -195,9 +195,9 @@ let builtin_error = function
(* -------------------------------------------------------------------------- *)
let float_of_real f a =
- match Context.get model with
- | Real -> a
- | Float -> e_fun (flt_rnd f) [a]
+ match Context.get model with
+ | Real -> a
+ | Float -> e_fun (flt_rnd f) [a]
let float_of_int f a = float_of_real f (Cmath.real_of_int a)
let real_of_float _f a = a
diff --git a/src/plugins/wp/Letify.ml b/src/plugins/wp/Letify.ml
index cd4f63db13d..a6d1257b1a4 100644
--- a/src/plugins/wp/Letify.ml
+++ b/src/plugins/wp/Letify.ml
@@ -48,15 +48,15 @@ struct
F.is_primitive e ||
begin
try Tmap.find e env.ground with Not_found ->
- let r = match F.repr e with
- | Rdef fvs -> List.for_all (fun (_,e) -> is_ground env e) fvs
- | Fun(f,es) ->
- begin match Fun.category f with
- | Constructor -> List.for_all (is_ground env) es
- | _ -> false
- end
- | _ -> false in
- env.ground <- Tmap.add e r env.ground ; r
+ let r = match F.repr e with
+ | Rdef fvs -> List.for_all (fun (_,e) -> is_ground env e) fvs
+ | Fun(f,es) ->
+ begin match Fun.category f with
+ | Constructor -> List.for_all (is_ground env) es
+ | _ -> false
+ end
+ | _ -> false in
+ env.ground <- Tmap.add e r env.ground ; r
end
let merge a b =
@@ -75,7 +75,7 @@ struct
| Model { m_category = Injection } -> 1
| Model { m_category = Operator _ } -> 2
| Model { m_category = Constructor } -> 3
-
+
let add_reduce env a b =
env.domain <- Tmap.add a b env.domain
@@ -83,18 +83,18 @@ struct
if F.is_subterm a b then add_reduce env b a else
if F.is_subterm b a then add_reduce env a b else
begin
- match F.repr a , F.repr b with
- | Fun(f,_) , Fun(g,_) when Wp_parameters.Reduce.get () ->
- let cmp = frank f - frank g in
+ match F.repr a , F.repr b with
+ | Fun(f,_) , Fun(g,_) when Wp_parameters.Reduce.get () ->
+ let cmp = frank f - frank g in
if cmp < 0 then add_reduce env a b else
if cmp > 0 then add_reduce env b a
- | Fun(f,_) , _ when frank f = 0 ->
+ | Fun(f,_) , _ when frank f = 0 ->
add_reduce env a b
- | _ , Fun(f,_) when frank f = 0 ->
+ | _ , Fun(f,_) when frank f = 0 ->
add_reduce env b a
- | _ -> ()
+ | _ -> ()
end
-
+
let rec walk env h =
match F.repr h with
| True | False -> ()
@@ -128,7 +128,7 @@ struct
let e_apply env =
let sigma = F.sigma () in
F.e_subst ~sigma (lookup env.domain)
-
+
let p_apply env =
let sigma = F.sigma () in
F.p_subst ~sigma (lookup env.domain)
@@ -145,12 +145,12 @@ struct
[@@@ warning "+32"]
let pretty fmt env = pp_sigma fmt env.domain
-
+
let assume env p =
let p = F.p_subst (lookup env.domain) p in
walk env (F.e_prop p) ; p
- let top () = { ground = Tmap.empty ; domain = Tmap.empty }
+ let top () = { ground = Tmap.empty ; domain = Tmap.empty }
let copy env = { domain = env.domain ; ground = env.ground }
let compute seq =
@@ -200,7 +200,7 @@ struct
match F.p_expr p with
| And ps -> F.p_all (assume env) (List.rev ps)
| _ -> assume env p
-
+
end
(* -------------------------------------------------------------------------- *)
@@ -402,7 +402,7 @@ struct
end
let is_kint e = match F.repr e with Qed.Logic.Kint _ -> true | _ -> false
-
+
let rec add_pred sigma p = match F.repr p with
| And ps -> List.fold_left add_pred sigma ps
| Eq(a,b) ->
diff --git a/src/plugins/wp/MemTyped.ml b/src/plugins/wp/MemTyped.ml
index 4ee4dae4e3d..daaac67fe85 100644
--- a/src/plugins/wp/MemTyped.ml
+++ b/src/plugins/wp/MemTyped.ml
@@ -265,7 +265,7 @@ let is_separated args = F.is_true (r_separated args)
logic a : int
logic b : int
-predicate R = p.base = q.base
+predicate R = p.base = q.base
/\ (q.offset <= p.offset)
/\ (p.offset + a <= q.offset + b)
@@ -368,19 +368,19 @@ let phi_addr_of_int p =
(* -------------------------------------------------------------------------- *)
let () = Context.register
- begin fun () ->
- F.set_builtin_1 f_base phi_base ;
- F.set_builtin_1 f_offset phi_offset ;
- F.set_builtin_2 f_shift (phi_shift f_shift) ;
- F.set_builtin_eqp f_shift eq_shift ;
- F.set_builtin_eqp f_global eq_shift ;
- F.set_builtin p_separated r_separated ;
- F.set_builtin p_included r_included ;
- F.set_builtin f_havoc r_havoc ;
- F.set_builtin_get f_havoc r_get_havoc ;
- F.set_builtin_1 a_addr_of_int phi_addr_of_int ;
- F.set_builtin_1 a_int_of_addr phi_int_of_addr ;
- end
+ begin fun () ->
+ F.set_builtin_1 f_base phi_base ;
+ F.set_builtin_1 f_offset phi_offset ;
+ F.set_builtin_2 f_shift (phi_shift f_shift) ;
+ F.set_builtin_eqp f_shift eq_shift ;
+ F.set_builtin_eqp f_global eq_shift ;
+ F.set_builtin p_separated r_separated ;
+ F.set_builtin p_included r_included ;
+ F.set_builtin f_havoc r_havoc ;
+ F.set_builtin_get f_havoc r_get_havoc ;
+ F.set_builtin_1 a_addr_of_int phi_addr_of_int ;
+ F.set_builtin_1 a_int_of_addr phi_int_of_addr ;
+ end
(* -------------------------------------------------------------------------- *)
(* --- Model Parameters --- *)
@@ -707,7 +707,7 @@ module STRING = Model.Generator(LITERAL)
let fresh () =
let eid = succ (EID.get ()) in
EID.set eid ; eid
-
+
let compile (_,cst) =
let eid = fresh () in
let lfun = Lang.generated_f ~result:L.Int "Str_%d" eid in
@@ -875,7 +875,7 @@ struct
[Trigger.of_pred eqmem ; Trigger.of_term phi ] ;
[Trigger.of_pred eqmem ; Trigger.of_term phi'] ;
] ;
- l_forall = F.p_vars lemma ;
+ l_forall = F.p_vars lemma ;
l_lemma = lemma ;
l_cluster = cluster_memory () ;
}
@@ -1274,7 +1274,7 @@ let stored s obj l v =
| C_float _ -> updated s M_float l v
| C_pointer _ -> updated s M_pointer l v
| C_comp _ | C_array _ ->
- Set(loadvalue s.post obj l, v) ::
+ Set(loadvalue s.post obj l, v) ::
(List.map (fun p -> Assert p) (havoc s obj l))
let copied s obj p q = stored s obj p (loadvalue s.pre obj q)
@@ -1288,7 +1288,7 @@ let assigned_loc s obj l =
| C_int _ | C_float _ | C_pointer _ ->
let x = Lang.freshvar ~basename:"v" (Lang.tau_of_object obj) in
List.map Cvalues.equation (stored s obj l (e_var x))
- | C_comp _ | C_array _ ->
+ | C_comp _ | C_array _ ->
havoc s obj l
let equal_loc s obj l =
@@ -1462,7 +1462,7 @@ and lookup_f f es =
| RS_Field(fd,_) , [e] -> Mstate.field (lookup_lv e) fd
| RS_Shift _ , [e;k] -> Mstate.index (lookup_lv e) k
| _ -> raise Not_found
- with Not_found when es = [] ->
+ with Not_found when es = [] ->
Sigs.(Mvar (RegisterBASE.find f),[])
and lookup_lv e = try lookup_a e with Not_found -> Sigs.(Mmem e,[])
diff --git a/src/plugins/wp/Model.ml b/src/plugins/wp/Model.ml
index 996d4520bb8..041f5ec4acc 100644
--- a/src/plugins/wp/Model.ml
+++ b/src/plugins/wp/Model.ml
@@ -105,7 +105,7 @@ let register ~id ?(descr=id) ?(tuning=[]) ?(hypotheses=nohyp) () =
let get_id m = m.id
let get_descr m = m.descr
let get_hypotheses m = m.hypotheses
-
+
type scope = Kernel_function.t option
let scope : scope Context.value = Context.create "Wp.Scope"
let model : model Context.value = Context.create "Wp.Model"
@@ -232,7 +232,7 @@ struct
e.index <- MAP.remove k e.index ;
e.lock <- SET.remove k e.lock ;
end
-
+
let mem k = let e = entries () in MAP.mem k e.index || SET.mem k e.lock
let find k = let e = entries () in MAP.find k e.index
@@ -338,7 +338,7 @@ struct
e.index <- MAP.remove k e.index ;
e.lock <- SET.remove k e.lock ;
end
-
+
let mem k = let e = entries () in MAP.mem k e.index || SET.mem k e.lock
let find k = let e = entries () in MAP.find k e.index
@@ -366,7 +366,7 @@ struct
e.index <- MAP.add k d e.index ;
fire k d ;
end
-
+
let memoize f k =
let e = entries () in
try MAP.find k e.index
diff --git a/src/plugins/wp/Plang.ml b/src/plugins/wp/Plang.ml
index 7e24129a277..6b50f33ff85 100644
--- a/src/plugins/wp/Plang.ml
+++ b/src/plugins/wp/Plang.ml
@@ -20,7 +20,7 @@
(* *)
(**************************************************************************)
-open Format
+open Format
open Qed.Logic
open Qed.Engine
open Lang
@@ -37,7 +37,7 @@ type pool = {
let pool () = { vars = Vars.empty ; mark = Tset.empty }
let alloc_domain p = p.vars
-
+
let rec walk p f e =
if not (Tset.mem e p.mark) &&
not (Vars.subset (F.vars e) p.vars)
@@ -75,7 +75,7 @@ class engine =
inherit E.engine as super
inherit Lang.idprinting
method infoprover w = w.altergo
-
+
val mutable iformat : iformat = `Dec
method get_iformat = iformat
method set_iformat (f : iformat) = iformat <- f
@@ -97,7 +97,7 @@ class engine =
fprintf fmt "@[<hov 2>%a[%a]@]" self#pp_subtau t self#pp_tau k
method pp_datatype a fmt ts =
Qed.Plib.pp_call_var ~f:(self#datatype a) self#pp_tau fmt ts
-
+
(* --- Primitives --- *)
method e_true _ = "true"
@@ -128,9 +128,9 @@ class engine =
Format.fprintf fmt "%s.0" (Z.to_string num)
else
Format.fprintf fmt "(%s.0/%s)" (Z.to_string num) (Z.to_string den)
-
+
(* --- Atomicity --- *)
-
+
method callstyle = CallVar
method is_atomic e =
match F.repr e with
@@ -139,7 +139,7 @@ class engine =
| Apply _ -> true
| Aset _ | Aget _ | Fun _ -> true
| _ -> F.is_simple e
-
+
(* --- Operators --- *)
method op_spaced = Qed.Export.is_identifier
@@ -172,7 +172,7 @@ class engine =
fprintf fmt "@ else %a" self#pp_atom pelse ;
fprintf fmt "@]" ;
end
-
+
(* --- Arrays --- *)
method pp_array_cst fmt (_ : F.tau) v =
@@ -189,7 +189,7 @@ class engine =
method pp_get_field fmt a fd =
Format.fprintf fmt "%a.%s" self#pp_atom a (self#field fd)
-
+
method pp_def_fields fmt fvs =
let base,fvs = match F.record_with fvs with
| None -> None,fvs | Some(r,fvs) -> Some r,fvs in
@@ -225,7 +225,7 @@ class engine =
method pp_apply (_:cmode) (_:term) (_:formatter) (_:term list) =
failwith "Qed: higher-order application"
-
+
method pp_lambda (_:formatter) (_: (string * tau) list) =
failwith "Qed: lambda abstraction"
@@ -253,5 +253,5 @@ class engine =
(* --- Predicates --- *)
method pp_pred fmt p = self#pp_prop fmt (F.e_prop p)
-
+
end
diff --git a/src/plugins/wp/ProverScript.ml b/src/plugins/wp/ProverScript.ml
index fc9fb31807f..b253a78e790 100644
--- a/src/plugins/wp/ProverScript.ml
+++ b/src/plugins/wp/ProverScript.ml
@@ -118,7 +118,7 @@ struct
mutable backtrack : int ;
mutable backtracking : backtracking option ;
}
-
+
and backtracking = {
bk_node : ProofEngine.node ;
bk_depth : int ; (* depth of search *)
@@ -181,7 +181,7 @@ struct
bk_depth = depth ;
bk_pending = pending env ;
}
-
+
let search env node ~depth =
if env.auto <> [] && depth < env.depth && pending env < env.width
then
@@ -211,7 +211,7 @@ struct
with None -> None | Some fork -> Some (point.bk_depth,fork)
let provers env = env.provers
-
+
let make tree
~valid ~failed ~provers
~depth ~width ~backtrack ~auto
@@ -246,11 +246,11 @@ let reconcile nodes scripts =
| [] , [] -> ()
| [_,n] , [_,s] -> ProofEngine.bind n s
| _ ->
- if List.for_all (fun (k,_) -> k = "") scripts
- then zip fst_order nodes scripts
- else zip key_order
- (List.stable_sort key_order nodes)
- (List.stable_sort key_order scripts)
+ if List.for_all (fun (k,_) -> k = "") scripts
+ then zip fst_order nodes scripts
+ else zip key_order
+ (List.stable_sort key_order nodes)
+ (List.stable_sort key_order scripts)
let rec forall phi = function
| x::xs ->
@@ -277,35 +277,35 @@ let prove_node env node prv =
let rec auto env ?(depth=0) node : bool Task.task =
exists (prove_node env node) (Env.provers env) >>= fun ok ->
if ok then Task.return true else
- if depth > 0 then
- autosearch env ~depth node
- else
- begin
- autosearch env ~depth node >>= fun ok ->
- if ok then Task.return true else
- match Env.backtrack env with
- | Some (depth,fork) ->
- Env.progress env "Backtracking" ;
- autofork env ~depth fork
- | None ->
- Task.return false
- end
+ if depth > 0 then
+ autosearch env ~depth node
+ else
+ begin
+ autosearch env ~depth node >>= fun ok ->
+ if ok then Task.return true else
+ match Env.backtrack env with
+ | Some (depth,fork) ->
+ Env.progress env "Backtracking" ;
+ autofork env ~depth fork
+ | None ->
+ Task.return false
+ end
and autosearch env ~depth node : bool Task.task =
match Env.search env node ~depth with
- | None -> Task.return false
+ | None -> Task.return false
| Some fork -> autofork env ~depth fork
and autofork env ~depth fork =
- let _,children = ProofEngine.commit ~resolve:true fork in
- let pending = Env.pending env in
- if pending > 0 then
- begin
- Env.progress env (Printf.sprintf "Auto %d" pending) ;
- let depth = succ depth in
- forall (auto env ~depth) (List.map snd children)
- end
- else
+ let _,children = ProofEngine.commit ~resolve:true fork in
+ let pending = Env.pending env in
+ if pending > 0 then
+ begin
+ Env.progress env (Printf.sprintf "Auto %d" pending) ;
+ let depth = succ depth in
+ forall (auto env ~depth) (List.map snd children)
+ end
+ else
( Env.validate env ; Task.return true )
(* -------------------------------------------------------------------------- *)
@@ -313,13 +313,13 @@ and autofork env ~depth fork =
(* -------------------------------------------------------------------------- *)
let rec crawl env on_child node = function
-
+
| [] ->
let node = ProofEngine.anchor (Env.tree env) ?node () in
auto env node >>= fun ok ->
if ok then Env.validate env else Env.stuck env ;
Task.return ()
-
+
| Error(msg,json) :: alternative ->
Wp_parameters.error "@[<hov 2>Script Error %S: %a@]@." msg Json.pp json ;
crawl env on_child node alternative
@@ -461,7 +461,7 @@ let has_proof wpo =
try Hashtbl.find proofs wid
with Not_found ->
if ProofSession.exists wpo then
- let ok =
+ let ok =
try
let script = ProofScript.decode (ProofSession.load wpo) in
ProofScript.status script = 0
diff --git a/src/plugins/wp/StmtSemantics.ml b/src/plugins/wp/StmtSemantics.ml
index c8653dd8aa4..b4fb518b70e 100644
--- a/src/plugins/wp/StmtSemantics.ml
+++ b/src/plugins/wp/StmtSemantics.ml
@@ -80,7 +80,7 @@ struct
let flow =
List.fold_left (fun flow (l, n) -> LabelMap.add l n flow) env.flow lns
in { env with flow }
-
+
let (@:) env lbl =
try
LabelMap.find lbl env.flow
@@ -103,7 +103,7 @@ struct
(* -------------------------------------------------------------------------- *)
(* --- Paths & Cfg Utilities --- *)
(* -------------------------------------------------------------------------- *)
-
+
let paths_of_cfg cfg = {
paths_cfg = cfg;
paths_goals = Bag.empty;
@@ -140,9 +140,9 @@ struct
| [] -> goto (env @: Clabels.here) (env @: Clabels.next)
| [ elt ] -> f env elt
| stmt :: stmts ->
- let n = Cfg.node () in
- let paths = f (bind Clabels.next n env) stmt in
- paths @^ (sequence f (bind Clabels.here n env) stmts)
+ let n = Cfg.node () in
+ let paths = f (bind Clabels.next n env) stmt in
+ paths @^ (sequence f (bind Clabels.here n env) stmts)
let choice ?(pre=Clabels.here) ?(post=Clabels.next) f env =
let pre_node = env @: pre in
@@ -152,11 +152,11 @@ struct
let rec aux env ns = function
| [] -> goto (env @: pre) (env @: post)
| [ elt ] ->
- let n, paths = apply f env elt in
- paths @^ either pre_node (n :: ns)
+ let n, paths = apply f env elt in
+ paths @^ either pre_node (n :: ns)
| elt :: elts ->
- let n, paths = apply f env elt in
- paths @^ (aux env (n :: ns) elts)
+ let n, paths = apply f env elt in
+ paths @^ (aux env (n :: ns) elts)
in
aux env []
@@ -169,11 +169,11 @@ struct
let rec aux env ns = function
| [] -> goto (env @: pre) (env @: post)
| [ elt ] ->
- let n, (c,paths) = apply f env elt in
- paths @^ implies pre_node ((c,n) :: ns)
+ let n, (c,paths) = apply f env elt in
+ paths @^ implies pre_node ((c,n) :: ns)
| elt :: elts ->
- let n, (c,paths) = apply f env elt in
- paths @^ (aux env ((c,n) :: ns) elts)
+ let n, (c,paths) = apply f env elt in
+ paths @^ (aux env ((c,n) :: ns) elts)
in
aux env []
@@ -455,7 +455,7 @@ struct
(** TODO: Kglobal is it always Kglobal ? *)
let prop_id = WpPropId.mk_pre_id env.kf Kglobal b ip in
pre_cond env ip prop_id)
- (env @* [Clabels.next, nrequires]) b.b_requires
+ (env @* [Clabels.next, nrequires]) b.b_requires
@^ assigns (env @* [Clabels.here, nrequires; Clabels.next, nassigns]) b.b_assigns
@^ either nassigns [post_normal_behavior;post_at_exit_behavior]
@^ List.fold_left
@@ -517,39 +517,39 @@ struct
let transition
: env -> nodes -> Automata.t Interpreted_automata.transition -> paths
= fun env nodes tr ->
- let open Interpreted_automata in
- match tr with
- | Skip | Enter { blocals = [] } | Leave { blocals = [] } ->
- goto (env @: Clabels.here) (env @: Clabels.next)
- | Enter {blocals} -> scope env Sigs.Enter blocals
- | Leave {blocals} -> scope env Sigs.Leave blocals
- | Return (r,_) -> return env r
+ let open Interpreted_automata in
+ match tr with
+ | Skip | Enter { blocals = [] } | Leave { blocals = [] } ->
+ goto (env @: Clabels.here) (env @: Clabels.next)
+ | Enter {blocals} -> scope env Sigs.Enter blocals
+ | Leave {blocals} -> scope env Sigs.Leave blocals
+ | Return (r,_) -> return env r
| Prop ({kind = Assert|Invariant} as a, _) ->
- let env = Logic_label.Map.fold
- (fun logic_label vertex acc ->
- let c_label = Clabels.of_logic logic_label in
- let node = get_node nodes vertex in
- bind c_label node acc
+ let env = Logic_label.Map.fold
+ (fun logic_label vertex acc ->
+ let c_label = Clabels.of_logic logic_label in
+ let node = get_node nodes vertex in
+ bind c_label node acc
) a.labels env in
assert_ env a.predicate (WpPropId.mk_property a.property)
| Prop ({kind = Assume} as a, _)->
- let env = Logic_label.Map.fold
- (fun logic_label vertex acc ->
- let c_label = Clabels.of_logic logic_label in
- let node = get_node nodes vertex in
- bind c_label node acc
+ let env = Logic_label.Map.fold
+ (fun logic_label vertex acc ->
+ let c_label = Clabels.of_logic logic_label in
+ let node = get_node nodes vertex in
+ bind c_label node acc
) a.labels env in
assume (pred env `Negative a.predicate.ip_content) @^
- goto (env @: Clabels.here) (env @: Clabels.next)
+ goto (env @: Clabels.here) (env @: Clabels.next)
| Prop _ ->
- not_yet "[StmtSemantics] Annots other than 'assert'"
- | Guard (exp,b,_) ->
- let here = Sigma.create () in
- let cond = C.cond here exp in
- let condition = Cfg.C.create here cond in
- (if b = Then then guard else guard')
- (env @: Clabels.here) condition (env @: Clabels.next)
- | Instr (i,_) -> instr env i
+ not_yet "[StmtSemantics] Annots other than 'assert'"
+ | Guard (exp,b,_) ->
+ let here = Sigma.create () in
+ let cond = C.cond here exp in
+ let condition = Cfg.C.create here cond in
+ (if b = Then then guard else guard')
+ (env @: Clabels.here) condition (env @: Clabels.next)
+ | Instr (i,_) -> instr env i
let rec get_invariants g n (l:Automata.t Wto.partition) =
let open Interpreted_automata in
@@ -652,7 +652,7 @@ struct
partition nodes nop wto
(** connect init to here. [is_pre_main] indicate if here is the
- pre-state of main. *)
+ pre-state of main. *)
let init ~is_pre_main env =
let ninit = (env @: Clabels.init) in
let sinit = Sigma.create () in
@@ -693,8 +693,8 @@ struct
else cfg
) nop
else nop
- in
- cfg_init @^ effect ninit havoc nconst @^ consts @^ goto nconst (env @: Clabels.here)
+ in
+ cfg_init @^ effect ninit havoc nconst @^ consts @^ goto nconst (env @: Clabels.here)
let pre_spec env spec =
let pre_cond polarity env p =
diff --git a/src/plugins/wp/TacSplit.ml b/src/plugins/wp/TacSplit.ml
index f10a7d100e1..afb0697cc5f 100644
--- a/src/plugins/wp/TacSplit.ml
+++ b/src/plugins/wp/TacSplit.ml
@@ -366,14 +366,14 @@ class split =
end
| _ -> Not_applicable
end
- | Or xs ->
+ | Or xs ->
let n = List.length xs in
feedback#set_title "Split (or)" ;
feedback#set_descr "Distinguish the %d parts of the Disjunction" n ;
let hyp i n e = Printf.sprintf "Case %d/%d" i n , When (F.p_bool e) in
let cases = Tactical.mapi hyp xs in
Applicable (Tactical.replace ~at:step.id cases)
- | Eq(x,y) when (F.is_prop x)&&(F.is_prop y) ->
+ | Eq(x,y) when (F.is_prop x)&&(F.is_prop y) ->
feedback#set_title "Split (iff)";
feedback#set_descr "Decompose Equivalence into both True/False" ;
let p = F.p_bool x in
@@ -383,7 +383,7 @@ class split =
"Both False" , When F.(p_and (p_not p) (p_not q)) ;
] in
Applicable (Tactical.replace ~at:step.id cases)
- | Neq(x,y) when (F.is_prop x)&&(F.is_prop y) ->
+ | Neq(x,y) when (F.is_prop x)&&(F.is_prop y) ->
feedback#set_title "Split (xor)";
feedback#set_descr "Decompose Dis-Equivalence into alternated True/False" ;
let p = F.p_bool x in
diff --git a/src/plugins/wp/proof.ml b/src/plugins/wp/proof.ml
index 80ac0f08fd6..66f5ca87aa9 100644
--- a/src/plugins/wp/proof.ml
+++ b/src/plugins/wp/proof.ml
@@ -220,7 +220,7 @@ let find_script_for_goal ~gid ~legacy =
Some(proof,qed)
with Not_found ->
None
-
+
let update_hints_for_goal goal hints =
try
let old_hints,script,qed = Hashtbl.find scriptbase goal in
@@ -283,7 +283,7 @@ let script_for ~pid ~gid ~legacy =
let all = List.merge String.compare required hints in
update_hints_for_goal gid all ) ;
found
-
+
let rec head n = function [] -> []
| x::xs -> if n > 0 then x :: head (pred n) xs else []
diff --git a/src/plugins/wp/proof.mli b/src/plugins/wp/proof.mli
index 61a67225229..73093ed6f3f 100644
--- a/src/plugins/wp/proof.mli
+++ b/src/plugins/wp/proof.mli
@@ -33,7 +33,7 @@ val delete_script_for : gid:string -> unit
(** [delete_script ~gid] remove known script for goal. *)
val add_script_for : gid:string -> string list -> string -> string -> unit
-(** [new_script goal keys proof qed] registers the script [proof]
+(** [new_script goal keys proof qed] registers the script [proof]
terminated by [qed] for goal [gid] and keywords [keys] *)
val parse_coqproof : string -> (string * string) option
diff --git a/src/plugins/wp/wpPropId.ml b/src/plugins/wp/wpPropId.ml
index e56f25358ce..71796b10c04 100644
--- a/src/plugins/wp/wpPropId.ml
+++ b/src/plugins/wp/wpPropId.ml
@@ -31,7 +31,7 @@ open Cil_datatype
* depending on which part of the computation is involved.
* For instance, properties on loops are split in 2 parts : establishment and
* preservation.
- *)
+*)
type prop_kind =
| PKTactic (** tactical sub-goal *)
@@ -352,7 +352,7 @@ struct
Annotations.global_state ]
let size = 97
end)
-
+
let compute_ip ip =
let truncate = max 20 (Wp_parameters.TruncPropIdFileName.get ()) in
let basename = Property.Names.get_prop_basename ~truncate ip in
@@ -371,7 +371,7 @@ struct
let unique_name = compute_ip ip in
IndexTbl.add ip unique_name ;
unique_name
-
+
let get_prop_id_base p =
match p.p_kind , p.p_prop with
| (PKTactic | PKCheck | PKProp | PKPropLoop) , p -> get_ip p
--
GitLab