PC-lint protests on line 209.
There is no break statement after the previous line.
PC-lint does not know the semantics of the state-machine's primitives like DELAY.
We tried to inform PC-lint that it should treat f.ex. DELAY as having exit semantics. No success. But:
c: #ifdef DO_BREAK
#define BREAK_ break
/*lint -save +fce -e309 : Continue on error, filter #error */
#error DO_BREAK filters some PC-lint warnings 616, undef to create functional code!
/*lint -restore */
#else
#define BREAK_
#endif
We also added BREAK_ at the end of the following macros:
x: INPUTx, OUTPUTx, ALTWT, DELAY, ENDP, WAITP, CALL, RETURN y: ALTEND z: GOTO
We do wish to receive proper (616) warnings from other parts of the program
We still need filter. SPoC inserts individual state machine entries that just flows into next case for f.ex. this occam code:
o: IF
a = b
c := FALSE
TRUE
SKIP
In addition, SPoC also generates separate states for incrementing the counter value in a SEQ i=0 FOR N loop and WHILE(i<N) loop's bottom code.
SPoC code layout errors will not be spotted with the help of PC-lint's 616-warning, since we have to disable it.
By inspecting every complaint with the filter disabled we did not find any such error - SPoC is a solid piece of code.
We do not actually see how SPoC could have "solved" this without adding extra run-time code to "correctly" enter next case.
Inserting the BREAK_ macro is dangerous since the program is left non-runnable, the inserted breaks severely disrupt some of the the macros modified to silent PC-lint.
We are however, reluctant to repairing things that do work.