Software Foundations第5册forward_call报no applicable tactic错误如何解决

问题原因和解决方法 #

你遇到的No applicable tactic错误主要有以下几个可能的原因，按出现概率从高到低排序：

• 调用forward_call时未显式指定目标函数规范
  VST的forward_call语法要求你明确指定要匹配的函数规范名，你漏掉了_push参数，正确的调用写法为：

forward_call _push (p, i + 1, decreasing i, gv)

• 缺少PROP约束的前置证明
  你当前的上下文中没有显式的i+1符合整数范围的假设，push规范要求压入值满足Int.min_signed <= i <= Int.max_signed，你需要先把这个可推导的条件加入上下文：

assert (Int.min_signed <= i + 1 <= Int.max_signed) by lia.

再执行上述的forward_call命令即可。

• 函数参数类型不匹配
  你声明的push规范第一个参数是struct cons **类型（对应stack *），如果你的C代码中push调用传入的第一个参数是p（struct cons *类型），就会出现类型匹配失败的问题，需要确认C代码的调用写法为push(&p, i)或者调整规范的参数类型定义。

内容的提问来源于stack exchange，提问作者NoLongerBreathedIn