When I type in the following wrong(!) pr0gram:

int i = +7; // intentional error here ‘+’ sign
init{
for (i : 5 .. 8) {printf(" %d \n", i)}
};

Episin correctly notices an error in line 1.
However, Spin also notices an error in line 3: the variable i has not been declared.

Presumably, Epispin enters the variable of a illegal declaration into the symbol table, whereas Spin does not.

Submitted on 19 August 2011 at 14:46

Although it is not the same as Spin treats it, I’m not sure if this is really unwanted behaviour. If another error would by shown when using the variable ‘i’, this would imply there is something wrong with its definition, where there is only a problem with its declaration.

Also note that Spin gives another error when the faulty declaration is INSIDE the init block: it says there is no runnable process at all.