From 3b38931bbb1df41aff50166a8fb7b05ef8f42a96 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Tue, 7 Apr 2020 11:08:49 +0200
Subject: [PATCH] [e-acsl:typing] predicates with reads or inductively defined
may occur
---
src/plugins/e-acsl/src/analyses/typing.ml | 9 +++++++--
1 file changed, 7 insertions(+), 2 deletions(-)
diff --git a/src/plugins/e-acsl/src/analyses/typing.ml b/src/plugins/e-acsl/src/analyses/typing.ml
index a2612ee906f..04731a08f3c 100644
--- a/src/plugins/e-acsl/src/analyses/typing.ml
+++ b/src/plugins/e-acsl/src/analyses/typing.ml
@@ -512,7 +512,7 @@ let rec type_term ~use_gmp_opt ?(arith_operand=false) ?ctx t =
| LBreads _ ->
Error.not_yet "logic functions performing read accesses"
| LBinductive _ ->
- Error.not_yet "logic functions inductively defined"
+ Error.not_yet "inductive logic functions"
end
| Tunion _ -> Error.not_yet "tset union"
@@ -585,8 +585,13 @@ let rec type_predicate p =
c_int
| LBnone -> (* Eg: \is_finite *)
Error.not_yet "predicate with no definition nor reads clause"
- | LBreads _ | LBterm _ | LBinductive _ ->
+ | LBreads _ ->
+ Error.not_yet "predicate performing read accesses"
+ | LBinductive _ ->
+ Error.not_yet "inductive predicate"
+ | LBterm _ ->
Options.fatal "unexpected logic definition"
+ Printer.pp_predicate p
end
| Pseparated _ -> Error.not_yet "\\separated"
| Pdangling _ -> Error.not_yet "\\dangling"
--
GitLab