While working with Frama-Clang, I ran into a problem. The following code shows the problem broken down to the minimum:

const long long value = -1;

int main(){
    return 0;
}

Running the Frama-C (Frama-Clang) analysis leads to the following output.

> 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.

There are several ways to work around this error.

1. works if value is type short or int, fails for long and long long
2. works without the const keyword
3. works if the variable value is defined inside the main function instead of global definition

Where could this error come from and can it be solved?

CodePudding user response：

The error comes from a miscommunication between Frama-Clang and the Frama-C kernel itsef. Specifically, in the case of initializers of global integer variables, Frama-Clang neglects to convert a negative constant into the application of unary minus to a positive integer, which is what the kernel is expecting at this point. I've taken the liberty to open an issue on Frama-Clang's BTS.