Spinroot

The Source process in the following small example contains an infinite loop:

my_example.pml:
01  byte sharedData = 0;
02 
03  init {
04      run Sink();
05      run Source();
06  }
07 
08  proctype Sink() {
09      (sharedData == 3);
10      (sharedData == 2);
11      (sharedData == 1);
12  }
13 
14  proctype Source() {
15      do
16      :: true -> {
17              sharedData = 1;
18              sharedData = 2;
19              sharedData = 3;
20          }
21      od
22  }

When calling spin --search my_example.pml, Spin (Version 6.4.3) correctly reports that line 22 is never reached. However, it does not treat this issue as an error, although it states that the full statespace search includes checking for invalid end states.
Adding the end label ("end:") in line 15 does not make any difference. The report by spin --search my_example.pml is exactly the same as before.

Is this behavior intended? How can I ensure by a full statespace search that each process always reaches one of the defined end states?