1

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

正如预期的那样，Safety->check 算术溢出之一是不可证明的，但似乎 neg_limit 也应该是不可证明的。

背景：我正在使用 Frama-C-Boron、Jessie 以及通过 gWhy、Alt-Ergo 来学习如何编写规范并证明函数符合它们。任何关于规范策略、工具等的线索测试、RTFMing 等也值得赞赏。到目前为止，我正在阅读 ACSL 1.7 实施手册（比 -Boron 的更新）和 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))
4

1 回答 1

2

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

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

即，第二个后置条件包含(integer_of_int32(result) = (-integer_of_int32(v_2)))可以重写为的假设(integer_of_int32(result) = 2147483648)。这与 Jessie 前奏曲中的一条公理相矛盾，即 forall v:int32. integer_of_int32(v)<=2147483647.

我想这再次概述了您不能声称已验证 ACSL 注释，只要某些证明义务仍未得到检查，即使它们不直接源于此注释。

于 2013-07-31T09:34:20.490 回答