From 1915258c8b2cd2e171bbce93658047a765232bc9 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 13 Oct 2014 09:00:12 +0200 Subject: Revised translation of '&&' and '||' to Clight. The previous translation (in SimplExpr) produced references to the same temporary variable with two different types (bool and int), which is not nice if we want to typecheck the generated Clight. The new translation avoids this and also gets rid of the double cast to bool then to int. The trick is to change Eparen (in CompCert C expressions) to take two types: the type to which the argument must be converted, and the type with which the resulting expression is seen. --- driver/Interp.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'driver/Interp.ml') diff --git a/driver/Interp.ml b/driver/Interp.ml index db4537cb..e277ebe0 100644 --- a/driver/Interp.ml +++ b/driver/Interp.ml @@ -452,7 +452,7 @@ let diagnose_stuck_expr p ge w f a kont e m = | RV, Eassignop(op, l1, r2, tyres, ty) -> diagnose LV l1 ||| diagnose RV r2 | RV, Epostincr(id, l, ty) -> diagnose LV l | RV, Ecomma(r1, r2, ty) -> diagnose RV r1 - | RV, Eparen(r1, ty) -> diagnose RV r1 + | RV, Eparen(r1, tycast, ty) -> diagnose RV r1 | RV, Ecall(r1, rargs, ty) -> diagnose RV r1 ||| diagnose_list rargs | RV, Ebuiltin(ef, tyargs, rargs, ty) -> diagnose_list rargs | _, _ -> false in -- cgit