add notion about non-null master
authorMart Lubbers <mart@martlubbers.net>
Wed, 25 Jan 2017 11:07:08 +0000 (12:07 +0100)
committerMart Lubbers <mart@martlubbers.net>
Wed, 25 Jan 2017 11:07:08 +0000 (12:07 +0100)
mock/mock.txt

index 9f687b0..054de8c 100644 (file)
        equal than 0 and smaller than 10. This can be done with an 
        "requires i >= 0" and a "requires i<10"
 
        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
 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