Change void to Void.
Add invariant for 'object' , object_no_null /= Void
This commit is contained in:
@@ -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
|
||||
|
||||
Reference in New Issue
Block a user