确保即使代码有缺陷也能得到证明

Question

在下文中，当注释掉相关的C代码时，如何证明行为neg_limit的后置条件为真？

正如预期的那样，其中一个安全->检查算术溢出是不可证明的，但似乎neg_limit也应该是不可证实的。

上下文：我正在使用Frama-C-Boron、Jessie，以及通过gWhy和Alt-Ergo来学习如何编写规范并证明函数满足这些规范。任何关于规范策略、工具等的提示、RTF Ming等也将不胜感激。到目前为止，我正在阅读ACSL1.7的实施手册（这是最近的-Bornon的）和Jessie教程&参考手册。

谢谢！

/*@ behavior non_neg:
        assumes v >= 0;
        ensures result == v;
    behavior neg_in_range:
        assumes INT32_MIN < v < 0;
        ensures result == -v;
    behavior neg_limit:
        assumes v == INT32_MIN;
        ensures result == INT32_MAX;
    disjoint behaviors;
    complete behaviors;
*/
int32_t my_abs32(int32_t v)
{
  if (v >= 0)
    return v;
  //if (v == INT32_MIN)
  //  return INT32_MAX;
  return -v;
}

以下是第一个后置条件的gWhy目标：

goal my_abs32_ensures_neg_limit_po_1:
  forall v_2:int32.
  (integer_of_int32(v_2) = ((-2147483647) - 1)) ->
  (integer_of_int32(v_2) >= 0) ->
  forall __retres:int32.
  (__retres = v_2) ->
  forall return:int32.
  (return = __retres) ->
  ("JC_13": (integer_of_int32(return) = 2147483647))

第二个：

goal my_abs32_ensures_neg_limit_po_2:
  forall v_2:int32.
  (integer_of_int32(v_2) = ((-2147483647) - 1)) ->
  (integer_of_int32(v_2) < 0) ->
  forall result:int32.
  (integer_of_int32(result) = (-integer_of_int32(v_2))) ->
  forall __retres:int32.
  (__retres = result) ->
  forall return:int32.
  (return = __retres) ->
  ("JC_13": (integer_of_int32(return) = 2147483647))

Answer 1

关于文档，您可能需要查看Fraunhofer FOKUS'ACSL示例：http://www.fokus.fraunhofer.de/de/quest/_download_quest/_projekte/acsl_by_example.pdf

关于你的问题，我已经用Frama-C Fluorine重复了你的结果（顺便说一句，你的代码中缺少一个#include <stdint.h>"），Jessie+Alt-ergo仍然设法证明了后置条件。但请记住，后条件是在假设不发生运行时错误的情况下被证明的，这不是您的代码的情况，正如失败的安全PO所示。

即，第二后条件包含假设(integer_of_int32(result) = (-integer_of_int32(v_2)))，该假设可以被重写为(integer_of_int32(result) = 2147483648)。这与杰西序言中的一条公理相矛盾，即forall v:int32. integer_of_int32(v)<=2147483647。

我想这再次表明，只要某些证明义务未经检查，即使它们不是直接源于该注释，您就不能声称已经验证了ACSL注释。