[SAL-HELP] How can I generate TCCs in SAL?

[umemuraa at nttdata.co.jp]

Hi,

I'm currently studying SAL.

According to SAL Language Manual, proof obligations 
will be generated during typechecking if necessary.
However,  it seems that sal-wfc does not generate any such obligations.
Is there any other typechecker in SAL?
Or, is there any special option of sal-wfc to generate obligations?

Many Thanks.
--
Akihiro Umemura
NTT DATA CORPORATION
umemuraa at nttdata.co.jp