Nested loop example

[lwli11]

To save time, some templates for annotations for common constructs should be provided. I had to look through the git issues to find this was how to write the nested loop annotation. It was not clear that in inner loop needed the annotation to be i<10i32 instead of i<=10i32:

int test(){
        //int i=0;
        //int j=0;
        int v=0;
        for (int i=0; i<10; ++i)
                /*@
                  inv i>=0i32; i<=10i32;
                  @*/

        {
                for (int j=0; j<10; j++)

                        /*@
                          inv
                          i>=0i32; i<10i32;
                          j>=0i32; j<=10i32;
                          @*/
                {

                        v=0;
                }


        }
        return 1;
}

[lwli11]

Probably worth noting that you don't need any annotations in a single loop if iterating over a variable, but seems you do for nested loops:

This verifies with no annotations:

int test(int num)
{
        for (int i=0; i<num; i++)
        {

                        int j=0;




        }
       

But this needs annotations:

int test(int num)
/*@
        requires num>=0i32;
@*/

{
        for (int i=0; i<num; i++)
        /*@
                inv i>=0i32; i<=num;
        @*/
        {
                for (int k=0; k<10; k++)
                /*@
                        inv i>=0i32; i<num;
                @*/
                {
                        int j=0;

                }


        }
        return 1;
}