From a73ef1f1aa40602cd82fd5091b3235828406b6b3 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Thu, 10 Mar 2011 14:11:40 +0000
Subject: [PATCH] update TODO-list
---
src/plugins/e-acsl/TODO | 4 ++--
src/plugins/e-acsl/visit.ml | 7 +++----
2 files changed, 5 insertions(+), 6 deletions(-)
diff --git a/src/plugins/e-acsl/TODO b/src/plugins/e-acsl/TODO
index f2b0831be27..57f3984c007 100644
--- a/src/plugins/e-acsl/TODO
+++ b/src/plugins/e-acsl/TODO
@@ -1,12 +1,12 @@
-- déboguer opérateurs binaires logiques
-- tester les opérations binaires sur les pointeurs
+- tester les opérations binaires sur les pointeurs (requiert complex left value)
- amélioration des locs quand possible (genre Prel)
- améliorer test "comparison.i" quand bug fixed #744
- remettre test "cast.i" quand bug fixed #744
- améliorer test "integer_constant.i" quand bug fixed #745
+- améliorer test "arith.i" quand bug fixed #744
en lien avec bts #743:
- make distrib
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index ab246dd079b..a5df3eccacd 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -265,14 +265,13 @@ let rec term_to_exp t = match t.term_node with
New_vars.push_and_mpz_init (fun _ e -> mk_call name [ e; e1; e2 ])
| TBinOp(Lt | Gt | Le | Ge | Eq | Ne as bop, t1, t2) ->
(* comparison operators *)
- (* [TODO] don't work; see code comment in arith.i *)
comparison_to_exp bop t1 t2
- | TBinOp((LOr | LAnd | BOr | BXor | BAnd), _, _) ->
- (* left/right shift *)
- not_yet "missing binary operator"
| TBinOp((Shiftlt | Shiftrt), _, _) ->
(* left/right shift *)
not_yet "left/right shift"
+ | TBinOp((LOr | LAnd | BOr | BXor | BAnd), _, _) ->
+ (* other logic/arith operators *)
+ not_yet "missing binary operator"
| TBinOp(PlusPI | IndexPI | MinusPI | MinusPP as bop, t1, t2) ->
(* binary operation over pointers *)
(* [TODO] untested *)
--
GitLab