From eee5ff8fdb6d518923fc05cdb83c514cab906cc4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Thu, 17 Oct 2019 11:22:56 +0200
Subject: [PATCH] [qed+wp] fix typo in inductive types for native coq
---
src/plugins/qed/export_coq.ml | 2 +-
src/plugins/wp/tests/wp_bts/bts_2471.i | 22 +++++++++++++++++++
.../oracle_qualif/bts_2471.0.res.oracle | 14 ++++++++++++
.../oracle_qualif/bts_2471.1.res.oracle | 15 +++++++++++++
.../oracle_qualif/bts_2471.2.res.oracle | 16 ++++++++++++++
5 files changed, 68 insertions(+), 1 deletion(-)
create mode 100644 src/plugins/wp/tests/wp_bts/bts_2471.i
create mode 100644 src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2471.0.res.oracle
create mode 100644 src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2471.1.res.oracle
create mode 100644 src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2471.2.res.oracle
diff --git a/src/plugins/qed/export_coq.ml b/src/plugins/qed/export_coq.ml
index 0c4862c0175..8e06fa9404c 100644
--- a/src/plugins/qed/export_coq.ml
+++ b/src/plugins/qed/export_coq.ml
@@ -320,7 +320,7 @@ struct
(fun (c,ts) ->
fprintf fmt "@ | @[<hov 2>%s : " (link_name (self#link c)) ;
List.iter (fun t -> fprintf fmt "@ %a ->" self#pp_tau t) ts ;
- fprintf fmt "@ %a.@]" self#pp_tau result ;
+ fprintf fmt "@ %a@]" self#pp_tau result ;
) cases ;
fprintf fmt ".@]@\n" ;
end
diff --git a/src/plugins/wp/tests/wp_bts/bts_2471.i b/src/plugins/wp/tests/wp_bts/bts_2471.i
new file mode 100644
index 00000000000..2419c0debd8
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bts/bts_2471.i
@@ -0,0 +1,22 @@
+/* run.config
+ DONTRUN:
+ */
+
+/* run.config_qualif
+ OPT: -wp-timeout 1
+ OPT: -wp-prover native:alt-ergo -wp-timeout 1
+ OPT: -wp-prover native:coq
+ */
+
+/*@ axiomatic maps {
+ type model_digit = octet | sextet;
+ logic integer foo(model_digit i);
+ }
+*/
+
+int foo()
+{
+ // Shall not fail (parse error in BTS issue)
+ //@assert ko: \forall int i; i == foo(octet);
+ return 0;
+}
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2471.0.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2471.0.res.oracle
new file mode 100644
index 00000000000..98f16227983
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2471.0.res.oracle
@@ -0,0 +1,14 @@
+# frama-c -wp -wp-timeout 1 [...]
+[kernel] Parsing tests/wp_bts/bts_2471.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
+[wp] 1 goal scheduled
+[wp] [Failed] Goal typed_foo_assert_ko
+[wp] Proved goals: 0 / 1
+[wp] Report in: 'tests/wp_bts/oracle_qualif/bts_2471.0.report.json'
+[wp] Report out: 'tests/wp_bts/result_qualif/bts_2471.0.report.json'
+-------------------------------------------------------------
+Functions WP Alt-Ergo Total Success
+foo - - 1 0.0%
+-------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2471.1.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2471.1.res.oracle
new file mode 100644
index 00000000000..68dc1319cde
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2471.1.res.oracle
@@ -0,0 +1,15 @@
+# frama-c -wp -wp-timeout 1 [...]
+[kernel] Parsing tests/wp_bts/bts_2471.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
+[wp] 1 goal scheduled
+[wp] [Alt-Ergo (Native)] Goal typed_foo_assert_ko : Unsuccess
+[wp] Proved goals: 0 / 1
+ Alt-Ergo: 0 (unsuccess: 1)
+[wp] Report in: 'tests/wp_bts/oracle_qualif/bts_2471.1.report.json'
+[wp] Report out: 'tests/wp_bts/result_qualif/bts_2471.1.report.json'
+-------------------------------------------------------------
+Functions WP Alt-Ergo Total Success
+foo - - 1 0.0%
+-------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2471.2.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2471.2.res.oracle
new file mode 100644
index 00000000000..6c44b75068c
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2471.2.res.oracle
@@ -0,0 +1,16 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_bts/bts_2471.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
+[wp] 1 goal scheduled
+[wp] [Coq] Goal typed_foo_assert_ko : Default tactic
+[wp] [Coq (Native)] Goal typed_foo_assert_ko : Unsuccess
+[wp] Proved goals: 0 / 1
+ Coq: 0 (unsuccess: 1)
+[wp] Report in: 'tests/wp_bts/oracle_qualif/bts_2471.2.report.json'
+[wp] Report out: 'tests/wp_bts/result_qualif/bts_2471.2.report.json'
+-------------------------------------------------------------
+Functions WP Alt-Ergo Total Success
+foo - - 1 0.0%
+-------------------------------------------------------------
--
GitLab