bugLiberty Eiffel - Bugs: bug #47905, LE generates 'unreachabel code'...


bug #47905: LE generates 'unreachabel code' for 'and-then' statements

Submitter:  - <_92048>
Submitted:  Thu 12 May 2016 07:00:00 AM UTC
Category:  Liberty tools Severity:  3 - Normal
Priority:  * 5 - Normal Status:  Confirmed
Assigned to:  None Open/Closed:  Open
Release:  bell Fixed Release:  None
Planned Release:  None
* Mandatory Fields

Add a New Comment Rich Markup

Tue 08 Feb 2022 08:30:04 PM UTC, comment #2: 

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)

Raphael Mack <ramack>
Group administrator
Tue 08 Feb 2022 11:25:41 AM UTC, comment #1: 

What is needed to remove this issue?   I'd like to look into this, but have no idea where to start...

- <_92048>
Thu 12 May 2016 07:00:00 AM UTC, original submission:  

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.

- <_92048>


(Note: upload size limit is set to 16384 kB, after insertion of the required escape characters.)

Attach Files:

No files currently attached


Depends on the following items: None found

Items that depend on this one: None found


Carbon-Copy List
  • -email is unavailable- added by ramack (Posted a comment)
  • -email is unavailable- added by _92048 (Submitted the item)

    There are 0 votes so far. Votes easily highlight which items people would like to see resolved in priority, independently of the priority of the item set by tracker managers.

    Only logged-in users can vote.


    Follows 1 latest change.

    Date Changed by Updated Field Previous Value => Replaced by
    2018-07-31 _92048 StatusNone Confirmed

    Back to the top

    Powered by Savane 3.13-599c.
    Corresponding source code