From: Mart Lubbers <mart@martlubbers.net>
Date: Wed, 25 Jan 2017 11:07:08 +0000 (+0100)
Subject: add notion about non-null
X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;ds=inline;p=ss1617.git

add notion about non-null
---

diff --git a/mock/mock.txt b/mock/mock.txt
index 9f687b0..054de8c 100644
--- 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