From 2c42c0dd1a57f020bfc1114e328e53b39dc32a67 Mon Sep 17 00:00:00 2001 From: jvelilla Date: Fri, 8 Aug 2008 11:04:33 +0000 Subject: [PATCH] Change void to Void. Add invariant for 'object' , object_no_null /= Void --- json/json_object.e | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/json/json_object.e b/json/json_object.e index 40531f99..b75a9b2b 100644 --- a/json/json_object.e +++ b/json/json_object.e @@ -51,7 +51,7 @@ feature -- Change Element l_value: JSON_VALUE do l_value:=value - if value = void then + if value = Void then create l_json_null l_value:=l_json_null end @@ -133,4 +133,7 @@ feature {NONE} -- Implementation object: HASH_TABLE[JSON_VALUE,JSON_STRING] +invariant + object_not_null: object /= Void + end