问题标签 [spark-ada]

SPARK 限制从受保护对象中调用可能阻塞的子程序。

但是，我注意到如果我在受保护对象所在的包之外调用任何子程序，我会收到有关潜在阻塞子程序的警告。

我想用来告诉它调用将是非阻塞的外部包中缺少什么？我试过在另一个包中放一个“添加一个参数”子程序，但它不起作用。如果我将它移动到包含受保护对象的包中，它会这样做。

我错过了什么？

我正在使用 Ravenscar 配置文件来构建一个利用任务的应用程序。

举个简单的例子，我有一个任务有一个障碍，它只在障碍为真时执行。

但是，我注意到如果主控制线程正在执行，然后屏障设置为 true（从而释放），则任务会阻止主线程的执行，直到屏障再次关闭。

我正在研究 NRF52840 芯片。我应该注意，每当我将应用程序（没有修改）定位到 Native 时，这个问题都不会发生，并且任务不会阻止执行。

为了在嵌入式设备上启用 ravenscar（完整）RTS 的并行执行，我需要做些什么吗？

一些额外的颜色：如果我在任务循环中添加延迟，它确实允许主控制线程运行。

这可能是优先上限协议的问题吗？板上的处理器只有一个内核，所以我想知道这是否可能是问题所在——也就是说，除非它正在睡眠，否则该任务不允许主要任务抢占。

我写了一个非常简单的程序，但我未能证明它的功能正确性。它使用一个项目列表，每个项目都有一个字段指示它是免费的还是使用过的：

还有一个计数器指示使用的元素数量：

append_item过程检查used_items计数器以查看列表是否已满。如果不是，则第一个空闲条目被标记为已使用，并且used_items计数器递增：

我不知道如何证明used_items等于列表中已使用元素的数量。另请注意，gnatprove 消息有时令人费解，我不知道在哪里可以在许多 gnatprove/* 文件中查找更多信息。事实上，对我来说主要的困难是弄清楚证明者需要什么。如果你对这一切有一些迹象，我会很高兴。

据我了解，Ravenscar 配置文件的一个限制是任务不应终止。

这在裸机上当然是有意义的，但是在本机系统（作为可执行程序）上进行测试时，它的副作用是Control-C退出主任务会使程序在后台运行。

我计划最终将我的程序移至裸机，并希望能够使用 Ravenscar 配置文件——在执行此类操作时如何让程序正确退出？中止语句是被禁止的。如果没有应用Ravenscar 配置文件，我可以通过允许任务终止来轻松完成这项工作。现在我正在做一个killall -9，它有效，但看起来不是很优雅。

代码如下所示：

规格：

身体：

正文中没有证明错误，错误仅在规范上：

后置条件可能失败，无法证明 Record_Field_X(Record) = Record_Field_X(Record'Old)

规范和程序结束时的 Assert_And_Cut 之间的“其他后置条件”相同。

请注意使用更简单字段的检查，例如 X_Count：

Record_Field_X_Count(Record) = Record_Field_X_Count(Record'Old)

不要让 gnatprove 抱怨。

过程中的证明者有很多工作，所以通常，当证明后置条件出现问题时，它有助于在过程结束时断言该条件以“提醒”证明者这是重要的事实。通常，这是可行的，但在一种情况下，由于某种原因它不起作用。

我在这里有什么选择？

这可能是什么原因？

也许我应该只增加运行证明程序的机器上的 RAM，这样它就不会丢失Record_Field_X(Record) = Record_Field_X(Record_Old)程序结束与其后置条件之间的事实？（我目前正在一台具有 32GB 内存的机器上执行此操作，该内存专门用于运行 gnatprove，使用--memlimit=32000 --prover=cvc4,altergo --steps=0）

也许有一些我不知道的技术？

也许我唯一的选择是手动证明？

我正在使用 spark 社区 2019 版。

我正在尝试编写一个简单的验证代码块以确保参数（Ada.Command_Line.Argument）和来自 GetLine 的输入是有效的，在我的情况下，我需要输入字符串中的所有字符都是数字（0 到 9 ）。

主.adb：

test_procedure.ads：

test_procedure.adb

该程序运行良好。如果我输入./main 01234它将返回aaaaa，如果我输入./main f00它将不返回任何内容。但是，当我使用 GNATprove（在 GPS -> SPARK -> Prove All 中）时，它给了我precondition might fail, cannot prove S(I) >= '0' (e.g. when I = 1 and user_str = (2 => '0', others => 'NUL')). 我不确定为什么会发生这种情况，因为如果没有数字字符存在，则不应调用 ToA 过程。

我正在用 SPARK Ada 编写一个软件，它需要后置条件来验证函数返回值是否等于数组的总和值。在证明函数所在的文件后，我不断收到一个错误，这个错误并没有完全叠加，没有双关语的意思（我将发布代码的屏幕截图以便更好地查看）。大小为 10 的数组中允许的唯一可接受的值是 0 或 1。

我想做一个程序来接受通用约束数组，即 ecgReadings 和 eegReadings：

尝试制定通用程序：

测试通用产品

我想在 SPARK_Mode 中创建一个利用 GNAT GCC 内在函数“__builtin_ctzll”的函数。

我想假设后置条件为真，因为它是文档所暗示的尾随零数量的定义。但是，我不确定如何做到这一点，阅读了大量文档并尝试使用“pragma Assume”。我对 Ada/SPARK 比较陌生，并且正在使用 GNAT Community 2020。有人可以帮我解决这个问题，以便 gnatprove 能够证明 CTZLL 的后置条件吗？

我有一个大致的数据结构（我无法分享完整的来源，但可以根据要求提供其他信息）如下：

完整代码编译时没有错误和警告，但 SPARK 证明步骤失败并显示以下内容：

我已经阅读了SPARK 手册的相应部分，但我不明白如何根据它们修复我的代码。TIA。