0

我正在尝试在具有一个主中断的大型嵌入式软件堆栈上使用 CBMC。.c 文件解析得很好，但我坚持使用以下代码对中断行为进行建模：

void main_interrupt(void);

void BMC_intr_0() {
    __CPROVER_atomic_begin();
    main_interrupt();
    __CPROVER_atomic_end();
}

main_interrupt()做了各种各样的事情，比如读取输入、设置输出、安全检查等。我想测试空指针解引用的 ADC 读取功能，这需要main_interrupt()运行。测试看起来像这样：

void BMC_intr_0(void);
void main_interrupt(void);

void ADC_Read_test()
{
    __CPROVER_ASYNC_0: BMC_intr_0();

    int    val;
    bool   fresh;

    ADC_Read(adc0, &val, &fresh);
}

BMC_intr_0() 中的main_interrupt()调用包含在__CPROVER_atomic_begin ()和__CPROVER_atomic_end()中，因为据我了解，CBMC 将BMC_intr_0()建模为与 ADC_Read_test 并发运行的额外线程。因此，为了防止在BMC_intr_0（中断）运行时执行 ADC_Read_test，它被包装在一个原子块中。问题是 CBMC 向我抛出了这个：

: atomic sections differ across branches

从这个文件：line。

我的问题是，为什么？这个错误是什么意思？我在这方面找到了 0 个文档，我将不胜感激！

4

0 回答 0