Index: test/small1/logical2.c
===================================================================
--- test/small1/logical2.c	(revision 0)
+++ test/small1/logical2.c	(revision 0)
@@ -0,0 +1,10 @@
+int main() {
+  int x = 0;
+  int keep1 = x && x;
+  int keep2 = x || x;
+  int keep3 = x++ && x;
+  int keep4 = x++ || x;
+  int unfold1 = x && x++;
+  int unfold2 = x || ++x;
+  return 0;
+}
Index: test/small1/logical3.c
===================================================================
--- test/small1/logical3.c	(revision 0)
+++ test/small1/logical3.c	(revision 0)
@@ -0,0 +1,6 @@
+#include <stdio.h>
+int main() {
+  long long x = 0x100000000LL;
+  if (x && x) printf("x\n");
+  return 0;
+}
Index: test/small1/question3.c
===================================================================
--- test/small1/question3.c	(revision 0)
+++ test/small1/question3.c	(revision 0)
@@ -0,0 +1,12 @@
+int main() {
+  int x, y, z;
+  int keep1   = x ? y : z;
+  int unfold1 = x ? y : z++;
+  int unfold2 = x ? y++ : z;
+  int unfold3 = x ? y++ : z++;
+  int keep2   = x++ ? y : z;
+  int unfold4 = x++ ? y : z++;
+  int unfold5 = x++ ? y++ : z;
+  int unfold6 = x++ ? y++ : z++;
+  return 0;
+}
Index: test/small1/booleanOp.c
===================================================================
--- test/small1/booleanOp.c	(revision 0)
+++ test/small1/booleanOp.c	(revision 0)
@@ -0,0 +1,4 @@
+int main() {
+	int x = 0;
+	return 1 && x == 4;
+}
Index: test/small1/logical1.c
===================================================================
--- test/small1/logical1.c	(revision 0)
+++ test/small1/logical1.c	(revision 0)
@@ -0,0 +1,18 @@
+#include "testharness.h"
+
+int main() {
+  int *p = 0;
+  if(!(1 || *p)) {
+    E(1);
+  }
+  if(!(*p || 1)) {
+    E(2);
+  }
+  if(*p && 0) {
+    E(3);
+  }
+  if(0 && *p) {
+    E(4);
+  }
+  SUCCESS;
+}
Index: src/check.ml
===================================================================
--- src/check.ml	(revision 11933)
+++ src/check.ml	(working copy)
@@ -547,6 +547,17 @@
               typeMatch tres intType;
               tres
       end
+
+      | Question (e1, e2, e3, tres) -> begin
+          let t1 = checkExp isconst e1 in
+          let t2 = checkExp isconst e2 in
+          let t3 = checkExp isconst e3 in
+          checkBooleanType t1;
+          typeMatch t2 t3;
+          typeMatch t2 tres;
+          tres
+      end
+
       | AddrOf (lv) -> begin
           let tlv = checkLval isconst true lv in
           (* Only certain types can be in AddrOf *)
Index: src/cil.mli
===================================================================
--- src/cil.mli	(revision 11933)
+++ src/cil.mli	(working copy)
@@ -593,6 +593,9 @@
     (** Binary operation. Includes the type of the result. The arithmetic 
      * conversions are made explicit for the arguments. *)
 
+  | Question   of exp * exp * exp * typ
+    (** (a ? b : c) operation. Includes the type of the result *)
+
   | CastE      of typ * exp            
     (** Use {!Cil.mkCast} to make casts.  *)
 
Index: src/ext/pta/ptranal.ml
===================================================================
--- src/ext/pta/ptranal.ml	(revision 11933)
+++ src/ext/pta/ptranal.ml	(working copy)
@@ -244,6 +244,7 @@
       | AlignOf _ -> A.bottom ()
       | UnOp (op, e, t) -> analyze_expr e
       | BinOp (op, e, e', t) -> A.join (analyze_expr e) (analyze_expr e')
+      | Question (_, e, e', _) -> A.join (analyze_expr e) (analyze_expr e')
       | CastE (t, e) -> analyze_expr e
       | AddrOf l ->
           if !fun_ptrs_as_funs && isFunctionType (typeOfLval l) then
Index: src/ext/simplify.ml
===================================================================
--- src/ext/simplify.ml	(revision 11933)
+++ src/ext/simplify.ml	(working copy)
@@ -104,6 +104,8 @@
   | Lval lv -> Lval (simplifyLval setTemp lv)
   | BinOp(bo, e1, e2, tres) -> 
       BinOp(bo, makeBasic setTemp e1, makeBasic setTemp e2, tres)
