Mh, to be honest I believe this is a very hard task, as the compiler needs to statically evaluate conditions and decide if they are always true (or false) - which finally boils down to the Entscheidungsproblem if we'd like to solve it completely :-)

For sure there are situations in which the answer is trivial, simple in many others and still solvable in furthers. It would be great to work on such static evaluations as it would practically mean that we'd prove some contracts of the program. Great as we could avoid evaluation of proven contracts and even (partially) prove the program to be correct (in the sense of "if it terminates, it will satisfy it's postcondition") but I fear we'd need a few PhDs on this to reach a meaningful result.

(Yes, I worked in this direction to transform contracts of Eiffel but also in C into existing languages of SAT solvers during my time at university, but I claim LibertyEiffel to be not quite there yet. -> I propose this to be shifted to the "M" release)

Continuing my experiments with Pelles-C, I noticed that a lot of the code that it flags as 'unreachable code' is generated for Eiffel 'and then' statements, especially so when multiple of them are chained together..

Despite doing global analysis when in boost-mode, Liberty cannot or does not determine, that an 'and then' condition can never happen and generates unneeded code for it.

Just a single example of the many in the current (May 11, 2016) germ:   compile_to_c8.c, lines 1079, 1081, 1082, 1177, 1179, 1180, 1543, 1545, 1546.
As noted, Pelles-C flags many more of these (currently) 135 c-files with the same warning message.