From 414814aee11612fc23bb75e3482288b2a066947b Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Mon, 7 Sep 2020 11:14:50 +0200
Subject: [PATCH] [tests] fix wp-qualif ml script
---
src/plugins/wp/tests/wp/stmtcompiler_test_rela.ml | 3 ++-
1 file changed, 2 insertions(+), 1 deletion(-)
diff --git a/src/plugins/wp/tests/wp/stmtcompiler_test_rela.ml b/src/plugins/wp/tests/wp/stmtcompiler_test_rela.ml
index 72ab4fc4ef1..513c205deea 100644
--- a/src/plugins/wp/tests/wp/stmtcompiler_test_rela.ml
+++ b/src/plugins/wp/tests/wp/stmtcompiler_test_rela.ml
@@ -54,7 +54,8 @@ let run () =
pred_content = Cil_types.Ptrue;
}
in
- let annot = Logic_const.new_code_annotation (AAssert ([],Assert,pred)) in
+ let pred = Logic_const.toplevel_predicate pred in
+ let annot = Logic_const.new_code_annotation (AAssert ([],pred)) in
let po = Wpo.{
po_gid = "";
po_leg = "";
--
GitLab