From fa928a5b12baa98217813d72deba3be8044041f4 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Tue, 1 Oct 2024 09:51:49 +0200
Subject: [PATCH] [wp] test importer
---
.../wp/tests/wp_plugin/import_inductive.i | 8 ++
src/plugins/wp/tests/wp_plugin/import_int.i | 3 +
.../wp/tests/wp_plugin/import_option.i | 27 +++++
.../wp/tests/wp_plugin/import_real_infix.i | 3 +
.../wp/tests/wp_plugin/import_unexisting.i | 9 ++
.../wp/tests/wp_plugin/import_unitex.i | 68 +++++++++++
.../wp/tests/wp_plugin/import_unitex.mlw | 64 ++++++++++
.../oracle/import_inductive.res.oracle | 17 +++
.../wp_plugin/oracle/import_int.res.oracle | 11 ++
.../wp_plugin/oracle/import_option.res.oracle | 38 ++++++
.../oracle/import_real_infix.res.oracle | 11 ++
.../oracle/import_unexisting.res.oracle | 7 ++
.../wp_plugin/oracle/import_unitex.res.oracle | 113 ++++++++++++++++++
.../oracle_qualif/import_inductive.res.oracle | 12 ++
.../oracle_qualif/import_int.res.oracle | 11 ++
.../oracle_qualif/import_option.res.oracle | 22 ++++
.../import_real_infix.res.oracle | 11 ++
.../oracle_qualif/import_unitex.res.oracle | 25 ++++
18 files changed, 460 insertions(+)
create mode 100644 src/plugins/wp/tests/wp_plugin/import_inductive.i
create mode 100644 src/plugins/wp/tests/wp_plugin/import_int.i
create mode 100644 src/plugins/wp/tests/wp_plugin/import_option.i
create mode 100644 src/plugins/wp/tests/wp_plugin/import_real_infix.i
create mode 100644 src/plugins/wp/tests/wp_plugin/import_unexisting.i
create mode 100644 src/plugins/wp/tests/wp_plugin/import_unitex.i
create mode 100644 src/plugins/wp/tests/wp_plugin/import_unitex.mlw
create mode 100644 src/plugins/wp/tests/wp_plugin/oracle/import_inductive.res.oracle
create mode 100644 src/plugins/wp/tests/wp_plugin/oracle/import_int.res.oracle
create mode 100644 src/plugins/wp/tests/wp_plugin/oracle/import_option.res.oracle
create mode 100644 src/plugins/wp/tests/wp_plugin/oracle/import_real_infix.res.oracle
create mode 100644 src/plugins/wp/tests/wp_plugin/oracle/import_unexisting.res.oracle
create mode 100644 src/plugins/wp/tests/wp_plugin/oracle/import_unitex.res.oracle
create mode 100644 src/plugins/wp/tests/wp_plugin/oracle_qualif/import_inductive.res.oracle
create mode 100644 src/plugins/wp/tests/wp_plugin/oracle_qualif/import_int.res.oracle
create mode 100644 src/plugins/wp/tests/wp_plugin/oracle_qualif/import_option.res.oracle
create mode 100644 src/plugins/wp/tests/wp_plugin/oracle_qualif/import_real_infix.res.oracle
create mode 100644 src/plugins/wp/tests/wp_plugin/oracle_qualif/import_unitex.res.oracle
diff --git a/src/plugins/wp/tests/wp_plugin/import_inductive.i b/src/plugins/wp/tests/wp_plugin/import_inductive.i
new file mode 100644
index 00000000000..ec676ef0c28
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/import_inductive.i
@@ -0,0 +1,8 @@
+//@ import why3: list::Distinct ;
+
+// WP cannot deal with a fully polymorphic value for now
+// @ lemma L1 <A> : Distinct::distinct([| |]) ;
+
+
+//@ lemma L2: Distinct::distinct([| 0 |]) ;
+//@ lemma L3: Distinct::distinct([| 1 , 2 |]) ;
diff --git a/src/plugins/wp/tests/wp_plugin/import_int.i b/src/plugins/wp/tests/wp_plugin/import_int.i
new file mode 100644
index 00000000000..7a661141451
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/import_int.i
@@ -0,0 +1,3 @@
+//@ import why3: int::Int \as I ;
+
+//@ lemma iso: I::zero == 0 ;
diff --git a/src/plugins/wp/tests/wp_plugin/import_option.i b/src/plugins/wp/tests/wp_plugin/import_option.i
new file mode 100644
index 00000000000..ca692214f4d
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/import_option.i
@@ -0,0 +1,27 @@
+//@ import why3: option::Option \as O ;
+
+//@ logic O::option<integer> to_opt_t(integer p) = O::Some(p);
+//@ lemma bar_1: \forall integer p ; to_opt_t(p) == O::Some(p);
+//@ lemma bar_2: \forall integer p ; to_opt_t(p) != O::None;
+
+/*@ logic O::option<integer> to_opt(int* p) =
+ p == \null ? O::None : O::Some(*p);
+*/
+
+int g ;
+
+/*@ behavior zero:
+ assumes i == 0 ;
+ ensures to_opt(\result) == O::None ;
+
+ behavior other:
+ assumes i != 0 ;
+ ensures to_opt(\result) == O::Some(42) ;
+*/
+int* f(int i){
+ if(i == 0) return (void*)0;
+ else {
+ g = 42 ;
+ return &g ;
+ }
+}
diff --git a/src/plugins/wp/tests/wp_plugin/import_real_infix.i b/src/plugins/wp/tests/wp_plugin/import_real_infix.i
new file mode 100644
index 00000000000..ec1dad5feb8
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/import_real_infix.i
@@ -0,0 +1,3 @@
+//@ import why3: real::RealInfix \as RI ;
+
+//@ lemma infix: RI::(<.)((RI::(+.)(0., 1.)), 2.) ;
diff --git a/src/plugins/wp/tests/wp_plugin/import_unexisting.i b/src/plugins/wp/tests/wp_plugin/import_unexisting.i
new file mode 100644
index 00000000000..cd6a13893cd
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/import_unexisting.i
@@ -0,0 +1,9 @@
+/* run.config
+ EXIT: 1
+ OPT:
+*/
+/* run.config_qualif
+ DONTRUN:
+*/
+
+//@ import why3: unexisting::Module ;
diff --git a/src/plugins/wp/tests/wp_plugin/import_unitex.i b/src/plugins/wp/tests/wp_plugin/import_unitex.i
new file mode 100644
index 00000000000..12ea1f3c54c
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/import_unitex.i
@@ -0,0 +1,68 @@
+/* run.config*
+ DEPS: @PTEST_NAME@.mlw
+ OPT: -wp-library "."
+*/
+
+// Builtin types + synonyms
+
+//@ import why3: int::Int \as I ;
+//@ import why3: real::Real \as R ;
+//@ import why3: bool::Bool \as B ;
+
+//@ import why3: import_unitex::Builtin \as BI ;
+
+/*@ predicate compat_int(integer a, BI::bint b) = a == b ;
+ lemma L_compat_int_1: compat_int(I::zero, 0) ;
+ lemma L_compat_int_2: compat_int(0, I::zero) ;
+*/
+/*@ predicate compat_real(real a, BI::breal b) = a == b ;
+ lemma L_compat_real_1: compat_real(R::zero, 0) ;
+ lemma L_compat_real_2: compat_real(0, R::zero) ;
+*/
+/*@ predicate compat_bool(boolean a, BI::bbool b) = B::andb(a, b) == \true ;
+ lemma L_compat_bool: compat_bool(\true, \true) ;
+*/
+
+// Type without definition
+
+//@ import why3: import_unitex::No_def ;
+//@ import why3: import_unitex::No_def_syn ;
+//@ lemma L_no_def: No_def::x == No_def_syn::y ;
+
+// ADT
+
+//@ import why3: import_unitex::ADT ;
+
+/*@ predicate compat_adt(ADT::t<real> a, ADT::s<real> b) = a == b ;
+ lemma L_compat_adt_1: compat_adt(ADT::A, ADT::A) ;
+ lemma L_compat_adt_2: compat_adt(ADT::B(1), ADT::B(1)) ;
+ lemma L_compat_adt_3: compat_adt(ADT::C(0.), ADT::C(0.)) ;
+*/
+
+// Range
+
+//@ import why3: import_unitex::Range \as Rg ;
+
+/*@ lemma L_rg_1:
+ \forall integer i ;
+ -42 <= i <= 42 ==> Rg::to_int (Rg::of_int (i)) == i ;
+*/
+
+//@ lemma L_rg_2: \forall Rg::r42 i ; -42 <= Rg::to_int (i) <= 42 ;
+
+// Float
+
+//@ import why3: import_unitex::Float8 \as F8 ;
+
+//@ lemma L_f8: F8::is_finite(F8::f1) ;
+
+// Symbols
+
+//@ import why3: import_unitex::Symbols \as S1 ;
+//@ import why3: import_unitex::Symbols \as S2 ;
+//@ import why3: import_unitex::Symbols ;
+//@ import why3: import_unitex::Symbols ; // should not fail
+
+//@ lemma L_sym_1: S1::(==)(S1::(!)(0), 42) ;
+//@ lemma L_sym_2: S2::pred(S2::func(0), 42) ;
+//@ lemma L_sym_3: Symbols::pos(4);
diff --git a/src/plugins/wp/tests/wp_plugin/import_unitex.mlw b/src/plugins/wp/tests/wp_plugin/import_unitex.mlw
new file mode 100644
index 00000000000..8fbfd479d1a
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/import_unitex.mlw
@@ -0,0 +1,64 @@
+module Builtin
+ use int.Int
+ use real.Real
+ use bool.Bool
+
+ type bint = int
+ type breal = real
+ type bbool = bool
+end
+
+module No_def
+ type t
+ constant x: t
+end
+
+module No_def_syn
+ use No_def
+
+ type t = No_def.t
+ constant y: t = x
+end
+
+module ADT
+ use int.Int
+ type t 'a = A | B int | C 'a
+ type s 'a = t 'a
+end
+
+module Range
+ use int.Int
+
+ type r42 = < range -42 42 >
+ function to_int (x: r42) : int = r42'int x
+
+ function of_int (x: int) : r42
+ axiom ax:
+ forall x: int.
+ -42 <= x <= 42 -> to_int(of_int(x)) = x
+end
+
+module Float8
+ use real.Real
+
+ type f8 = < float 4 3 >
+
+ constant f1: f8 = (0.5:f8)
+ predicate is_finite(f: f8) = f8'isFinite(f)
+end
+
+module Symbols
+ use int.Int
+
+ predicate pred(i j: int) = i = j
+ predicate (==) (i j: int) = pred i j
+
+ function func(i: int) : int = i + 42
+ function (!) (i : int) : int = func i
+
+ lemma x: !0 == 42
+
+ inductive pos(i: int) =
+ | Base : pos(1)
+ | Plus : forall i : int. pos (i-1) -> pos i
+end
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/import_inductive.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/import_inductive.res.oracle
new file mode 100644
index 00000000000..4e83e5029fb
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle/import_inductive.res.oracle
@@ -0,0 +1,17 @@
+# frama-c -wp [...]
+[kernel] Parsing import_inductive.i (no preprocessing)
+[wp] Running WP plugin...
+------------------------------------------------------------
+ Global
+------------------------------------------------------------
+
+Goal Lemma 'L2':
+Prove: list.Distinct.distinct([ 0 ]).
+
+------------------------------------------------------------
+
+Goal Lemma 'L3':
+Assume Lemmas: 'L2'
+Prove: list.Distinct.distinct([ 1, 2 ]).
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/import_int.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/import_int.res.oracle
new file mode 100644
index 00000000000..1b815532ea6
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle/import_int.res.oracle
@@ -0,0 +1,11 @@
+# frama-c -wp [...]
+[kernel] Parsing import_int.i (no preprocessing)
+[wp] Running WP plugin...
+------------------------------------------------------------
+ Global
+------------------------------------------------------------
+
+Goal Lemma 'iso':
+Prove: int.Int.zero = 0.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/import_option.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/import_option.res.oracle
new file mode 100644
index 00000000000..d9f15236082
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle/import_option.res.oracle
@@ -0,0 +1,38 @@
+# frama-c -wp [...]
+[kernel] Parsing import_option.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] [Valid] Goal f_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal f_terminates (Cfg) (Trivial)
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+ Global
+------------------------------------------------------------
+
+Goal Lemma 'bar_1':
+Prove: L_to_opt_t(p) = option.Option.Some(p).
+
+------------------------------------------------------------
+
+Goal Lemma 'bar_2':
+Assume Lemmas: 'bar_1'
+Prove: L_to_opt_t(p) != option.Option.None.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function f with behavior other
+------------------------------------------------------------
+
+Goal Post-condition for 'other' (file import_option.i, line 19) in 'f':
+Let a = global(G_g_31).
+Assume { Type: is_sint32(i). (* Pre-condition for 'other' *) Have: i != 0. }
+Prove: L_to_opt(Mint_0[a <- 42], a) = option.Option.Some(42).
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function f with behavior zero
+------------------------------------------------------------
+
+Goal Post-condition for 'zero' (file import_option.i, line 15) in 'f':
+Prove: L_to_opt(Mint_0, null) = option.Option.None.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/import_real_infix.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/import_real_infix.res.oracle
new file mode 100644
index 00000000000..5b0227df806
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle/import_real_infix.res.oracle
@@ -0,0 +1,11 @@
+# frama-c -wp [...]
+[kernel] Parsing import_real_infix.i (no preprocessing)
+[wp] Running WP plugin...
+------------------------------------------------------------
+ Global
+------------------------------------------------------------
+
+Goal Lemma 'infix':
+Prove: real.RealInfix.infix <.(real.RealInfix.infix +.(.0, 1.0), 2.0).
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/import_unexisting.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/import_unexisting.res.oracle
new file mode 100644
index 00000000000..d5852e56a17
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle/import_unexisting.res.oracle
@@ -0,0 +1,7 @@
+# frama-c -wp [...]
+[kernel] Parsing import_unexisting.i (no preprocessing)
+[wp] User Error: Library Module not found
+[wp] Running WP plugin...
+[wp] No proof obligations
+[wp] User Error: Deferred error message was emitted during execution. See above messages for more information.
+[kernel] Plug-in wp aborted: invalid user input.
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/import_unitex.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/import_unitex.res.oracle
new file mode 100644
index 00000000000..7a372ba5797
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle/import_unitex.res.oracle
@@ -0,0 +1,113 @@
+# frama-c -wp [...]
+[kernel] Parsing import_unitex.i (no preprocessing)
+[wp] Running WP plugin...
+------------------------------------------------------------
+ Global
+------------------------------------------------------------
+
+Goal Lemma 'L_compat_adt_1':
+Assume Lemmas: 'L_no_def' 'L_compat_bool' 'L_compat_real_2' 'L_compat_real_1'
+ 'L_compat_int_2' 'L_compat_int_1'
+Prove: P_compat_adt(import_unitex.ADT.A, import_unitex.ADT.A).
+
+------------------------------------------------------------
+
+Goal Lemma 'L_compat_adt_2':
+Assume Lemmas: 'L_compat_adt_1' 'L_no_def' 'L_compat_bool' 'L_compat_real_2'
+ 'L_compat_real_1' 'L_compat_int_2' 'L_compat_int_1'
+Let a = import_unitex.ADT.B(1). Prove: P_compat_adt(a, a).
+
+------------------------------------------------------------
+
+Goal Lemma 'L_compat_adt_3':
+Assume Lemmas: 'L_compat_adt_2' 'L_compat_adt_1' 'L_no_def' 'L_compat_bool'
+ 'L_compat_real_2' 'L_compat_real_1' 'L_compat_int_2' 'L_compat_int_1'
+Let a = import_unitex.ADT.C(.0). Prove: P_compat_adt(a, a).
+
+------------------------------------------------------------
+
+Goal Lemma 'L_compat_bool':
+Assume Lemmas: 'L_compat_real_2' 'L_compat_real_1' 'L_compat_int_2'
+ 'L_compat_int_1'
+Prove: P_compat_bool(true, true).
+
+------------------------------------------------------------
+
+Goal Lemma 'L_compat_int_1':
+Prove: P_compat_int(int.Int.zero, 0).
+
+------------------------------------------------------------
+
+Goal Lemma 'L_compat_int_2':
+Assume Lemmas: 'L_compat_int_1'
+Prove: P_compat_int(0, int.Int.zero).
+
+------------------------------------------------------------
+
+Goal Lemma 'L_compat_real_1':
+Assume Lemmas: 'L_compat_int_2' 'L_compat_int_1'
+Prove: P_compat_real(real.Real.zero, .0).
+
+------------------------------------------------------------
+
+Goal Lemma 'L_compat_real_2':
+Assume Lemmas: 'L_compat_real_1' 'L_compat_int_2' 'L_compat_int_1'
+Prove: P_compat_real(.0, real.Real.zero).
+
+------------------------------------------------------------
+
+Goal Lemma 'L_f8':
+Assume Lemmas: 'L_rg_2' 'L_rg_1' 'L_compat_adt_3' 'L_compat_adt_2'
+ 'L_compat_adt_1' 'L_no_def' 'L_compat_bool' 'L_compat_real_2'
+ 'L_compat_real_1' 'L_compat_int_2' 'L_compat_int_1'
+Prove: import_unitex.Float8.is_finite(import_unitex.Float8.f1).
+
+------------------------------------------------------------
+
+Goal Lemma 'L_no_def':
+Assume Lemmas: 'L_compat_bool' 'L_compat_real_2' 'L_compat_real_1'
+ 'L_compat_int_2' 'L_compat_int_1'
+Prove: import_unitex.No_def_syn.y = import_unitex.No_def.x.
+
+------------------------------------------------------------
+
+Goal Lemma 'L_rg_1':
+Assume Lemmas: 'L_compat_adt_3' 'L_compat_adt_2' 'L_compat_adt_1' 'L_no_def'
+ 'L_compat_bool' 'L_compat_real_2' 'L_compat_real_1' 'L_compat_int_2'
+ 'L_compat_int_1'
+Assume { Have: (-42) <= i. Have: i <= 42. }
+Prove: import_unitex.Range.to_int(import_unitex.Range.of_int(i)) = i.
+
+------------------------------------------------------------
+
+Goal Lemma 'L_rg_2':
+Assume Lemmas: 'L_rg_1' 'L_compat_adt_3' 'L_compat_adt_2' 'L_compat_adt_1'
+ 'L_no_def' 'L_compat_bool' 'L_compat_real_2' 'L_compat_real_1'
+ 'L_compat_int_2' 'L_compat_int_1'
+Let x = import_unitex.Range.to_int(i). Prove: ((-42) <= x) /\ (x <= 42).
+
+------------------------------------------------------------
+
+Goal Lemma 'L_sym_1':
+Assume Lemmas: 'L_f8' 'L_rg_2' 'L_rg_1' 'L_compat_adt_3' 'L_compat_adt_2'
+ 'L_compat_adt_1' 'L_no_def' 'L_compat_bool' 'L_compat_real_2'
+ 'L_compat_real_1' 'L_compat_int_2' 'L_compat_int_1'
+Prove: import_unitex.Symbols.infix ==(import_unitex.Symbols.prefix !(0), 42).
+
+------------------------------------------------------------
+
+Goal Lemma 'L_sym_2':
+Assume Lemmas: 'L_sym_1' 'L_f8' 'L_rg_2' 'L_rg_1' 'L_compat_adt_3'
+ 'L_compat_adt_2' 'L_compat_adt_1' 'L_no_def' 'L_compat_bool'
+ 'L_compat_real_2' 'L_compat_real_1' 'L_compat_int_2' 'L_compat_int_1'
+Prove: import_unitex.Symbols.pred(import_unitex.Symbols.func(0), 42).
+
+------------------------------------------------------------
+
+Goal Lemma 'L_sym_3':
+Assume Lemmas: 'L_sym_2' 'L_sym_1' 'L_f8' 'L_rg_2' 'L_rg_1' 'L_compat_adt_3'
+ 'L_compat_adt_2' 'L_compat_adt_1' 'L_no_def' 'L_compat_bool'
+ 'L_compat_real_2' 'L_compat_real_1' 'L_compat_int_2' 'L_compat_int_1'
+Prove: import_unitex.Symbols.pos(4).
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/import_inductive.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/import_inductive.res.oracle
new file mode 100644
index 00000000000..0a4554a8131
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/import_inductive.res.oracle
@@ -0,0 +1,12 @@
+# frama-c -wp [...]
+[kernel] Parsing import_inductive.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] 2 goals scheduled
+[wp] [Valid] typed_lemma_L2 (Alt-Ergo) (Cached)
+[wp] [Valid] typed_lemma_L3 (Alt-Ergo) (Cached)
+[wp] Proved goals: 2 / 2
+ Alt-Ergo: 2
+------------------------------------------------------------
+ Axiomatics WP Alt-Ergo Total Success
+ Lemma - 2 2 100%
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/import_int.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/import_int.res.oracle
new file mode 100644
index 00000000000..40e0ceaa69b
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/import_int.res.oracle
@@ -0,0 +1,11 @@
+# frama-c -wp [...]
+[kernel] Parsing import_int.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] 1 goal scheduled
+[wp] [Valid] typed_lemma_iso (Alt-Ergo) (Trivial)
+[wp] Proved goals: 1 / 1
+ Alt-Ergo: 1
+------------------------------------------------------------
+ Axiomatics WP Alt-Ergo Total Success
+ Lemma - 1 1 100%
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/import_option.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/import_option.res.oracle
new file mode 100644
index 00000000000..dbb2897a04f
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/import_option.res.oracle
@@ -0,0 +1,22 @@
+# frama-c -wp [...]
+[kernel] Parsing import_option.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] [Valid] Goal f_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal f_terminates (Cfg) (Trivial)
+[wp] Warning: Missing RTE guards
+[wp] 4 goals scheduled
+[wp] [Valid] typed_lemma_bar_1 (Alt-Ergo) (Trivial)
+[wp] [Valid] typed_lemma_bar_2 (Alt-Ergo) (Cached)
+[wp] [Valid] typed_f_zero_ensures (Alt-Ergo) (Cached)
+[wp] [Valid] typed_f_other_ensures (Alt-Ergo) (Cached)
+[wp] Proved goals: 6 / 6
+ Terminating: 1
+ Unreachable: 1
+ Alt-Ergo: 4
+------------------------------------------------------------
+ Axiomatics WP Alt-Ergo Total Success
+ Lemma - 2 2 100%
+------------------------------------------------------------
+ Functions WP Alt-Ergo Total Success
+ f - 2 2 100%
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/import_real_infix.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/import_real_infix.res.oracle
new file mode 100644
index 00000000000..a4392218e7f
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/import_real_infix.res.oracle
@@ -0,0 +1,11 @@
+# frama-c -wp [...]
+[kernel] Parsing import_real_infix.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] 1 goal scheduled
+[wp] [Valid] typed_lemma_infix (Alt-Ergo) (Cached)
+[wp] Proved goals: 1 / 1
+ Alt-Ergo: 1
+------------------------------------------------------------
+ Axiomatics WP Alt-Ergo Total Success
+ Lemma - 1 1 100%
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/import_unitex.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/import_unitex.res.oracle
new file mode 100644
index 00000000000..56543743d00
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/import_unitex.res.oracle
@@ -0,0 +1,25 @@
+# frama-c -wp [...]
+[kernel] Parsing import_unitex.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] 15 goals scheduled
+[wp] [Valid] typed_lemma_L_compat_adt_1 (Alt-Ergo) (Trivial)
+[wp] [Valid] typed_lemma_L_compat_adt_2 (Alt-Ergo) (Trivial)
+[wp] [Valid] typed_lemma_L_compat_adt_3 (Alt-Ergo) (Trivial)
+[wp] [Valid] typed_lemma_L_compat_bool (Alt-Ergo) (Cached)
+[wp] [Valid] typed_lemma_L_compat_int_1 (Alt-Ergo) (Trivial)
+[wp] [Valid] typed_lemma_L_compat_int_2 (Alt-Ergo) (Trivial)
+[wp] [Valid] typed_lemma_L_compat_real_1 (Alt-Ergo) (Trivial)
+[wp] [Valid] typed_lemma_L_compat_real_2 (Alt-Ergo) (Trivial)
+[wp] [Valid] typed_lemma_L_f8 (Alt-Ergo) (Cached)
+[wp] [Valid] typed_lemma_L_no_def (Alt-Ergo) (Trivial)
+[wp] [Valid] typed_lemma_L_rg_1 (Alt-Ergo) (Cached)
+[wp] [Valid] typed_lemma_L_rg_2 (Alt-Ergo) (Cached)
+[wp] [Valid] typed_lemma_L_sym_1 (Alt-Ergo) (Cached)
+[wp] [Valid] typed_lemma_L_sym_2 (Alt-Ergo) (Cached)
+[wp] [Valid] typed_lemma_L_sym_3 (Alt-Ergo) (Cached)
+[wp] Proved goals: 15 / 15
+ Alt-Ergo: 15
+------------------------------------------------------------
+ Axiomatics WP Alt-Ergo Total Success
+ Lemma - 15 15 100%
+------------------------------------------------------------
--
GitLab