[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[PVS-Help] Could I don't deliver prf file ?

Hi all,

    I am thinking something about delivery of pvs context. I don't like prf file, because it is generated and will always change when re-run. In contrast, ProofLite script is clean. But I found that  tcc  and judgment script can't be installed by ProofLite when there is no prf file there, is it a bug for pvs or I just did something wrong ? I pushed my context to https://github.com/pluswave/mips-pipeline-proof , but there are two prf files because of this.  Could somebody help me ? Thanks in advance.

Best Regards,