summaryrefslogtreecommitdiffstats
path: root/src/file_txt.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/file_txt.c')
-rw-r--r--src/file_txt.c1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/file_txt.c b/src/file_txt.c
index 005b4d62..8c3984ea 100644
--- a/src/file_txt.c
+++ b/src/file_txt.c
@@ -493,6 +493,7 @@ static double is_random(const unsigned char *buffer, const unsigned int buffer_s
@ loop invariant \forall integer j; (0 <= j < i) ==> stats[j] == 0;
@ loop invariant \initialized(&stats[0 .. i-1]);
@ loop assigns i, stats[0 ..i];
+ @ loop variant 256-i;
@ */
for(i=0; i < 256; i++)
stats[i] = 0;