@@ -813,10 +813,9 @@ std::string expr2ct::convert_trinary(
813813 if (src.operands ().size ()!=3 )
814814 return convert_norep (src, precedence);
815815
816- const exprt::operandst &operands=src.operands ();
817- const exprt &op0=operands.front ();
818- const exprt &op1=*(++operands.begin ());
819- const exprt &op2=operands.back ();
816+ const exprt &op0=src.op0 ();
817+ const exprt &op1=src.op1 ();
818+ const exprt &op2=src.op2 ();
820819
821820 unsigned p0, p1, p2;
822821
@@ -1028,6 +1027,61 @@ std::string expr2ct::convert_binary(
10281027 const std::string &symbol,
10291028 unsigned precedence,
10301029 bool full_parentheses)
1030+ {
1031+ if (src.operands ().size ()!=2 )
1032+ return convert_norep (src, precedence);
1033+
1034+ const exprt &op0=src.op0 ();
1035+ const exprt &op1=src.op1 ();
1036+
1037+ unsigned p0, p1;
1038+
1039+ std::string s_op0=convert_with_precedence (op0, p0);
1040+ std::string s_op1=convert_with_precedence (op1, p1);
1041+
1042+ std::string dest;
1043+
1044+ // In pointer arithmetic, x+(y-z) is unfortunately
1045+ // not the same as (x+y)-z, even though + and -
1046+ // have the same precedence. We thus add parentheses
1047+ // for the case x+(y-z). Similarly, (x*y)/z is not
1048+ // the same as x*(y/z), but * and / have the same
1049+ // precedence.
1050+
1051+ bool use_parentheses0=
1052+ precedence>p0 ||
1053+ (precedence==p0 && full_parentheses) ||
1054+ (precedence==p0 && src.id ()!=op0.id ());
1055+
1056+ if (use_parentheses0)
1057+ dest+=' (' ;
1058+ dest+=s_op0;
1059+ if (use_parentheses0)
1060+ dest+=' )' ;
1061+
1062+ dest+=' ' ;
1063+ dest+=symbol;
1064+ dest+=' ' ;
1065+
1066+ bool use_parentheses1=
1067+ precedence>p1 ||
1068+ (precedence==p1 && full_parentheses) ||
1069+ (precedence==p1 && src.id ()!=op1.id ());
1070+
1071+ if (use_parentheses1)
1072+ dest+=' (' ;
1073+ dest+=s_op1;
1074+ if (use_parentheses1)
1075+ dest+=' )' ;
1076+
1077+ return dest;
1078+ }
1079+
1080+ std::string expr2ct::convert_multi_ary (
1081+ const exprt &src,
1082+ const std::string &symbol,
1083+ unsigned precedence,
1084+ bool full_parentheses)
10311085{
10321086 if (src.operands ().size ()<2 )
10331087 return convert_norep (src, precedence);
@@ -3386,7 +3440,7 @@ std::string expr2ct::convert_with_precedence(
33863440 precedence=16 ;
33873441
33883442 if (src.id ()==ID_plus)
3389- return convert_binary (src, " +" , precedence=12 , false );
3443+ return convert_multi_ary (src, " +" , precedence=12 , false );
33903444
33913445 else if (src.id ()==ID_minus)
33923446 return convert_binary (src, " -" , precedence=12 , true );
@@ -3690,7 +3744,7 @@ std::string expr2ct::convert_with_precedence(
36903744 return convert_unary (src, " ~" , precedence=15 );
36913745
36923746 else if (src.id ()==ID_mult)
3693- return convert_binary (src, " *" , precedence=13 , false );
3747+ return convert_multi_ary (src, " *" , precedence=13 , false );
36943748
36953749 else if (src.id ()==ID_div)
36963750 return convert_binary (src, " /" , precedence=13 , true );
@@ -3739,22 +3793,22 @@ std::string expr2ct::convert_with_precedence(
37393793 return convert_complex (src, precedence=16 );
37403794
37413795 else if (src.id ()==ID_bitand)
3742- return convert_binary (src, " &" , precedence=8 , false );
3796+ return convert_multi_ary (src, " &" , precedence=8 , false );
37433797
37443798 else if (src.id ()==ID_bitxor)
3745- return convert_binary (src, " ^" , precedence=7 , false );
3799+ return convert_multi_ary (src, " ^" , precedence=7 , false );
37463800
37473801 else if (src.id ()==ID_bitor)
3748- return convert_binary (src, " |" , precedence=6 , false );
3802+ return convert_multi_ary (src, " |" , precedence=6 , false );
37493803
37503804 else if (src.id ()==ID_and)
3751- return convert_binary (src, " &&" , precedence=5 , false );
3805+ return convert_multi_ary (src, " &&" , precedence=5 , false );
37523806
37533807 else if (src.id ()==ID_or)
3754- return convert_binary (src, " ||" , precedence=4 , false );
3808+ return convert_multi_ary (src, " ||" , precedence=4 , false );
37553809
37563810 else if (src.id ()==ID_xor)
3757- return convert_binary (src, " ^" , precedence=7 , false );
3811+ return convert_multi_ary (src, " ^" , precedence=7 , false );
37583812
37593813 else if (src.id ()==ID_implies)
37603814 return convert_binary (src, " ==>" , precedence=3 , true );
0 commit comments