How to convert your code to be void-safe?

by Manu (modified: 2014 Feb 27)

More and more code is becoming void-safe and today you want to turn an existing library into a completely void-safe one. If you start by setting the void-safety level to its highest setting, you might get discouraged quickly by the sheer number of errors. Instead we recommend that you migrate your code step by step by enabling the various void-safety levels, starting from the lowest one until you fix all the errors and going to the next one and repeat the operation until you reach the highest level. At this point you will have a completely void-safe library.

The article does not aim at being exhaustive in all the things you can do to convert code to void-safety, but we believe that if followed it can help a lot in migrating code without introducing ugly code.


  1. Edit your project configuration file to use void-safe versions of existing libraries you are referring to.
  2. Make sure that the setting `attached by default' is set to True. It is most likely that the Eiffel standard specification will not allow to change this.
  3. Read the documentation on how to create a void-safe project from the Eiffel documentation site.

Conformance level

Enabling this level means that now attachment marks are not ignored. If it was just that, your code would compile out of the box. Fortunately (or unfortunately depending on the point of view you are taking), your code is most likely using void-safe libraries such as EiffelBase, EiffelVision, .... This actually might cause your code to fail. For example, the type of the source of an assignment is detachable and the target is attached. This is where you need to ask yourself the question or whether or not you should add the detachable keyword to your type declaration, if not then you need to change the code flow of your code to handle the possible Void value your might get.

In this mode of compilation, the second thing you will find yourself doing the most in addition of adding detachable to type declaration is adding object tests. For example, if you had:

target: X .... target := detachable_query if target /= Void then target.do_something end

you will need to do:if attached detachable_query as l_target then l_target.do_something end

Once you have fixed all those errors, you will gain the following:

  • A better understanding of your code by clearly marking what is attached and what is detachable
  • A step closer to complete void-safety

At the end of this steps, perform your regression testing as everything should still work as before.

Initialization level

Once your code compiles at the conformance level, enabling the initialization level will most likely cause errors for all attached entities that are not set before usage. To be precise:

  • For attached attributes, they need to be properly initialized in all creation procedures of the current class and its descendants.
  • For attached locals, they need to be set via an explicit creation or via an assignment from an attached expression.

In this step, you might add more detachable declarations. After that it is just a matter of making sure that everything is set before usage. This step should be the quickest of all the steps to convert existing code to void-safety.

At the end of this step, perform all the regression testing.

Complete level

Now we can go all the way to complete. In this compilation mode, the compiler will now check that:

  • No direct or indirect usage of Current is done before all attributes have been set.
  • All qualified calls are done on attached expressions.

One typical issue you might face in creation procedures is related to Current and the usage of agent on unqualified calls (case of indirect use of Current). You can only use it when all attributes have been set. Which means that calls involving Current or agent creation on unqualified calls need to be postponed to the very end of a creation procedure.

Depending on the library it might be easy, or it could be difficult and require you to change some fundamental designs. Here there is not much recommendation we can make, it is up to you to step back and think more about the whole architecture.

Once you have achieved this goal, perform your final regression testing to be sure nothing is broken. Congratulation! You just made your library completely void-safe.

The thing not to do

Never use anything like to please the compiler in thinking that the code is void-safe.check attached entity as l_entity then l_entity.do_something endIf not done properly, it means you will get an exception at runtime which is most likely something you do not want. Instead you have to think about the reason why you think it is indeed correct (see below). In very few cases, you have to resort to this but it should be done very carefully with comments to explain the rationale why you cannot do otherwise.


There is a precondition that states it is attached. In this case, I distinguish 4 cases depending on the nature of the routine:

  • Boolean query: Depending of the nature of the query, often answering False is always good, so you can remove the precondition and simply have:

Result := not attached entity as l_entity or else l_entity.some_boolean_property

  • Detachable query: the result is detachable, this is very similar to the boolean query case, and you can thus remove the precondition and simply have:

if attached entity as l_entity then Result := .... end

  • Attached query: this is where it is probably the most difficult thing to answer. If you can create a dummy object then

if attached entity as l_entity then .... else check entity_attached: False end create Result.some_creation_procedure endthis is completely fine because if you violate the precondition, you still get a precondition violation. The check instruction is to show the reader you understood that this should not happen, and the creation to satisfy void-safety. In the event you are running with precondition disabled and check enabled, you will catch this defect too. If you run without any assertions, you are getting an unspecified behavior which is the expected outcome when you violate a precondition.

  • Command: it is like an attached query in much simpler since we just need to keep the check:

-- Per precondition if attached entity as l_entity then .... else check entity_attached: False end end


The state of the current instance tells you it is attached. But if there is nothing to tell you otherwise, it means you are lacking some contracts, either invariants or preconditions. The resolution is often close to what is described for when the attached status of an entity is given by the precondition.

Things to look for

Thanks for Alexander Kogtenkov to raising this. They are a few things you should look out for that can help finding out when to use an attached or detachable type.

Type of arguments

If you have an existing precondition checking that the argument cannot be Void, you should make sure that the type of the corresponding formal argument is attached. When it is a class type, usually there is nothing to do since it is attached by default. But if this is an anchor to something detachable, you need to add the attached mark.

On the other hand, if by reading the precondition you see that the argument may be Void, then you should change the type declaration to be detachable.

Type of Result

Similarly to arguments, if the postcondition states Result /= Void clearly the type of Result should be attached, and otherwise detachable.

Stable attribute

Sometime you have some attributes of a class that do not need to be set in the creation procedure and that once set will always be attached. We call them stable attributes. Although they are not standardized, we have introduced a syntax for them:

stable_attribute: detachable X note option: stable attribute end

This will tell the compiler that it is ok to use this attribute once it has been proven to be set, and the compiler will forbid reattachment where the source is detachable.

if stable_attribute /= Void then stable_attribute.do_something end

If it was not stable, you would have to use an object test to use it.

  • Alexander Kogtenkov (10 years ago 28/2/2014)

    Using attached types instead of assertions

    Some assertions clearly indicate whether a particular type should be declared as attached (this is the default status when void safety is enabled and the keyword detachable is not added to the type declaration). In particular, a precondition of the form arg1 /= Void indicates that the argument arg1 is better declared as attached all the time. Similarly, a postcondition of the form Result /= Void indicates that the type of the feature is attached.

    On the other hand, if "something" in the code is checked against Void then most probably this "something" is of a detachable type.

  • Victorien Elvinger (10 years ago 3/4/2014)


    What is the difference between:

    if attached entity as l_entity then .... else check entity_attached: False then end end


    check entity_attached: attached entity as l_entity then ... end ?

    I would rather the second choice...

    • Manu (10 years ago 16/4/2014)

      There is no difference in what you proposed. However what I was proposing was different since the else's compound should read check entity_attached: False end, that is to say I'm not using the check ... then ... end syntax but the traditional check for assertion. I want to emphasize that you can do that when for a query returning a default value is an acceptable answer even if your assumptions are wrong. Or for a command that not doing something is also a good behavior.

      The difference now is more flagrant because now if I run production code without assertion monitoring the application is not going to crash unexpectedly. However during testing/development we might get an assertion violation and then the person who will get the failure will understand that some assumptions were not true.

      For example, in the following command, I would never use check ... then ... end and could simply write the following which is fully correct per the specification:

      do_something require x_attached: x /= Void do if attached x as l_x then l_x.do_something end end

      It is too bad that we have to check the attachment status of x a second time since we already have the precondition that attribute x should be attached when calling do_something, but that's one of the downside of code migration. Nevertheless thanks to the precondition, we do not need to add a check instruction to test if <eiffe>x</eiffel> is attached in the body of do_something. However to show to the reader that we understood what we were doing, I recommend writing: do_something require x_attached: x /= Void do if attached x as l_x then l_x.do_something else -- Per precondition check x_attached: x /= Void end end end It is mostly a question of style and what we want to achieve at the end. Especially in the case of queries, I like them to not have any preconditions so that if you ask the question and it does not make sense to ask it, instead of raising a precondition violation, you can simply return the default value. For boolean queries it is obviously False, for integer queries it is 0, for references it is Void (meaning that now the query should return detachable X instead of just X),....

      • Victorien Elvinger (10 years ago 19/4/2014)

        A bit disturbed...

        Tanks for the reply.

        Please, help me to understand your viewpoint...

        If I have the query: count: INTEGER require structure /= Void do check attached structure as l_structure then Result := l_structure.count end end

        You propose to refactor it with: count: INTEGER require structure /= Void do if attached structure as l_structure then Result := l_structure.count else check structure /= Void end -- Result = 0 end end

        Thanks to this, in production mode the query is running even if `structure ' is Void. But since the execution is out of the routine domain why acept this? It disturbs me a bit, since the routine domain definition in the debug mode is different of the one in the production mode...

        I don't understand the real advantage. Maybe safety? So, in this case, why not weaken the routine precondition?

        count: INTEGER then if attached structure as l_structure then l_structure.count end end

        I like them to not have any preconditions so that if you ask the question and it does not make sense to ask it, instead of raising a precondition violation, you can simply return the default value.

        I accept it and I'm glad to be on the same line ;) Most of the queries should be without preconditions on state requirement (I talk of state requirement or preconditions on Current because I think precondition on arguments are legitimate). However in some cases, preconditions on state requirement are very useful. e.g.: item (a_key: K): G require has (a_key) I wouldn't like that item' answers to two questions: Is a_key' existing? and what is the item associated with `a_key'? such as here: maybe_item (a_key: K): detachable G ensure not has (a_key) implies Result = Void (Yes, the example is badly choosen since `G' could be a detachable type...)

        However, when we don't know if `a key' exists, this code is not very satisfying: if map.has (l_key) then l_item := map.item (l_key) ... end I prefer: if attached map.maybe_item (l_key) as l_item then ... end Maybe the both queries (item' and maybe_item') should coexist...

        What is your opinion on this?

        For boolean queries it is obviously False, for integer queries it is 0, for references it is Void (meaning that now the query should return detachable X

        I am not so sure... I think the default value depends on the context... It is a reason why I proposed to explicitly initialize expanded variables (Why "False" would be more legitimate than "True" as default value?).

        I think it is a bit different with detachable types, since detachable seems optional, the Void value is naturally the default one.