Automating NULL check contracts

[sonntag benoit]

Nicolas Boulay <nicolas.boulay at gmail.com> a écrit :

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

Tu ne peux pas le faire dans tous les cas...

Mais j'ai due me planter de papier (je pensais que
c'était celui-ci en vue du simple titre),
l'idée est de mettre une autre valeur que 0 pour la valeur NULL.
Une valeur illégale pour un pointeur de mémoire (pour garantir le crash),
et qui code statiquement l'emplacement dans le code source de l'origine
de l'affectation avec NULL. Ainsi, au moment du crash, le programmeur a aussi
l'information de la ligne où le NULL a été généré.

The idea is to put another value that 0 for NULL value.
An illegal value for a memory store pointer (to guarantee the crash),
and with statically position source code for assignment' position
with NULL.
Thus, at the time of the crash, the programmer has information on the
line where NULL was generated.

>
> 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
>> ?????????? ???????????????????? ??????????
>> ? 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
>>
>>
>