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/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/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/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/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 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/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/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/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/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/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/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 Prevosto