问题标签 [acsl]

我试图指定外部函数的行为，更准确地说，它们的终止。ACSL 文档说该\terminates p;属性指定如果谓词p成立，则保证函数终止，但在p不成立时不指定任何内容。它还解释了一个永远不会返回的函数可以通过以下方式指定：

此外，ACSL 提供了一个属性\exits p;来指定在突然终止的情况下的后置条件。所以我想知道是否：

会指定函数总是永远循环吗？

此外，规范是什么：

意味着关于可能的无限循环？

我正在为将给定字符串附加到动态字符数组末尾的函数编写 ACSL 规范。

这是我到目前为止所拥有的：

因为还不支持动态内存分配的验证，所以我添加了一个占位符函数char_vector_reallocate()和 ACSL 规范，但没有展示实现。

使用 Frama-C Sodium-20150201 和 WP 插件，我无法验证 6 个属性：

• typed_char_vector_append_disjoint_ok_err
• typed_char_vector_append_err_post
• typed_char_vector_append_err_post_length_unchanged
• typed_char_vector_append_ok_post
• typed_char_vector_append_ok_post_str_length_added_to_length
• typed_char_vector_append_ok_post_string_appended

我没想到验证前 5 个属性会遇到任何困难。

如何修复 ACSL 以便char_vector_append()验证？

（作为旁注，是否有我可以参考的动态数组的示例 ACSL 规范？）

我试图证明这个功能，但徒劳无功。我也在使用另一个功能，但我证明了这一点。

有人可以帮我吗？

这是我到目前为止编写的代码和规范：

我需要有关 ACSL 问题的帮助。比赛于 2014-2015 年完成。这只是练习，我想看看我是否正确地解决了问题。

位串闪烁：

求解以下等式中的 x（5 位）。有多少独特的解决方案？

(RCIRC-2(LSHIFT-1 (非 X)))=00101

解决后我得到了 16 个独特的解决方案，虽然我无法在任何地方找到答案，需要你们聪明和有创造力的人的帮助！

谢谢

我的老师让我们做一个旧的 ACSL 程序来练习，他说我们可以使用任何我们想要的资源。该计划是从 2013 年开始的。链接在这里：https ://s3.amazonaws.com/iedu-attachments-question/5a989d787772b7fd88c063aff8393d34_1bee2d300c35eec13edf0a3af515a5a5.pdf

我们启动了程序，但遇到了墙，我们不知道从这里开始做什么：

谁能给我们一些提示？我们正在用 Python 编码。

抱歉，伙计们预先警告我编码很烂，但是有一个大项目需要帮助！

输入：一个完整​​的句子。

输出：句子的排序顺序（ASCii Chart Order）（忽略大小写。）

输出以下类别的直方图：
1）元音
2）辅音
3）标点符号
4）大写字母
5）小写字母

我不知道该做什么

假设我们有这样一个数据结构：

在以下示例中，Frama-C 似乎没有为 C 类型的结构的字段分配位置：

Frama-C 完全可以接受上述注释吗？

代码详述如下。主要目标是将字段 C_Field 重置为 0：

函数 Reset 的合约得到满足，但 Initialize 函数的合约不满足。如何为 Initialize 的合约写一个正确的“assigns”？

让我从这个例子开始我的问题：

现在让我们在代码中添加 ACSL 注释：

我让 Frama-C 通过执行“frama-c-gui -wp file.c”来检查代码。在函数 A 中调用函数 B、C 和 D 时，合约标记为有效。通过添加函数 E 和可能更多其他函数的调用，合约被标记为无效。我们提出了在每个函数调用之后立即添加“断言”的想法，以便为 Frama-C 提供假设满足哪些后置条件的线索。通过这种方法，合同被标记为有效。查看代码：

问题来了：有没有更好的方法来检查包含多个函数调用的函数的合同，而不是在每个函数调用之后立即添加“断言”？

更新代码：

file.h 如下所示：

file.c 如下所示：

我正在尝试学习 ACSL，但在尝试编写完整的规范时遇到了困难。我的代码

我运行它

frama-c -wp -wp-rte test.c

我看到以下日志

所以似乎我的两种行为和“分配\无”无法得到证明。那么我该如何从这里开始呢？

编辑：所以我想出了眼前的问题。我没有注释我的循环：

我更大的问题仍然存在：调试问题的好方法是什么？我通过更改和删除代码并查看已证明/未证明的内容来解决这个问题。

我这样定义设备访问

我已经使用

现在的问题是，当我启用 RTE 检查时，无法证明生成的有效性检查

有什么方法可以注释我的代码，以使 MY_DEVICE_ADDRESS 到 MY_DEVICE_ADDRESS+sizeof(struct mydevice) 被认为是有效的？

编辑：这是一个不起作用的尝试

运行

frama-c-wp -wp-rte -wp-init-const -wp-model 类型化 test.c