Automating NULL check contracts

Nicolas Boulay nicolas.boulay at gmail.com
Wed Sep 30 17:20:10 UTC 2009


normalement le compilo doit vérifier cela. C'était la feature majeur l'an
passé.

2009/9/30 Mildred Ki'Lya <ml.mildred593 at gmail.com>

>  More explanations ...
> (french translation afterwards)
>
> On 09/30/2009 06:05 PM, Mildred Ki'Lya wrote:
>
> Now, Bertrang Meyer's version of Eiffel have something to avoid calls on
> NULL:
>
> http://bertrandmeyer.com/2009/08/04/void-safety-getting-rid-of-the-spectre-of-null-pointer-dereferencing/
> http://docs.eiffel.com/sites/default/files/void-safe-eiffel.pdf
>
>
> The main idea in this paper is that types can be either attached or
> detached (a keyword specifies this)
>
> Variables with unattached types can contain NULL values. This is the
> default for most languages.
>
> Variables having an attached types are not allowed to contain NULL. This is
> checked at compile time by ensuring that these variables cannot be affected
> with unattached expression. If you want to affect them with unattached
> expressions, you have to check for NULL before.
>
> Now, the compiler can give you an error when you try to call a slot on an
> unattached variables because this may be a cause of call on NULL.
>
>
> ------------------------------
>
> La version d'Eiffel de Bertrand Meyer a corrigé ce problème pour éviter
> tout appel sur NULL:
>
> http://bertrandmeyer.com/2009/08/04/void-safety-getting-rid-of-the-spectre-of-null-pointer-dereferencing/
> http://docs.eiffel.com/sites/default/files/void-safe-eiffel.pdf
>
>
> L'idée principale de ce papier c'est qu'un type peux être soit attaché ou
> détaché (un mot chef est rajouté au langage).
>
> Les variables avec un type détaché peuvent contenir des valeurs NULL. C'est
> le cas par défaut pour la majorité des langages.
>
> Les variables avec un type attaché ne sont pas autorisées à contenir des
> valeurs NULL. C'est vérifié au moment de la compilation. Le compilateur
> vérifie que ces variables ne peuvent pas être affectées par des expression
> de type détaché. Si on veut tout de même faire une affectation, on doit
> vérifier que l'expression n'est pas NULL avant.
>
> Cela permet au compilateur de signaler une erreur lorsqu'il y a un appel
> sur un type détaché, car il est la cause potentielle de crash "call on
> NULL".
>
> --
> Mildred Ki'Lya
> ╭───────── mildred593@online.fr ──────────
> │ Jabber, GoogleTalk: <mildred at jabber.fr> <mildred at jabber.fr>
> │ Website: <http://ki.lya.online.fr> <http://ki.lya.online.fr>           GPG ID: 9A7D 2E2B
> │ Fingerprint: 197C A7E6 645B 4299 6D37 684B 6F9D A8D6 9A7D 2E2B
>
>
> _______________________________________________
> Lisaac-devel mailing list
> Lisaac-devel at lists.alioth.debian.org
> http://lists.alioth.debian.org/mailman/listinfo/lisaac-devel
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.alioth.debian.org/pipermail/lisaac-devel/attachments/20090930/f5b40026/attachment-0001.htm>


More information about the Lisaac-devel mailing list