是否可以在frama-c中指定缓冲区访问子句？

假设我有以下功能：是否可以在frama-c中指定缓冲区访问子句？

void process_data(uint32_t * data, size_t length) { 
    for (size_t i = 0; i < length; i++) { 
     foo(data[i]); 
    } 
}

我怎么能告诉邮资-C“这个功能，确保每次访问data[i]满足条件i < length”？据我所知，我可以在每行代码data附近放置断言，但有没有更好的方法？

来源

2016-12-15 John Doe

问题给你 - 是绝对保证，'data'将是非NULL并指向'uint32_t'的集合？在进入'for'循环之前可能需要断言？ – t0mm13b

是的，'data'是'\ valid'，它指向一个uint32_t的数组。 –

“这个功能确保...”是什么意思？在我看来，你想说“这个功能需要......”（否则，你有无效的内存访问），不是吗？ – Anne

要防止无效的内存访问，您需要检查是否始终使用data指针调用此函数，从中可以读取至少length元素。所以，你需要写一个前提条件：

//@ requires \valid_read (data + (0 .. length-1)); 
void process_data(uint32_t * data, size_t length) {

所以，如果你能保证这个属性是有效的，它保证你不会有任何无效的内存访问。

来源

2016-12-16 09:28:13 Anne

也许我在解释这个时太不清楚了，对不起。当'process_data'函数可能会在'length'维度之外访问'data'时，我希望frama-c wp失败。例如，如果'process_data'包含语句'uint32_t a = data [length + 1]''，则检查失败。 –

@JohnDoe恐怕答案取决于你对Frama-C的使用。例如，如果你想用'-wp-rte'来使用WP，Anne的注解就是你所需要的：因为WP只知道在需求中写的是什么，所以任何访问大于'length'的索引都会导致RTE注释中的未知状态。如果您使用Value并且使用大于'length'的缓冲区调用'process_data'，则需要更多特定注释，您必须提供自己（或通过自定义脚本）提供的更多特定注释。随时优化您的问题，以便我们可以提供适当的答案。 – Virgile

这解释了它。我以为需求条款只影响价值分析，谢谢。 –

是否可以在frama-c中指定缓冲区访问子句？

回答

相关问题