Frama-Clang：无效的整数常量

Question

在使用 Frama-Clang 时，我 运行 遇到了一个问题。 以下代码将问题分解为最小值：

const long long value = -1;

int main(){
    return 0;
}

运行 Frama-C (Frama-Clang) 分析导致以下输出。

> frama-c invalid_integer.cpp 
[kernel] Parsing invalid_integer.cpp (external front-end)
Now output intermediate result
[kernel] invalid_integer.cpp:3: Failure: Invalid integer constant: -1
[kernel] User Error: stopping on file "invalid_integer.cpp" that has errors.
[kernel] Frama-C aborted: invalid user input.

有多种方法可以解决此错误。

1. 如果值为 short 或 int 类型则有效，对于 long 和 long long 则无效
2. 没有 const 关键字也能工作
3. 如果变量值是在主函数内部定义而不是全局定义，则有效

这个错误可能来自哪里，是否可以解决？

Answer 1

错误来自 Frama-Clang 和 Frama-C 内核本身之间的错误通信。具体来说，在全局整数变量的初始值设定项的情况下，Frama-Clang 忽略了将负常量转换为一元减号对正整数的应用，这是内核此时所期望的。我冒昧地在 Frama-Clang 的 BTS 上开了一个 issue。