diff --git a/src/plugins/e-acsl/TODO b/src/plugins/e-acsl/TODO index f2b0831be27079545fc61a38c280f7991a93b844..57f3984c007b27bd912c16d76d797852235b313d 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 ab246dd079b16b2f8b20c8614dfc131c00363ea8..a5df3eccacdf65740837c448cb981a0de431efb4 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 *)