+  | Question _ ->
+      E.s (bug "Simplify: There should not be a \"?:\" operator here.")
   | UnOp(uo, e1, tres) -> 
       UnOp(uo, makeBasic setTemp e1, tres)
   | CastE(t, e) -> 
Index: src/ext/predabst.ml
===================================================================
--- src/ext/predabst.ml	(revision 11933)
+++ src/ext/predabst.ml	(working copy)
@@ -207,6 +207,11 @@
 	  let e1 = transExp e1 in
 	  let e2 = transExp e2 in
 	  transBinOp op e1 e2
+      | Question (e1,e2,e3,_) ->
+	  let e1 = transExp e1 in
+	  let e2 = transExp e2 in
+	  let e3 = transExp e3 in
+	  T.mkIte e1 e2 e3
       | SizeOf typ -> T.mkConst ((bitsSizeOf typ)/8)
       | SizeOfE e -> transExp (SizeOf(typeOf e))
       | SizeOfStr s -> T.mkConst (1 + String.length s)
Index: src/ciloptions.ml
===================================================================
--- src/ciloptions.ml	(revision 11933)
+++ src/ciloptions.ml	(working copy)
@@ -292,6 +292,12 @@
     (" Prevent small chunks of code from being duplicated" ^
        is_default (not !Cabs2cil.allowDuplication));
 
