From 23561e0c4cc13e72befd957da8e53837c48979f0 Mon Sep 17 00:00:00 2001 From: Mart Lubbers Date: Wed, 25 Jan 2017 12:07:08 +0100 Subject: [PATCH] add notion about non-null --- mock/mock.txt | 2 ++ 1 file changed, 2 insertions(+) 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 -- 2.20.1