diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 1c81de3fe6a4ef67fef9bb0ea53a5a0f13ebe488..855cd1b3312d97a4a887f7dff4df4546b6f6f69b 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -1629,6 +1629,8 @@ src/plugins/wp/TacFilter.ml: CEA_WP
src/plugins/wp/TacFilter.mli: CEA_WP
src/plugins/wp/TacHavoc.ml: CEA_WP
src/plugins/wp/TacHavoc.mli: CEA_WP
+src/plugins/wp/TacInduction.ml: CEA_WP
+src/plugins/wp/TacInduction.mli: CEA_WP
src/plugins/wp/TacInstance.ml: CEA_WP
src/plugins/wp/TacInstance.mli: CEA_WP
src/plugins/wp/TacLemma.ml: CEA_WP
diff --git a/src/plugins/wp/Changelog b/src/plugins/wp/Changelog
index 44f1a41fa592ba989f0ad4cf32651c3d90ec1bba..c05bb98d44e9e1698c19a4752fdfdc3088c06e7c 100644
--- a/src/plugins/wp/Changelog
+++ b/src/plugins/wp/Changelog
@@ -24,6 +24,9 @@
Plugin WP <next-release>
#########################
+- WP [2020-11-05] New tactic: Induction
+- WP [2020-11-04] Removed option -wp-bits (now always enabled)
+
#########################
Plugin WP 22.0 (Titanium)
#########################
diff --git a/src/plugins/wp/Cint.ml b/src/plugins/wp/Cint.ml
index ab9d1aaa714c09cae2ff0019e63ee05542569669..5b642e95417c65194d21da73eebc461f66b0bebe 100644
--- a/src/plugins/wp/Cint.ml
+++ b/src/plugins/wp/Cint.ml
@@ -800,41 +800,40 @@ type l_builtin = {
let () =
Context.register
begin fun () ->
- if Wp_parameters.Bits.get () then
- begin
- let mk_builtin n f ?eq ?leq smp = n, { f ; eq; leq; smp } in
-
- (* From [smp_mk_bit_stdlib], the built-in [f_bit_stdlib] is such that there is
- no creation of [e_fun f_bit_stdlib args] *)
- let bi_lbit_stdlib = mk_builtin "f_bit_stdlib" f_bit_stdlib smp_mk_bit_stdlib in
- let bi_lbit = mk_builtin "f_bit" f_bit_positive smp_bitk_positive in
- let bi_lnot = mk_builtin "f_lnot" f_lnot ~eq:smp_eq_with_lnot
- (smp1 Integer.lognot) in
- let bi_lxor = mk_builtin "f_lxor" f_lxor ~eq:smp_eq_with_lxor
- (smp2 f_lxor Integer.logxor) in
- let bi_lor = mk_builtin "f_lor" f_lor ~eq:smp_eq_with_lor
- (smp2 f_lor Integer.logor) in
- let bi_land = mk_builtin "f_land" f_land ~eq:smp_eq_with_land ~leq:smp_leq_with_land
- smp_land in
- let bi_lsl = mk_builtin "f_lsl" f_lsl ~eq:smp_eq_with_lsl ~leq:smp_leq_with_lsl
- (smp_shift Integer.shift_left) in
- let bi_lsr = mk_builtin "f_lsr" f_lsr ~eq:smp_eq_with_lsr ~leq:smp_leq_with_lsr
- (smp_shift Integer.shift_right) in
-
- List.iter
- begin fun (_name, { f; eq; leq; smp }) ->
- F.set_builtin f smp ;
- (match eq with
- | None -> ()
- | Some eq -> F.set_builtin_eq f eq);
- (match leq with
- | None -> ()
- | Some leq -> F.set_builtin_leq f leq)
- end
- [bi_lbit_stdlib ; bi_lbit; bi_lnot; bi_lxor; bi_lor; bi_land; bi_lsl; bi_lsr];
+ begin
+ let mk_builtin n f ?eq ?leq smp = n, { f ; eq; leq; smp } in
+
+ (* From [smp_mk_bit_stdlib], the built-in [f_bit_stdlib] is such that there is
+ no creation of [e_fun f_bit_stdlib args] *)
+ let bi_lbit_stdlib = mk_builtin "f_bit_stdlib" f_bit_stdlib smp_mk_bit_stdlib in
+ let bi_lbit = mk_builtin "f_bit" f_bit_positive smp_bitk_positive in
+ let bi_lnot = mk_builtin "f_lnot" f_lnot ~eq:smp_eq_with_lnot
+ (smp1 Integer.lognot) in
+ let bi_lxor = mk_builtin "f_lxor" f_lxor ~eq:smp_eq_with_lxor
+ (smp2 f_lxor Integer.logxor) in
+ let bi_lor = mk_builtin "f_lor" f_lor ~eq:smp_eq_with_lor
+ (smp2 f_lor Integer.logor) in
+ let bi_land = mk_builtin "f_land" f_land ~eq:smp_eq_with_land ~leq:smp_leq_with_land
+ smp_land in
+ let bi_lsl = mk_builtin "f_lsl" f_lsl ~eq:smp_eq_with_lsl ~leq:smp_leq_with_lsl
+ (smp_shift Integer.shift_left) in
+ let bi_lsr = mk_builtin "f_lsr" f_lsr ~eq:smp_eq_with_lsr ~leq:smp_leq_with_lsr
+ (smp_shift Integer.shift_right) in
+
+ List.iter
+ begin fun (_name, { f; eq; leq; smp }) ->
+ F.set_builtin f smp ;
+ (match eq with
+ | None -> ()
+ | Some eq -> F.set_builtin_eq f eq);
+ (match leq with
+ | None -> ()
+ | Some leq -> F.set_builtin_leq f leq)
+ end
+ [bi_lbit_stdlib ; bi_lbit; bi_lnot; bi_lxor; bi_lor; bi_land; bi_lsl; bi_lsr];
- Lang.For_export.set_builtin_eq f_land export_eq_with_land
- end
+ Lang.For_export.set_builtin_eq f_land export_eq_with_land
+ end
end
(* ACSL Semantics *)
diff --git a/src/plugins/wp/Conditions.mli b/src/plugins/wp/Conditions.mli
index 878a73afc7608f9025682971c2580694a1aaf5c9..3e6aa0e00a2f60811af8053cbc273ec3539c9538 100644
--- a/src/plugins/wp/Conditions.mli
+++ b/src/plugins/wp/Conditions.mli
@@ -142,7 +142,7 @@ val map_sequence : (pred -> pred) -> sequence -> sequence
(** Rewrite all root predicates in sequence *)
val map_sequent : (pred -> pred) -> sequent -> sequent
-(** Rewrite all root predocates in hypotheses and goal *)
+(** Rewrite all root predicates in hypotheses and goal *)
val insert : ?at:int -> step -> sequent -> sequent
(** Insert a step in the sequent immediately [at] the specified position.
diff --git a/src/plugins/wp/GuiTactic.ml b/src/plugins/wp/GuiTactic.ml
index 0edcc8430adf32d77818ab7f4fc51f6f5345aae4..550a6caed14f304d3c20aae06570cec7a5b2f9ed 100644
--- a/src/plugins/wp/GuiTactic.ml
+++ b/src/plugins/wp/GuiTactic.ml
@@ -198,6 +198,7 @@ class mkcomposer
Wutil.on filter (fun f -> wvalid <- f) ;
Wutil.on range (fun r -> ranged <- r) ;
ignore vmin ; ignore vmax ;
+ self#updated
end
end
diff --git a/src/plugins/wp/Makefile.in b/src/plugins/wp/Makefile.in
index 22e89bcbd9090137e7b584cab41d32f51ef0731b..2f7ebfb458abb852409764942639b31e831e2e90 100644
--- a/src/plugins/wp/Makefile.in
+++ b/src/plugins/wp/Makefile.in
@@ -85,7 +85,7 @@ PLUGIN_CMO:= \
CfgCompiler StmtSemantics \
VCS script proof wpo wpReport \
Footprint Tactical Strategy \
- TacSplit TacChoice TacRange \
+ TacSplit TacChoice TacRange TacInduction \
TacArray TacCompound TacUnfold \
TacHavoc TacInstance TacLemma \
TacFilter TacCut WpTac TacNormalForm \
diff --git a/src/plugins/wp/TacInduction.ml b/src/plugins/wp/TacInduction.ml
new file mode 100644
index 0000000000000000000000000000000000000000..630d6be6e535abfb3efd0624598165bb5c46d674
--- /dev/null
+++ b/src/plugins/wp/TacInduction.ml
@@ -0,0 +1,119 @@
+(**************************************************************************)
+(* *)
+(* This file is part of WP plug-in of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2020 *)
+(* CEA (Commissariat a l'energie atomique et aux energies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open Lang
+
+type env = {
+ n : F.var ;
+ sigma : F.sigma ;
+ mutable hind : F.pred list ;
+}
+
+let rec strip env p =
+ match F.p_expr p with
+ | And ps -> F.p_all (strip env) ps
+ | _ ->
+ let p = F.p_subst env.sigma p in
+ if F.occursp env.n p then
+ ( env.hind <- p :: env.hind ; F.p_true )
+ else p
+
+let process value n0 seq =
+
+ (* Transfrom seq into: hyps => (forall n, goal) *)
+ let n = Lang.freshvar ~basename:"n" Qed.Logic.Int in
+ let i = Lang.freshvar ~basename:"i" Qed.Logic.Int in
+ let vn = F.e_var n in
+ let vi = F.e_var i in
+ let sigma = Lang.sigma () in
+ F.Subst.add sigma value vn ;
+ let env = { n ; sigma ; hind = [] } in
+ let hyps = Conditions.map_sequence (strip env) (fst seq) in
+ let goal_n = F.p_hyps env.hind @@ F.p_subst sigma (snd seq) in
+ let goal_i = F.p_subst_var n vi goal_n in
+
+ (* Base: n = n0 *)
+ let goal_base = F.p_imply (F.p_equal vn n0) goal_n in
+
+ (* Hind: n0 <= i < n *)
+ let goal_sup =
+ let hsup = [ F.p_leq n0 vi ; F.p_lt vi vn ] in
+ let hind = F.p_forall [i] (F.p_hyps hsup goal_i) in
+ F.p_hyps [F.p_lt n0 vn; hind] goal_n in
+
+ (* Hind: n < i <= n0 *)
+ let goal_inf =
+ let hinf = [ F.p_lt vn vi ; F.p_leq vi n0 ] in
+ let hind = F.p_forall [i] (F.p_hyps hinf goal_i) in
+ F.p_hyps [F.p_lt vn n0; hind] goal_n in
+
+ (* All Cases *)
+ List.map (fun (name,goal) -> name , (hyps,goal)) [
+ "Base" , goal_base ;
+ "Induction (sup)" , goal_sup ;
+ "Induction (inf)" , goal_inf ;
+ ]
+
+(* -------------------------------------------------------------------------- *)
+(* --- Induction Tactical --- *)
+(* -------------------------------------------------------------------------- *)
+
+let vbase,pbase = Tactical.composer ~id:"base"
+ ~title:"Base" ~descr:"Value of base case" ()
+
+class induction =
+ object(self)
+ inherit Tactical.make
+ ~id:"Wp.induction"
+ ~title:"Induction"
+ ~descr:"Proof by integer induction"
+ ~params:[pbase]
+
+ method private get_base () =
+ match self#get_field vbase with
+ | Tactical.Compose(Code(t, _, _))
+ | Inside(_, t) when Lang.F.typeof t = Lang.t_int ->
+ Some t
+ | Compose(Cint i) ->
+ Some (Lang.F.e_bigint i)
+ | _ ->
+ None
+
+ method select feedback (s : Tactical.selection) =
+ begin match self#get_field vbase with
+ | Empty ->
+ self#set_field vbase (Tactical.int 0) ;
+ feedback#update_field vbase
+ | _ -> ()
+ end ;
+ let value = Tactical.selected s in
+ if F.is_int value then
+ match self#get_base () with
+ | Some base -> Applicable(process value base)
+ | None -> Not_configured
+ else Not_applicable
+
+ end
+
+let tactical = Tactical.export (new induction)
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/TacInduction.mli b/src/plugins/wp/TacInduction.mli
new file mode 100644
index 0000000000000000000000000000000000000000..21c817a0b338fb729bb658c15ecfe0cb907526b8
--- /dev/null
+++ b/src/plugins/wp/TacInduction.mli
@@ -0,0 +1,29 @@
+(**************************************************************************)
+(* *)
+(* This file is part of WP plug-in of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2020 *)
+(* CEA (Commissariat a l'energie atomique et aux energies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(** Built-in Range Tactical (auto-registered) *)
+
+open Tactical
+
+val tactical : tactical
+
+(**************************************************************************)
diff --git a/src/plugins/wp/cfgWP.ml b/src/plugins/wp/cfgWP.ml
index 0a837cbf7378b488a8eb1bea384c7b4b93c72326..cffc2b552ff4bd455dfd384d366a042954c8c13a 100644
--- a/src/plugins/wp/cfgWP.ml
+++ b/src/plugins/wp/cfgWP.ml
@@ -90,7 +90,7 @@ struct
(* Authorized written region from an assigns specification *)
type effect = {
e_pid : P.t ; (* Assign Property *)
- e_kind : a_kind ; (* Requires post effects (in case of loop-assigns) *)
+ e_post : bool ; (* Requires post effects (loop-assigns or post-assigns) *)
e_label : c_label ; (* scope for collection *)
e_valid : L.sigma ; (* sigma where locations are filtered for validity *)
e_region : L.region ; (* expected from spec *)
@@ -444,21 +444,23 @@ struct
ainfo.a_assigns
in match authorized_region with
| None -> None
- | Some region -> Some {
- e_pid = pid ;
- e_kind = ainfo.a_kind ;
- e_label = from ;
- e_valid = sigma ;
- e_region = region ;
- e_warn = Warning.Set.empty ;
- }
+ | Some region ->
+ let post = match ainfo.a_kind with
+ | LoopAssigns -> true
+ | StmtAssigns -> NormAtLabels.has_postassigns ainfo.a_assigns
+ in Some {
+ e_pid = pid ;
+ e_post = post ;
+ e_label = from ;
+ e_valid = sigma ;
+ e_region = region ;
+ e_warn = Warning.Set.empty ;
+ }
let cc_posteffect e vcs =
- match e.e_kind with
- | StmtAssigns -> vcs
- | LoopAssigns ->
- let vc = { empty_vc with vars = L.vars e.e_region } in
- Gmap.add (Gposteffect e.e_pid) (Splitter.singleton vc) vcs
+ if not e.e_post then vcs else
+ let vc = { empty_vc with vars = L.vars e.e_region } in
+ Gmap.add (Gposteffect e.e_pid) (Splitter.singleton vc) vcs
(* -------------------------------------------------------------------------- *)
(* --- WP RULES : adding axioms, hypotheses and goals --- *)
@@ -549,14 +551,13 @@ struct
vars = xs }
in
let group =
- match e.e_kind with
- | StmtAssigns ->
- Splitter.singleton (setup empty_vc)
- | LoopAssigns ->
- try Splitter.map setup (Gmap.find (Gposteffect e.e_pid) vcs)
- with Not_found ->
- Wp_parameters.fatal "Missing post-effect for %a"
- WpPropId.pretty e.e_pid
+ if not e.e_post then
+ Splitter.singleton (setup empty_vc)
+ else
+ try Splitter.map setup (Gmap.find (Gposteffect e.e_pid) vcs)
+ with Not_found ->
+ Wp_parameters.fatal "Missing post-effect for %a"
+ WpPropId.pretty e.e_pid
in
let target = match sloc with
| None -> Gprop e.e_pid
diff --git a/src/plugins/wp/clabels.ml b/src/plugins/wp/clabels.ml
index c9f7ecf037f95fc9b6ef920628cf923778d33d05..f9e26a0db028f01cb19e437f3fc277cacd4f1fd5 100644
--- a/src/plugins/wp/clabels.ml
+++ b/src/plugins/wp/clabels.ml
@@ -74,6 +74,11 @@ let of_logic = function
| BuiltinLabel LoopEntry -> loopentry
| StmtLabel s -> stmt !s
+let is_post = function
+ | BuiltinLabel Post -> true
+ | FormalLabel a -> a = post
+ | _ -> false
+
let name = function FormalLabel a -> a | _ -> ""
let lookup labels a =
diff --git a/src/plugins/wp/clabels.mli b/src/plugins/wp/clabels.mli
index 26bdbfb4fcbdce2eb8ea16e372f9147ba91b926e..33812ec5f1377b696943adbbdfbd50cb110555cf 100644
--- a/src/plugins/wp/clabels.mli
+++ b/src/plugins/wp/clabels.mli
@@ -65,6 +65,9 @@ val of_logic : Cil_types.logic_label -> c_label
labels. Ambiguous labels are: Old, LoopEntry and LoopCurrent, since
they points to different program points dependending on the context. *)
+val is_post : Cil_types.logic_label -> bool
+(** Checks whether the logic-label is [Post] or [to_logic post] *)
+
val pretty : Format.formatter -> c_label -> unit
open Cil_types
diff --git a/src/plugins/wp/doc/manual/wp_plugin.tex b/src/plugins/wp/doc/manual/wp_plugin.tex
index d72e45d025b283b8c21b9b21886431de6233473e..c85ce39e4a49fcb2189c3635009f6b597231acf1 100644
--- a/src/plugins/wp/doc/manual/wp_plugin.tex
+++ b/src/plugins/wp/doc/manual/wp_plugin.tex
@@ -251,26 +251,43 @@ c. Consolidating the Bench.
This mode replays the automated proofs and the interactive ones, re-running Alt-Ergo on every \textsf{WP} goals and every proof tactic sub-goals. The user scripts are never modified — this is a replay mode only.
-\clearpage
-\subsection{Available Tactics}
+\subsection{Strategies}
+
+Strategies are heuristics that generate a prioritized bunch of tactics to be tried on the current goal.
+Few built-in strategies are provided by the \textsf{WP} plug-in ; however, the user can extends the proof editor with
+custom ones, as explained in section~\ref{wp-custom-tactics} below.
+
+To run strategies, the interactive proof editor provide a single button \texttt{Strategies} in the tactic panel.
+Configure the heuristics you want to include in your try, then click the button. The generated with highest priority is immediately applied. The proof summary now display \texttt{backtrack} buttons revealing proof nodes where alternative tactics are available. You can use those backtracking button to cycle over the generated tactics.
+
+Of course, strategies are meant to be used multiple times, in sequence. Recall that strategies apply highest priority tactic first, on the current goal. When using strategies several times, you shall see several \texttt{backtrack}ing buttons in your proof script. You backtrack from any point at any time.
+
+You shall also alternate strategies \emph{and} manually triggered tactics. Though, strategies are only used to
+\emph{infer} or \emph{suggest} interesting tactics to the user. Once your are finished with your proved, only the tactics are saved in the script, not the strategies used to find them. Hence, replaying a script generated with strategies would not involve backtracking any more. The script will directly replay your chosen alternatives.
+
+It is also possible to call strategies from the command line, with option \texttt{-wp-auto}. The strategies are tried up to some depth, and while a limited number of pending goals
+remains unproved by \textsf{Qed} or the selected provers. More precisely:
+\begin{description}
+\item[\tt -wp-auto s,...] applies strategies \texttt{s,...} recursively to unproved goals.
+\item[\tt -wp-auto-depth <$n$>] limit recursive application of strategies to depth $n$ (default is 5).
+\item[\tt -wp-auto-width <$n$>] limit application of strategies when there is less than $n$ pending goals (default is 10).
+\item[\tt -wp-auto-backtrack <$n$>] when the first tried strategies do not close a branch, allows for backtracking
+ on $n$ alternative strategies. Backtracking is performed on goals which are closed to the root proof obligation, hence
+ performing a kind of width-first search strategy, which tends to be more efficient in practice.
+ Backtracking is deactivated by default ($n=0$) and only used when \verb+-wp-auto+ is set.
+\end{description}
+
+The name of registered strategies is printed on console by using \texttt{-wp-auto '?'}. Custom strategies can be loaded by plug-ins, see below.
\newcommand{\TACTIC}[2]{#1\quad\quad\triangleright\quad\quad#2}
+\subsection{General Tactics}
+
\paragraph{Absurd} Contradict a Hypothesis\\
The user can select a hypothesis $H$, and change the goal to $\neg H$:
$$ \TACTIC{\Delta,H\models\,G}{\Delta\models\,\neg H} $$
-
-\paragraph{Array} Decompose array access-update patterns\\
-The use select an expression $e\equiv a[k_1\mapsto v][k_2]$. Then:
-
-$$ \TACTIC{\Delta\models\,G}{%
-\begin{array}[t]{ll}
-\Delta,\,k_1=k_2,\,e = v &\models G \\
-\Delta,\,k_1\neq k_2,\,e = a[k_2] &\models G
-\end{array}} $$
-
\paragraph{Choice} Select a Goal Alternative\\
When the goal is a disjunction, the user select one alternative and discard the others:
$$ \TACTIC{\Delta\models\,\Gamma,G}{\Delta\models\,G} $$
@@ -280,7 +297,6 @@ When the user select an equality between two records, it is decomposed field by
$$ \TACTIC{ a = b }{ \bigwedge a.f_i = b.f_i } $$
-
\paragraph{Contrapose} Swap and Negate Hypothesis with Conclusion\\
The user select a hypothesis (typically, a negation) and swap it with the goal.
$$ \TACTIC{\Delta,H\models\,G}{\Delta,\neg G\models\,\neg H} $$
@@ -303,14 +319,14 @@ $$\TACTIC{\Delta\models\,G}{%
\Delta,\neg C \models G
\end{array}} $$
+\paragraph{Definition} Unfold predicate and logic function definition\\
+The user simply select a term $f(e_1,\ldots,e_n)$ or a predicate $P(e_1,\ldots,e_n)$ which is replaced by its definition, when available.
+
\paragraph{Filter} Erase Hypotheses \\
The tactic is always applicable. It removes hypotheses from the goal on a variable used basis. When variables are compounds (record and arrays) a finer heuristics is used to detect which parts of the variable is relevant. A transitive closure of dependencies is also used. However, it is always possible that too many hypotheses are removed.
The tactic also have a variant where only hypotheses \emph{not relevant} to the goal are retained. This is useful to find absurd hypotheses that are completely disjoint from the goal.
-\paragraph{Havoc} Go Through Assigns \\
-This is a variant of the \texttt{Lemma} tactic dedicated to \texttt{Havoc} predicate generate by complex assigns clause. The user select an address, and if the address is not assigned by the \texttt{Havoc} clause, the memory at this address is unchanged.
-
\paragraph{Instance} Instantiate properties\\
The user selects a hypothesis with one or several $\forall$ quantifiers, or an $\exists$ quantified goal. Then, with the composer, the use choose to instantiate one or several of the quantified parameters. In case of $\forall$ quantifier over integer, a range of values can be instantiated instead.
@@ -323,22 +339,11 @@ $$\TACTIC{\Delta,\,\forall x\, P(x)\models G}{\Delta,P(n)\ldots P(m)\models G}$$
When instantiating a goal with an expression $e$:
$$\TACTIC{\Delta\models \exists x\,G(x)}{\Delta\models G(e)}$$
-\paragraph{Lemma} Search \& Instantiate Lemma\\
-The user start by selecting a term in the goal. Then, the search button in the tactic panel will display a list of lemma related to the term. Then, he can instantiate the parameters of the lemma, like with the Instance tactic.
-
\paragraph{Intuition} Decompose with Conjunctive/Disjunctive Normal Form\\
The user can select a hypothesis or a goal with nested conjunctions and disjunctions. The tactics then computes the conjunctive or disjunctive normal form of the selection and split the goal accordingly.
-\paragraph{Range} Enumerate a range of values for an integer term\\
-The user select any integer expression $e$ in the proof, and a range of numerical values $a\ldots b$. The proof goes by case for each $e=a\ldots e=b$, plus the side cases $e<a$ and $e>b$:
-$$\TACTIC{\Delta\models\,G}{%
-\begin{array}[t]{ll}
-\Delta,e<a &\models G \\
-\Delta,e=a &\models G \\
-&\vdots \\
-\Delta,e=b &\models G \\
-\Delta,e>b &\models G
-\end{array}} $$
+\paragraph{Lemma} Search \& Instantiate Lemma\\
+The user start by selecting a term in the goal. Then, the search button in the tactic panel will display a list of lemma related to the term. Then, he can instantiate the parameters of the lemma, like with the Instance tactic.
\paragraph{Rewrite} Replace Terms\\
This tactic uses an equality in a hypothesis to replace each occurrence of term by another one.
@@ -348,9 +353,6 @@ The original equality hypothesis is removed from the goal.
$$\TACTIC{\Delta,a=b\models\,G}{\Delta[a\leftarrow b]\models\,G[a\leftarrow b]}$$
-\paragraph{Separated} Expand Separation Cases\\
-This tactic decompose a \texttt{separated}$(a,n,b,m)$ predicate into its four base cases: $a$ and $b$ have different bases, $a+n \leq b$, $b+m \leq a$, and $a[0..n-1]$ and $b[0..m-1]$ overlaps. The regions are separated in the first three cases, and not separated in the overlapping case. This is kind of normal disjunctive form of the separation clause.
-
\paragraph{Split} Decompose Logical Connectives and Conditionals\\
This is the most versatile available tactic. It decompose merely any logical operator following the sequent calculus rules. Typically:
@@ -376,7 +378,8 @@ When the user selects a arbitrary boolean expression $e$, the tactic is similar
\Delta,\neg e\models G
\end{array}} \]
-Finally, when the user select a arithmetic comparison over $a$ and $b$, the tactics makes a split over $a=b$, $a<b$ and $a>b$:
+Finally, when the user select a arithmetic comparison over $a$ and $b$,
+the tactics makes a split over $a=b$, $a<b$ and $a>b$:
\[\TACTIC{\Delta\models\,G}{%
\begin{array}[t]{ll}
\Delta,a<b&\models G \\
@@ -384,49 +387,7 @@ Finally, when the user select a arithmetic comparison over $a$ and $b$, the tact
\Delta,a>b&\models G
\end{array}} \]
-\paragraph{Definition} Unfold predicate and logic function definition\\
-The user simply select a term $f(e_1,\ldots,e_n)$ or a predicate $P(e_1,\ldots,e_n)$ which is replaced by its definition, when available.
-
-\paragraph{Bitwise} Decompose equalities over $N$-bits\\
-The use selects an integer equality and a number of bits.
-Providing the two members of the equality are in range $0..2^N-1$,
-the equality is decomposed into $N$ bit-tests equalities:
-\[\TACTIC{\Delta\models G}{%
-\begin{array}[t]{rcl}
-\Delta\phantom{)} &\models & 0 \leq a,b < 2^N \\
-\sigma(\Delta) & \models & \sigma(G)
-\end{array}
-}\]
-where $\sigma$ is the following subsitution:
-\[ \sigma \equiv
-\left[ a=b \quad \leftarrow
-\bigwedge_{k\in 0..N-1} \mathtt{bit\_test}(a,k) = \mathtt{bit\_test}(b,k)
-\right]
-\]
-
-The \lstinline{bit_test(a,b)} function is predefined in \textsf{WP} and is equivalent
-to the \textsf{ACSL} expression \lstinline{(a & (1 << k)) != 0}. The
-\textsf{Qed}Â engine has many simplification rules that applies to
-such patterns, and the a tactic is good way to reason over bits.
-
-\paragraph{Shift} Transform logical shifts into arithmetics\\
-For positive integers, logical shifts such as \lstinline{a << k}
-and \lstinline{a >> k} where \lstinline$k$ is a constant can be interpreted into a multiplication or a division by $2^k$.
-
-When selecting a logical-shift, the tactic performs:
-\[\TACTIC{\Delta\models G}{%
-\begin{array}[t]{rcl}
-\Delta\phantom{)} &\models& 0 \leq a \\
-\sigma(\Delta) &\models& \sigma(G)
-\end{array}
-}\]
-where:
-\begin{tabular}[t]{ll}
-$\sigma = [ \mathtt{lsl}(a,k) \leftarrow a * 2^k ]$ &
-for left-shift, \\
-$\sigma = [ \mathtt{lsr}(a,k) \leftarrow a / 2^k ]$ &
-for right-shifts.
-\end{tabular}
+\subsection{Integers \& Bit-wised Tactics}
\paragraph{BitRange} Range of logical bitwise operators \\
This tactical applies the two following lemmas to the current goal.
@@ -453,6 +414,28 @@ to apply the theorems. Such a strategy is \emph{not} complete in general.
Typically, $\mathtt{land}(x,y) < 38$ is true whenever both $x$ and $y$ are in range $0\ldots 31$, but this is also true
in other cases.
+\paragraph{Bitwise} Decompose equalities over $N$-bits\\
+The use selects an integer equality and a number of bits.
+Providing the two members of the equality are in range $0..2^N-1$,
+the equality is decomposed into $N$ bit-tests equalities:
+\[\TACTIC{\Delta\models G}{%
+\begin{array}[t]{rcl}
+\Delta\phantom{)} &\models & 0 \leq a,b < 2^N \\
+\sigma(\Delta) & \models & \sigma(G)
+\end{array}
+}\]
+where $\sigma$ is the following subsitution:
+\[ \sigma \equiv
+\left[ a=b \quad \leftarrow
+\bigwedge_{k\in 0..N-1} \mathtt{bit\_test}(a,k) = \mathtt{bit\_test}(b,k)
+\right]
+\]
+
+The \lstinline{bit_test(a,b)} function is predefined in \textsf{WP} and is equivalent
+to the \textsf{ACSL} expression \lstinline{(a & (1 << k)) != 0}. The
+\textsf{Qed}Â engine has many simplification rules that applies to
+such patterns, and the a tactic is good way to reason over bits.
+
\paragraph{Congruence} Simplify Divisions and Products \\
This tactic rewrites integer comparisons involving products and divisions.
The tactic applies one of the following theorems to the current goal.
@@ -470,8 +453,23 @@ n|k, n|k', & (k/n).a = (k'/n).b &\Longleftrightarrow& k.a = k'.b
\end{array}
\]
+\paragraph{Induction} Start a proof by integer induction \\
+The user select any integer expression $e$ in the proof and a base value $b$ (which defaults to
+0). The tactic generates a proof by induction on $e$, that is, the base case
+$e = b$ and then the cases $e < b$ and $b < e$. Formally, the initial goal
+$\Delta_0\models\,G_0$ is first generalized into $\Delta,P(e)\models\,Q(e)$. The tactic
+then proceed by (strong) induction over $n$ for
+$G(n) \equiv P(n)\Longrightarrow\,Q(n)$:
+
+\[\TACTIC{\Delta\models\,G(n)}{%
+\begin{array}[t]{lll}
+\Delta,\; \quad n = b & \models G(n) \\
+\Delta,\; \forall i,\, b \leq i < n \Longrightarrow G(i) \; & \models G(n) \\
+\Delta,\; \forall i,\, n < i \leq b \Longrightarrow G(i) \; & \models G(n)
+\end{array}} \]
+
\paragraph{Overflow} Integer Conversions \\
-This tactic rewrites machine integer conversions by identify,
+This tactic rewrites machine integer conversions by identity,
providing the converted value is in available range. The tactic applies on expression
with pattern $\mathtt{to\_iota(e)}$ where \texttt{iota} is a a machine-integer name,
\emph{eg.} \texttt{to\_uint32}.
@@ -485,33 +483,54 @@ with pattern $\mathtt{to\_iota(e)}$ where \texttt{iota} is a a machine-integer n
where $\sigma = [ \mathtt{to\_iota}(e) \mapsto e ]$ and $[a..b]$ is the range
of the \texttt{iota} integer domain.
-\subsection{Strategies}
+\paragraph{Range} Enumerate a range of values for an integer term\\
+The user select any integer expression $e$ in the proof, and a range of numerical values $a\ldots b$. The proof goes by case for each $e=a\ldots e=b$, plus the side cases $e<a$ and $e>b$:
+$$\TACTIC{\Delta\models\,G}{%
+\begin{array}[t]{ll}
+\Delta,e<a &\models G \\
+\Delta,e=a &\models G \\
+&\vdots \\
+\Delta,e=b &\models G \\
+\Delta,e>b &\models G
+\end{array}} $$
-Strategies are heuristics that generate a prioritized bunch of tactics to be tried on the current goal.
-Few built-in strategies are provided by the \textsf{WP} plug-in ; however, the user can extends the proof editor with
-custom ones, as explained in section~\ref{wp-custom-tactics} below.
+\paragraph{Shift} Transform logical shifts into arithmetics\\
+For positive integers, logical shifts such as \lstinline{a << k}
+and \lstinline{a >> k} where \lstinline$k$ is a constant can be interpreted into a multiplication or a division by $2^k$.
-To run strategies, the interactive proof editor provide a single button \texttt{Strategies} in the tactic panel.
-Configure the heuristics you want to include in your try, then click the button. The generated with highest priority is immediately applied. The proof summary now display \texttt{backtrack} buttons revealing proof nodes where alternative tactics are available. You can use those backtracking button to cycle over the generated tactics.
+When selecting a logical-shift, the tactic performs:
+\[\TACTIC{\Delta\models G}{%
+\begin{array}[t]{rcl}
+\Delta\phantom{)} &\models& 0 \leq a \\
+\sigma(\Delta) &\models& \sigma(G)
+\end{array}
+}\]
+where:
+\begin{tabular}[t]{ll}
+$\sigma = [ \mathtt{lsl}(a,k) \leftarrow a * 2^k ]$ &
+for left-shift, \\
+$\sigma = [ \mathtt{lsr}(a,k) \leftarrow a / 2^k ]$ &
+for right-shifts.
+\end{tabular}
-Of course, strategies are meant to be used multiple times, in sequence. Recall that strategies apply highest priority tactic first, on the current goal. When using strategies several times, you shall see several \texttt{backtrack}ing buttons in your proof script. You backtrack from any point at any time.
+\subsection{Domain Specific Tactics}
-You shall also alternate strategies \emph{and} manually triggered tactics. Though, strategies are only used to
-\emph{infer} or \emph{suggest} interesting tactics to the user. Once your are finished with your proved, only the tactics are saved in the script, not the strategies used to find them. Hence, replaying a script generated with strategies would not involve backtracking any more. The script will directly replay your chosen alternatives.
+\paragraph{Array} Decompose array access-update patterns\\
+The use select an expression $e\equiv a[k_1\mapsto v][k_2]$. Then:
-It is also possible to call strategies from the command line, with option \texttt{-wp-auto}. The strategies are tried up to some depth, and while a limited number of pending goals
-remains unproved by \textsf{Qed} or the selected provers. More precisely:
-\begin{description}
-\item[\tt -wp-auto s,...] applies strategies \texttt{s,...} recursively to unproved goals.
-\item[\tt -wp-auto-depth <$n$>] limit recursive application of strategies to depth $n$ (default is 5).
-\item[\tt -wp-auto-width <$n$>] limit application of strategies when there is less than $n$ pending goals (default is 10).
-\item[\tt -wp-auto-backtrack <$n$>] when the first tried strategies do not close a branch, allows for backtracking
- on $n$ alternative strategies. Backtracking is performed on goals which are closed to the root proof obligation, hence
- performing a kind of width-first search strategy, which tends to be more efficient in practice.
- Backtracking is deactivated by default ($n=0$) and only used when \verb+-wp-auto+ is set.
-\end{description}
+\[
+\TACTIC{\Delta\models\,G}{%
+\begin{array}[t]{ll}
+\Delta,\,k_1=k_2,\,e = v &\models G \\
+\Delta,\,k_1\neq k_2,\,e = a[k_2] &\models G
+\end{array}
+}\]
-The name of registered strategies is printed on console by using \texttt{-wp-auto '?'}. Custom strategies can be loaded by plug-ins, see below.
+\paragraph{Havoc} Go Through Assigns \\
+This is a variant of the \texttt{Lemma} tactic dedicated to \texttt{Havoc} predicate generate by complex assigns clause. The user select an address, and if the address is not assigned by the \texttt{Havoc} clause, the memory at this address is unchanged.
+
+\paragraph{Separated} Expand Separation Cases\\
+This tactic decompose a \texttt{separated}$(a,n,b,m)$ predicate into its four base cases: $a$ and $b$ have different bases, $a+n \leq b$, $b+m \leq a$, and $a[0..n-1]$ and $b[0..m-1]$ overlaps. The regions are separated in the first three cases, and not separated in the overlapping case. This is kind of normal disjunctive form of the separation clause.
\subsection{Custom Tactics and Strategies}
\label{wp-custom-tactics}
diff --git a/src/plugins/wp/normAtLabels.ml b/src/plugins/wp/normAtLabels.ml
index bb41fa3dcc6df86fe0ec09c7535d61c721de45a2..197b12f968517c08056b5183ade17088df4863a3 100644
--- a/src/plugins/wp/normAtLabels.ml
+++ b/src/plugins/wp/normAtLabels.ml
@@ -210,9 +210,27 @@ let preproc_assigns labels asgns =
let visitor = new norm_at labels in
List.map (Visitor.visitFramacFrom visitor) asgns
+let has_postassigns = function
+ | WritesAny -> false
+ | Writes froms ->
+ let exception HAS_POST in
+ let visitor = new norm_at (fun l ->
+ if Clabels.is_post l then raise HAS_POST
+ else Clabels.of_logic l
+ ) in
+ try
+ List.iter
+ (fun fr -> ignore @@ Visitor.visitFramacFrom visitor fr)
+ froms ;
+ false
+ with HAS_POST ->
+ true
+
let catch_label_error ex txt1 txt2 = match ex with
| LabelError lab ->
Wp_parameters.warning
"Unexpected label %a in %s : ignored %s"
Wp_error.pp_logic_label lab txt1 txt2
| _ -> raise ex
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/normAtLabels.mli b/src/plugins/wp/normAtLabels.mli
index 14b653d70999ee5479a490f546d475601b2726df..0dd24f825450e8170399fcf7ab9f0de90b6fd320 100644
--- a/src/plugins/wp/normAtLabels.mli
+++ b/src/plugins/wp/normAtLabels.mli
@@ -42,5 +42,5 @@ val labels_predicate : (logic_label * logic_label) list -> label_mapping
val labels_axiom : label_mapping
val preproc_annot : label_mapping -> predicate -> predicate
-
val preproc_assigns : label_mapping -> from list -> from list
+val has_postassigns : assigns -> bool
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/postassigns.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/postassigns.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..8abc928d33f1abe77a4033024acc964ece36ba7c
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle/postassigns.res.oracle
@@ -0,0 +1,230 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_acsl/postassigns.c (with preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+ Function job1
+------------------------------------------------------------
+
+Goal Post-condition (file tests/wp_acsl/postassigns.c, line 4) in 'job1':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_acsl/postassigns.c, line 5) in 'job1' (1/9):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_acsl/postassigns.c, line 5) in 'job1' (2/9):
+Effect at line 10
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_acsl/postassigns.c, line 5) in 'job1' (3/9):
+Effect at line 10
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_acsl/postassigns.c, line 5) in 'job1' (4/9):
+Effect at line 11
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_acsl/postassigns.c, line 5) in 'job1' (5/9):
+Effect at line 11
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_acsl/postassigns.c, line 5) in 'job1' (6/9):
+Effect at line 12
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_acsl/postassigns.c, line 5) in 'job1' (7/9):
+Effect at line 12
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_acsl/postassigns.c, line 5) in 'job1' (8/9):
+Effect at line 13
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_acsl/postassigns.c, line 5) in 'job1' (9/9):
+Effect at line 13
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function job2
+------------------------------------------------------------
+
+Goal Post-condition (file tests/wp_acsl/postassigns.c, line 19) in 'job2':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_acsl/postassigns.c, line 20) in 'job2' (1/9):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_acsl/postassigns.c, line 20) in 'job2' (2/9):
+Effect at line 25
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_acsl/postassigns.c, line 20) in 'job2' (3/9):
+Effect at line 25
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_acsl/postassigns.c, line 20) in 'job2' (4/9):
+Effect at line 26
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_acsl/postassigns.c, line 20) in 'job2' (5/9):
+Effect at line 26
+Let x = A[1].
+Assume {
+ Type: is_sint32(x).
+ (* Heap *)
+ Type: (region(p.base) <= 0) /\ IsArray_sint32(A) /\ linked(Malloc_0).
+ (* Goal *)
+ When: !invalid(Malloc_0, shift_sint32(p, x), 1).
+}
+Prove: exists i : Z. (A[i] = x) /\ (0 <= i) /\ (i <= 3).
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_acsl/postassigns.c, line 20) in 'job2' (6/9):
+Effect at line 27
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_acsl/postassigns.c, line 20) in 'job2' (7/9):
+Effect at line 27
+Let x = A[2].
+Assume {
+ Type: is_sint32(x).
+ (* Heap *)
+ Type: (region(p.base) <= 0) /\ IsArray_sint32(A) /\ linked(Malloc_0).
+ (* Goal *)
+ When: !invalid(Malloc_0, shift_sint32(p, x), 1).
+}
+Prove: exists i : Z. (A[i] = x) /\ (0 <= i) /\ (i <= 3).
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_acsl/postassigns.c, line 20) in 'job2' (8/9):
+Effect at line 28
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_acsl/postassigns.c, line 20) in 'job2' (9/9):
+Effect at line 28
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function job3
+------------------------------------------------------------
+
+Goal Preservation of Invariant (file tests/wp_acsl/postassigns.c, line 38):
+Assume {
+ Type: is_sint32(N) /\ is_sint32(i) /\ is_sint32(1 + i).
+ (* Pre-condition *)
+ Have: 0 <= N.
+ (* Invariant *)
+ Have: (i <= N) /\ (0 <= i).
+ (* Then *)
+ Have: i < N.
+}
+Prove: (-1) <= i.
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant (file tests/wp_acsl/postassigns.c, line 38):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns (file tests/wp_acsl/postassigns.c, line 39) (1/3):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns (file tests/wp_acsl/postassigns.c, line 39) (2/3):
+Effect at line 41
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns (file tests/wp_acsl/postassigns.c, line 39) (3/3):
+Effect at line 42
+Let a = shift_sint32(p, i).
+Assume {
+ Type: is_sint32(N) /\ is_sint32(i).
+ (* Heap *)
+ Type: (region(p.base) <= 0) /\ linked(Malloc_0).
+ (* Goal *)
+ When: !invalid(Malloc_0, a, 1).
+ (* Pre-condition *)
+ Have: 0 <= N.
+ (* Invariant *)
+ Have: (i <= N) /\ (0 <= i).
+ (* Then *)
+ Have: i < N.
+}
+Prove: included(a, 1, shift_sint32(p, 0), N).
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_acsl/postassigns.c, line 33) in 'job3' (1/2):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_acsl/postassigns.c, line 33) in 'job3' (2/2):
+Effect at line 41
+Prove: true.
+
+------------------------------------------------------------
+[wp] tests/wp_acsl/postassigns.c:7: Warning:
+ Memory model hypotheses for function 'job1':
+ /*@
+ behavior wp_typed:
+ requires \separated(p + (..), &N);
+ ensures \separated(p + (0 .. \at(N,Post) - 1), &N);
+ */
+ void job1(int *p);
+[wp] tests/wp_acsl/postassigns.c:22: Warning:
+ Memory model hypotheses for function 'job2':
+ /*@
+ behavior wp_typed:
+ requires \separated(p + (..), (int *)A + (..), &N);
+ ensures \separated(p + A[0 .. \at(N,Post) - 1], (int *)A + (..), &N);
+ */
+ void job2(int *p);
+[wp] tests/wp_acsl/postassigns.c:35: Warning:
+ Memory model hypotheses for function 'job3':
+ /*@
+ behavior wp_typed:
+ requires \separated(p + (..), &N);
+ ensures \separated(p + (0 .. \at(N,Post)), &N);
+ */
+ void job3(int *p);
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/postassigns.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/postassigns.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..ef70c9d2f6e56db04fc30ccefa62a3d4ac6c3ea5
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/postassigns.res.oracle
@@ -0,0 +1,65 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_acsl/postassigns.c (with preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+[wp] 27 goals scheduled
+[wp] [Qed] Goal typed_job1_ensures : Valid
+[wp] [Qed] Goal typed_job1_assigns_part1 : Valid
+[wp] [Qed] Goal typed_job1_assigns_part2 : Valid
+[wp] [Qed] Goal typed_job1_assigns_part3 : Valid
+[wp] [Qed] Goal typed_job1_assigns_part4 : Valid
+[wp] [Qed] Goal typed_job1_assigns_part5 : Valid
+[wp] [Qed] Goal typed_job1_assigns_part6 : Valid
+[wp] [Qed] Goal typed_job1_assigns_part7 : Valid
+[wp] [Qed] Goal typed_job1_assigns_part8 : Valid
+[wp] [Qed] Goal typed_job1_assigns_part9 : Valid
+[wp] [Qed] Goal typed_job2_ensures : Valid
+[wp] [Qed] Goal typed_job2_assigns_part1 : Valid
+[wp] [Qed] Goal typed_job2_assigns_part2 : Valid
+[wp] [Qed] Goal typed_job2_assigns_part3 : Valid
+[wp] [Qed] Goal typed_job2_assigns_part4 : Valid
+[wp] [Alt-Ergo] Goal typed_job2_assigns_part5 : Valid
+[wp] [Qed] Goal typed_job2_assigns_part6 : Valid
+[wp] [Alt-Ergo] Goal typed_job2_assigns_part7 : Valid
+[wp] [Qed] Goal typed_job2_assigns_part8 : Valid
+[wp] [Qed] Goal typed_job2_assigns_part9 : Valid
+[wp] [Alt-Ergo] Goal typed_job3_loop_invariant_preserved : Valid
+[wp] [Qed] Goal typed_job3_loop_invariant_established : Valid
+[wp] [Qed] Goal typed_job3_loop_assigns_part1 : Valid
+[wp] [Qed] Goal typed_job3_loop_assigns_part2 : Valid
+[wp] [Alt-Ergo] Goal typed_job3_loop_assigns_part3 : Valid
+[wp] [Qed] Goal typed_job3_assigns_part1 : Valid
+[wp] [Qed] Goal typed_job3_assigns_part2 : Valid
+[wp] Proved goals: 27 / 27
+ Qed: 23
+ Alt-Ergo: 4
+------------------------------------------------------------
+ Functions WP Alt-Ergo Total Success
+ job1 10 - 10 100%
+ job2 8 2 10 100%
+ job3 5 2 7 100%
+------------------------------------------------------------
+[wp] tests/wp_acsl/postassigns.c:7: Warning:
+ Memory model hypotheses for function 'job1':
+ /*@
+ behavior wp_typed:
+ requires \separated(p + (..), &N);
+ ensures \separated(p + (0 .. \at(N,Post) - 1), &N);
+ */
+ void job1(int *p);
+[wp] tests/wp_acsl/postassigns.c:22: Warning:
+ Memory model hypotheses for function 'job2':
+ /*@
+ behavior wp_typed:
+ requires \separated(p + (..), (int *)A + (..), &N);
+ ensures \separated(p + A[0 .. \at(N,Post) - 1], (int *)A + (..), &N);
+ */
+ void job2(int *p);
+[wp] tests/wp_acsl/postassigns.c:35: Warning:
+ Memory model hypotheses for function 'job3':
+ /*@
+ behavior wp_typed:
+ requires \separated(p + (..), &N);
+ ensures \separated(p + (0 .. \at(N,Post)), &N);
+ */
+ void job3(int *p);
diff --git a/src/plugins/wp/tests/wp_acsl/postassigns.c b/src/plugins/wp/tests/wp_acsl/postassigns.c
new file mode 100644
index 0000000000000000000000000000000000000000..a2c1b7d1ba8ca26344e485d05bf64119cac34a0c
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/postassigns.c
@@ -0,0 +1,44 @@
+int N;
+
+/*@
+ ensures N == 4;
+ assigns N, p[0..\at(N,Post)-1];
+*/
+void job1(int *p)
+{
+ N = 0;
+ p[N++] = 0;
+ p[N++] = 0;
+ p[N++] = 0;
+ p[N++] = 0;
+}
+
+int A[4];
+
+/*@
+ ensures N == 4;
+ assigns N, *(p + A[0..\at(N,Post)-1]);
+*/
+void job2(int *p)
+{
+ N = 0;
+ p[A[N++]] = 0;
+ p[A[N++]] = 0;
+ p[A[N++]] = 0;
+ p[A[N++]] = 0;
+}
+
+/*@
+ requires 0 <= N;
+ assigns N, p[0..\at(N,Post)];
+*/
+void job3(int *p)
+{
+ /*@
+ loop invariant 0 <= i <= N;
+ loop assigns i, p[0..N-1];
+ */
+ for (int i = 0; i < N; i++)
+ p[i] = 0;
+ N++;
+}
diff --git a/src/plugins/wp/tests/wp_tip/induction.i b/src/plugins/wp/tests/wp_tip/induction.i
new file mode 100644
index 0000000000000000000000000000000000000000..5ff948c0f86fd357cbf3cc3393e3a402887f08dd
--- /dev/null
+++ b/src/plugins/wp/tests/wp_tip/induction.i
@@ -0,0 +1,28 @@
+/* run.config
+ DONTRUN:
+*/
+
+/* run.config_qualif
+ OPT: -wp-prover script,alt-ergo -wp-timeout 1
+ OPT: -wp-prover script,alt-ergo -wp-timeout 1
+ OPT: -wp-prover script,alt-ergo -wp-timeout 1
+*/
+
+// Script 0: induction on f(x) => success
+// Script 1: induction on x => unsuccess
+// Script 2: induction on y => unsuccess
+
+/*@
+ axiomatic Inductive {
+
+ logic integer f(integer x);
+ predicate P(integer x, integer y);
+
+ axiom Hbse: \forall integer y; P(0,y);
+ axiom Hsup: \forall integer i,y; 0 <= i ==> P(i,y) ==> P(i+1,y);
+ axiom Hinf: \forall integer i,y; i <= 0 ==> P(i,y) ==> P(i-1,y);
+
+ lemma ByInd: \forall integer x,y; P(f(x),y);
+
+ }
+*/
diff --git a/src/plugins/wp/tests/wp_tip/oracle_qualif/induction.0.res.oracle b/src/plugins/wp/tests/wp_tip/oracle_qualif/induction.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..6a84303d1b466fcdff16540ca4971992efa2684d
--- /dev/null
+++ b/src/plugins/wp/tests/wp_tip/oracle_qualif/induction.0.res.oracle
@@ -0,0 +1,12 @@
+# frama-c -wp -wp-timeout 1 [...]
+[kernel] Parsing tests/wp_tip/induction.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] 1 goal scheduled
+[wp] [Script] Goal typed_lemma_ByInd : Valid
+[wp] Proved goals: 1 / 1
+ Qed: 0
+ Script: 1
+------------------------------------------------------------
+ Axiomatics WP Alt-Ergo Total Success
+ Axiomatic Inductive - - 1 100%
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_tip/oracle_qualif/induction.0.session/script/lemma_ByInd.json b/src/plugins/wp/tests/wp_tip/oracle_qualif/induction.0.session/script/lemma_ByInd.json
new file mode 100644
index 0000000000000000000000000000000000000000..2a359dbab3ad22d87d88d11534edd84db6f4497e
--- /dev/null
+++ b/src/plugins/wp/tests/wp_tip/oracle_qualif/induction.0.session/script/lemma_ByInd.json
@@ -0,0 +1,12 @@
+[ { "header": "Induction", "tactic": "Wp.induction",
+ "params": { "base": { "select": "kint", "val": "0" } },
+ "select": { "select": "inside-goal", "occur": 0, "target": "(L_f x_0)",
+ "pattern": "L_f$x" },
+ "children": { "Base": [ { "prover": "Alt-Ergo:2.2.0", "verdict": "valid",
+ "time": 0.0047, "steps": 6 } ],
+ "Induction (sup)": [ { "prover": "Alt-Ergo:2.2.0",
+ "verdict": "valid", "time": 0.0041,
+ "steps": 21 } ],
+ "Induction (inf)": [ { "prover": "Alt-Ergo:2.2.0",
+ "verdict": "valid", "time": 0.0054,
+ "steps": 20 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_tip/oracle_qualif/induction.1.res.oracle b/src/plugins/wp/tests/wp_tip/oracle_qualif/induction.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..68fc7293ba5097e47a387ee3483e9d2496a1d0fb
--- /dev/null
+++ b/src/plugins/wp/tests/wp_tip/oracle_qualif/induction.1.res.oracle
@@ -0,0 +1,10 @@
+# frama-c -wp -wp-timeout 1 [...]
+[kernel] Parsing tests/wp_tip/induction.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] 1 goal scheduled
+[wp] [Script] Goal typed_lemma_ByInd : Unsuccess
+[wp] Proved goals: 0 / 1
+------------------------------------------------------------
+ Axiomatics WP Alt-Ergo Total Success
+ Axiomatic Inductive - - 1 0.0%
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_tip/oracle_qualif/induction.1.session/script/lemma_ByInd.json b/src/plugins/wp/tests/wp_tip/oracle_qualif/induction.1.session/script/lemma_ByInd.json
new file mode 100644
index 0000000000000000000000000000000000000000..d5763f40f15dd0fb0e845177f6d42085f36486ca
--- /dev/null
+++ b/src/plugins/wp/tests/wp_tip/oracle_qualif/induction.1.session/script/lemma_ByInd.json
@@ -0,0 +1,12 @@
+[ { "prover": "Alt-Ergo:2.2.0", "verdict": "unknown" },
+ { "prover": "script", "verdict": "unknown" },
+ { "header": "Induction", "tactic": "Wp.induction",
+ "params": { "base": { "select": "kint", "val": "0" } },
+ "select": { "select": "inside-goal", "occur": 0, "target": "x_0",
+ "pattern": "$x" },
+ "children": { "Base": [ { "prover": "Alt-Ergo:2.2.0",
+ "verdict": "unknown" } ],
+ "Induction (sup)": [ { "prover": "Alt-Ergo:2.2.0",
+ "verdict": "unknown" } ],
+ "Induction (inf)": [ { "prover": "Alt-Ergo:2.2.0",
+ "verdict": "timeout", "time": 1. } ] } } ]
diff --git a/src/plugins/wp/tests/wp_tip/oracle_qualif/induction.2.res.oracle b/src/plugins/wp/tests/wp_tip/oracle_qualif/induction.2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..68fc7293ba5097e47a387ee3483e9d2496a1d0fb
--- /dev/null
+++ b/src/plugins/wp/tests/wp_tip/oracle_qualif/induction.2.res.oracle
@@ -0,0 +1,10 @@
+# frama-c -wp -wp-timeout 1 [...]
+[kernel] Parsing tests/wp_tip/induction.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] 1 goal scheduled
+[wp] [Script] Goal typed_lemma_ByInd : Unsuccess
+[wp] Proved goals: 0 / 1
+------------------------------------------------------------
+ Axiomatics WP Alt-Ergo Total Success
+ Axiomatic Inductive - - 1 0.0%
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_tip/oracle_qualif/induction.2.session/script/lemma_ByInd.json b/src/plugins/wp/tests/wp_tip/oracle_qualif/induction.2.session/script/lemma_ByInd.json
new file mode 100644
index 0000000000000000000000000000000000000000..5e068a85c7f8f2ef58ef88d2b0b651607423e155
--- /dev/null
+++ b/src/plugins/wp/tests/wp_tip/oracle_qualif/induction.2.session/script/lemma_ByInd.json
@@ -0,0 +1,12 @@
+[ { "prover": "Alt-Ergo:2.2.0", "verdict": "unknown" },
+ { "prover": "script", "verdict": "unknown" },
+ { "header": "Induction", "tactic": "Wp.induction",
+ "params": { "base": { "select": "kint", "val": "0" } },
+ "select": { "select": "inside-goal", "occur": 0, "target": "y_0",
+ "pattern": "$y" },
+ "children": { "Base": [ { "prover": "Alt-Ergo:2.2.0",
+ "verdict": "unknown" } ],
+ "Induction (sup)": [ { "prover": "Alt-Ergo:2.2.0",
+ "verdict": "unknown" } ],
+ "Induction (inf)": [ { "prover": "Alt-Ergo:2.2.0",
+ "verdict": "timeout", "time": 1. } ] } } ]
diff --git a/src/plugins/wp/tests/wp_tip/oracle_qualif/induction.res.oracle b/src/plugins/wp/tests/wp_tip/oracle_qualif/induction.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..1524fcd67af880eeea3ae07ea547aae8eb0d7ea1
--- /dev/null
+++ b/src/plugins/wp/tests/wp_tip/oracle_qualif/induction.res.oracle
@@ -0,0 +1,10 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_tip/induction.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] 1 goal scheduled
+[wp] [Script] Goal typed_lemma_Simple : Unsuccess
+[wp] Proved goals: 0 / 1
+------------------------------------------------------------
+ Axiomatics WP Alt-Ergo Total Success
+ Axiomatic Inductive - - 1 0.0%
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_tip/oracle_qualif/induction_prove.0.session/script/lemma_ByInd.json b/src/plugins/wp/tests/wp_tip/oracle_qualif/induction_prove.0.session/script/lemma_ByInd.json
new file mode 100644
index 0000000000000000000000000000000000000000..5a4345732238664a27f4c2cf710df871d69c5f6d
--- /dev/null
+++ b/src/plugins/wp/tests/wp_tip/oracle_qualif/induction_prove.0.session/script/lemma_ByInd.json
@@ -0,0 +1,13 @@
+[ { "prover": "script", "verdict": "valid", "time": 0.0549, "steps": 117 },
+ { "header": "Induction", "tactic": "Wp.induction",
+ "params": { "base": 0, "hsup": true, "hinf": true },
+ "select": { "select": "inside-goal", "occur": 0, "target": "(L_f x_0)",
+ "pattern": "L_f$x" },
+ "children": { "Base": [ { "prover": "Alt-Ergo:2.2.0", "verdict": "valid",
+ "time": 0.0083, "steps": 6 } ],
+ "Induction (sup)": [ { "prover": "Alt-Ergo:2.2.0",
+ "verdict": "valid", "time": 0.0549,
+ "steps": 117 } ],
+ "Induction (inf)": [ { "prover": "Alt-Ergo:2.2.0",
+ "verdict": "valid", "time": 0.0274,
+ "steps": 86 } ] } } ]
diff --git a/src/plugins/wp/wp_parameters.ml b/src/plugins/wp/wp_parameters.ml
index 661340a06cac4a55f71232edca60236a7e379eaf..233f8cb1f45c84386b52e41635e93dd28a1011da 100644
--- a/src/plugins/wp/wp_parameters.ml
+++ b/src/plugins/wp/wp_parameters.ml
@@ -543,13 +543,6 @@ module Prenex =
let help = "Normalize nested foralls into prenex-form"
end)
-let () = Parameter_customize.set_group wp_simplifier
-module Bits =
- True(struct
- let option_name = "-wp-bits"
- let help = "Use bit-test simplifications."
- end)
-
let () = Parameter_customize.set_group wp_simplifier
module SimplifyIsCint =
True(struct
diff --git a/src/plugins/wp/wp_parameters.mli b/src/plugins/wp/wp_parameters.mli
index ab805c2b51ff00e88db86e089f7729756a71ca73..a276a4b4a33b01b914e6da3f7a18e9d1db89be1d 100644
--- a/src/plugins/wp/wp_parameters.mli
+++ b/src/plugins/wp/wp_parameters.mli
@@ -85,7 +85,6 @@ module Clean: Parameter_sig.Bool
module Filter: Parameter_sig.Bool
module Parasite: Parameter_sig.Bool
module Prenex: Parameter_sig.Bool
-module Bits: Parameter_sig.Bool
module Ground: Parameter_sig.Bool
module Reduce: Parameter_sig.Bool
module ExtEqual : Parameter_sig.Bool