From 38a48ecec60cc3e1edd30f2e839e83274721fe39 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Wed, 10 Feb 2021 12:07:18 +0100
Subject: [PATCH] [wp] CFG: force order of evaluation for conditions
---
src/plugins/wp/cfgCalculus.ml | 10 ++++++----
1 file changed, 6 insertions(+), 4 deletions(-)
diff --git a/src/plugins/wp/cfgCalculus.ml b/src/plugins/wp/cfgCalculus.ml
index 8c35871f631..796e211fe48 100644
--- a/src/plugins/wp/cfgCalculus.ml
+++ b/src/plugins/wp/cfgCalculus.ml
@@ -216,11 +216,13 @@ struct
and control env a s : W.t_prop =
match a.vertex_control with
| If { cond ; vthen ; velse } ->
- W.test env.we s cond (wp env vthen) (wp env velse)
+ let wthen = wp env vthen in
+ let welse = wp env velse in
+ W.test env.we s cond wthen welse
| Switch { value ; cases ; default } ->
- W.switch env.we s value
- (List.map (fun (e,v) -> [e], wp env v) cases)
- (wp env default)
+ let wcases = List.map (fun (e,v) -> [e], wp env v) cases in
+ let wdefault = wp env default in
+ W.switch env.we s value wcases wdefault
| Loop _ ->
let m = env.mode in
let smoking =
--
GitLab