frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2021-06-09T06:23:25Zhttps://git.frama-c.com/pub/frama-c/-/issues/2562[frama-clang] Cannot parse C++14 variable template2021-06-09T06:23:25ZStefan Gränitz[frama-clang] Cannot parse C++14 variable template<!--
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/b452f30e405c34a0f73e45e7c47049c5/fails.cpp)
[works.cpp](/uploads/f3e16883180db5fcb3d9c7c3f50523a7/works.cpp)
```
> cat fails.cpp
template <class _Tp>
struct in_place_type_t {};
template <class _Tp>
in_place_type_t<_Tp> in_place_type{};
int main() {
return 0;
}
> 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 main:
\result FROM \nothing
[from] ====== END OF DEPENDENCIES ======
```
### Actual output
```
[kernel] Parsing fails.ii (external front-end)
fails.cpp:5:22: Unsupported Type (uninstantiated template specialization):in_place_type_t<_Tp>
Aborting
[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 avoid the unused `in_place_type` variable:
```
> diff -u fails.cpp works.cpp
--- fails.cpp 2021-06-08 22:57:23.374859568 +0000
+++ works.cpp 2021-06-08 23:04:33.305251313 +0000
@@ -1,8 +1,8 @@
template <class _Tp>
struct in_place_type_t {};
-template <class _Tp>
-in_place_type_t<_Tp> in_place_type{};
+//template <class _Tp>
+//in_place_type_t<_Tp> in_place_type{};
int main() {
return 0;
```
### 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
Variable templates are a C++14 language feature:
https://isocpp.org/wiki/faq/cpp14-language#variable-templatesVirgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/2546Problems with a simplest Arduino program, that contain only "Arduino.h" include.2021-10-06T07:49:50ZvarosiProblems with a simplest Arduino program, that contain only "Arduino.h" include.Hello!
I'm trying to evaluate if Frama-C could be used for verification of embedded software.
I have a simple program which just include "Arduino.h".
I run this commands:
```
export FC_COMPILER=$'-Os -mlong-calls -falign-functions=4 -...Hello!
I'm trying to evaluate if Frama-C could be used for verification of embedded software.
I have a simple program which just include "Arduino.h".
I run this commands:
```
export FC_COMPILER=$'-Os -mlong-calls -falign-functions=4 -U__STRICT_ANSI__ -ffunction-sections -fdata-sections -fno-exceptions -DPLATFORMIO=50101 -DESP8266 -DARDUINO_ARCH_ESP8266 -DARDUINO_ESP8266_ESP12 -DF_CPU=160000000L -D__ets__ -DICACHE_FLASH -DARDUINO=10805 -DARDUINO_BOARD=PLATFORMIO_ESP12E -DFLASHMODE_DIO -DLWIP_OPEN_SRC -DNONOSDK22x_190703=1 -DTCP_MSSß=536 -DLWIP_FEATURES=1 -DLWIP_IPV6=0 -DVTABLES_IN_FLASH -I.platformio/packages/framework-arduinoespressif8266/cores/esp8266 -I.platformio/packages/framework-arduinoespressif8266/tools/sdk/include -I.platformio/packages/framework-arduinoespressif8266/tools/sdk/libc/xtensa-lx106-elf/include'
export FC_ERRORS="-kernel-warn-key annot-error=error"
frama-c ${FC_ERRORS} -fclang-cpp-extra-args="${FC_COMPILER}" -machdep x86_32 -wp -wp-rte src/main.cpp
```
in a Docker container varosi/frama-c-clang:21.1
I get a lot of errors such as:
```
In file included from /app/src/main.cpp:4:
In file included from .platformio/packages/framework-arduinoespressif8266/cores/esp8266/Arduino.h:238:
In file included from /usr/local/share/frama-c/frama-clang/libc++/algorithm:26:
In file included from /usr/local/share/frama-c/frama-clang/libc++/functional:27:
In file included from /usr/local/share/frama-c/frama-clang/libc++/utility:28:
/usr/local/share/frama-c/frama-clang/libc++/type_traits:284:46: error: template argument for template type parameter must be a type
using conditional_t = typename conditional<B,T,F>::type;
^
/usr/local/share/frama-c/frama-clang/libc++/type_traits:278:25: note: template parameter is declared here
template <bool, class T, class F> struct conditional;
^
/usr/local/share/frama-c/frama-clang/libc++/type_traits:284:54: error: expected a qualified name after 'typename'
using conditional_t = typename conditional<B,T,F>::type;
^
/usr/local/share/frama-c/frama-clang/libc++/type_traits:284:54: error: type-id cannot have a name
using conditional_t = typename conditional<B,T,F>::type;
----------------
In file included from /app/src/main.cpp:4:
In file included from .platformio/packages/framework-arduinoespressif8266/cores/esp8266/Arduino.h:238:
In file included from /usr/local/share/frama-c/frama-clang/libc++/algorithm:26:
In file included from /usr/local/share/frama-c/frama-clang/libc++/functional:27:
/usr/local/share/frama-c/frama-clang/libc++/utility:33:23: error: unknown type name '_Bool'
template<class T> bool operator!=(const T& x, const T& y) { return !(x == y); }
^
/usr/local/share/frama-c/libc/stdbool.h:25:14: note: expanded from macro 'bool'
#define bool _Bool
----------------
In file included from /app/src/main.cpp:4:
In file included from .platformio/packages/framework-arduinoespressif8266/cores/esp8266/Arduino.h:238:
In file included from /usr/local/share/frama-c/frama-clang/libc++/algorithm:26:
In file included from /usr/local/share/frama-c/frama-clang/libc++/functional:27:
/usr/local/share/frama-c/frama-clang/libc++/utility:68:40: error: expected a qualified name after 'typename'
const T&, T&&>::type
^
/usr/local/share/frama-c/frama-clang/libc++/utility:68:40: warning: variable templates are a C++14 extension
/usr/local/share/frama-c/frama-clang/libc++/utility:68:44: error: expected ';' at end of declaration
const T&, T&&>::type
^
;
/usr/local/share/frama-c/frama-clang/libc++/utility:69:20: error: unknown type name 'T'
move_if_noexcept(T& x) noexcept { return std::move<T&>(x); }
--------------------
In file included from /app/src/main.cpp:4:
In file included from .platformio/packages/framework-arduinoespressif8266/cores/esp8266/Arduino.h:238:
In file included from /usr/local/share/frama-c/frama-clang/libc++/algorithm:26:
In file included from /usr/local/share/frama-c/frama-clang/libc++/functional:27:
/usr/local/share/frama-c/frama-clang/libc++/utility:110:16: error: template argument for template type parameter must be a type; did you forget 'typename'?
__and<
^
typename
/usr/local/share/frama-c/frama-clang/libc++/type_traits:274:25: note: template parameter is declared here
template <bool, class T=void> struct enable_if;
--------------------
```
What can be fixed here?Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/906exception identifier from catch() statement unknown in contracts, but not in ...2021-02-22T13:28:04ZJochen Burghardtexception identifier from catch() statement unknown in contracts, but not in codeID0002071:
**This issue was created automatically from Mantis Issue 2071. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002071:
**This issue was created automatically from Mantis Issue 2071. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002071 | Frama-Clang | Plug-in > clang | public | 2015-02-02 | 2015-02-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **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 447.cpp (external front-end)
447.cpp:6:17: unknown identifier 'e'
Now output intermediate result
The message disappears if the "assert" in line 6 is deactivated.
## Attachments
- [447.cpp](/uploads/25b6f25f7846390e808821adc8820019/447.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/903can't compare pointer and reference for equality in contract2021-02-22T13:14:31ZJochen Burghardtcan't compare pointer and reference for equality in contractID0002060:
**This issue was created automatically from Mantis Issue 2060. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002060:
**This issue was created automatically from Mantis Issue 2060. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002060 | Frama-Clang | Plug-in > clang | public | 2015-01-22 | 2015-02-14 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **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 441.cpp (external front-end)
441.cpp:2:22: invalid implicit conversion
441.cpp:2:22: unknown type comparison for the operator ==
Now output intermediate result
When line 2 is commented out, the comparison in C++ code in line 3 is accepted.
## Attachments
- [441.cpp](/uploads/da2cc8f3623d5563d069827341da0b18/441.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/900type def'd as template typename causes SEGV when used in logic functions2021-02-22T13:14:28ZJochen Burghardttype def'd as template typename causes SEGV when used in logic functionsID0002057:
**This issue was created automatically from Mantis Issue 2057. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002057:
**This issue was created automatically from Mantis Issue 2057. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002057 | Frama-Clang | Plug-in > clang | public | 2015-01-22 | 2015-02-14 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | fvedrine | **Resolution** | open |
| **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 :
In its current version, the program apparently causes a SEGV of the front-end:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing 438.cpp (external front-end)
Segmentation fault (core dumped)
[kernel] user error: Failed to parse C++ file. See Clang messages for more information
Several variations cause different behaviors, such as:
(1) changing "integer" to "int " in line 8:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing 438.cpp (external front-end)
438.cpp:8:51: invalid implicit conversion
438.cpp:8:51: expecting a term as body of function
Now output intermediate result
(2) omitting the template parameter, and changing "T" to "int" in line 3:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing 438.cpp (external front-end)
Now output intermediate result
[fclang] failure: Cannot understand intermediate AST: line 799: unexpected unknown constructor 39702768 (Unknown constructor for term_node)
[kernel] Current source was: FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i:43
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/frama_Clang_register.ml", line 83, characters 6-75
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.
(3) changing "pointer" to "T*" in line 7:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing 438.cpp (external front-end)
438.cpp:8:55: predicates do not support binary '+' operation
Now output intermediate result
438.cpp:7:[fclang] failure: predicate definition with a term as body
[kernel] Current source was: 438.cpp:7
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 2393, characters 18-54
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.
## Attachments
- [438.cpp](/uploads/4ab4dc04efdff7cdadbd1e41d15d47e0/438.cpp)
- [438a.cpp](/uploads/957036da370283dcaa88f2713cd9f18a/438a.cpp)Franck VedrineFranck Vedrinehttps://git.frama-c.com/pub/frama-c/-/issues/898catching a superclass causes crash2021-02-22T13:14:26ZJochen Burghardtcatching a superclass causes crashID0002051:
**This issue was created automatically from Mantis Issue 2051. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002051:
**This issue was created automatically from Mantis Issue 2051. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002051 | Frama-Clang | Plug-in > clang | public | 2015-01-15 | 2015-02-14 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **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:
Now output intermediate result
[fclang] failure: Did not find struct for mangled class name _Z9Underflow
[kernel] Current source was: 432.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_link.ml", line 71, characters 36-53
Called from file "src/lib/FCSet.ml", line 332, characters 37-58
Called from file "src/frama-clang/convert_link.ml", line 86, characters 16-112
Called from file "src/frama-clang/convert_link.ml", line 104, characters 16-62
Called from file "list.ml", line 57, characters 20-23
Called from file "src/frama-clang/convert_link.ml", line 102, characters 12-142
Called from file "src/kernel/visitor.ml", line 75, characters 14-33
Called from file "cil/src/cil.ml", line 2046, characters 15-31
Called from file "cil/src/cil.ml", line 3095, characters 5-86
Called from file "cil/src/cil.ml", line 2085, characters 13-16
Called from file "cil/src/cil.ml", line 3255, characters 16-40
Called from file "cil/src/cil.ml", line 2061, characters 21-41
Called from file "cil/src/cil.ml", line 3484, characters 14-39
Called from file "cil/src/cil.ml", line 2061, characters 21-41
Called from file "cil/src/cil.ml", line 3446, characters 5-91
Called from file "cil/src/cil.ml", line 3538, characters 16-38
Called from file "cil/src/cil.ml", line 2085, characters 13-16
Called from file "cil/src/cil.ml", line 2130, characters 24-57
Called from file "cil/src/cil.ml", line 3532, characters 5-53
Called from file "cil/src/cil.ml", line 6151, characters 16-36
Called from file "list.ml", line 69, characters 12-15
Called from file "cil/src/cil.ml", line 5741, characters 3-30
Called from file "cil/src/cil.ml", line 6152, characters 2-420
Called from file "cil/src/cil.ml", line 2061, characters 21-41
Called from file "cil/src/cil.ml", line 6185, characters 7-84
Called from file "src/kernel/file.ml", line 1803, characters 2-8
Called from file "queue.ml", line 134, characters 6-20
Called from file "src/kernel/file.ml", line 1880, characters 2-36
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 remains if some member variable (e.g. "int x;") is added to the body of class "Matherr" in line 2 or/and the body of class "Underflow" in line 3.
The problem disappears if either:
(1) the definition of "Underflow" in line 3 is deleted,
(2) the definition of "foo" in line 5-10 is deleted,
(3) "Matherr" is changed to "Underflow" in the catch statement in line 8, or
(4) "public" is changed to "private" in line 3.
## Attachments
- [432.cpp](/uploads/c3a89685372790a4946ec88f8e54c293/432.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/897recursive logic integer function definition causes error2021-02-22T13:27:11ZJochen Burghardtrecursive logic integer function definition causes errorID0002050:
**This issue was created automatically from Mantis Issue 2050. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002050:
**This issue was created automatically from Mantis Issue 2050. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002050 | Frama-Clang | Plug-in > clang | public | 2015-01-15 | 2015-02-14 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **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:
431.cpp:2:56: unknown identifier 'fac'
Now output intermediate result
The problem disappears when the file is renamed to "431.c".
## Attachments
- [431.cpp](/uploads/50a3448bd9c7ec87a3c7205370803f6e/431.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/896ACSL comment rejected in function template2021-02-22T13:27:13ZJochen BurghardtACSL comment rejected in function templateID0002048:
**This issue was created automatically from Mantis Issue 2048. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002048:
**This issue was created automatically from Mantis Issue 2048. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002048 | Frama-Clang | Plug-in > clang | public | 2015-01-12 | 2015-02-14 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **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 430.cpp (external front-end)
inadequate comment at 430.cpp:5:2
If line 2 is commented-in and line 3 is commented-out, the error message disappears.
## Attachments
- [430.cpp](/uploads/fb7c1b9a2c7e740eb0e5c7200661ce99/430.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/895unprovable obligation generated for "ensures" in presence of exceptions2021-02-22T13:14:24ZJochen Burghardtunprovable obligation generated for "ensures" in presence of exceptionsID0002046:
**This issue was created automatically from Mantis Issue 2046. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002046:
**This issue was created automatically from Mantis Issue 2046. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002046 | Frama-Clang | Plug-in > clang | public | 2015-01-08 | 2015-02-14 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **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 :
Running "frama-c -wp 429.cpp" on the attached program, the goal "typed__Z3bari_post_part1" cannot be proven by Alt-Ergo, i.e. it can't be proven that the postcondition of "foo" implies that of "bar" if the former doesn't throw an exception.
The goal in the file "_Z3bari_post_part1_Alt-Ergo.mlw" reads:
585 goal _Z3bari_post_part1:
586 forall i : int.
587 forall f : S___fc_exn_struct.
588 let x = (f.F___fc_exn_struct_exn_uncaught) : int in
589 (1 <> x) ->
590 is_sint32(i) ->
591 is_sint32(f.F___fc_exn_struct_exn_kind) ->
592 is_sint32(x) ->
593 ((0 = x) -> (42 <= i)) ->
594 (24 <= i)
If line 589 is changed to "(0 = x) ->", Alt-Ergo can prove it without problems; likewise if line 593 is changed to "((1 <> x) -> (42 <= i)) ->".
## Attachments
- [429.cpp](/uploads/8924b97702a6b0ba13c4daf1f56285ca/429.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/894throw without argument causes crash2021-02-22T13:41:11ZJochen Burghardtthrow without argument causes crashID0002045:
**This issue was created automatically from Mantis Issue 2045. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002045:
**This issue was created automatically from Mantis Issue 2045. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002045 | Frama-Clang | Plug-in > clang | public | 2015-01-08 | 2015-02-14 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **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:
Now output intermediate result
[kernel] Current source was: 428.cpp:2
The full backtrace is:
Raised at file "stack.ml", line 36, characters 20-25
Called from file "src/kernel/exn_flow.ml", line 98, characters 23-44
Called from file "src/kernel/visitor.ml", line 75, characters 14-33
Called from file "cil/src/cil.ml", line 2046, characters 15-31
Called from file "cil/src/cil.ml", line 3095, characters 5-86
Called from file "cil/src/cil.ml", line 2085, characters 13-16
Called from file "cil/src/cil.ml", line 3255, characters 16-40
Called from file "cil/src/cil.ml", line 2061, characters 21-41
Called from file "cil/src/cil.ml", line 3484, characters 14-39
Called from file "cil/src/cil.ml", line 2061, characters 21-41
Called from file "cil/src/cil.ml", line 3446, characters 5-91
Called from file "cil/src/cil.ml", line 3538, characters 16-38
Called from file "cil/src/cil.ml", line 2085, characters 13-16
Called from file "cil/src/cil.ml", line 2130, characters 24-57
Called from file "cil/src/cil.ml", line 3532, characters 5-53
Called from file "cil/src/cil.ml", line 6151, characters 16-36
Called from file "list.ml", line 69, characters 12-15
Called from file "cil/src/cil.ml", line 5741, characters 3-30
Called from file "cil/src/cil.ml", line 6152, characters 2-420
Called from file "cil/src/cil.ml", line 2061, characters 21-41
Called from file "cil/src/cil.ml", line 6185, characters 7-84
Called from file "src/kernel/visitor.ml", line 827, characters 2-45
Called from file "src/kernel/file.ml", line 1803, characters 2-8
Called from file "queue.ml", line 134, characters 6-20
Called from file "src/kernel/file.ml", line 1880, characters 2-36
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
Unexpected error (Stack.Empty).
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Neon-20140301+dev-STANCE.
## Attachments
- [428.cpp](/uploads/ec15e3525df0c4c9340947fc89b631c9/428.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/889use of template class in default template argument in namespace causes crash2021-02-22T13:14:16ZJochen Burghardtuse of template class in default template argument in namespace causes crashID0001970:
**This issue was created automatically from Mantis Issue 1970. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001970:
**This issue was created automatically from Mantis Issue 1970. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001970 | Frama-Clang | Plug-in > clang | public | 2014-11-17 | 2015-02-15 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
Now output intermediate result
135.cpp:6:[fclang] failure: Unknown aggregate type std::vector<...,...>
[kernel] Current source was: 135.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_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.
The problem remains if the "std::" prefix is removed in line 5.
However, the problem disappears if no namespaces are used at all, i.e. if line 2 and 7 are deleted, and the "std::" prefixes are removed in line 5 and 9.
(Importance: this code is used via #include <vector>.)
## Attachments
- [135.cpp](/uploads/ea988c45a4d3e96baf392b9da299f9f7/135.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/887use of initialized array causes crash2021-02-22T13:27:04ZJochen Burghardtuse of initialized array causes crashID0001986:
**This issue was created automatically from Mantis Issue 1986. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001986:
**This issue was created automatically from Mantis Issue 1986. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001986 | Frama-Clang | Plug-in > clang | public | 2014-11-24 | 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
149.cpp:4:[fclang] failure: Unknown local variable a
[kernel] Current source was: 149.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 "src/frama-clang/convert.ml", line 210, characters 8-39
Called from file "src/frama-clang/convert.ml", line 387, characters 33-55
Called from file "src/frama-clang/convert.ml", line 434, characters 29-52
Called from file "src/frama-clang/convert.ml", line 567, characters 29-52
Called from file "src/frama-clang/convert.ml", line 421, characters 29-52
Called from file "src/frama-clang/convert.ml", line 1082, characters 25-48
Called from file "src/frama-clang/convert.ml", line 1275, characters 20-46
Called from file "list.ml", line 74, characters 24-34
Called from file "src/frama-clang/convert.ml", line 1265, characters 17-40
Called from file "src/frama-clang/convert.ml", line 2151, characters 21-44
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 "a" isn't initialized in line 3, i.e. if "= {11,22,33}" is removed there.
## Attachments
- [149.cpp](/uploads/51ab1c38b8c7d36f3e7e7306fef9b130/149.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/885constructor overloading resolution with templates causes dubious "contract me...2021-02-22T13:27:09ZJochen Burghardtconstructor overloading resolution with templates causes dubious "contract merge" warningID0002043:
**This issue was created automatically from Mantis Issue 2043. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002043:
**This issue was created automatically from Mantis Issue 2043. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002043 | Frama-Clang | Plug-in > clang | public | 2015-01-05 | 2015-02-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 :
Running "frama-c -wp 426.cpp" produces the output:
Now output intermediate result
426.cpp:5:[kernel] warning: found two contracts. Merging them
[wp] Running WP plugin...
The warning remains if
(1) the contract in line 7 is activated, or
(2) the contract in line 11 is deactivated.
The warning disappears if
(3) lines 4-5 are deleted,
(4) line 8 is deleted, or
(5) "char" is changed to "int" in line 13.
Even if the warning is printed, the proof obligation for the constructor call in line 13 seems to be correct, viz.:
(* ---------------------------------------------------------- *)
(* --- Instance of 'Pre-condition (file 426.cpp, line 4) in '_ZN7complexIcEEC1vci'' in 'main' at call '_ZN7complexIcEEC1vci' (file 426.cpp, line 13)
--- *)
(* ---------------------------------------------------------- *)
goal main_call__ZN7complexIcEEC1vci_pre:
forall i : int.
forall t : int farray.
(i <= 6) ->
linked(t) ->
is_sint32(i) ->
(1 = i)
So it is not clear which contracts are merged. Possibly this is a revival of issue #1611. However, it could also indicate that the contract in line 4 is merged with the (empty) contract of the constructor in line 8 (since the warning disappears when line 8 is removed) - which would be wrong in general.
## Attachments
- [426.cpp](/uploads/83b16ec11a724e4803101543fe3e06de/426.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/883"ensures" clause of function template not supplied to Alt-Ergo2021-02-22T13:27:02ZJochen Burghardt"ensures" clause of function template not supplied to Alt-ErgoID0002034:
**This issue was created automatically from Mantis Issue 2034. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002034:
**This issue was created automatically from Mantis Issue 2034. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002034 | Frama-Clang | Plug-in > clang | public | 2014-12-15 | 2015-02-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 :
Running "frama-c -wp 411.cpp" generates, from the "assert" in line 12, an unprovable obligation (for Alt-Ergo), viz: "goal main_assert: forall i : int. is_sint32(i) -> (1 = i)", see line 570 of file "main_assert_Alt-Ergo.mlw".
If the function "nop" is made a non-template function (by uncommenting the typedef in line 4, and commenting-out the "template<class T>" prefix in line 7), the obligation reads "goal main_assert: forall i : int. (2 = (2 * i)) -> is_sint32(i) -> (1 = i)", and is proven without problems by Alt-Ergo.
## Attachments
- [411.cpp](/uploads/f4d3734df967c73ae7c415efd8c5d1de/411.cpp)
- [main_assert_Alt-Ergo.mlw](/uploads/13ed07ef6485c5aa5d0eafa5599fabbf/main_assert_Alt-Ergo.mlw)
- [411a.cpp](/uploads/0ffcaa8993e4cb1ec8e78eb5d2774ac2/411a.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/881method contract in template specialization class unimplemented2021-02-22T13:14:05ZJochen Burghardtmethod contract in template specialization class unimplementedID0002037:
**This issue was created automatically from Mantis Issue 2037. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002037:
**This issue was created automatically from Mantis Issue 2037. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002037 | Frama-Clang | Plug-in > clang | public | 2014-12-18 | 2015-02-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:
unimplemented next attachment
[kernel] user error: Failed to parse C++ file. See Clang messages for more information
The error remains if "<T*>" is removed from line 4, turning the template specialization into an ordinary template definition.
The error disappears if line 5 is deleted.
## Attachments
- [418.cpp](/uploads/41c07d4334cfd74c52b3a0c1d86a481c/418.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/880public variables of superclass not visible in subclass invariant2021-02-22T14:02:19ZJochen Burghardtpublic variables of superclass not visible in subclass invariantID0001959:
**This issue was created automatically from Mantis Issue 1959. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001959:
**This issue was created automatically from Mantis Issue 1959. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001959 | Frama-Clang | Plug-in > clang | public | 2014-11-10 | 2015-02-15 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **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 :
output:
Now output intermediate result
120.cpp:9:[kernel] user error: Cannot find field a
If "a ==" is deleted from line 9, the error message disappears.
Note that "a" is visible in the code in line 11.
## Attachments
- [120.cpp](/uploads/64602eaf38dd440ae1fe439ce89706fd/120.cpp)
- [127.cpp](/uploads/cd8fe9eacdedaad20a6a8966f6923c25/127.cpp)
- [120a.cpp](/uploads/00f63c1e84fb84a81269bc2d3301d26d/120a.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/876suggest to document Frama-C's handling of return value optimization2021-02-22T13:13:56ZJochen Burghardtsuggest to document Frama-C's handling of return value optimizationID0002022:
**This issue was created automatically from Mantis Issue 2022. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002022:
**This issue was created automatically from Mantis Issue 2022. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002022 | Frama-Clang | Plug-in > clang | public | 2014-12-08 | 2015-02-15 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | text | **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 192.cpp" on the attached program verifies all obligations, thus showing that Frama-C assumes that no return value optimization (RVO) is done (the copy constructor "X()" from line 13 is called once for the "return" in line 21, and a second time for the initialization in line 25; as a result, the digit "2" is appended to variable "s" twice).
I suggest that Frama-C prints a warning that it assumes that no RVO is done. The g++ compiler doesn't do this; however, Frama-C/Wp users are expected to be far more interested in semantic details than g++ users are. As an alternative, Frama-C's handling of RVO issues should eventually be explained in the manual.
## Attachments
- [192.cpp](/uploads/315524f9cdd77995005dd6b3cf7d4c6e/192.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/872different error messages for "0<x" and "0<x<9" when x is of class type2021-02-22T13:13:50ZJochen Burghardtdifferent error messages for "0<x" and "0<x<9" when x is of class typeID0002007:
**This issue was created automatically from Mantis Issue 2007. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002007:
**This issue was created automatically from Mantis Issue 2007. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002007 | Frama-Clang | Plug-in > clang | public | 2014-12-01 | 2015-02-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **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 of "frama-c -wp 185.cpp" in its current version:
185.cpp:4:24: comparison of incompatible types
Now output intermediate result
185.cpp:4:[kernel] user error: comparison of incompatible types: struct _Z1X and ℤ in annotation.
[kernel] user error: skipping file "185.cpp" that has errors.
[kernel] Frama-C aborted: invalid user input.
Output of the same command after deleting "< 9" (or, alternatively, deleting "0 <") in line 4:
185.cpp:4:20: comparison of incompatible types
185.cpp:4:20: expecting a term or predicate
185.cpp:4:20: expecting a predicate
Now output intermediate result
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[wp] warning: Missing RTE guards
[wp] 0 goal scheduled
[wp] Proved goals: 0 / 0
While both behaviors of Frama-C are ok, their difference (in particular not running / running the Wp plugin) could indicate a bug.
## Attachments
- [185.cpp](/uploads/b1c887234898b1febb2313938115a12a/185.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/868suggest to suppress warning about passing void value via return statement2021-02-22T13:26:54ZJochen Burghardtsuggest to suppress warning about passing void value via return statementID0001998:
**This issue was created automatically from Mantis Issue 1998. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001998:
**This issue was created automatically from Mantis Issue 1998. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001998 | Frama-Clang | Plug-in > clang | public | 2014-11-27 | 2015-02-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **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 for file "165.cpp":
Now output intermediate result
165.cpp:4:[kernel] warning: Return statement with a value in function returning void
According to Stroustrup, sect.7.3 "Value Return", the code is ok, and can make sense in templates with type parameters, cf. file "165a.cpp".
Running "g++ -Wall -pedantic 165.cpp" doesn't give a warning either.
## Attachments
- [165.cpp](/uploads/de64441631b47caf183ef875ea08a786/165.cpp)
- [165a.cpp](/uploads/e805233d81f78ff5dc0a6e47430d449d/165a.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/867identifier declared in condition is unknown in assert clause2021-02-22T14:01:53ZJochen Burghardtidentifier declared in condition is unknown in assert clauseID0001996:
**This issue was created automatically from Mantis Issue 1996. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001996:
**This issue was created automatically from Mantis Issue 1996. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001996 | Frama-Clang | Plug-in > clang | public | 2014-11-27 | 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:
159.cpp:4:17: unknown identifier 'i'
Now output intermediate result
If the assertion in line 4 is changed to a statement, like "i = 2;", the message disappears.
## Attachments
- [159.cpp](/uploads/70c4933a06e4a73d20c28472895a233a/159.cpp)Virgile PrevostoVirgile Prevosto