| Log Message: |
Added missing assertions for `eif_id_object' and `eif_object_id_free' so that the ID is always non-negative.
Fixed postcondition violation in `object_id' after a call to `free_id', assuming that `object_id' was
already called before. The solution is to assign `internal_id' with a negative value when freeing
the `object_id' and to update `object_id' postcondition.
Minor optimization for `id_object' to do something only when the ID is strictly positive.
|
FreeELKS/trunk/library/support/identified.e