backup/EWF
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Fixed wrong code for postcondition on HTTP_HEADER.string

Browse Source 
Patch provided by Paul-G.Crismer
This commit is contained in:
Jocelyn Fiat
2012-02-01 16:53:24 +01:00
parent 67e6b460b3
commit d8476edf36
1 changed files with 2 additions and 2 deletions
Download Patch File Download Diff File Expand all files Collapse all files

4
library/protocol/http/src/http_header.e
View File

@@ -116,8 +116,8 @@ feature -- Access
create Result.make_empty create Result.make_empty
end end
ensure ensure
result_has_ending_cr_lf: Result.count >= 2 implies Result.substring (Result.count - 2, Result.count).same_string ("%R%N") result_has_ending_cr_lf: Result.count >= 2 implies Result.substring (Result.count - 1, Result.count).same_string ("%R%N")
result_has_single_ending_cr_lf: Result.count >= 4 implies not Result.substring (Result.count - 4, Result.count).same_string ("%R%N%R%N") result_has_single_ending_cr_lf: Result.count >= 4 implies not Result.substring (Result.count - 3, Result.count).same_string ("%R%N%R%N")
end end
feature -- Header change: general feature -- Header change: general