Spinとgcc
Spinは検証器としてCのソースを出力するのでCコンパイラが必要になるのだが，それ以外にも，一部のマクロの処理にC++プリプロセッサを使う．#defineでの定数宣言や#ifdefは自前で何とかしているようだが，#defineでマクロ関数を宣言したり#ifを使ったりすると内部的にgccが呼び出される．ちなみに"gcc"はハードコードされており*1，"gcc.exe"をパスの通ったところに置いていないとハマる．
コマンドラインで実行する際は，spinの実行時引数でプリプロセッサを指定することが出来るらしいのだが，Xspinを使う場合は不可能．XspinのTclスクリプト冒頭を見ると定数宣言を書き換えれば指定できそうに見えるのだが，その定数が使われていないという見事なフェイント．何とか修正出来ないか試みてみたが挫折した．
どーせなら配布物にGCCを同梱してしまえば良いのに…と思うのだが，Spinは「宣伝条項付き」かつ「ソース開示」というどうしようも無いライセンス*2で配布されているから，それも無理っぽい．何かと扱いづらいなぁこのツール…
