Easy: Misuse of loop changing clause #452 (10 hrs)

[AdityaSenthilvel]

Including a changing clause for a loop but listing only a subset of changing variables is an error.

• [x] Look into where specifications are processed
• [ ] Create standardized warning/error format
• [ ] Write prototype
• [ ] Write tests for correct errors/warnings
• [ ] Do code review

[drholly77]

@rhit-csse-projects/t17-2425

Here is an example RESOLVE loop:

6       While ( 1 <= Length(Q) )
7           changing Q, T, E;
8           maintaining #Q = T o <E> o Q;
9           decreasing |Q|;
10      do
11          Enqueue(E,T);
12          Dequeue(E,Q);
13      end;

Inclusion (or not) of the changing clause by the developer:

• if it is completely left out, then all variables used in the loop body may change, no error, no warning, the verifier will work correctly in this case
• if it is included then a misuse occurs when: the developer fails to include a variable X in the changing clause's list of variables, where X is actually changed by the loop body, for this we want the compiler to issue an error; in the example code above, if E were left out of the changing clause, then that indicates that E is not changing, which is incorrect, if Q or T were left out, then incorrect

How to know if X is changed in the loop body:

1. X is used as an actual parameter in a call to an operation where the corresponding formal parameter mode is not one of these: restores, preserves, or evaluates
2. X appears in a swap statement, e.g., X :=: Y
3. X appears in left hand side of an assignment statement, e.g., X := Replica(Y);