add notion about non-null

[ss1617.git] / mock / mock.txt

diff --git a/mock/mock.txt b/mock/mock.txt
index 9f687b0..054de8c 100644 (file)
--- a/mock/mock.txt
+++ b/mock/mock.txt
@@ -115,6 +115,8 @@
        equal than 0 and smaller than 10. This can be done with an 
        "requires i >= 0" and a "requires i<10"
 
+       Moreover the array may never be null. Thus we add the non_null invariant to
+       the array contains.
 12.
        The execution time of i and ii will be the same because the PPC code will
        not insert runtime checks. It will just statically analyse whether the code