Polyspace Code Prover Ubuntu Server端报‘Error Limit reached’错误求助

我之前在Ubuntu上用Polyspace Code Prover命令行模式时也碰到过几乎一模一样的问题！当时也是GUI跑同一个项目完全正常，但命令行用从官方网站拿的options.txt就触发了Error Limit reached，折腾了好一阵才找到几个可能的原因和解决办法，分享给你：

• 先排查options.txt的参数差异
  Windows GUI的默认配置和命令行模式的默认配置其实有不少区别，尤其是错误限制相关的参数。你可以检查下你的options.txt里有没有设置-error-limit这类参数，GUI可能默认把这个值设得比较高（甚至不限制），而命令行的配置里可能把阈值调得过低，导致还没完成完整分析就触发了限制。另外，建议你把Windows GUI上运行成功的项目配置导出成选项文件（一般在项目设置里有“导出配置”的选项），然后和你现在用的options.txt逐行对比，重点看分析深度、错误过滤、路径配置这些部分，肯定能找到不一样的地方。

• 试试强制命令行和GUI配置兼容
  直接在命令行里加上-gui-compatible参数，比如：

  ./polyspace-bug-finder -gui-compatible options.txt
  

  这个参数会让命令行模式完全沿用GUI的默认分析策略，很多时候能直接解决两者结果不一致的问题，我当时就是加了这个参数就好了。

• 检查路径和文件引用问题
  Ubuntu用的是/路径分隔符，而Windows是\，如果你的options.txt里引用了项目文件、头文件的路径，有没有改成Ubuntu兼容的格式？要是路径写错了导致工具找不到文件，可能会不断抛出文件缺失的错误，积累到一定数量就触发错误限制了。

• 开启 verbose 模式看详细日志
  运行命令时加上-verbose参数，让输出更详细：

  ./polyspace-bug-finder -verbose options.txt
  

  这样你就能看到触发错误限制前到底出现了哪些错误，是真实的代码错误积累，还是工具本身的配置问题导致的误判。另外，分析完成后（哪怕报错），输出目录里会有详细的日志文件，里面会统计各类错误的数量，能帮你定位到底是哪种错误达到了阈值。

• 确认版本一致性
  最后检查下Ubuntu上安装的Polyspace版本和Windows上的是不是完全一致，不同版本的参数可能有变化，有时候同样的options.txt在旧版本上就会出问题。

希望这些方法能帮你解决问题！

备注：内容来源于stack exchange，提问作者Beni