EiffelStudio finalize with contracts enabled

Question

How to produce the Finalized executable with contract checking enabled? It is possible to keep the check statements intact, but can we keep all the pre/postconditions and class invariants?

I need this for testing a computationally expensive application and frozen with contracts executable is a bit too slow in my case.

Answer 1

The IDE shows a dialog on request for finalization that asks whether the assertions should be kept in the generated executable. The dialog is discardable. If you select the checkbox "Do not ask me again", the assertions will NOT be generated and the IDE will NOT show this dialog anymore. You can reset this selection by going to the Parameters (e.g., from the main menu: Tools | Parameters), and restoring the default value for the finalization dialog under Interface | Dialogs.

In the command line, the compiler accepts an option -keep right after -finalize. It tells the compiler to keep assertions when finalizing the executable.

Both the IDE and the compiler pick the settings which assertions should be generated from the project settings. You can specify them for every group (system/library/cluster) and every class individually.

Edit. Here is a minimal example with 2 files:

example.e:

class EXAMPLE create make feature
    make
        local
            n: INTEGER
        do
            if n = 0 then f
            elseif n = 1 then g
            end
        rescue
            n := n + 1
            print ({EXCEPTIONS}.tag_name)
            retry
        end
    f require pre: out = "x" do end
    g do ensure post: out = "x" end
end

example.ecf:

<?xml version="1.0" encoding="ISO-8859-1"?>
<system xmlns="http://www.eiffel.com/developers/xml/configuration-1-21-0" name="example">
    <target name="example">
        <root class="EXAMPLE" feature="make"/>
        <option>
            <assertions precondition="true" postcondition="true"/>
        </option>
        <setting name="console_application" value="true"/>
        <library name="base" location="$ISE_LIBRARY\library\base\base.ecf"/>
        <cluster name="test" location="."/>
    </target>
</system>

Compilation with the options -finalize -keep -config example.ecf -c_compile produces an executable that prints prepost.