Cyril ADRIAN ha scritto:
> Hello,
>
> I don't understand the following postcondtion:
>
> string_item (a_column: INTEGER): STRING is
> do
> Result ::= item(a_column)
> ensure
> result_not_void: Result /= Void
> end
>
> It looks strange to me, and furthermore it does not hold when the
> column really contains a NULL :-(
>
> Can someone explain why there is this ensure?
>
I assume that you're writing about SQLITE_RESULT_ROW;
I usually put preconditions like that when the underlying function call
primise not to return NULL. I made the assumption that string item would
never be NULL and it could actually be wrong; I'm already adding a
proper check to fix it in trunk.
I'm not sure it is really wrong; in fact I'm pretty sure it is right as
SQLite documentation says sqlite3_column_text will return NULL only when
an "sql NULL" is converted to text; this should never happen in an
Eiffel program because we have preconditions in string_item requiring to
call it only on real string columns.
Paolo
_______________________________________________
Eiffel-libraries-devel mailing list
[email protected]
https://mail.gna.org/listinfo/eiffel-libraries-devel
