frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2022-09-28T11:13:02Zhttps://git.frama-c.com/pub/frama-c/-/issues/128Syntax error in reorder_defs.ml after running make2022-09-28T11:13:02Zmantis-gitlab-migrationSyntax error in reorder_defs.ml after running makeID0002480:
**This issue was created automatically from Mantis Issue 2480. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002480:
**This issue was created automatically from Mantis Issue 2480. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002480 | Frama-C | Plug-in > clang | public | 2019-10-03 | 2019-10-06 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | gpajela | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | block | **Reproducibility** | have not tried |
| **Platform** | Linux x86_64 | **OS** | Ubuntu | **OS Version** | 18.04.3 LTS |
| **Product Version** | Frama-C 19-Potassium | **Target Version** | - | **Fixed in Version** | - |
### Description :
I am trying to follow the instructions at https://frama-c.com/frama-clang.html to install Frama-Clang. However, I get a "Syntax error" after I run make:
$ make
Generating .Makefile.plugin.generated
Ocamlc intermediate_format.cmi
Ocamlc intermediate_format_parser.cmi
Ocamlc intermediate_format_parser.cmo
Ocamlc frama_Clang_option.cmi
Ocamlc frama_Clang_option.cmo
Ocamlc fclang_datatype.cmi
Ocamlc fclang_datatype.cmo
Ocamlc reorder_defs.cmi
Ocamlc reorder_defs.cmo
File "reorder_defs.ml", line 310, characters 6-10:
Error: Syntax error
/data/loewenheim/a/gpajela/.opam/default/share/frama-c/Makefile.generic:77: recipe for target 'reorder_defs.cmo' failed
make: *** [reorder_defs.cmo] Error 2
### Additional Information :
I am using Frama-C 19.0 Potassium, which I installed using opam pin. I am using version 2.0.4 of opam. I am using the default versions of OCaml and Clang for this version of Ubuntu: OCaml 4.05.0 and clang version 6.0.0.Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/141Error in frama-clang make file2022-09-28T11:09:55Zmantis-gitlab-migrationError in frama-clang make fileID0002463:
**This issue was created automatically from Mantis Issue 2463. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002463:
**This issue was created automatically from Mantis Issue 2463. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002463 | Frama-C | Plug-in > clang | public | 2019-07-07 | 2019-07-08 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | ainne26 | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | high | **Severity** | major | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | Ubuntu | **OS Version** | ubuntu-18.04.2 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
I am trying to install frama-clang by following the instruction given on this website. However when I run make the following errors comes
~/Desktop/frama-clang-0.0.6$ make
ocamlfind ocamlc -c -I . -I "/usr/lib"/frama-c/plugins -package findlib -package ocamlgraph -package num -package unix -package str -package dynlink -package bytes -package zarith -w -a -bin-annot -strict-sequence -safe-string -g -I ""/usr/lib"/frama-c" convert_acsl.ml
File "convert_acsl.ml", line 84, characters 15-24:
Error: Unbound constructor ASinteger
Hint: Did you mean Linteger or LTinteger?
/usr/share/frama-c/Makefile.generic:77: recipe for target 'convert_acsl.cmo' failed
make: *** [convert_acsl.cmo] Error 2
I do not understand, please give me some suggestions to solve these problems.Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/142frama-clang failed to install2022-09-28T11:12:41Zmantis-gitlab-migrationframa-clang failed to installID0002462:
**This issue was created automatically from Mantis Issue 2462. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002462:
**This issue was created automatically from Mantis Issue 2462. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002462 | Frama-C | Plug-in > clang | public | 2019-07-04 | 2019-07-05 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | ainne26 | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | high | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | windows | **OS Version** | windows 10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Hi,
I'm trying to install the Frama-Clang plugin on windows 10 following the instruction on the website. But the command
$ ./configure
checking for frama-c-gui... yes
checking for Makefile.config.in... yes
frama_clang... yes
checking for g++... g++
checking whether the C++ compiler works... yes
checking for C++ compiler default output file name... a.exe
checking for suffix of executables... .exe
checking whether we are cross compiling... no
checking for suffix of object files... o
checking whether we are using the GNU C++ compiler... yes
checking whether g++ accepts -g... yes
checking for camlp4o... yes
checking for clang... clang
checking for clang++... clang++
checking for llvm-config... llvm-config
checking for D:\llvm-project-master\llvm\build\Debug/include/clang... no
configure: WARNING: frama_clang disabled because clang dev headers not found.
configure: frama_clang: no
configure: creating ./config.status
config.status: creating ./Makefile.config
chmod: ./Makefile.config: new permissions are r--rw-r--, not r--r--r--`
I don't know how to solve this problem, any suggestions?Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/240frama-clang fails to compile2022-09-28T11:04:53Zmantis-gitlab-migrationframa-clang fails to compileID0002402:
**This issue was created automatically from Mantis Issue 2402. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002402:
**This issue was created automatically from Mantis Issue 2402. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002402 | Frama-C | Plug-in > clang | public | 2018-10-01 | 2018-10-03 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | barafael | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | block | **Reproducibility** | always |
| **Platform** | Ubuntu | **OS** | Linux | **OS Version** | 18.04 LTS |
| **Product Version** | Frama-C 17-Chlorine | **Target Version** | - | **Fixed in Version** | - |
### Description :
When trying to compile frama-clang, I encounter
Error: Unbounded constructor ASinteger
in file convert_acsl.ml.
ASidentifier is also missing.
### Steps To Reproduce :
Get sources for frama-clang-0.0.6, configure, makeVirgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/242Missing __END_DECLS in ./share/libc/__fc_alloc_axiomatic.h2021-02-22T13:34:04Zmantis-gitlab-migrationMissing __END_DECLS in ./share/libc/__fc_alloc_axiomatic.hID0002400:
**This issue was created automatically from Mantis Issue 2400. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002400:
**This issue was created automatically from Mantis Issue 2400. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002400 | Frama-C | Plug-in > clang | public | 2018-09-21 | 2018-09-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | richardlford | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | x86_64 | **OS** | Ubuntu via WSL | **OS Version** | 16 |
| **Product Version** | Frama-C 17-Chlorine | **Target Version** | - | **Fixed in Version** | Frama-C 17-Chlorine |
### Description :
In file ./share/libc/__fc_alloc_axiomatic.h there is a
__BEGIN_DECLS but no matching __END_DECLS.
When __BEGIN_DECLS expands to 'extern "C" {' and __END_DECLS expands
to '}' this results in miss-matched braces and the following
code appears to be under and extern "C". This leads to
errors, e.g. when template definitions are encountered.
### Additional Information :
Adding in the missing __END_DECLS removes this problem.
### Steps To Reproduce :
Install Frama-C Chlorine and frama-clang-0.0.6.
use the command "frama-c version.cpp" where version.cpp has this content:
// 'Hello World!' program
#include <iostream>
int main()
{
std::cout << "Hello World, version is "<< __cplusplus << "!" << std::endl;
return 0;
}
## Attachments
- [version.cpp](/uploads/346834ddcee99405a81e7ee8cce118f4/version.cpp)https://git.frama-c.com/pub/frama-c/-/issues/250cast error with reference fields2021-03-30T08:44:29Zmantis-gitlab-migrationcast error with reference fieldsID0002396:
**This issue was created automatically from Mantis Issue 2396. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002396:
**This issue was created automatically from Mantis Issue 2396. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002396 | Frama-C | Plug-in > clang | public | 2018-08-24 | 2018-08-24 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | abhishek.anand.iitg@gmail.com | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | manjaro | **OS Version** | 8/23/3018 |
| **Product Version** | Frama-C 17-Chlorine | **Target Version** | - | **Fixed in Version** | - |
### Description :
```
class B {
};
template <typename T>
class A {
public:
T &x;
A(T &y): x(y) {}
};
int main()
{
B b;
B & y=b;
A<B> a(y);
}
```
I get the following error:
```
root@27db7a69b96a:/hostshare# frama-c -print refFieldBug.cpp
[kernel] Parsing refFieldBug.cpp (external front-end)
Now output intermediate result
[kernel] refFieldBug.cpp:8: Failure: castTo struct _Z1B -> struct _Z1B *
[kernel] User Error: stopping on file "refFieldBug.cpp" that has errors.
[kernel] Frama-C aborted: invalid user inp
```
I don't see what could be the problem because the following succeeds:
```
class A {
public:
T &x;
A(T &y): x(y) {}
};
int main()
{
int x=0;
int & y=x;
A<int> a(y);
}
```Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/256Crash on attempt to start framaCIRGen when libs are linked statically and dyn...2021-02-22T12:57:36Zmantis-gitlab-migrationCrash on attempt to start framaCIRGen when libs are linked statically and dynamically.ID0002368:
**This issue was created automatically from Mantis Issue 2368. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002368:
**This issue was created automatically from Mantis Issue 2368. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002368 | Frama-C | Plug-in > clang | public | 2018-02-15 | 2018-07-11 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | DeMaze | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | GNU/Linux | **OS** | Debian | **OS Version** | 9.3 |
| **Product Version** | Frama-C 16-Sulfur | **Target Version** | - | **Fixed in Version** | Frama-C 17-Chlorine |
### Description :
On the attempt to install Frama-Clang regularly as described (see
attached file installation.txt), the executable framaCIRGen exits with
an error when executed. The error message points to a problem with
LLVM. In fact, it depicts one commandline option to be registered more
than once. This occurs on the attempt of using Frama-C to parse C++
source code and when the executable framaCIRGen is invoked manually on
the commandline. I get the following error:
<output nr="0" command="./frama-clang-0.0.4/bin/framaCIRGen">
: CommandLine Error: Option 'asm-macro-max-nesting-depth' registered more than once!
LLVM ERROR: inconsistency in registered CommandLine options
</output>
However, this has only been observed ith llvm-5.0 on Debian GNU/Linux
9.3 (my system, see lsb_release_3ffbf_2018-02-10000905) for now. With
llvm 3.9, no such errors happen. Presumably, versions of llvm > 5.0
could also be affected. This seems to be a problem many people have
experienced with llvm related programs [2][3][4][5]. In fact, it has
even been reported for frama-clang [6].
### Additional Information :
Root Cause
==========
As far as my investigations revealed, this problem occurs because of
the linking mechanism on Debian GNU/Linux. On this distribution,
libraries of LLVM are built two-fold:
Static archives (lib*.a):
clangFrontend, clangDriver, clangTooling, clanParse, clangSema,
clangAnalysis, clangEdit, clangAST, clangLex, clangSerialization,
clangBasic, LLVMTransformUtils, LLVMBitReader, LLVMMCParser,
LLVMOption
Shared object (lib*.so):
LLVM-5.0
Therefore, it is tried to link them according to their type (lines 74-77, 82-85):
<output nr="1" command="cat frama-clang-0.0.4/Makefile.clang -n | grep 'USEDLIBS' -A 5 -B 5 ">
69 CFLAGS+=-g
70 CLANG_LINKFLAGS+=-g
71 endif
72
73 #LINK_COMPONENTS := $(TARGETS_TO_BUILD) asmparser support mc
74 USEDLIBS = clangFrontend \
75 clangDriver clangTooling clangParse clangSema \
76 clangAnalysis clangEdit clangAST clangLex clangSerialization \
77 clangBasic LLVMTransformUtils LLVMBitReader LLVMMCParser LLVMOption
78
79 # for use in main Makefile
80 default: $(PLUGIN_DIR)/bin/$(TOOLNAME)
81
82 $(PLUGIN_DIR)/bin/$(TOOLNAME): $(OBJS) $(PLUGIN_DIR)/bin
83 $(PRINT_LINKING) $@
84 $(CXX) $(CLANG_LINKFLAGS) -o $@ \
85 $(OBJS) $(addprefix -l,$(USEDLIBS)) $(LLVM_LIBS) $(CLANG_SYSLIBS) $(CLANG_LINKFLAGS)
86
87 $(PLUGIN_DIR)/bin:
88 $(MKDIR) $@
89
90 clean:
</output>
This results in the following dependencies on dynamic libraries as follows:
<output n="2" command="ldd ./frama-clang-0.0.4/bin/framaCIRGen">
linux-vdso.so.1 (0x00007ffe31ff5000)
libLLVM-5.0.so.1 => /usr/lib/x86_64-linux-gnu/libLLVM-5.0.so.1 (0x00007fb4c4825000)
libstdc++.so.6 => /usr/lib/x86_64-linux-gnu/libstdc++.so.6 (0x00007fb4c44a3000)
libm.so.6 => /lib/x86_64-linux-gnu/libm.so.6 (0x00007fb4c419f000)
libgcc_s.so.1 => /lib/x86_64-linux-gnu/libgcc_s.so.1 (0x00007fb4c3f88000)
libc.so.6 => /lib/x86_64-linux-gnu/libc.so.6 (0x00007fb4c3be9000)
libffi.so.6 => /usr/lib/x86_64-linux-gnu/libffi.so.6 (0x00007fb4c39e0000)
libedit.so.2 => /usr/lib/x86_64-linux-gnu/libedit.so.2 (0x00007fb4c37a8000)
librt.so.1 => /lib/x86_64-linux-gnu/librt.so.1 (0x00007fb4c35a0000)
libdl.so.2 => /lib/x86_64-linux-gnu/libdl.so.2 (0x00007fb4c339c000)
libtinfo.so.5 => /lib/x86_64-linux-gnu/libtinfo.so.5 (0x00007fb4c3172000)
libpthread.so.0 => /lib/x86_64-linux-gnu/libpthread.so.0 (0x00007fb4c2f55000)
libz.so.1 => /lib/x86_64-linux-gnu/libz.so.1 (0x00007fb4c2d3b000)
/lib64/ld-linux-x86-64.so.2 (0x00007fb4c9431000)
libncurses.so.5 => /lib/x86_64-linux-gnu/libncurses.so.5 (0x00007fb4c2b18000)
libbsd.so.0 => /lib/x86_64-linux-gnu/libbsd.so.0 (0x00007fb4c2902000)
</output>
From this output, this assumption can be confirmed because
ligcc_s.so.1 as well as libLLVM-5.0.so.1 occurs. A response on a bug
report of LLVM considers this as rather bad practice
however. Moreover, this is mentioned as a classical problem of LLVM's
"global object-based commandline switch registration" [1]:
"The command line option error is the classical problem one gets due
to the LLVM's global object-based command line switch registration. If
you somehow link the same global object (that registers the command
line option) twice via dynamic loading of the LLVM library twice or
more to the same process, it registers the same command line object
again (when calling the global object initializer), resulting in this
error." [1]
The aforementioned symbol 'asm-macro-max-nesting-depth' occurs both in
libLLVMMCParser.a and libLLVM-5.0.so.1 . Hence, I conjecture these are
the files in conflict.
My Solution
===========
Just link without libLLVMMCParser.a or more precisely, remove
LLVMMCParser from USEDLIBS in Makefile.clang. This seems to work as
C++ code is analyzable again. Please find patches for Makefile.clang
attached which circumvent this problem according to my proposal
(Makefile.clang.patch / Makefile.clang.patch.better). Feel free to
contacting me in case of any further quesions / comments.
References
==========
[1] https://bugs.llvm.org/show_bug.cgi?id=30587#c6
[2] https://bugs.debian.org/cgi-bin/bugreport.cgi?bug=768185
[3] https://bugs.llvm.org/show_bug.cgi?id=31571
[4] http://llvm.1065342.n5.nabble.com/llvm-dev-LLD-and-LLVM-LINK-LLVM-DYLIB-td104570.html
[5] https://github.com/zig-lang/zig/issues/67
[6] https://stackoverflow.com/questions/45647503/errors-when-using-the-frama-clang-plugin
### Steps To Reproduce :
1. Manually install llvm-5.0 as described on https://apt.llvm.org/
2. Download and build frama-clang as described officially with llvm-5.0
3. Execute ./bin/framaCIRGen
## Attachments
- [logs_and_more.tar.xz](/uploads/d2a4d0490b88cd4c21961e8a55ab0ca2/logs_and_more.tar.xz)https://git.frama-c.com/pub/frama-c/-/issues/267C-function returning a struct causes warning on missing Ctor code/spec when i...2021-03-30T08:24:10ZJochen BurghardtC-function returning a struct causes warning on missing Ctor code/spec when inside 'extern "C" {...}'ID0002367:
**This issue was created automatically from Mantis Issue 2367. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002367:
**This issue was created automatically from Mantis Issue 2367. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002367 | Frama-C | Plug-in > clang | public | 2018-02-12 | 2018-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Sulfur-20171101 | **OS** | - | **OS Version** | Ubuntu 17.10 |
| **Product Version** | Frama-C 16-Sulfur | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp equal_range_cpp.cpp" prints
[kernel] warning: Assuming declared function pair::Ctor can't throw any exception
equal_range_cpp.cpp:6:[kernel] warning: Neither code nor specification for function pair::Ctor, generating default assigns from the prototype
Both messages disappear when the file is renamed to "equal_range_cpp.c" and/or the leading 'extern "C" {' and the trailing '}' are removed.
## Attachments
- [equal_range_cpp.cpp](/uploads/345e6cc5ed90e78e5878e8d5736cbef8/equal_range_cpp.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/268loop assigns clause ginored under strange circumstances2021-03-30T08:17:49ZJochen Burghardtloop assigns clause ginored under strange circumstancesID0002366:
**This issue was created automatically from Mantis Issue 2366. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002366:
**This issue was created automatically from Mantis Issue 2366. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002366 | Frama-C | Plug-in > clang | public | 2018-02-12 | 2018-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Sulfur-20171101 | **OS** | - | **OS Version** | Ubuntu 17.10 |
| **Product Version** | Frama-C 16-Sulfur | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp reverse_cpp.cpp" on the attached program reports
reverse_cpp.cpp:13:37: Ambiguity when choosing overloaded function Rev.
reverse_cpp.cpp:16:[wp] warning: Missing assigns clause (assigns 'everything' instead)
For the 1st message, cf. #2364, using a similar program.
The 2nd message disappears if
(1) the file is renamed to "reverse_cpp.c",
(2) the "assert" clause in line 10 is removed,
(3) the "loop invariant" clause in line 13 is removed, or
(4) the (possibly imaginary, cf. #2364) "Rev" ambiguity is resolved by removing one of the overloaded predicate definitions in lines 3 and 5.
## Attachments
- [reverse_cpp.cpp](/uploads/8c82fdfbc3ec2d18a714a489c7d8a4df/reverse_cpp.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/278predicate argument type "struct S" accepted by Frama-C, but not by Frama-clang2021-03-30T08:05:33ZJochen Burghardtpredicate argument type "struct S" accepted by Frama-C, but not by Frama-clangID0002358:
**This issue was created automatically from Mantis Issue 2358. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002358:
**This issue was created automatically from Mantis Issue 2358. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002358 | Frama-C | Plug-in > clang | public | 2018-02-08 | 2018-02-08 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | Sulfur-20171101 | **OS** | - | **OS Version** | Ubuntu 17.10 |
| **Product Version** | Frama-C 16-Sulfur | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c stack_init_cpp.cpp" in the attached file results in an error message "keyword 'keyword -> struct' encountered when parsing a type" for line 6 (C++/C subroutine), but not for line 4 (Acsl predicate). When the file is renamed to "frama-c stack_init_cpp.c" , the error message disappears.
## Attachments
- [stack_init_cpp.cpp](/uploads/655f490009c017323d0b16f5261f5c9f/stack_init_cpp.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/279kernel warns about invalid implicit conversion2021-03-30T08:04:31ZJens Gerlachkernel warns about invalid implicit conversionID0002350:
**This issue was created automatically from Mantis Issue 2350. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002350:
**This issue was created automatically from Mantis Issue 2350. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002350 | Frama-C | Plug-in > clang | public | 2018-01-31 | 2018-02-08 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 16-Sulfur | **Target Version** | - | **Fixed in Version** | - |
### Description :
When processing the attached (C-)code with Fram-Clang the kernels sends a diagnostic as follows
frama-c -wp -wp-rte implicit_conversion.cpp
[kernel] Parsing implicit_conversion.cpp (external front-end)
implicit_conversion.cpp:16:44: invalid implicit conversion
Now output intermediate result
When processed as a ACSL/C file by WP no warning occurs.
## Attachments
- [implicit_conversion.cpp](/uploads/fe14759cabb542c2f83d85b61b0e28e9/implicit_conversion.cpp)
- [imcCnv2.cpp](/uploads/d6c96e86d9b3ff6a2032499013b2aac0/imcCnv2.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/282no diagnostics on wrong keyword2021-03-30T07:48:10ZJens Gerlachno diagnostics on wrong keywordID0002351:
**This issue was created automatically from Mantis Issue 2351. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002351:
**This issue was created automatically from Mantis Issue 2351. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002351 | Frama-C | Plug-in > clang | public | 2018-01-31 | 2018-01-31 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 16-Sulfur | **Target Version** | - | **Fixed in Version** | - |
### Description :
The attached ACSL/C code contains a typo in the assigns clause:
"assign" instead of "assigns".
Frama-Clang provides no diagnostic message on this
frama-c -wp -wp-rte wrong_keyword.cpp
[kernel] Parsing wrong_keyword.cpp (external front-end)
Now output intermediate result
[rte] annotating function foo
[wp] 0 goal scheduled
[wp] Proved goals: 0 / 0
When processed as a normal C file by Frama-C/WP a more appropriated message is shown
frama-c -wp -wp-rte wrong_keyword.c
[kernel] Parsing wrong_keyword.c (with preprocessing)
wrong_keyword.c:5:[kernel] user error: unexpected token 'a'
[kernel] user error: stopping on file "wrong_keyword.c" that has errors. Add '-kernel-msg-key pp'
for preprocessing command.
[kernel] Frama-C aborted: invalid user input.
## Attachments
- [wrong_keyword.cpp](/uploads/577364237c433e7a05c5ae2104548eda/wrong_keyword.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/636float constant in contract causes crash2021-03-29T17:27:14ZJochen Burghardtfloat constant in contract causes crashID0001981:
**This issue was created automatically from Mantis Issue 1981. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001981:
**This issue was created automatically from Mantis Issue 1981. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001981 | Frama-Clang | Plug-in > clang | public | 2014-11-24 | 2015-05-11 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
Now output intermediate result
Could not parse floating point number ""
[kernel] Current source was: 143.cpp:3
The full backtrace is:
Called from file "cil/src/logic/logic_utils.ml", line 288, characters 16-65
Called from file "cil/src/logic/logic_typing.ml", line 2116, characters 17-60
Called from file "cil/src/logic/logic_typing.ml", line 2000, characters 14-60
Called from file "cil/src/logic/logic_typing.ml", line 2630, characters 15-26
Called from file "cil/src/logic/logic_typing.ml", line 3172, characters 56-76
Called from file "list.ml", line 57, characters 20-23
Called from file "cil/src/logic/logic_typing.ml", line 3304, characters 15-129
Called from file "list.ml", line 57, characters 20-23
Called from file "cil/src/logic/logic_typing.ml", line 3291, characters 12-1023
Called from file "cil/src/frontc/cabshelper.ml", line 58, characters 17-23
Called from file "cil/src/frontc/cabs2cil.ml", line 7411, characters 2-370
Called from file "cil/src/frontc/cabs2cil.ml", line 7702, characters 22-80
Called from file "list.ml", line 74, characters 24-34
Called from file "cil/src/frontc/cabs2cil.ml", line 7719, characters 15-54
Called from file "cil/src/frontc/cabs2cil.ml", line 9145, characters 12-35
Called from file "list.ml", line 69, characters 12-15
Called from file "cil/src/frontc/cabs2cil.ml", line 9150, characters 2-26
Called from file "src/frama-clang/frama_Clang_register.ml", line 89, characters 12-34
Called from file "src/kernel/file.ml", line 1073, characters 10-43
Called from file "src/kernel/file.ml", line 1117, characters 23-30
Called from file "list.ml", line 74, characters 24-34
Called from file "src/kernel/file.ml", line 1114, characters 6-520
Called from file "src/kernel/file.ml", line 2179, characters 12-30
Called from file "src/kernel/file.ml", line 2264, characters 4-27
Called from file "src/kernel/ast.ml", line 111, characters 2-28
Called from file "src/kernel/ast.ml", line 123, characters 53-71
Called from file "src/kernel/boot.ml", line 29, characters 6-20
Called from file "src/kernel/cmdline.ml", line 761, characters 2-9
Called from file "src/kernel/cmdline.ml", line 216, characters 4-8
Unexpected error (File "src/lib/floating_point.ml", line 204, characters 7-13: Assertion failed).
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Neon-20140301+dev-stance.
## Attachments
- [143.cpp](/uploads/64a8df8b99e6b641a9b44ed842186bc2/143.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/639declaration of static class-type variable in function body causes crash2021-03-29T17:24:54ZJochen Burghardtdeclaration of static class-type variable in function body causes crashID0002109:
**This issue was created automatically from Mantis Issue 2109. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002109:
**This issue was created automatically from Mantis Issue 2109. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002109 | Frama-Clang | Plug-in > clang | public | 2015-04-27 | 2015-05-07 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Sodium-20150201 | **OS** | - | **OS Version** | xubuntu14.04 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing 472.cpp (external front-end)
Now output intermediate result
472.cpp:5:[fclang] failure: Unknown local variable a
[kernel] Current source was: 472.cpp:5
The full backtrace is:
Raised at file "src/kernel/log.ml", line 524, characters 30-31
Called from file "src/kernel/log.ml", line 518, characters 9-16
Re-raised at file "src/kernel/log.ml", line 521, characters 15-16
Called from file "convert.ml", line 256, characters 8-39
Called from file "convert.ml", line 441, characters 33-55
Called from file "convert.ml", line 485, characters 29-52
Called from file "convert.ml", line 894, characters 29-54
Called from file "list.ml", line 84, characters 24-34
Called from file "convert.ml", line 891, characters 4-213
Called from file "convert.ml", line 910, characters 24-55
Called from file "convert.ml", line 972, characters 31-71
Called from file "convert.ml", line 1201, characters 20-53
Called from file "convert.ml", line 1344, characters 20-46
Called from file "list.ml", line 84, characters 24-34
Called from file "convert.ml", line 1334, characters 17-40
Called from file "convert.ml", line 2508, characters 21-44
Called from file "convert.ml", line 2642, characters 21-41
Called from file "list.ml", line 84, characters 24-34
Called from file "convert.ml", line 2645, characters 4-74
Called from file "frama_Clang_register.ml", line 120, characters 13-36
Called from file "src/kernel/file.ml", line 1248, characters 8-41
Called from file "src/kernel/file.ml", line 1296, characters 23-30
Called from file "list.ml", line 84, characters 24-34
Called from file "src/kernel/file.ml", line 1293, characters 6-864
Called from file "src/kernel/file.ml", line 2287, characters 12-30
Called from file "src/kernel/file.ml", line 2372, characters 4-27
Called from file "src/kernel/ast.ml", line 111, characters 2-28
Called from file "src/kernel/ast.ml", line 123, characters 53-71
Called from file "src/kernel/boot.ml", line 29, characters 6-20
Called from file "src/kernel/cmdline.ml", line 763, characters 2-9
Called from file "src/kernel/cmdline.ml", line 216, characters 4-8
Plug-in fclang aborted: internal error.
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Sodium-20150201.
The crash disappears if:
(1) the type of "a" is changed from "A" to "int" in line 5, or
(2) the "static" is removed in line 5.
### Additional Information :
Ubuntu clang version 3.4-1ubuntu3 (tags/RELEASE_34/final) (based on LLVM 3.4)
## Attachments
- [472.cpp](/uploads/3d558269abe175d97792e6b3cef32c24/472.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/644different signatures for "linked" in definition and use in generated Alt-Ergo...2021-03-29T17:11:27ZJochen Burghardtdifferent signatures for "linked" in definition and use in generated Alt-Ergo mlw fileID0002111:
**This issue was created automatically from Mantis Issue 2111. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002111:
**This issue was created automatically from Mantis Issue 2111. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002111 | Frama-Clang | Plug-in > clang | public | 2015-05-04 | 2015-05-04 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Sodium-20150201 | **OS** | - | **OS Version** | xubuntu14.04 |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp -wp-rte -wp-out wp-out 475.cpp" generated the file "_Z3fooR1X_assert_rte_mem_access_Alt-Ergo.mlw" which seems to contain different signatures of "linked":
...
493 logic linked : (int,int) farray -> prop
...
766 forall t : int farray.
767 forall t_1 : (addr,int) farray.
768 forall a : addr.
769 let a_1 = shiftfield_F__Z1X_x(a) : addr in
770 linked(t) ->
...
"linked" is declared as taking an argument of type "(int,int) farray", but at its single use it is given an argument of type "int farray".
I'm not sure whether this is ok (maybe Alt-Ergo provides overloading?) or indicates an error. Alt-Ergo doesn't complain, anyway.
## Attachments
- [475.cpp](/uploads/013ed2b11f15bf97426688f7c8b9ee1b/475.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/651postcondition of destructor unconsidered2021-02-22T14:01:54ZJochen Burghardtpostcondition of destructor unconsideredID0002103:
**This issue was created automatically from Mantis Issue 2103. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002103:
**This issue was created automatically from Mantis Issue 2103. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002103 | Frama-Clang | Plug-in > clang | public | 2015-04-09 | 2015-04-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | duplicate |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Sodium-20150201 | **OS** | xubuntu14.04 | **OS Version** | - |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | - |
### Description :
The "ensures" in line 9 can't be proven. The goal given to Alt-Ergo reads:
759 goal _Z3foo_post:
760 forall i : int.
761 forall t : int farray.
762 linked(t) ->
763 is_sint32(i) ->
764 (3 = i)
which apparently doesn't reflect the fact that before "foo" exists, the destructor "~A" is called for variable "aa", and assigns 3 to "x".
There are two more unproven goals, viz. in file "_Z3foo_assign_exit_Alt-Ergo.mlw":
493 logic linked : (int,int) farray -> prop
...
554 (* ---------------------------------------------------------- *)
555 (* --- Assigns (file 466.cpp, line 9) in '_Z3foo' --- *)
556 (* ---------------------------------------------------------- *)
557
558 goal _Z3foo_assign_exit: forall t : int farray. not linked(t)
where the prodicate "linked" doesn't appear anywhere outside the shown lines, and hence the goal is unprovable, and in file "_Z3foo_assign_normal_Alt-Ergo.mlw", which is literally identical to the above, except for the goal's name.
## Attachments
- [466.cpp](/uploads/564031d9eacadce7745391f86f6b4e12/466.cpp)https://git.frama-c.com/pub/frama-c/-/issues/652syntax error in contract causes rest to be tacitly ignored2021-02-22T14:01:54ZJochen Burghardtsyntax error in contract causes rest to be tacitly ignoredID0001821:
**This issue was created automatically from Mantis Issue 1821. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001821:
**This issue was created automatically from Mantis Issue 1821. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001821 | Frama-Clang | Plug-in > clang | public | 2014-06-27 | 2015-04-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | xubuntu-cfe13.10 (64 bit) | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c-gui -wp -wp-rte Fault2.cpp" on the attached program causes a message "Fault2.cpp:4:2: expecting function spec" on stderr (that's ok), but doesn't prevent the gui to appear (that's at least different to the behavior on a renamed version "Fault2.c").
More important, no error or warning message is visible in the gui (I checked the tabs "Information", "Messages", "Console", "Properties", "WP Goals"), and the contract rest after the error is tacitly ignored.
## Attachments
- [Fault2.cpp](/uploads/2ea7598b48027d199c2e89b9df46f36c/Fault2.cpp)https://git.frama-c.com/pub/frama-c/-/issues/653using "delete" causes warning for "free"2021-02-22T14:01:55ZJochen Burghardtusing "delete" causes warning for "free"ID0001946:
**This issue was created automatically from Mantis Issue 1946. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001946:
**This issue was created automatically from Mantis Issue 1946. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001946 | Frama-Clang | Plug-in > clang | public | 2014-10-30 | 2015-04-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | xubuntu-cfe13.10 | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
Now output intermediate result
072.cpp:3:[kernel] warning: Calling undeclared function free. Old style K&R code?
[kernel] warning: Assuming declared function free can't throw any exception
Similar to issue #1596, but now for "delete"/"free" rather than "new"/"malloc", cf. the note #4424 there.
## Attachments
- [072.cpp](/uploads/076e092452147592d1b383b325ade662/072.cpp)https://git.frama-c.com/pub/frama-c/-/issues/654"__is_trivial" causes abort2021-02-22T13:08:13ZJochen Burghardt"__is_trivial" causes abortID0001967:
**This issue was created automatically from Mantis Issue 1967. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001967:
**This issue was created automatically from Mantis Issue 1967. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001967 | Frama-Clang | Plug-in > clang | public | 2014-11-13 | 2015-04-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
Unsupported expressions:UnaryTypeTraitExpr 0x253e888 <134.cpp:2:10, col:26> '_Bool'
Aborting
[kernel] user error: Failed to parse C++ file. See Clang messages for more information
(Importance: this code is used via #include <vector>.)
## Attachments
- [134.cpp](/uploads/fc0e0514a33ec9a94e33e11fd592e5b0/134.cpp)https://git.frama-c.com/pub/frama-c/-/issues/655double index causes error2021-02-22T13:26:10ZJochen Burghardtdouble index causes errorID0001987:
**This issue was created automatically from Mantis Issue 1987. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001987:
**This issue was created automatically from Mantis Issue 1987. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001987 | Frama-Clang | Plug-in > clang | public | 2014-11-24 | 2015-04-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
Now output intermediate result
150.cpp:5:[kernel] user error: Cast over a non-scalar type int *[4]
When renamed to "150.c", the file is handled pretty well by Frama-C.
## Attachments
- [150.cpp](/uploads/aebbefedb6dddb821eed8858253fd454/150.cpp)https://git.frama-c.com/pub/frama-c/-/issues/656extra "//" comment within "//@" annotation causes abort2021-02-22T13:08:15ZJochen Burghardtextra "//" comment within "//@" annotation causes abortID0002013:
**This issue was created automatically from Mantis Issue 2013. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002013:
**This issue was created automatically from Mantis Issue 2013. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002013 | Frama-Clang | Plug-in > clang | public | 2014-12-04 | 2015-04-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
framaCIRGen: src/frama-clang/ACSLToken.h:563: Acsl::DLexer::AbstractToken Acsl::DLexer::Token::getFullToken() const: Assertion `_type != 0' failed.
Aborted (core dumped)
[kernel] user error: Failed to parse C++ file. See Clang messages for more information
The problem disappears if "// comment" is deleted in line 2, or if the file is renamed to "190.c".
## Attachments
- [190.cpp](/uploads/6e7ae2cf72d87f620e534fcf2c6a03dd/190.cpp)https://git.frama-c.com/pub/frama-c/-/issues/657logic function with typedef'd result type causes crash2021-02-22T13:08:16ZJochen Burghardtlogic function with typedef'd result type causes crashID0002056:
**This issue was created automatically from Mantis Issue 2056. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002056:
**This issue was created automatically from Mantis Issue 2056. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002056 | Frama-Clang | Plug-in > clang | public | 2015-01-22 | 2015-04-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | Neon-20140301+dev-STANCE-Jan2015 | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing 437.cpp (external front-end)
Now output intermediate result
437.cpp:6:[fclang] failure: predicate definition with a term as body
[kernel] Current source was: 437.cpp:6
The full backtrace is:
Raised at file "src/kernel/log.ml", line 524, characters 30-31
Called from file "src/kernel/log.ml", line 518, characters 9-16
Re-raised at file "src/kernel/log.ml", line 521, characters 15-16
Called from file "src/frama-clang/convert_acsl.ml", line 622, characters 12-76
Called from file "src/frama-clang/convert.ml", line 2233, characters 18-54
Called from file "list.ml", line 74, characters 24-34
Called from file "src/frama-clang/convert.ml", line 2241, characters 19-78
Called from file "src/frama-clang/convert.ml", line 2554, characters 21-48
Called from file "list.ml", line 74, characters 24-34
Called from file "src/frama-clang/convert.ml", line 2558, characters 4-79
Called from file "src/frama-clang/frama_Clang_register.ml", line 86, characters 13-36
Called from file "src/kernel/file.ml", line 1248, characters 8-41
Called from file "src/kernel/file.ml", line 1296, characters 23-30
Called from file "list.ml", line 74, characters 24-34
Called from file "src/kernel/file.ml", line 1293, characters 6-864
Called from file "src/kernel/file.ml", line 2287, characters 12-30
Called from file "src/kernel/file.ml", line 2372, characters 4-27
Called from file "src/kernel/ast.ml", line 111, characters 2-28
Called from file "src/kernel/ast.ml", line 123, characters 53-71
Called from file "src/kernel/boot.ml", line 29, characters 6-20
Called from file "src/kernel/cmdline.ml", line 761, characters 2-9
Called from file "src/kernel/cmdline.ml", line 216, characters 4-8
Plug-in fclang aborted: internal error.
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Neon-20140301+dev-STANCE.
The problem disappears if the return type is changed to "int" in line 6.
Line 7 just demonstrates that the same expression is accepted in C++ code.
## Attachments
- [437.cpp](/uploads/b80e0c84f1ccd4254f37a850575ad463/437.cpp)https://git.frama-c.com/pub/frama-c/-/issues/658method can't be used in member initializer before its declaration2021-02-22T13:08:18ZJochen Burghardtmethod can't be used in member initializer before its declarationID0002064:
**This issue was created automatically from Mantis Issue 2064. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002064:
**This issue was created automatically from Mantis Issue 2064. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002064 | Frama-Clang | Plug-in > clang | public | 2015-01-26 | 2015-04-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Neon-20140301+dev-STANCE-Jan2015 | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing 443.cpp (external front-end)
Now output intermediate result
443.cpp:7:[kernel] warning: Calling undeclared function _ZNK5PointE1x. Old style K&R code?
The error message is not observed for any of the variants in lines 4 to 6 (currently commented-out). It also disappears if the definition of x() is moved before line 4.
## Attachments
- [443.cpp](/uploads/a5451bc00dc4425f63032528113647d7/443.cpp)https://git.frama-c.com/pub/frama-c/-/issues/659class expression causes abort in presence of user-defined destructor2021-03-29T17:06:09ZJochen Burghardtclass expression causes abort in presence of user-defined destructorID0002004:
**This issue was created automatically from Mantis Issue 2004. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002004:
**This issue was created automatically from Mantis Issue 2004. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002004 | Frama-Clang | Plug-in > clang | public | 2014-12-01 | 2015-04-15 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
Unsupported expressions:ExprWithCleanups 0x17e7dc0 <179.cpp:8:6, col:17> '_Bool'
`-CXXMemberCallExpr 0x17e7d98 <col:6, col:17> '_Bool'
`-MemberExpr 0x17e7d68 <col:6, col:12> '<bound member function type>' .test 0x1799820
`-CXXBindTemporaryExpr 0x17e7d48 <col:6, col:10> 'struct cls' (CXXTemporary 0x17e7d40)
`-CXXTemporaryObjectExpr 0x17e7d00 <col:6, col:10> 'struct cls' 'void (void)' zeroing
Aborting
[kernel] user error: Failed to parse C++ file. See Clang messages for more information
The problem disappears if the destructor definition in line 3 is deleted.
## Attachments
- [179.cpp](/uploads/4356f9770e055afebc91022a33e22f7c/179.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/801neither "allocates" nor "frees" clause recognized2021-02-22T13:12:15ZJochen Burghardtneither "allocates" nor "frees" clause recognizedID0002062:
**This issue was created automatically from Mantis Issue 2062. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002062:
**This issue was created automatically from Mantis Issue 2062. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002062 | Frama-Clang | Plug-in > clang | public | 2015-01-26 | 2015-03-10 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | low | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | Neon-20140301+dev-STANCE-Jan2015 | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing 442.cpp (external front-end)
442.cpp:2:6: expecting function spec
Now output intermediate result
A similar error message is observed if line 2 is commented-out and line 3 commented-in. Both messages disappear if the file is renamed to "442.c".
## Attachments
- [442.cpp](/uploads/893ffee0f7a0eb42835710b568815b70/442.cpp)https://git.frama-c.com/pub/frama-c/-/issues/808function called in initialization of a static/global variable2021-03-29T16:50:16ZFranck Vedrinefunction called in initialization of a static/global variableID0001728:
**This issue was created automatically from Mantis Issue 1728. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001728:
**This issue was created automatically from Mantis Issue 1728. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001728 | Frama-Clang | Plug-in > clang | public | 2014-04-01 | 2015-02-18 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | fvedrine | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | Frama-C GIT, precise the release id | **Fixed in Version** | - |
### Description :
C++ authorizes the call of function to initialize static variables.
In C this can only be done with __attribute__((constructor)).
It requires modification in Cabs to accept it.
initialization.cpp:7:[kernel] warning: CALL in constant
initialization.cpp:7:[kernel] user error: invalid global initializer tmp
{/*() <-
Calls:
tmp = _ZN1AE1f();
*/
tmp = _ZN1AE1f();}
## Attachments
- [initialization.cpp](/uploads/f74ef7ad9e674a067ea3b5b37f3fe0a5/initialization.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/834Inheritance of members does not work when chained2021-02-22T13:12:59Zmantis-gitlab-migrationInheritance of members does not work when chainedID0001826:
**This issue was created automatically from Mantis Issue 1826. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001826:
**This issue was created automatically from Mantis Issue 1826. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001826 | Frama-Clang | Plug-in > clang | public | 2014-07-04 | 2015-02-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | lapawczykt | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | ubuntu 14.04 | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | - |
### Description :
If struct B derives from struct A and struct C derives from struct B, struct C includes members of struct B but not of struct A, eventhough it should.
## Attachments
- [problem303.cpp](/uploads/180e398597977d06dbde1dda79f063d8/problem303.cpp)https://git.frama-c.com/pub/frama-c/-/issues/835Simple exceptions are not supported2021-02-22T13:27:45Zmantis-gitlab-migrationSimple exceptions are not supportedID0001845:
**This issue was created automatically from Mantis Issue 1845. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001845:
**This issue was created automatically from Mantis Issue 1845. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001845 | Frama-Clang | Plug-in > clang | public | 2014-07-18 | 2015-02-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | lapawczykt | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | - |
### Description :
It looks like the Try-Catch-block is recognized but not supported. (See the Output in the Additional Information)
### Additional Information :
Output: Unsupported Statement:
CXXTryStmt 0x20ac1d0 <foo013.cpp:2:2, line:4:20>
|-CompoundStmt 0x20ac108 <line:2:6, line:4:2>
| `-CXXThrowExpr 0x20ac0e8 <line:3:3, col:9> 'void'
| `-IntegerLiteral 0x20ac0c8 <col:9> 'int' 42
`-CXXCatchStmt 0x20ac1b0 <line:4:4, col:20>
|-VarDecl 0x20ac140 <col:11, col:15> i 'int'
`-CompoundStmt 0x20ac198 <col:18, col:20>
Aborting
[kernel] user error: Failed to parse C++ file. See Clang messages for more information
[kernel] user error: skipping file "foo013.cpp" that has errors.
[kernel] Frama-C aborted: invalid user input.
## Attachments
- [problem304.cpp](/uploads/8f2aeb621f6626492d052b2f8000cb3e/problem304.cpp)https://git.frama-c.com/pub/frama-c/-/issues/836Parsing error with arrow operator2021-02-22T13:13:02Zmantis-gitlab-migrationParsing error with arrow operatorID0001861:
**This issue was created automatically from Mantis Issue 1861. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001861:
**This issue was created automatically from Mantis Issue 1861. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001861 | Frama-Clang | Plug-in > clang | public | 2014-07-25 | 2015-02-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | lapawczykt | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | ubuntu 14.04 | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | - |
### Description :
"A->a <= A->b <= A->c" causes a parsing error.
On the other hand "A->a <= A->b && A->b <= A->c" works.
When multiple comparrisons are chained without "&&" an arrow operator in the third or higher term causes an "invalid type for 'operator ->'" error.
(Works in c)
## Attachments
- [problem310.cpp](/uploads/3f7eb7890e4ed1dcace89ca08099b866/problem310.cpp)https://git.frama-c.com/pub/frama-c/-/issues/837Comparison of different types in acsl clause causes segmentation fault2021-02-22T13:51:23Zmantis-gitlab-migrationComparison of different types in acsl clause causes segmentation faultID0001902:
**This issue was created automatically from Mantis Issue 1902. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001902:
**This issue was created automatically from Mantis Issue 1902. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001902 | Frama-Clang | Plug-in > clang | public | 2014-07-30 | 2015-02-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | lapawczykt | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | xubuntu 64 bit | **OS Version** | 14.04 |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | Frama-C Neon-20140301 | **Fixed in Version** | - |
### Description :
A comparison between e.g. an int and a short is normaly translated to a cast and a following comparison in the normalised version. This works fine in C but in C++ a comparison of e.g. an int and a short in an acsl clause causes a segmentation fault.
## Attachments
- [problem311.cpp](/uploads/52700e19e5d6a83f949b1919c42187a1/problem311.cpp)https://git.frama-c.com/pub/frama-c/-/issues/838ACSL parsing of greater-than relation with references2021-02-22T13:13:04ZVirgile PrevostoACSL parsing of greater-than relation with referencesID0001921:
**This issue was created automatically from Mantis Issue 1921. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001921:
**This issue was created automatically from Mantis Issue 1921. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001921 | Frama-Clang | Plug-in > clang | public | 2014-09-12 | 2015-02-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | virgile | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | - |
### Description :
On the following code:
/*@
ensures \result >= x;
*/
int f(int& x) { return ++x; }
/*@
ensures \result == x;
*/
int g(int& x) { return x; }
/*@
ensures \result >= x;
*/
int h(int x) { return x; }
contracts for g and h are correctly parsed, while contract of f produces the following error messages:
tests/specs/ref_spec.cpp:2:23: comparison of incompatible array types
tests/specs/ref_spec.cpp:2:23: expecting a term or predicate
tests/specs/ref_spec.cpp:2:23: the term is not a predicatehttps://git.frama-c.com/pub/frama-c/-/issues/840#include <foo> falls back to #include "foo" with misleading warning text2021-02-22T13:31:00ZJochen Burghardt#include <foo> falls back to #include "foo" with misleading warning textID0001947:
**This issue was created automatically from Mantis Issue 1947. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001947:
**This issue was created automatically from Mantis Issue 1947. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001947 | Frama-Clang | Plug-in > clang | public | 2014-10-30 | 2015-02-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | won't fix |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | xubuntu-cfe13.10 | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Calling 'frama-c 080.cpp', with 080foo.h residing in the same directory, the following output results:
080.cpp:2:10: error: '080foo.h' file not found with <angled> include; use "quotes" instead
#include <080foo.h>
^~~~~~~~~~
"080foo.h"
In file included from 080.cpp:2:
./080foo.h:2:2: error: included file 080foo.h
#error included file 080foo.h
^
code generation aborted due to compilation errors
[kernel] user error: Failed to parse C++ file. See Clang messages for more information
[kernel] user error: skipping file "080.cpp" that has errors.
[kernel] Frama-C aborted: invalid user input.
In contrast, the g++ compiler fails since '080foo.h' isn't found in '/usr/include'.
Apparently, Frama-C issues its first line as an error message, but then nevertheless continues, trying '#include "080foo.cpp"', rather than aborting. If that behavior (which is equivalent to have an implicit option '-I .' which can't be avoided by the user) is kept, Frama-C should issue a warning, saying '... using "quotes" ...' rather than '... use "quotes" ...'.
## Attachments
- [080.cpp](/uploads/172f1f34994145036a6e33d919dbc05c/080.cpp)
- [080foo.h](/uploads/5bcb61689d9dc88311188918e62d9d9b/080foo.h)https://git.frama-c.com/pub/frama-c/-/issues/852type "__fc_builtin_size_t" used in frama-c's own stddef.h version2021-02-22T13:32:42ZJochen Burghardttype "__fc_builtin_size_t" used in frama-c's own stddef.h versionID0001953:
**This issue was created automatically from Mantis Issue 1953. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001953:
**This issue was created automatically from Mantis Issue 1953. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001953 | Frama-Clang | Plug-in > clang | public | 2014-11-06 | 2015-02-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "gf 000.cpp" (both files attached) under linux, produces:
In file included from 000.cpp:2:
In file included from ./cstddef:5:
In file included from ./stddef.h:27:
./__fc_define_size_t.h:26:9: error: unknown type name '__fc_builtin_size_t'
typedef __SIZE_T size_t;
^
/usr/local/share/frama-c/libc/__fc_machdep.h:26:18: note: expanded from macro '__SIZE_T'
#define __SIZE_T __fc_builtin_size_t
^
code generation aborted due to one compilation error
[kernel] user error: Failed to parse C++ file. See Clang messages for more information
File cstddef has been set-up according to Vigile's suggestions, and is also attached; file stddef.h is a soft-link to share/libc/stddef.h in the frama-c-Neon-20140301+dev-stance distribution.
A grep showed that the name "__fc_builtin_size_t" occurs only in the following files of that distribution:
./share/libc/__fc_machdep.h:#define __SIZE_T __fc_builtin_size_t
./cil/src/frontc/cabs2cil.ml: | [A.Tnamed "__fc_builtin_size_t"] -> Cil.theMachine.typeOfSizeOf
./cil/src/frontc/cparser.ml: let sizeofType = [SpecType (Tnamed "__fc_builtin_size_t")], JUSTBASE in
./cil/src/frontc/clexer.mll: ("__fc_builtin_size_t", fun _loc -> NAMED_TYPE "__fc_builtin_size_t");
./cil/src/frontc/cparser.mly: let sizeofType = [SpecType (Tnamed "__fc_builtin_size_t")], JUSTBASE in
./cil/src/frontc/clexer.ml: ("__fc_builtin_size_t", fun _loc -> NAMED_TYPE "__fc_builtin_size_t");
./src/frama-clang/cxx_utils.ml:let builtin_types = [ "__builtin_va_list"; "__fc_builtin_size_t"; ]
So if it isn't known when processing the typedef in file __fc_define_size_t.h, this is an issue of some of the above *.ml* files, or some include file containing "#define __fc_builtin_size_t ..." is missing in the distribution. The problem remains if I omit the option "-machdep x86_64" in the sh-script "gf" calling frama-c.
I think the above error messages are from framaCIRGen, not from frama-c, but both are installed from the frama-c-Neon-20140301+dev-stance distribution, anyway.
## Attachments
- [gf](/uploads/813a6a133088b04f0501674d97243e30/gf)
- [000.cpp](/uploads/48b8be8be5770660df4940dc5263ee03/000.cpp)
- [cstddef](/uploads/0faceb25d955028e5976937aa7381075/cstddef)https://git.frama-c.com/pub/frama-c/-/issues/854destructor call ignored by WP2021-02-22T14:02:16ZJochen Burghardtdestructor call ignored by WPID0001961:
**This issue was created automatically from Mantis Issue 1961. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001961:
**This issue was created automatically from Mantis Issue 1961. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001961 | Frama-Clang | Plug-in > clang | public | 2014-11-10 | 2015-02-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | duplicate |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
The assertion in line 18 can't be proven by WP/Alt-Ergo. However, if the explicit constructor call is uncommented in line 16, the assertion (and any other obligation) can be proven. The .mlw files given to Alt-Ergo differ just in one precondition to the goal, viz. "(84 = (2 * i))", which is the translation of the destructor's contract (intentionally phrased in a clumsy way to prevent qed from proving the assertion). Both files are attached for convenience.
This problem is very likely the reason for issue #1738, too.
## Attachments
- [125.cpp](/uploads/d893d9e2adc21c127a9de88f0c7b3e7d/125.cpp)
- [impl.mlw](/uploads/9c7935b5e5c45dbbeeb1d46aaad07913/impl.mlw)
- [expl.mlw](/uploads/adde3ddc6b5101b2a3f4044702eccb4d/expl.mlw)https://git.frama-c.com/pub/frama-c/-/issues/856"->" in rhs of "==" in contract causes crash2021-02-22T13:32:43ZJochen Burghardt"->" in rhs of "==" in contract causes crashID0001958:
**This issue was created automatically from Mantis Issue 1958. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001958:
**This issue was created automatically from Mantis Issue 1958. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001958 | Frama-Clang | Plug-in > clang | public | 2014-11-10 | 2015-02-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
framaCIRGen: src/frama-clang/ACSLTermOrPredicate.h:276: void Acsl::TermOrPredicate::Operator::setLocation(location): Assertion `!_startLocation' failed.
Aborted (core dumped)
[kernel] user error: Failed to parse C++ file. See Clang messages for more information
The same file (renamed to "118.c") is handled pretty well by Frama-C for plain C.
The error disappears if the arguments of "==" are swapped in line 4.
It also disappears if "->" is changed to "." in line 4, and "A*" is changed to "A" in line 5.
Changing "==" to ">" keeps the error.
## Attachments
- [118.cpp](/uploads/ae1e6ab674c9dfa19b187bb1214b3fec/118.cpp)https://git.frama-c.com/pub/frama-c/-/issues/858parsing of hex int constant swallows following semicolon2021-03-29T16:45:10ZJochen Burghardtparsing of hex int constant swallows following semicolonID0001980:
**This issue was created automatically from Mantis Issue 1980. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001980:
**This issue was created automatically from Mantis Issue 1980. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001980 | Frama-Clang | Plug-in > clang | public | 2014-11-24 | 2015-02-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
142.cpp:2:26: Expecting ';' after post-condition
Now output intermediate result
The problem disappears if the "x" and the "0x" is omitted in line 2, thus changing the hexadecimal constant to an octal and decimal one, respectively.
The problem also disappears if the file is renamed to "142.c".
## Attachments
- [142.cpp](/uploads/bc26ae501b50d3387fca4ecd361abe51/142.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/862namespace prefix in annotation causes segmentation fault2021-03-29T16:41:05ZJochen Burghardtnamespace prefix in annotation causes segmentation faultID0001985:
**This issue was created automatically from Mantis Issue 1985. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001985:
**This issue was created automatically from Mantis Issue 1985. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001985 | Frama-Clang | Plug-in > clang | public | 2014-11-24 | 2015-02-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
Segmentation fault (core dumped)
[kernel] user error: Failed to parse C++ file. See Clang messages for more information
## Attachments
- [147.cpp](/uploads/ee910fafdfbabeb2abdb356f31ad4a03/147.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/869side effect of constructor call from global variable initialization ignored2021-02-22T14:02:18ZJochen Burghardtside effect of constructor call from global variable initialization ignoredID0002002:
**This issue was created automatically from Mantis Issue 2002. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002002:
**This issue was created automatically from Mantis Issue 2002. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002002 | Frama-Clang | Plug-in > clang | public | 2014-12-01 | 2015-02-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | duplicate |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
The attached program can be verified by "frama-c -wp 177.cpp", although printing x's value after line 11 reveals that the proven assertion there is false.
The reason is that x was set to 42 by the constructor call cls() from the declaration in line 8, but Frama-C doesn't consider the body code of line 5 when determining the value of x in line 11.
On the other hand, it seems that Frama-C is well aware about the declaration in line 8 calling the constructor in line 5: annotating the latter with "requires \false" produces an unproven obligation that vanishes again if line 8 is deleted.
## Attachments
- [177.cpp](/uploads/723d9cb3d39ae9300cad25f31ece596a/177.cpp)https://git.frama-c.com/pub/frama-c/-/issues/870insufficient preconditions given to Alt-Ergo to prove obligation originating ...2021-02-22T14:02:18ZJochen Burghardtinsufficient preconditions given to Alt-Ergo to prove obligation originating from virtual methodsID0001974:
**This issue was created automatically from Mantis Issue 1974. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001974:
**This issue was created automatically from Mantis Issue 1974. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001974 | Frama-Clang | Plug-in > clang | public | 2014-11-17 | 2015-02-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | duplicate |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp -wp-rte 138.cpp" on the attached 9-line program generates 98 proof obligations of which 71 turn out to be unprovable (by Qed and Alt-Ergo) after a total user-time of 3 minutes (see session protocol in file "138".txt"). These figures by their own may indicate a problem in scaling-up the current approach to C++ inheritance and virtual functions.
A closer look at e.g. the file "_Z26_frama_c_find_dynamic_castP28_frama_c_rtti_name_info_____10_Alt-Ergo.mlw" shows that Alt-Ergo is given insufficient preconditions to prove the goal
"forall i_2,i_1,i : int. forall t_2,t_1 : (addr,int) farray. ... -> is_sint32(i_2) -> is_sint32(t_2[...]) -> -2147483648 <= i_2 + t_2[...]".
Neither "i_2" nor "t_2" appear in the goal formula, except in the shown slice.
Knowing that both i_2 and t_2[...] are signed 32-bit ints is insufficient to prove that their sum won't underflow.
## Attachments
- [138.cpp](/uploads/9bb17093b31c46f1c71a4b8455b1c907/138.cpp)
- [138.txt](/uploads/0d56b0f35ac408035605037a1316ad19/138.txt)
- [_Z26_frama_c_find_dynamic_castP28_frama_c_rtti_name_info_____10_Alt-Ergo.mlw](/uploads/8e72ed9402b727d86b81bb8cca28f534/_Z26_frama_c_find_dynamic_castP28_frama_c_rtti_name_info_____10_Alt-Ergo.mlw)https://git.frama-c.com/pub/frama-c/-/issues/874clause labels not accepted by cxx plugin2021-02-22T13:13:53ZJochen Burghardtclause labels not accepted by cxx pluginID0002010:
**This issue was created automatically from Mantis Issue 2010. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002010:
**This issue was created automatically from Mantis Issue 2010. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002010 | Frama-Clang | Plug-in > clang | public | 2014-12-01 | 2015-02-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
187.cpp:2:27: expecting a term or predicate
187.cpp:2:27: expecting a predicate
Now output intermediate result
When the file is renamed to "187.c", Frama-C processes it without complaints, so I guess my syntax is correct. I failed to find this detail in the manual "acsl-implementation-Neon-20140301.pdf", cf. #2009.
## Attachments
- [187.cpp](/uploads/38bdf3aaabc360f9919bbc99cddd8bb1/187.cpp)https://git.frama-c.com/pub/frama-c/-/issues/875variable in then-part of "?:" in ACSL clause causes syntax error2021-02-22T13:13:55ZJochen Burghardtvariable in then-part of "?:" in ACSL clause causes syntax errorID0001993:
**This issue was created automatically from Mantis Issue 1993. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001993:
**This issue was created automatically from Mantis Issue 1993. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001993 | Frama-Clang | Plug-in > clang | public | 2014-11-27 | 2015-02-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
157.cpp:2:27: unexpected end of expression
The message disappears if "i" is replaced by "2" in the contract in line 2.
## Attachments
- [157.cpp](/uploads/f1b07e5429c0ae36142e24e8e7cf2eeb/157.cpp)https://git.frama-c.com/pub/frama-c/-/issues/877"&p->a" causes abort when "->" is user-defined2021-02-22T13:13:58ZJochen Burghardt"&p->a" causes abort when "->" is user-definedID0002025:
**This issue was created automatically from Mantis Issue 2025. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002025:
**This issue was created automatically from Mantis Issue 2025. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002025 | Frama-Clang | Plug-in > clang | public | 2014-12-11 | 2015-02-15 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
framaCIRGen: src/frama-clang/ACSLTermOrPredicate.h:276: void Acsl::TermOrPredicate::Operator::setLocation(location): Assertion `!_startLocation' failed.
Aborted (core dumped)
[kernel] user error: Failed to parse C++ file. See Clang messages for more information
The problem disappears if the assertion is replaced by the statement "if (&p->a == 0);".
## Attachments
- [199.cpp](/uploads/3e0bcc51008398612e7ce3d387855f6a/199.cpp)
- [400.cpp](/uploads/f61316995b878a4df7118757094715ba/400.cpp)https://git.frama-c.com/pub/frama-c/-/issues/879protected variable not visible in contract in subclass2021-02-22T14:02:19ZJochen Burghardtprotected variable not visible in contract in subclassID0002032:
**This issue was created automatically from Mantis Issue 2032. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002032:
**This issue was created automatically from Mantis Issue 2032. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002032 | Frama-Clang | Plug-in > clang | public | 2014-12-15 | 2015-02-15 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | duplicate |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
Now output intermediate result
405.cpp:6:[kernel] user error: Cannot find field salary
The error message remains even if "salary" is made "public" in line 2.
It disappears if the assigns clause in line 5 is deleted.
If "salary" is changed to "Employee::salary" in line 5 (contract), Frama-C aborts with the output:
framaCIRGen: SemaLookup.cpp:1622: bool clang::Sema::LookupQualifiedName(clang::LookupResult &, clang::DeclContext *, bool): Assertion `(!isa<TagDecl>(LookupCtx) || LookupCtx->isDependentContext() || cast<TagDecl>(LookupCtx)->isCompleteDefinition() || cast<TagDecl>(LookupCtx)->isBeingDefined()) && "Declaration context must already be complete!"' failed.
Aborted (core dumped)
## Attachments
- [405.cpp](/uploads/2604415c974ca132ad21fa0bfb2e0f9a/405.cpp)
- [406.cpp](/uploads/8f70ac40f88399771a698c999ed6a392/406.cpp)
- [408a.c](/uploads/0b0359c6a4713e4d26344413bba10744/408a.c)
- [408b.c](/uploads/2f8a39a246fa56a8f647e4698a807cf2/408b.c)https://git.frama-c.com/pub/frama-c/-/issues/882compile-time template recursion causes "multiply-defined" errors2021-02-22T13:43:19ZJochen Burghardtcompile-time template recursion causes "multiply-defined" errorsID0002038:
**This issue was created automatically from Mantis Issue 2038. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002038:
**This issue was created automatically from Mantis Issue 2038. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002038 | Frama-Clang | Plug-in > clang | public | 2014-12-18 | 2015-02-15 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
Now output intermediate result
421.cpp:8:[kernel] user error: redefinition of '_Z3val' in the same scope. Previous declaration was at 421.cpp:8
421.cpp:8:[kernel] user error: redefinition of '_Z3val' in the same scope. Previous declaration was at 421.cpp:8
421.cpp:8:[kernel] user error: redefinition of '_Z3val' in the same scope. Previous declaration was at 421.cpp:8
421.cpp:8:[kernel] user error: redefinition of '_Z3val' in the same scope. Previous declaration was at 421.cpp:8
421.cpp:8:[kernel] user error: redefinition of '_Z3val' in the same scope. Previous declaration was at 421.cpp:8
421.cpp:8:[kernel] user error: redefinition of '_Z3val' in the same scope. Previous declaration was at 421.cpp:8
421.cpp:8:[kernel] user error: redefinition of '_Z3val' in the same scope. Previous declaration was at 421.cpp:8
421.cpp:8:[kernel] user error: redefinition of '_Z3val' in the same scope. Previous declaration was at 421.cpp:8
421.cpp:8:[kernel] user error: redefinition of '_Z3val' in the same scope. Previous declaration was at 421.cpp:8
421.cpp:8:[kernel] user error: redefinition of '_Z3val' in the same scope. Previous declaration was at 421.cpp:8
421.cpp:8:[kernel] user error: redefinition of '_Z3val' in the same scope. Previous declaration was at 421.cpp:8
421.cpp:12:[kernel] user error: redefinition of '_Z3val' in the same scope. Previous declaration was at 421.cpp:8
[kernel] user error: skipping file "421.cpp" that has errors.
The problem remains if line 8 is simplified to "enum { val = 2 };".
## Attachments
- [421.cpp](/uploads/9cf0a89e99ce408e9dc6f580aa78d893/421.cpp)https://git.frama-c.com/pub/frama-c/-/issues/884contract of template function specialization taken to refer to next plain fun...2021-02-22T13:14:10ZJochen Burghardtcontract of template function specialization taken to refer to next plain function belowID0002042:
**This issue was created automatically from Mantis Issue 2042. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002042:
**This issue was created automatically from Mantis Issue 2042. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002042 | Frama-Clang | Plug-in > clang | public | 2015-01-05 | 2015-02-15 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Using "frama-c -wp 424.cpp" the attached program can be verified, although e.g. foo<int>(0) yields 2 whereas its contract says it should yield 4.
Apparently, Frama-C thinks the contract belongs to the plain function bar(). That would also be an explanation for issue #2034.
Moving the contract from line 4 down to line 6, or to line 8, keeps that behavior.
After moving it up to line 1 (i.e. before the generic template), no obligation at all is generated (which is ok since foo<>() isn't called anywhere).
## Attachments
- [424.cpp](/uploads/27785eb453be4b53b4f7843126234b75/424.cpp)
- [424a.cpp](/uploads/8bcfdd48f28c3257a7b0dbdfd882ce36/424a.cpp)https://git.frama-c.com/pub/frama-c/-/issues/886throw/catch of struct causes crash2021-03-29T16:21:09ZJochen Burghardtthrow/catch of struct causes crashID0001957:
**This issue was created automatically from Mantis Issue 1957. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001957:
**This issue was created automatically from Mantis Issue 1957. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001957 | Frama-Clang | Plug-in > clang | public | 2014-11-10 | 2015-02-15 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
Now output intermediate result
[kernel] Current source was: 117.cpp:12
The full backtrace is:
Raised at file "hashtbl.ml", line 229, characters 23-32
Called from file "src/kernel/exn_flow.ml", line 492, characters 23-63
Called from file "src/kernel/exn_flow.ml", line 509, characters 55-77
Called from file "list.ml", line 57, characters 20-23
Called from file "src/kernel/exn_flow.ml", line 624, characters 20-60
Called from file "src/kernel/visitor.ml", line 75, characters 14-33
Called from file "cil/src/cil.ml", line 2045, characters 15-31
Called from file "cil/src/cil.ml", line 3094, characters 5-86
Called from file "cil/src/cil.ml", line 2084, characters 13-16
Called from file "cil/src/cil.ml", line 3254, characters 16-40
Called from file "cil/src/cil.ml", line 2060, characters 21-41
Called from file "cil/src/cil.ml", line 3483, characters 14-39
Called from file "cil/src/cil.ml", line 2060, characters 21-41
Called from file "cil/src/cil.ml", line 3445, characters 5-91
Called from file "cil/src/cil.ml", line 3537, characters 16-38
Called from file "cil/src/cil.ml", line 2084, characters 13-16
Called from file "cil/src/cil.ml", line 2129, characters 24-57
Called from file "cil/src/cil.ml", line 3531, characters 5-53
Called from file "cil/src/cil.ml", line 6193, characters 17-37
Called from file "cil/src/cil.ml", line 6200, characters 3-20
Called from file "cil/src/cil.ml", line 2060, characters 21-41
Called from file "cil/src/cil.ml", line 6217, characters 15-39
Called from file "src/kernel/exn_flow.ml", line 687, characters 4-62
Called from file "src/kernel/file.ml", line 1617, characters 2-8
Called from file "queue.ml", line 134, characters 6-20
Called from file "src/kernel/file.ml", line 1694, characters 2-36
Called from file "src/kernel/file.ml", line 2264, characters 4-27
Called from file "src/kernel/ast.ml", line 111, characters 2-28
Called from file "src/kernel/ast.ml", line 123, characters 53-71
Called from file "src/kernel/boot.ml", line 29, characters 6-20
Called from file "src/kernel/cmdline.ml", line 761, characters 2-9
Called from file "src/kernel/cmdline.ml", line 216, characters 4-8
Unexpected error (Not_found).
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Neon-20140301+dev-stance.
The active code is probably minimal causing the crash; the problem remains if any of the commented-out lines is activated.
## Attachments
- [117.cpp](/uploads/033f024cfa988a542749b29f197f174f/117.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/888definition of virtual function in subclass causes crash2021-02-22T13:41:45ZJochen Burghardtdefinition of virtual function in subclass causes crashID0001973:
**This issue was created automatically from Mantis Issue 1973. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001973:
**This issue was created automatically from Mantis Issue 1973. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001973 | Frama-Clang | Plug-in > clang | public | 2014-11-17 | 2015-02-15 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
Now output intermediate result
137.cpp:5:[fclang] failure: No usable assign operator for ::Rectangle
[kernel] Current source was: 137.cpp:5
The full backtrace is:
Raised at file "src/kernel/log.ml", line 524, characters 30-31
Called from file "src/kernel/log.ml", line 518, characters 9-16
Re-raised at file "src/kernel/log.ml", line 521, characters 15-16
Called from file "src/frama-clang/convert.ml", line 1660, characters 30-71
Called from file "src/frama-clang/convert.ml", line 1683, characters 15-39
Called from file "list.ml", line 74, characters 24-34
Called from file "src/frama-clang/convert.ml", line 1686, characters 14-50
Called from file "src/frama-clang/convert.ml", line 1921, characters 21-142
Called from file "list.ml", line 74, characters 24-34
Called from file "src/frama-clang/convert.ml", line 1998, characters 19-78
Called from file "src/frama-clang/convert.ml", line 2262, characters 21-48
Called from file "list.ml", line 74, characters 24-34
Called from file "src/frama-clang/convert.ml", line 2266, characters 4-79
Called from file "src/frama-clang/frama_Clang_register.ml", line 86, characters 13-36
Called from file "src/kernel/file.ml", line 1073, characters 10-43
Called from file "src/kernel/file.ml", line 1117, characters 23-30
Called from file "list.ml", line 74, characters 24-34
Called from file "src/kernel/file.ml", line 1114, characters 6-520
Called from file "src/kernel/file.ml", line 2179, characters 12-30
Called from file "src/kernel/file.ml", line 2264, characters 4-27
Called from file "src/kernel/ast.ml", line 111, characters 2-28
Called from file "src/kernel/ast.ml", line 123, characters 53-71
Called from file "src/kernel/boot.ml", line 29, characters 6-20
Called from file "src/kernel/cmdline.ml", line 761, characters 2-9
Called from file "src/kernel/cmdline.ml", line 216, characters 4-8
Plug-in fclang aborted: internal error.
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Neon-20140301+dev-stance.
The problem disappears if
(1) the "virtual" is removed in line 6, or
(2) a copy of line 6 is inserted after line 2;
the problem remains if
(3) "area" is declared in class "Rectangle", too, but not as "virtual".
## Attachments
- [137.cpp](/uploads/b9c024091e5c2197c3677797a25f89a0/137.cpp)https://git.frama-c.com/pub/frama-c/-/issues/890use of template class from namespace causes crash2021-02-22T13:14:18ZJochen Burghardtuse of template class from namespace causes crashID0001971:
**This issue was created automatically from Mantis Issue 1971. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001971:
**This issue was created automatically from Mantis Issue 1971. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001971 | Frama-Clang | Plug-in > clang | public | 2014-11-17 | 2015-02-15 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
The file attached to issue #1970 can be simplified somewhat further while still causing the same crash message (however with a possibly different call stack - I didn't check that):
Now output intermediate result
135a.cpp:3:[fclang] failure: Unknown aggregate type std::vector<...>
[kernel] Current source was: 135a.cpp:3
The full backtrace is:
Raised at file "src/kernel/log.ml", line 524, characters 30-31
Called from file "src/kernel/log.ml", line 518, characters 9-16
Re-raised at file "src/kernel/log.ml", line 521, characters 15-16
Called from file "src/frama-clang/convert_env.ml", line 269, characters 43-71
Called from file "src/frama-clang/convert.ml", line 162, characters 17-69
Called from file "src/frama-clang/convert.ml", line 170, characters 17-52
Called from file "list.ml", line 57, characters 20-23
Called from file "src/frama-clang/convert.ml", line 1283, characters 13-45
Called from file "src/frama-clang/convert.ml", line 1910, characters 8-66
Called from file "list.ml", line 74, characters 24-34
Called from file "src/frama-clang/convert.ml", line 1998, characters 19-78
Called from file "src/frama-clang/convert.ml", line 2262, characters 21-48
Called from file "list.ml", line 74, characters 24-34
Called from file "src/frama-clang/convert.ml", line 2266, characters 4-79
Called from file "src/frama-clang/frama_Clang_register.ml", line 86, characters 13-36
Called from file "src/kernel/file.ml", line 1073, characters 10-43
Called from file "src/kernel/file.ml", line 1117, characters 23-30
Called from file "list.ml", line 74, characters 24-34
Called from file "src/kernel/file.ml", line 1114, characters 6-520
Called from file "src/kernel/file.ml", line 2179, characters 12-30
Called from file "src/kernel/file.ml", line 2264, characters 4-27
Called from file "src/kernel/ast.ml", line 111, characters 2-28
Called from file "src/kernel/ast.ml", line 123, characters 53-71
Called from file "src/kernel/boot.ml", line 29, characters 6-20
Called from file "src/kernel/cmdline.ml", line 761, characters 2-9
Called from file "src/kernel/cmdline.ml", line 216, characters 4-8
Plug-in fclang aborted: internal error.
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Neon-20140301+dev-stance.
Again, the problem disappears if the namespace environment is omitted (i.e. line 2,4 deleted, prefix "std::" deleted in line 6).
It also disappears if "vector" is made an unparametrized class, i.e. if "template<typename _Tp>" is deleted in line 3 and "<int>" is deleted in line 6.
## Attachments
- [135a.cpp](/uploads/6e2f98ce835744c14a137ab678a4f14a/135a.cpp)https://git.frama-c.com/pub/frama-c/-/issues/891struct type inside 'extern "C"' causes crash, except as lhs of typedef2021-03-29T16:16:35ZJochen Burghardtstruct type inside 'extern "C"' causes crash, except as lhs of typedefID0001965:
**This issue was created automatically from Mantis Issue 1965. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001965:
**This issue was created automatically from Mantis Issue 1965. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001965 | Frama-Clang | Plug-in > clang | public | 2014-11-13 | 2015-02-15 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
Now output intermediate result
132.cpp:4:[fclang] failure: Unknown declaration in extern C structure definition
[kernel] Current source was: 132.cpp:4
The full backtrace is:
Raised at file "src/kernel/log.ml", line 524, characters 30-31
Called from file "src/kernel/log.ml", line 518, characters 9-16
Re-raised at file "src/kernel/log.ml", line 521, characters 15-16
Called from file "list.ml", line 74, characters 24-34
Called from file "src/frama-clang/convert.ml", line 2032, characters 10-61
Called from file "src/frama-clang/convert.ml", line 2262, characters 21-48
Called from file "list.ml", line 74, characters 24-34
Called from file "src/frama-clang/convert.ml", line 2266, characters 4-79
Called from file "src/frama-clang/frama_Clang_register.ml", line 86, characters 13-36
Called from file "src/kernel/file.ml", line 1073, characters 10-43
Called from file "src/kernel/file.ml", line 1117, characters 23-30
Called from file "list.ml", line 74, characters 24-34
Called from file "src/kernel/file.ml", line 1114, characters 6-520
Called from file "src/kernel/file.ml", line 2179, characters 12-30
Called from file "src/kernel/file.ml", line 2264, characters 4-27
Called from file "src/kernel/ast.ml", line 111, characters 2-28
Called from file "src/kernel/ast.ml", line 123, characters 53-71
Called from file "src/kernel/boot.ml", line 29, characters 6-20
Called from file "src/kernel/cmdline.ml", line 761, characters 2-9
Called from file "src/kernel/cmdline.ml", line 216, characters 4-8
Plug-in fclang aborted: internal error.
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Neon-20140301+dev-stance.
When activated, each of the lines 5 and 6 causes a similar crash. This problem prohibits use of <stdio.h>.
## Attachments
- [132.cpp](/uploads/c8d869273866f020befb12a0e330ae22/132.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/899expression "&this->val" in logic function body causes framaCIRGen abort2021-02-22T13:52:47ZJochen Burghardtexpression "&this->val" in logic function body causes framaCIRGen abortID0002055:
**This issue was created automatically from Mantis Issue 2055. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002055:
**This issue was created automatically from Mantis Issue 2055. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002055 | Frama-Clang | Plug-in > clang | public | 2015-01-22 | 2015-02-14 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Neon-20140301+dev-STANCE-Jan2015 | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing 436.cpp (external front-end)
framaCIRGen: src/frama-clang/ACSLTermOrPredicate.h:276: void Acsl::TermOrPredicate::Operator::setLocation(location): Assertion `!_startLocation' failed.
Aborted (core dumped)
[kernel] user error: Failed to parse C++ file. See Clang messages for more information
Line 6 is just to demonstrate that the same expression is accepted in C++ code.
The problem disappears if
(1) both "*" and "&" is removed from line 5, or
(2) "this->" is removed from line 5.
## Attachments
- [436.cpp](/uploads/f2bc89ce2f0ad2fa74cdf8b1dd36eb15/436.cpp)https://git.frama-c.com/pub/frama-c/-/issues/901name in contract should refer to logic function, if defined, even in presence...2021-02-22T13:14:30ZJochen Burghardtname in contract should refer to logic function, if defined, even in presence of homonymous C++ methodID0002058:
**This issue was created automatically from Mantis Issue 2058. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002058:
**This issue was created automatically from Mantis Issue 2058. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002058 | Frama-Clang | Plug-in > clang | public | 2015-01-22 | 2015-02-14 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | low | **Severity** | feature | **Reproducibility** | always |
| **Platform** | Neon-20140301+dev-STANCE-Jan2015 | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
439.cpp:7:27: calls to functions/methods like 'size' are not allowed
Now output intermediate result
However, "size" in line 7 was intended to refer to the logic function from line 4, not to the C++ method of line 5. In fact, line 4 was added just because it isn't yet possible to refer to the "size" from line 5 in a contract.
(Low priority: eventually, the logic function from line 4 will be redundant; for the time being, a workaround is e.g. prefixing all logic functions with "l")
## Attachments
- [439.cpp](/uploads/9eaff3cdcef3f8e0efcc68066f62957e/439.cpp)https://git.frama-c.com/pub/frama-c/-/issues/902logic function call in rhs of relation chain causes abort2021-02-22T13:14:31ZJochen Burghardtlogic function call in rhs of relation chain causes abortID0002059:
**This issue was created automatically from Mantis Issue 2059. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002059:
**This issue was created automatically from Mantis Issue 2059. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002059 | Frama-Clang | Plug-in > clang | public | 2015-01-22 | 2015-02-14 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Neon-20140301+dev-STANCE-Jan2015 | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing 440.cpp (external front-end)
framaCIRGen: src/frama-clang/ACSLTermOrPredicate.h:633: void Acsl::TermOrPredicate::Operator::extractLastArgument(logic_type &, term &, predicate_named &): Assertion `targument' failed.
Aborted (core dumped)
[kernel] user error: Failed to parse C++ file. See Clang messages for more information
The problem remains if the return type of "lsize" is changed to "int", and its body to an int member of struct vector (e.g. "int sz;//@logic int lsize()=sz;").
The problem disappears if the use of "lsize()" is moved to any other position in the relation chain in line 4, or if that chain is shortened.
## Attachments
- [440.cpp](/uploads/7e043af6bff6f11766b4cbe3e8209001/440.cpp)https://git.frama-c.com/pub/frama-c/-/issues/904"\at" doesn't accept predicate argument label2021-02-22T13:14:33ZJochen Burghardt"\at" doesn't accept predicate argument labelID0002066:
**This issue was created automatically from Mantis Issue 2066. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002066:
**This issue was created automatically from Mantis Issue 2066. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002066 | Frama-Clang | Plug-in > clang | public | 2015-01-26 | 2015-02-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Neon-20140301+dev-STANCE-Jan2015 | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing 444.cpp (external front-end)
444.cpp:2:44: expecting a label in the \at construct
Now output intermediate result
The message disappears when the file is renamed to "444.c".
## Attachments
- [444.cpp](/uploads/3f08cdd8c2d7381ec3a22c2725f249af/444.cpp)https://git.frama-c.com/pub/frama-c/-/issues/905"*" in quantifier in axiom causes SEGV2021-02-22T13:14:34ZJochen Burghardt"*" in quantifier in axiom causes SEGVID0002069:
**This issue was created automatically from Mantis Issue 2069. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002069:
**This issue was created automatically from Mantis Issue 2069. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002069 | Frama-Clang | Plug-in > clang | public | 2015-01-29 | 2015-02-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Neon-20140301+dev-STANCE-Jan2015 | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing 445.cpp (external front-end)
Segmentation fault (core dumped)
[kernel] user error: Failed to parse C++ file. See Clang messages for more information
The problem disappears if the "*" in line 5 is deleted, or if the file is renamed to "445.c".
## Attachments
- [445.cpp](/uploads/e8bfff6a4322dfd90bf217aea81fd82e/445.cpp)https://git.frama-c.com/pub/frama-c/-/issues/939use of later-defined nested class type in method signature causes error2021-02-22T13:15:29ZJochen Burghardtuse of later-defined nested class type in method signature causes errorID0002027:
**This issue was created automatically from Mantis Issue 2027. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002027:
**This issue was created automatically from Mantis Issue 2027. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002027 | Frama-Clang | Plug-in > clang | public | 2014-12-11 | 2014-12-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | fvedrine | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C GIT, precise the release id |
### Description :
output:
Now output intermediate result
403.cpp:8:[kernel] user error: redefinition of '_ZN6StringE4Srep' in the same scope. Previous declaration was at 403.cpp:4
[kernel] user error: skipping file "403.cpp" that has errors.
The error remains if the definition of "Srep" is moved into "String".
The error disappears if the declarations of "foo" is deleted in line 4.
## Attachments
- [403.cpp](/uploads/4ea891dfc1b5ccbb91e068ab31096c71/403.cpp)https://git.frama-c.com/pub/frama-c/-/issues/940"catch(...)" causes crash2021-02-22T13:15:30ZJochen Burghardt"catch(...)" causes crashID0001966:
**This issue was created automatically from Mantis Issue 1966. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001966:
**This issue was created automatically from Mantis Issue 1966. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001966 | Frama-Clang | Plug-in > clang | public | 2014-11-13 | 2014-12-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C GIT, precise the release id |
### Description :
output:
Now output intermediate result
[kernel] Current source was: 133.cpp:3
The full backtrace is:
Raised at file "stack.ml", line 31, characters 20-25
Called from file "src/kernel/exn_flow.ml", line 120, characters 37-60
Called from file "list.ml", line 69, characters 12-15
Called from file "src/kernel/exn_flow.ml", line 112, characters 8-389
Called from file "src/kernel/visitor.ml", line 75, characters 14-33
Called from file "cil/src/cil.ml", line 2045, characters 15-31
Called from file "cil/src/cil.ml", line 3094, characters 5-86
Called from file "cil/src/cil.ml", line 2084, characters 13-16
Called from file "cil/src/cil.ml", line 3254, characters 16-40
Called from file "cil/src/cil.ml", line 2060, characters 21-41
Called from file "cil/src/cil.ml", line 3483, characters 14-39
Called from file "cil/src/cil.ml", line 2060, characters 21-41
Called from file "cil/src/cil.ml", line 3445, characters 5-91
Called from file "cil/src/cil.ml", line 3537, characters 16-38
Called from file "cil/src/cil.ml", line 2084, characters 13-16
Called from file "cil/src/cil.ml", line 2129, characters 24-57
Called from file "cil/src/cil.ml", line 3531, characters 5-53
Called from file "cil/src/cil.ml", line 6156, characters 16-36
Called from file "list.ml", line 69, characters 12-15
Called from file "cil/src/cil.ml", line 5746, characters 3-30
Called from file "cil/src/cil.ml", line 6157, characters 2-420
Called from file "cil/src/cil.ml", line 2060, characters 21-41
Called from file "cil/src/cil.ml", line 6190, characters 7-84
Called from file "src/kernel/visitor.ml", line 827, characters 2-45
Called from file "src/kernel/file.ml", line 1617, characters 2-8
Called from file "queue.ml", line 134, characters 6-20
Called from file "src/kernel/file.ml", line 1694, characters 2-36
Called from file "src/kernel/file.ml", line 2264, characters 4-27
Called from file "src/kernel/ast.ml", line 111, characters 2-28
Called from file "src/kernel/ast.ml", line 123, characters 53-71
Called from file "src/kernel/boot.ml", line 29, characters 6-20
Called from file "src/kernel/cmdline.ml", line 761, characters 2-9
Called from file "src/kernel/cmdline.ml", line 216, characters 4-8
Unexpected error (Stack.Empty).
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Neon-20140301+dev-stance.
Could be related to issue #1957?
(Importance: this code is used via #include <vector>.)
## Attachments
- [133.cpp](/uploads/ec10c3fb4d765ca86e6de649c4277911/133.cpp)https://git.frama-c.com/pub/frama-c/-/issues/941No access to inherited members of a struct in acsl clauses.2021-02-22T13:15:31Zmantis-gitlab-migrationNo access to inherited members of a struct in acsl clauses.ID0001852:
**This issue was created automatically from Mantis Issue 1852. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001852:
**This issue was created automatically from Mantis Issue 1852. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001852 | Frama-Clang | Plug-in > clang | public | 2014-07-23 | 2014-12-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | lapawczykt | **Assigned To** | fvedrine | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | ubuntu 64 14.04 | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | Frama-C GIT, precise the release id |
### Description :
It is not possible to access the members of the base class through a pointer to the derived class.
(pointer to object of derived struct -> member of base struct)
The problem only occurs if these two conditions are fullfilled:
1. The member is inherited from the base class.
2. The access happens inside an acsl clause. (i.e. after a requires or an ensures)
There are examples for all cases in the attached file "problem308.cpp".
### Additional Information :
Error message: Unsupported Field Access to i in struct B
## Attachments
- [problem308.cpp](/uploads/acbf063d1d601931880b131be79506fa/problem308.cpp)https://git.frama-c.com/pub/frama-c/-/issues/961contract completely ignored if preceeded by initial comment2021-02-22T13:51:35ZJochen Burghardtcontract completely ignored if preceeded by initial commentID0001819:
**This issue was created automatically from Mantis Issue 1819. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001819:
**This issue was created automatically from Mantis Issue 1819. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001819 | Frama-Clang | Plug-in > clang | public | 2014-06-27 | 2014-09-26 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | xubuntu-cfe13.10 (64 bit) | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | Frama-C GIT, precise the release id |
### Description :
Running "frama-c -wp -wp-rte Fault2.cpp -wp-out Fault2_64" on the attached program produces the attached file "_Z3fooi_assert.ergo", corresponding to the "assert" in line 8, but no .ergo file for the (non-trivial) "ensures" in line 5. The proof obligation in file "_Z3fooi_assert.ergo" shows that the requires from line 4 has been ignored, too.
In the gui, no contract at all is shown in the (left-hand side) normalized-code window.
The problem disappears if
(1) the file is renamed to "Fault2.c", or
(2) the comment is moved after the "requires" clause (, or removed completely).
## Attachments
- [Fault2.cpp](/uploads/065e1a4fe5bef2a28e0fc7ffb524867c/Fault2.cpp)
- [_Z3fooi_assert.ergo](/uploads/17ae2b20f01db327a5a4b6eda758bfc4/_Z3fooi_assert.ergo)https://git.frama-c.com/pub/frama-c/-/issues/962Frama-clang has problems with "decreases" clauses2021-02-22T13:16:01ZJens GerlachFrama-clang has problems with "decreases" clausesID0001815:
**This issue was created automatically from Mantis Issue 1815. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001815:
**This issue was created automatically from Mantis Issue 1815. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001815 | Frama-Clang | Plug-in > clang | public | 2014-06-20 | 2014-09-26 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **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 :
Frama-Clang reports a "expecting function spec" when it
encounters a decreases-clause in a function contract.
The decrease-clause and all following clauses in the same contract
are then ignored and do not appear in the normalised representation.
### Steps To Reproduce :
The attached file is also available under acslplusplus/C++Examples/Problems.
## Attachments
- [problem300.cpp](/uploads/61244a27776b55985918c660ae29041f/problem300.cpp)https://git.frama-c.com/pub/frama-c/-/issues/963array-type parameter causes "Old style K&R" kernel warning with cxx plugin2021-02-22T13:27:57ZJochen Burghardtarray-type parameter causes "Old style K&R" kernel warning with cxx pluginID0001814:
**This issue was created automatically from Mantis Issue 1814. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001814:
**This issue was created automatically from Mantis Issue 1814. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001814 | Frama-Clang | Plug-in > clang | public | 2014-06-20 | 2014-09-26 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | trivial | **Reproducibility** | always |
| **Platform** | - | **OS** | xubuntu-cfe13.10 | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | Frama-C GIT, precise the release id |
### Description :
output:
Now output intermediate result
taint02.cpp:7:[kernel] warning: Calling undeclared function _Z3fooPi. Old style K&R code?
The warning disappears if the file is renamed to "taint02.c".
## Attachments
- [taint02.cpp](/uploads/0071ae679c085de2390e5212762dc45d/taint02.cpp)https://git.frama-c.com/pub/frama-c/-/issues/964label argument of \at unrecognized2021-02-22T13:16:04ZJochen Burghardtlabel argument of \at unrecognizedID0001811:
**This issue was created automatically from Mantis Issue 1811. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001811:
**This issue was created automatically from Mantis Issue 1811. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001811 | Frama-Clang | Plug-in > clang | public | 2014-06-16 | 2014-09-26 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | xubuntu-cfe13.10 | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C GIT, precise the release id |
### Description :
output:
110.cpp:4:33: expecting a label in the \at construct
Now output intermediate result
The problem remains when "entry" in line 4 is replaced by any of the FRAMA-C predefined labels "Old", "Pre", "Here", or "Post".
The problem disappears when the file is renamed to "110.c".
## Attachments
- [110.cpp](/uploads/d68acdaeb675d2bcc606417edcfed286/110.cpp)https://git.frama-c.com/pub/frama-c/-/issues/965"\nothing" unrecognized in assigns clause2021-02-22T13:28:14ZJochen Burghardt"\nothing" unrecognized in assigns clauseID0001793:
**This issue was created automatically from Mantis Issue 1793. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001793:
**This issue was created automatically from Mantis Issue 1793. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001793 | Frama-Clang | Plug-in > clang | public | 2014-06-02 | 2014-09-26 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | xubuntu-cfe13.10 | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | Frama-C GIT, precise the release id |
### Description :
Running "frama-c from02.cpp" on the attached program yield the output:
from01.cpp:5:26: keyword 'keyword -> \nothing' encountered when parsing term or predicate
The error message disappears when the file is renamed to "from02.c"
## Attachments
- [from02.cpp](/uploads/cfe7e5a28737d3158b8d5f7d2f27fb1a/from02.cpp)https://git.frama-c.com/pub/frama-c/-/issues/987Use of axioms in axiomatic specification is not supported2021-02-22T13:16:42Zmantis-gitlab-migrationUse of axioms in axiomatic specification is not supportedID0001858:
**This issue was created automatically from Mantis Issue 1858. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001858:
**This issue was created automatically from Mantis Issue 1858. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001858 | Frama-Clang | Plug-in > clang | public | 2014-07-25 | 2014-08-08 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | lapawczykt | **Assigned To** | fvedrine | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | ubuntu 14.04 | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C GIT, precise the release id |
### Description :
As soon as an axiom is written inside an axiomatic specification frama-c complains: problem309.cpp:5:9: axiom foo_1should be declared inside an axiomatic.
However this works in c.
### Additional Information :
The problem309.c file can also be found in the acslplusplus repository.
### Steps To Reproduce :
frama-c-gui.byte -wp -rte -pp-annot -no-unicode problem309.cpp
## Attachments
- [problem309.cpp](/uploads/22b08fde2d4fe63f6d5f560958e94f6e/problem309.cpp)https://git.frama-c.com/pub/frama-c/-/issues/988Static attribute can not be accessed2021-02-22T13:16:43Zmantis-gitlab-migrationStatic attribute can not be accessedID0001820:
**This issue was created automatically from Mantis Issue 1820. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001820:
**This issue was created automatically from Mantis Issue 1820. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001820 | Frama-Clang | Plug-in > clang | public | 2014-06-27 | 2014-08-07 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | lapawczykt | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | ubuntu 14.04 | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | Frama-C GIT, precise the release id |
### Description :
Static attribute of a different object of the same class can not be accessed.
The error does not occur if the "static" is removed or the attribute belongs to the same object.
## Attachments
- [problem301.cpp](/uploads/f09f5c71368b0d5c21384fc7df9f087a/problem301.cpp)https://git.frama-c.com/pub/frama-c/-/issues/1016clause "n<9-1" normalized to "n-1<9"2021-02-22T13:17:26ZJochen Burghardtclause "n<9-1" normalized to "n-1<9"ID0001810:
**This issue was created automatically from Mantis Issue 1810. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001810:
**This issue was created automatically from Mantis Issue 1810. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001810 | Frama-Clang | Plug-in > clang | public | 2014-06-16 | 2014-06-19 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | xubuntu-cfe13.10 | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C GIT, precise the release id |
### Description :
Running "frama-c-gui -wp -wp-rte 108.cpp -wp-out wp-out" on the attached program shows in the gui's normalized-code window the clause "requires 0 <= n-1 && n-1 < 9;" as translation of source line 5 ("requires 0 <= n < 9-1;").
The same error is found in alt-ergo's input file "_Z4push_assert_rte_index_bound_2.ergo". As a consequence, alt-ergo can't prove the index bound for line 9.
The error disappears if
* the file is renamed to "108.c",
* "9-1" is replaced by "9" in line 5.
The error appears unchanged if "n" is made a procedure parameter of "push".
## Attachments
- [108.cpp](/uploads/f07695abe8c21809455ab3b47fd664b3/108.cpp)
- [_Z4push_assert_rte_index_bound_2.ergo](/uploads/e6b954a9726185b9f5ecdbb9bd90990d/_Z4push_assert_rte_index_bound_2.ergo)
- [109.cpp](/uploads/6aac1934cfc40814903aafd21efbc26b/109.cpp)https://git.frama-c.com/pub/frama-c/-/issues/1017Frama-Clang fails to parse simple predicate2021-02-22T13:17:27ZJens GerlachFrama-Clang fails to parse simple predicateID0001808:
**This issue was created automatically from Mantis Issue 1808. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...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. <eof> 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.cpphttps://git.frama-c.com/pub/frama-c/-/issues/1021Frama-clang include problem with directory hierarchy2021-02-22T13:17:33ZJens GerlachFrama-clang include problem with directory hierarchyID0001797:
**This issue was created automatically from Mantis Issue 1797. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001797:
**This issue was created automatically from Mantis Issue 1797. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001797 | Frama-Clang | Plug-in > clang | public | 2014-06-04 | 2014-06-11 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | - |
### Description :
The attached tar file contains a small directory hierarchy
problem206-dir
├── nonmutating
│ └── equal
│ ├── README
│ └── equal.c
└── typedefs.h
The file equal.c includes the file typedefs.h which is two layers up in the hierarchy.
When I call
frama-c.byte -cxx-clang-command="framaCIRGen -I../.." equal.c
then I receive the following error message
[kernel] preprocessing with "gcc -C -E -I. equal.c"
equal.c:2:20: fatal error: typedefs: No such file or directory
#include "typedefs"
^
compilation terminated.
[kernel] user error: failed to run: gcc -C -E -I. -o '/tmp/equal.c5f0bc4.i' 'equal.c'
you may set the CPP environment variable to select the proper preprocessor command or use the option "-cpp-command".
[kernel] user error: skipping file "equal.c" that has errors.
[kernel] Frama-C aborted: invalid user input.
### Additional Information :
I am particularly baffled by the kernels message to "use -cpp-command" because I thought this option is not to be used with frama-clang.
Also, the problem disappears when the header typedefs.h is only one level above equal.c.
(Of course, the command line has to be changed accordingly.)
The example can also be found in
acslplusplus/C++Examples/Problems/problem206-dir
## Attachments
- [problem206-dir.tar](/uploads/cca3489eeafcb5be7e26e3fdcc9308bb/problem206-dir.tar)https://git.frama-c.com/pub/frama-c/-/issues/2558[frama-clang] Cannot parse built-in function __underlying_type()2021-07-14T17:00:34ZStefan Gränitz[frama-clang] Cannot parse built-in function __underlying_type()<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the iss...<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- you installed Frama-C as prescribed in the [instructions](INSTALL.md).
If the issue applies to a specific Frama-C plug-in, please prefix the title
by the plug-in name: [Eva], [WP], [E-ACSL]…
-->
### Steps to reproduce the issue
Please find attached two example sources that demonstrate the issue:
[fails.cpp](/uploads/61673f65c32ca8006fd5da43333d0b96/fails.cpp)
[works.cpp](/uploads/1ed13606089f45a7eac4f3a3ce77b275/works.cpp)
```
> cat fails.cpp
enum class SelectedNumbers : int { One = 1 };
int main() {
return static_cast<__underlying_type(SelectedNumbers)>(SelectedNumbers::One);
}
> clang++-11 -E -o fails.ii fails.cpp
> frama-c -deps fails.ii
```
### Expected output
```
[kernel] Parsing fails.ii (external front-end)
Now output intermediate result
<...>
[from] Computing for function main
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
These dependencies hold at termination for the executions that terminate:
[from] Function main:
\result FROM \nothing
[from] ====== END OF DEPENDENCIES ======
```
### Actual output
```
[kernel] Parsing fails.ii (external front-end)
fails.cpp:4:10: Unsupported Type (unknown kind (48)):__underlying_type(enum SelectedNumbers)
Aborting
[kernel] User Error: Failed to parse C++ file. See Clang messages for more information
[kernel] User Error: stopping on file "fails1.ii" that has errors.
[kernel] Frama-C aborted: invalid user input.
```
### Minimal working diff
It works if we avoid the `__underlying_type()` built-in function and instead specify it manually:
```
diff -u fails.cpp works.cpp
--- fails.cpp 2021-05-26 10:25:30.839759691 +0000
+++ works.cpp 2021-05-26 10:40:31.251352326 +0000
@@ -1,5 +1,5 @@
enum class SelectedNumbers : int { One = 1 };
int main() {
- return static_cast<__underlying_type(SelectedNumbers)>(SelectedNumbers::One);
+ return static_cast<int>(SelectedNumbers::One);
}
```
### Contextual information
- Frama-C: framac/frama-c:22.0 Docker Image ID e45780e160f1
- Plug-in used: frama-clang-0.0.10 built from official source drop
- Compiler: Debian clang version 11.1.0
- Target: x86_64-pc-linux-gnuVirgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/2561[frama-clang] Cannot parse C++14 generic lambda2022-04-14T17:19:42ZStefan Gränitz[frama-clang] Cannot parse C++14 generic lambda<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the iss...<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- you installed Frama-C as prescribed in the [instructions](INSTALL.md).
If the issue applies to a specific Frama-C plug-in, please prefix the title
by the plug-in name: [Eva], [WP], [E-ACSL]…
-->
### Steps to reproduce the issue
Please find attached two example sources that demonstrate the issue:
[fails.cpp](/uploads/2a5f09fd150e99bb9978ee9eb06d252f/fails.cpp)
[works.cpp](/uploads/e4f05a0dd3348d8d0367afde1d2f1ec0/works.cpp)
```
> cat fails.cpp
int main(int argc, char *argv[]) {
auto lambda = [](auto argc) { return argc; };
return lambda(argc);
}
> clang++-11 -E -o fails.ii fails.cpp
> frama-c -deps -cpp-extra-args="-std=c++14" fails.ii
```
### Expected output
```
[kernel] Parsing fails.ii (external front-end)
Now output intermediate result
<...>
[from] Computing for function main
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
These dependencies hold at termination for the executions that terminate:
[from] Function UliEUcE__cons:
__fc_lam FROM __fc_closure; __fc_func
[from] Function __fc_lambda_def:
\result FROM argc
[from] Function main:
\result FROM argc
[from] ====== END OF DEPENDENCIES ======
```
### Actual output
```
[kernel] Parsing fails.ii (external front-end)
framaCIRGen: /usr/lib/llvm-11/include/clang/AST/Type.h:671: const clang::ExtQualsTypeCommonBase *clang::QualType::getCommonPtr() const: Assertion `!isNull() && "Cannot retrieve a NULL type pointer"' failed.
Aborted
[kernel] User Error: Failed to parse C++ file. See Clang messages for more information
[kernel] User Error: stopping on file "fails.ii" that has errors.
[kernel] Frama-C aborted: invalid user input.
```
### Minimal working diff
It works if we write `int` instead of `auto` for the type of the lambda parameter:
```
> diff -u fails.cpp works.cpp
--- fails.cpp 2021-06-08 22:42:13 +0200
+++ works.cpp 2021-06-08 22:43:48 +0200
@@ -1,4 +1,4 @@
int main(int argc, char *argv[]) {
- auto lambda = [](auto argc) { return argc; };
+ auto lambda = [](int argc) { return argc; };
return lambda(argc);
}
```
### Contextual information
- Frama-C: framac/frama-c:22.0 Docker Image ID e45780e160f1
- Plug-in used: frama-clang-0.0.10 built from official source drop
- Compiler: Debian clang version 11.1.0
- Target: x86_64-pc-linux-gnu
### Additional information
Generic lambdas are a C++14 language feature:
https://isocpp.org/wiki/faq/cpp14-language#generic-lambdasVirgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/2564[frama-clang] std::forward with non-primitive type causes NON TERMINATING2022-04-22T13:54:07ZStefan Gränitz[frama-clang] std::forward with non-primitive type causes NON TERMINATING<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the iss...<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- you installed Frama-C as prescribed in the [instructions](INSTALL.md).
If the issue applies to a specific Frama-C plug-in, please prefix the title
by the plug-in name: [Eva], [WP], [E-ACSL]…
-->
### Steps to reproduce the issue
~~Please find attached two example sources that demonstrate the issue: [fails.cpp](/uploads/69d2c79afe05be14b237e337c90f0d9b/fails.cpp) [works.cpp](/uploads/a28e5308e6b0f638172b084eb5572861/works.cpp)~~
Please find attached the narrowed example sources that demonstrate the issue with `std::forward` alone:
[fails.cpp](/uploads/8f135c54a38dc95e8cb162033dc7e29b/fails.cpp)[works.cpp](/uploads/1c2846a51c27d8cd745afff3baf6d950/works.cpp)
**Further investigation details can be found in the comments.** What follows here is the original issue description:
```
> cat fails.cpp
#include <memory>
struct Foo {
int val;
Foo(int val) : val(val) {}
int bar() { return val; }
};
int main(int argc, char **argv) {
std::unique_ptr<Foo> foo1(new Foo(argc));
std::unique_ptr<Foo> foo2 = std::move(foo1);
return foo2->bar();
}
> frama-c -deps fails.cpp
```
### Expected behaviour
```
[kernel] Parsing fails.cpp (external front-end)
Now output intermediate result
...
[from] Function main:
__malloc_main_l10 FROM argc
\result FROM argc
[from] ====== END OF DEPENDENCIES ======
```
### Actual behaviour
```
[kernel] Parsing fails.cpp (external front-end)
Now output intermediate result
...
[from] Function main:
NON TERMINATING - NO EFFECTS
[from] ====== END OF DEPENDENCIES ======
```
### Minimal working diff
It works if we avoid the move assignment:
```
> diff -u fails.cpp works.cpp
--- fails.cpp 2021-06-21 10:40:26.613967584 +0000
+++ works.cpp 2021-06-21 10:38:12.276859713 +0000
@@ -8,6 +8,5 @@
int main(int argc, char **argv) {
std::unique_ptr<Foo> foo1(new Foo(argc));
- std::unique_ptr<Foo> foo2 = std::move(foo1);
- return foo2->bar();
+ return foo1->bar();
}
```
### Contextual information
* Frama-C: framac/frama-c:22.0 Docker Image ID e45780e160f1
* Plug-in used: frama-clang-0.0.10 built from official source drop
* Compiler: Debian clang version 11.1.0
* Target: x86_64-pc-linux-gnu
### Additional information
One more observation is that the plugin is unable to parse a preprocessed source file:
```
> clang++-11 -E -o works.ii works.cpp
> frama-c -deps works.ii
[kernel] Parsing works.ii (external front-end)
works.ii:316:32: error: __int128 is not supported on this target
template<> struct __is_integer<__int128> { enum { __value = 1 }; typedef __true_type __type; }; template<> struct __is_integer<unsigned __int128> { enum { __value = 1 }; typedef __true_type __type; };
^
...
code generation aborted due to compilation errors
[kernel] User Error: Failed to parse C++ file. See Clang messages for more information
[kernel] User Error: stopping on file "works.ii" that has errors.
[kernel] Frama-C aborted: invalid user input.
```Virgile PrevostoVirgile Prevosto