+    "--useLogicalOperators",
+    Arg.Set Cil.useLogicalOperators,
+    (" Where possible (that is, if there are no side-effects),\n\t\t\t\t" ^
+       "retain &&, ||, and ?: (instead of transforming them to If statements)" ^
+       is_default !Cil.useLogicalOperators);
+
     "--keepunused",
     Arg.Set Rmtmps.keepUnused,
     (" Do not remove the unused variables and types" ^
Index: src/frontc/cabs2cil.ml
===================================================================
--- src/frontc/cabs2cil.ml	(revision 11933)
+++ src/frontc/cabs2cil.ml	(working copy)
@@ -3924,7 +3924,7 @@
         match ce with
           CEExp (se, ((Const _) as c)) -> 
             finishExp se (if isConstTrue c then one else zero) intType
-	| CEExp (se, (UnOp(LNot, _, _) as e)) ->
+	| CEExp (se, ((UnOp(LNot, _, _)|BinOp((Lt|Gt|Le|Ge|Eq|Ne|LAnd|LOr), _, _, _)) as e)) ->
 	    (* already normalized to 0 or 1 *)
 	    finishExp se e intType
         | CEExp (se, e) ->
@@ -4385,7 +4385,15 @@
              | Some e2' -> 
                  finishExp (se1 @@ se2) (snd (castTo t2 tresult e2')) tresult
            end
-
+        | CEExp (se1, e1') when !useLogicalOperators && isEmpty se2 && isEmpty se3 ->
+           let e2' = match e2'o with
+               None -> (* use e1' *)
+                 snd (castTo t2 tresult e1')
+             | Some e2' -> 
+                 snd (castTo t2 tresult e2')
+           in
+           let e3' = snd (castTo t3 tresult e3') in
+           finishExp se1 (Question (e1', e2', e3', tresult)) tresult
         | _ -> (* Use a conditional *) begin
             match e2'o with 
               None -> (* has form "e1 ? : e3"  *)
@@ -4661,11 +4669,14 @@
               ce1 
             else 
               CEAnd (ce1, ce2)
+      | CEExp(se1, _), CEExp (se2, ((Const _) as ci2)) when isEmpty se2 ->
+          if isConstTrue ci2 then (* The second argument is true, so drop it *)
+            ce1
+          else (* The second argument is false, so evaluate to false *)
+            CEExp (se1, zero)
       | CEExp(se1, e1'), CEExp (se2, e2') when 
-              !useLogicalOperators && isEmpty se1 && isEmpty se2 -> 
-          CEExp (empty, BinOp(LAnd, 
-                              makeCast e1' intType, 
-                              makeCast e2' intType, intType))
+              !useLogicalOperators && isEmpty se2 -> 
+          CEExp (se1, BinOp(LAnd, e1', e2', intType))
       | _ -> CEAnd (ce1, ce2)
     end
 
@@ -4682,11 +4693,14 @@
               ce1 
             else 
               CEOr (ce1, ce2)
-
+      | CEExp(se1, _), CEExp (se2, ((Const _) as ci2)) when isEmpty se2 ->
+          if isConstFalse ci2 then (* The second argument is false, so drop it *)
+            ce1
+          else (* The second argument is true, so evaluate to true *)
+            CEExp (se1, one)
       | CEExp (se1, e1'), CEExp (se2, e2') when 
-              !useLogicalOperators && isEmpty se1 && isEmpty se2 ->
-          CEExp (empty, BinOp(LOr, makeCast e1' intType, 
-                              makeCast e2' intType, intType))
+              !useLogicalOperators && isEmpty se2 ->
+          CEExp (se1, BinOp(LOr, e1', e2', intType))
       | _ -> CEOr (ce1, ce2)
     end
 
Index: src/cil.ml
===================================================================
--- src/cil.ml	(revision 11933)
+++ src/cil.ml	(working copy)
@@ -488,6 +488,9 @@
                                             type of the result. The arithemtic
                                             conversions are made  explicit
                                             for the arguments *)
+  | Question   of exp * exp * exp * typ
+                                        (** (a ? b : c) operation. Includes
+                                            the type of the result *)
   | CastE      of typ * exp            (** Use {!Cil.mkCast} to make casts *)
 
   | AddrOf     of lval                 (** Always use {!Cil.mkAddrOf} to 
@@ -1748,6 +1751,7 @@
 let questionLevel = 100
 let getParenthLevel (e: exp) = 
   match e with 
+  | Question _ -> questionLevel
   | BinOp((LAnd | LOr), _,_,_) -> 80
                                         (* Bit operations. *)
   | BinOp((BOr|BXor|BAnd),_,_,_) -> bitwiseLevel (* 75 *)
@@ -1860,8 +1864,9 @@
   | Lval(lv) -> typeOfLval lv
   | SizeOf _ | SizeOfE _ | SizeOfStr _ -> !typeOfSizeOf
   | AlignOf _ | AlignOfE _ -> !typeOfSizeOf
-  | UnOp (_, _, t) -> t
-  | BinOp (_, _, _, t) -> t
+  | UnOp (_, _, t)
+  | BinOp (_, _, _, t)
+  | Question (_, _, _, t)
   | CastE (t, _) -> t
   | AddrOf (lv) -> TPtr(typeOfLval lv, [])
   | StartOf (lv) -> begin
@@ -3268,6 +3273,13 @@
           ++ (self#pExpPrec level () e2)
           ++ unalign
 
+    | Question(e1,e2,e3,_) -> 
+        (self#pExpPrec level () e1)
+          ++ text " ? "
+          ++ (self#pExpPrec level () e2)
+          ++ text " : "
+          ++ (self#pExpPrec level () e3)
+
     | CastE(t,e) -> 
         text "(" 
           ++ self#pType None () t
@@ -4593,6 +4605,10 @@
       dprintf "%a(@[%a,@?%a@])" d_plainbinop b
         self#pExp e1 self#pExp e2
 
+  | Question(e1,e2,e3,_) -> 
+      dprintf "Question(@[%a,@?%a,@?%a@])"
+        self#pExp e1 self#pExp e2 self#pExp e3
+
   | SizeOf (t) -> 
       text "sizeof(" ++ self#pType None () t ++ chr ')'
   | SizeOfE (e) -> 
@@ -5091,6 +5107,9 @@
   | BinOp (bo, e1, e2, t) -> 
       let e1' = vExp e1 in let e2' = vExp e2 in let t' = vTyp t in
       if e1' != e1 || e2' != e2 || t' != t then BinOp(bo, e1',e2',t') else e
+  | Question (e1, e2, e3, t) -> 
+      let e1' = vExp e1 in let e2' = vExp e2 in let e3' = vExp e3 in let t' = vTyp t in
+      if e1' != e1 || e2' != e2 || e3' != e3 || t' != t then Question(e1',e2',e3',t') else e
   | CastE (t, e1) ->           
       let t' = vTyp t in let e1' = vExp e1 in
       if t' != t || e1' != e1 then CastE(t', e1') else e
@@ -5979,6 +5998,7 @@
   | Const _ -> true
   | UnOp (_, e, _) -> isConstant e
   | BinOp (_, e1, e2, _) -> isConstant e1 && isConstant e2
+  | Question (e1, e2, e3, _) -> isConstant e1 && isConstant e2 && isConstant e3
   | Lval (Var vi, NoOffset) -> 
       (vi.vglob && isArrayType vi.vtype || isFunctionType vi.vtype)
   | Lval _ -> false
