From 951c5398e3574504be884e04b46543c639ab999c Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Thu, 19 Dec 2019 11:16:16 +0100
Subject: [PATCH] [WP] Fix search for qed symbols in Why3 translation (#775)
---
src/plugins/wp/ProverWhy3.ml | 12 ++++++------
1 file changed, 6 insertions(+), 6 deletions(-)
diff --git a/src/plugins/wp/ProverWhy3.ml b/src/plugins/wp/ProverWhy3.ml
index 1284425bd98..61f6651c442 100644
--- a/src/plugins/wp/ProverWhy3.ml
+++ b/src/plugins/wp/ProverWhy3.ml
@@ -364,13 +364,13 @@ let rec of_term ~cnv expected t : Why3.Term.term =
a b
| Leq (a,b), _, Bool ->
int_or_real ~cnv
- ~fint:["qed"] ~lint:"Qed" ~pint:["zleq"]
- ~freal:["qed"] ~lreal:"Qed" ~preal:["rleq"]
+ ~fint:["frama_c_wp"; "qed"] ~lint:"Qed" ~pint:["zleq"]
+ ~freal:["frama_c_wp"; "qed"] ~lreal:"Qed" ~preal:["rleq"]
a b
| Lt (a,b), _, Bool ->
int_or_real ~cnv
- ~fint:["qed"] ~lint:"Qed" ~pint:["zlt"]
- ~freal:["qed"] ~lreal:"Qed" ~preal:["rlt"]
+ ~fint:["frama_c_wp"; "qed"] ~lint:"Qed" ~pint:["zlt"]
+ ~freal:["frama_c_wp"; "qed"] ~lreal:"Qed" ~preal:["rlt"]
a b
| And l, _, Bool ->
t_app_fold ~f:["bool"] ~l:"Bool" ~p:["andb"] ~cnv expected l
@@ -420,9 +420,9 @@ let rec of_term ~cnv expected t : Why3.Term.term =
| _ -> Why3.Term.t_neq (of_term' cnv a) (of_term' cnv b)
end
| Eq (a,b), _, Bool ->
- t_app ~cnv ~f:["qed"] ~l:"Qed" ~p:["eqb"] [of_term' cnv a; of_term' cnv b]
+ t_app ~cnv ~f:["frama_c_wp"; "qed"] ~l:"Qed" ~p:["eqb"] [of_term' cnv a; of_term' cnv b]
| Neq (a,b), _, Bool ->
- t_app ~cnv ~f:["qed"] ~l:"Qed" ~p:["neqb"] [of_term' cnv a; of_term' cnv b]
+ t_app ~cnv ~f:["frama_c_wp"; "qed"] ~l:"Qed" ~p:["neqb"] [of_term' cnv a; of_term' cnv b]
| If(a,b,c), _, _ ->
let cnv' = {cnv with polarity = `NoPolarity} in
Why3.Term.t_if (of_term cnv' Prop a) (of_term cnv expected b) (of_term cnv expected c)
--
GitLab