Frama-Clang fails to parse simple predicate
ID0001808: This issue was created automatically from Mantis Issue 1808. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001808 | Frama-Clang | Plug-in > clang | public | 2014-06-13 | 2014-06-19 |
| Reporter | jens | Assigned To | virgile | Resolution | fixed |
| Priority | high | Severity | major | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Neon-20140301 | Target Version | - | Fixed in Version | Frama-C GIT, precise the release id |
Description :
When Frama-Clang is called on the following code fragment
/@ predicate IsValidRange(int a, integer n) = (0 <= n) && \valid(a+(0.. n-1)); */
void foo(int* a, int);
with the command line
frama-c -cpp-command 'gcc -C -E -nostdinc -I/opt/local/include -I/Users/jens/.opam/system/lib/frama-c/share/frama-c/libc' -cxx-clang-command="framaCIRGen" -cxx-demangling-full -wp -wp-rte -wp-out problem208.wp problem208.cpp
then the following error message occurs
Stack dump: 0. parser at end of file Segmentation fault (core dumped) [kernel] user error: Failed to parse C++ file. See Clang messages for more information [kernel] user error: skipping file "problem208.cpp" that has errors. [kernel] Frama-C aborted: invalid user input.
As far as I can see the problem is related to the predicate definition. It is one of our simpler predicates in ACSL by Example.
Steps To Reproduce :
The example is available also under acslplusplus/C++Examples/Problems/problem208.cpp