When evaluating the value of an expr, the result now will be among +1/-1/0, instead of true/false, as 0 is used to specify that the expr does not exist (in the considered parent-expr context).

Author: theyoucheng

regression/cbmc-cover/mcdc7/main.c

@@ -0,0 +1,8 @@
+int main()
+{
+  signed x, y;
+
+  y = x*123<0 ? 0 : (x*123>100 ? 100 : x*123 );
+
+  return 1;
+}

regression/cbmc-cover/mcdc7/test.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+--cover mcdc
+^EXIT=0$
+^SIGNAL=0$
+^\[main.coverage.1\] file main.c line 5 function main decision/condition `x \* 123 > 100.* false: SATISFIED$
+^\[main.coverage.2\] file main.c line 5 function main decision/condition `x \* 123 > 100.* true: SATISFIED$
+^\[main.coverage.3\] file main.c line 5 function main decision/condition `x \* 123 < 0.* false: SATISFIED$
+^\[main.coverage.4\] file main.c line 5 function main decision/condition `x \* 123 < 0.* true: SATISFIED$
+^\*\* .* of .* covered (100.0%)$
+^\*\* Used 2 iterations$
+--
+^warning: ignoring