frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2021-02-22T13:07:34Zhttps://git.frama-c.com/pub/frama-c/-/issues/623Frama-C GUI crashes under OS X2021-02-22T13:07:34ZJens GerlachFrama-C GUI crashes under OS XID0002099:
**This issue was created automatically from Mantis Issue 2099. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002099:
**This issue was created automatically from Mantis Issue 2099. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002099 | Frama-C | Graphical User Interface | public | 2015-03-31 | 2015-06-29 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | - |
### Description :
If I start the Frama-C GUI on the attached program with 'frama-c-gui lemma.c',
then the GUI starts normally.
In the 'Source' panel I can see 'lemma.c.
When I try to see the lemma inside the file by clicking on the filename (or the little triangle left of it),
then the GUI crashes.
This does not happen under Linux.
### Additional Information :
frama-c was installed with opam
OS X (10.10.3 (14D127a))
opam --version: 1.2.0
frama-c -version
Version: Sodium-20150201
Compilation date: Tue Mar 31 09:48:58 CEST 2015
## Attachments
- [lemma.c](/uploads/f1e70f11f828611cc31af293e127a3c4/lemma.c)https://git.frama-c.com/pub/frama-c/-/issues/550Crash with \is_infinite2021-02-22T13:05:39Zmantis-gitlab-migrationCrash with \is_infiniteID0002082:
**This issue was created automatically from Mantis Issue 2082. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002082:
**This issue was created automatically from Mantis Issue 2082. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002082 | Frama-C | Plug-in > wp | public | 2015-02-24 | 2016-01-26 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Ian | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | Ubuntu | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | Frama-C Magnesium |
### Description :
Using the built-in \is_infinite causes wp to crash.
This is used in the provided libc specifications (math.h), and a call to these functions will cause a crash.
### Steps To Reproduce :
Create program:
#include <math.h>
/*@
ensures \true;
*/
void main() {
double val = acos(1);
}
Run frama-c, where FRAMA_C_LIBC is .../frama-c-Neon-20140301/share/libc:
frama-c -cpp-extra-args="-I${FRAMA_C_LIBC}" -wp is_infinte_test.c
Get output:
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
is_infinte_test.c:7:[kernel] warning: No code nor implicit assigns clause for function acos, generating default assigns from the specification
is_infinte_test.c:7:[kernel] warning: No code nor implicit assigns clause for function acosf, generating default assigns from the specification
is_infinte_test.c:7:[kernel] warning: No code nor implicit assigns clause for function acosh, generating default assigns from the specification
is_infinte_test.c:7:[kernel] warning: No code nor implicit assigns clause for function acoshf, generating default assigns from the specification
is_infinte_test.c:7:[kernel] warning: No code nor implicit assigns clause for function acoshl, generating default assigns from the specification
is_infinte_test.c:7:[kernel] warning: No code nor implicit assigns clause for function acosl, generating default assigns from the specification
is_infinte_test.c:7:[kernel] warning: No code nor implicit assigns clause for function asin, generating default assigns from the specification
is_infinte_test.c:7:[kernel] warning: No code nor implicit assigns clause for function asinf, generating default assigns from the specification
is_infinte_test.c:7:[kernel] warning: No code nor implicit assigns clause for function asinl, generating default assigns from the specification
[wp] warning: No definition for 'memchr' interpreted as reads nothing
[wp] warning: No definition for 'memset' interpreted as reads nothing
[wp] warning: No definition for 'strchr' interpreted as reads nothing
[wp] warning: No definition for 'strcmp' interpreted as reads nothing
[wp] warning: No definition for 'wcscmp' interpreted as reads nothing
[wp] warning: No definition for 'wcslen' interpreted as reads nothing
[wp] warning: No definition for 'wcsncmp' interpreted as reads nothing
[wp] warning: Missing RTE guards
[wp] user error: Builtin \is_infinite(float64) not defined
[wp] failure: Logic '\is_infinite' undefined
[kernel] Current source was: is_infinte_test.c:8
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/wp/LogicCompiler.ml", line 698, characters 20-51
Called from file "src/wp/LogicCompiler.ml", line 758, characters 10-23
Called from file "src/wp/LogicSemantics.ml", line 779, characters 12-37
Called from file "src/wp/Context.ml", line 31, characters 12-17
Re-raised at file "src/wp/Context.ml", line 34, characters 41-46
Called from file "src/wp/LogicCompiler.ml", line 357, characters 28-51
Called from file "src/wp/LogicSemantics.ml", line 779, characters 12-37
Called from file "src/wp/Context.ml", line 31, characters 12-17
Re-raised at file "src/wp/Context.ml", line 34, characters 41-46
Called from file "src/wp/LogicCompiler.ml", line 357, characters 28-51
Called from file "src/wp/LogicSemantics.ml", line 779, characters 12-37
Called from file "src/wp/Context.ml", line 31, characters 12-17
Re-raised at file "src/wp/Context.ml", line 34, characters 41-46
Called from file "list.ml", line 57, characters 20-23
Called from file "src/wp/Context.ml", line 68, characters 14-17
Re-raised at file "src/wp/Context.ml", line 69, characters 43-48
Called from file "src/wp/Context.ml", line 68, characters 14-17
Re-raised at file "src/wp/Context.ml", line 69, characters 43-48
Called from file "src/wp/Context.ml", line 68, characters 14-17
Re-raised at file "src/wp/Context.ml", line 69, characters 43-48
Called from file "src/wp/Context.ml", line 68, characters 14-17
Re-raised at file "src/wp/Context.ml", line 69, characters 43-48
Called from file "src/wp/cfgWP.ml", line 1069, characters 18-63
Called from file "src/wp/Warning.ml", line 155, characters 14-18
Called from file "src/wp/cfgWP.ml", line 1099, characters 23-207
Called from file "src/wp/Context.ml", line 68, characters 14-17
Re-raised at file "src/wp/Context.ml", line 69, characters 43-48
Called from file "src/wp/Context.ml", line 68, characters 14-17
Re-raised at file "src/wp/Context.ml", line 69, characters 43-48
Called from file "src/wp/Context.ml", line 68, characters 14-17
Re-raised at file "src/wp/Context.ml", line 69, characters 43-48
Called from file "src/wp/Context.ml", line 68, characters 14-17
Re-raised at file "src/wp/Context.ml", line 69, characters 43-48
Called from file "src/wp/calculus.ml", line 448, characters 14-224
Called from file "src/wp/calculus.ml", line 595, characters 10-57
Called from file "src/wp/calculus.ml", line 536, characters 19-40
Called from file "src/wp/calculus.ml", line 579, characters 20-43
Called from file "src/wp/calculus.ml", line 536, characters 19-40
Called from file "src/wp/calculus.ml", line 574, characters 20-43
Called from file "src/wp/calculus.ml", line 536, characters 19-40
Called from file "src/wp/calculus.ml", line 699, characters 40-59
Called from file "set.ml", line 288, characters 38-41
Called from file "map.ml", line 169, characters 20-25
Called from file "map.ml", line 169, characters 10-18
Called from file "map.ml", line 169, characters 10-18
Called from file "src/wp/calculus.ml", line 699, characters 4-64
Called from file "src/wp/calculus.ml", line 745, characters 19-51
Called from file "src/wp/cfgWP.ml", line 1382, characters 39-62
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/wp/cfgWP.ml", line 1371, characters 14-837
Called from file "src/wp/Model.ml", line 111, characters 17-20
Re-raised at file "src/wp/Model.ml", line 116, characters 25-28
Called from file "src/wp/Model.ml", line 117, characters 19-36
Called from file "src/wp/register.ml", line 435, characters 17-42
Called from file "src/wp/register.ml", line 574, characters 17-24
Re-raised at file "src/wp/register.ml", line 578, characters 29-31
Called from file "src/wp/register.ml", line 575, characters 17-24
Re-raised at file "src/wp/register.ml", line 579, characters 32-34
Called from file "src/wp/register.ml", line 575, characters 17-24
Re-raised at file "src/wp/register.ml", line 579, characters 32-34
Called from file "queue.ml", line 134, characters 6-20
Called from file "src/kernel/boot.ml", line 37, characters 4-20
Called from file "src/kernel/cmdline.ml", line 735, characters 2-9
Called from file "src/kernel/cmdline.ml", line 214, characters 4-8
Plug-in wp aborted: internal error.
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Neon-20140301.
Note that a version and a backtrace alone often do not contain enough
information to understand the bug. Guidelines for reporting bugs are at:
http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelineshttps://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/657logic function with typedef'd result type causes crash2021-02-22T13:08:16ZJochen Burghardtlogic function with typedef'd result type causes crashID0002056:
**This issue was created automatically from Mantis Issue 2056. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002056:
**This issue was created automatically from Mantis Issue 2056. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002056 | Frama-Clang | Plug-in > clang | public | 2015-01-22 | 2015-04-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | Neon-20140301+dev-STANCE-Jan2015 | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing 437.cpp (external front-end)
Now output intermediate result
437.cpp:6:[fclang] failure: predicate definition with a term as body
[kernel] Current source was: 437.cpp:6
The full backtrace is:
Raised at file "src/kernel/log.ml", line 524, characters 30-31
Called from file "src/kernel/log.ml", line 518, characters 9-16
Re-raised at file "src/kernel/log.ml", line 521, characters 15-16
Called from file "src/frama-clang/convert_acsl.ml", line 622, characters 12-76
Called from file "src/frama-clang/convert.ml", line 2233, characters 18-54
Called from file "list.ml", line 74, characters 24-34
Called from file "src/frama-clang/convert.ml", line 2241, characters 19-78
Called from file "src/frama-clang/convert.ml", line 2554, characters 21-48
Called from file "list.ml", line 74, characters 24-34
Called from file "src/frama-clang/convert.ml", line 2558, characters 4-79
Called from file "src/frama-clang/frama_Clang_register.ml", line 86, characters 13-36
Called from file "src/kernel/file.ml", line 1248, characters 8-41
Called from file "src/kernel/file.ml", line 1296, characters 23-30
Called from file "list.ml", line 74, characters 24-34
Called from file "src/kernel/file.ml", line 1293, characters 6-864
Called from file "src/kernel/file.ml", line 2287, characters 12-30
Called from file "src/kernel/file.ml", line 2372, characters 4-27
Called from file "src/kernel/ast.ml", line 111, characters 2-28
Called from file "src/kernel/ast.ml", line 123, characters 53-71
Called from file "src/kernel/boot.ml", line 29, characters 6-20
Called from file "src/kernel/cmdline.ml", line 761, characters 2-9
Called from file "src/kernel/cmdline.ml", line 216, characters 4-8
Plug-in fclang aborted: internal error.
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Neon-20140301+dev-STANCE.
The problem disappears if the return type is changed to "int" in line 6.
Line 7 just demonstrates that the same expression is accepted in C++ code.
## Attachments
- [437.cpp](/uploads/b80e0c84f1ccd4254f37a850575ad463/437.cpp)https://git.frama-c.com/pub/frama-c/-/issues/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/919WP-Plugin crashes due to an internal error when terms of sets during union ha...2021-04-15T13:59:49Zmantis-gitlab-migrationWP-Plugin crashes due to an internal error when terms of sets during union have different typesID0002039:
**This issue was created automatically from Mantis Issue 2039. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002039:
**This issue was created automatically from Mantis Issue 2039. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002039 | Frama-C | Plug-in > wp | public | 2014-12-22 | 2014-12-22 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | gaggarwal | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | - |
### Description :
In case type of terms of tset1 and tset2 is different, then assigns \union(tset1, tset2) causes WP to crash.
In the example in attached file, first set has terms of type int, and other set set has terms of type double. union is throwing following error:
failure: c-object of logic type (ℝ)
### Steps To Reproduce :
When attached file is called with the following command-line:
frama-c -wp-fct copy -wp-print -wp-out temp -continue-annot-error array_assigns.c
Frama-C produces below output:
[kernel] preprocessing with "gcc -C -E -I. EditorTest/src/FVal_Infer/array_assigns.c"
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[wp] warning: Missing RTE guards
EditorTest/src/FVal_Infer/array_assigns.c:9:[wp] failure: c-object of logic type (ℝ)
[kernel] Current source was: EditorTest/src/FVal_Infer/array_assigns.c:9
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/wp/LogicSemantics.ml", line 802, characters 2-35
Called from file "list.ml", line 55, characters 20-23
Called from file "src/wp/LogicSemantics.ml", line 808, characters 27-51
Called from file "src/wp/cfgWP.ml", line 412, characters 6-147
Called from file "src/wp/Warning.ml", line 155, characters 14-18
Called from file "src/wp/cfgWP.ml", line 468, characters 22-126
Called from file "src/wp/Context.ml", line 68, characters 14-17
Re-raised at file "src/wp/Context.ml", line 69, characters 43-48
Called from file "src/wp/Context.ml", line 68, characters 14-17
Re-raised at file "src/wp/Context.ml", line 69, characters 43-48
Called from file "src/wp/Context.ml", line 68, characters 14-17
Re-raised at file "src/wp/Context.ml", line 69, characters 43-48
Called from file "src/wp/Context.ml", line 68, characters 14-17
Re-raised at file "src/wp/Context.ml", line 69, characters 43-48
Called from file "src/wp/calculus.ml", line 334, characters 27-62
Called from file "src/wp/calculus.ml", line 341, characters 23-45
Called from file "src/wp/calculus.ml", line 613, characters 20-43
Called from file "src/wp/calculus.ml", line 536, characters 19-40
Called from file "src/wp/calculus.ml", line 586, characters 20-43
Called from file "src/wp/calculus.ml", line 536, characters 19-40
Called from file "src/wp/calculus.ml", line 589, characters 20-43
Called from file "src/wp/calculus.ml", line 536, characters 19-40
Called from file "src/wp/calculus.ml", line 589, characters 20-43
Called from file "src/wp/calculus.ml", line 536, characters 19-40
Called from file "src/wp/calculus.ml", line 583, characters 20-43
Called from file "src/wp/calculus.ml", line 536, characters 19-40
Called from file "src/wp/calculus.ml", line 599, characters 22-40
Called from file "src/wp/calculus.ml", line 536, characters 19-40
Called from file "src/wp/calculus.ml", line 583, characters 20-43
Called from file "src/wp/calculus.ml", line 536, characters 19-40
Called from file "src/wp/calculus.ml", line 396, characters 20-39
Called from file "src/wp/calculus.ml", line 610, characters 10-43
Called from file "src/wp/calculus.ml", line 536, characters 19-40
Called from file "src/wp/calculus.ml", line 589, characters 20-43
Called from file "src/wp/calculus.ml", line 536, characters 19-40
Called from file "src/wp/calculus.ml", line 579, characters 20-43
Called from file "src/wp/calculus.ml", line 536, characters 19-40
Called from file "src/wp/calculus.ml", line 574, characters 20-43
Called from file "src/wp/calculus.ml", line 536, characters 19-40
Called from file "src/wp/calculus.ml", line 699, characters 40-59
Called from file "set.ml", line 304, characters 38-41
Called from file "map.ml", line 168, characters 20-25
Called from file "map.ml", line 168, characters 10-18
Called from file "map.ml", line 168, characters 10-18
Called from file "map.ml", line 168, characters 10-18
Called from file "src/wp/calculus.ml", line 699, characters 4-64
Called from file "src/wp/calculus.ml", line 745, characters 19-51
Called from file "src/wp/cfgWP.ml", line 1382, characters 39-62
Called from file "src/wp/cfgWP.ml", line 1371, characters 14-837
Called from file "src/wp/Model.ml", line 111, characters 17-20
Re-raised at file "src/wp/Model.ml", line 116, characters 25-28
Called from file "src/wp/Model.ml", line 117, characters 19-36
Called from file "src/wp/register.ml", line 435, characters 17-42
Called from file "src/wp/register.ml", line 574, characters 17-24
Re-raised at file "src/wp/register.ml", line 578, characters 29-31
Called from file "src/wp/register.ml", line 575, characters 17-24
Re-raised at file "src/wp/register.ml", line 579, characters 32-34
Called from file "src/wp/register.ml", line 575, characters 17-24
Re-raised at file "src/wp/register.ml", line 579, characters 32-34
Called from file "queue.ml", line 134, characters 6-20
Called from file "src/kernel/boot.ml", line 37, characters 4-20
Called from file "src/kernel/cmdline.ml", line 735, characters 2-9
Called from file "src/kernel/cmdline.ml", line 214, characters 4-8
Plug-in wp aborted: internal error.
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Neon-20140301.
Note that a version and a backtrace alone often do not contain enough
information to understand the bug. Guidelines for reporting bugs are at:
http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelines
## Attachments
- [array_assigns.c](/uploads/fc8878d9ca24ca39c8b0ac9c83b61731/array_assigns.c)Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/674method call in initializer of global constant causes segmentation fault2021-02-22T13:08:42ZJochen Burghardtmethod call in initializer of global constant causes segmentation faultID0002005:
**This issue was created automatically from Mantis Issue 2005. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002005:
**This issue was created automatically from Mantis Issue 2005. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002005 | Frama-Clang | Plug-in > clang | public | 2014-12-01 | 2015-03-26 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | fvedrine | **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
If the "const" is removed from line 8, the output changes to:
Now output intermediate result
182.cpp:8:[kernel] warning: Call to _ZN3clsE1a in constant. Ignoring this call and returning 0.
If line 8 is embedded in the body of main(), the problem disappears (with and without "const").
## Attachments
- [182.cpp](/uploads/488e6187dc8b8a423989ecada7a407e0/182.cpp)Franck VedrineFranck Vedrinehttps://git.frama-c.com/pub/frama-c/-/issues/648use of body-declared variable in loop annotation causes crash2021-02-22T14:01:53ZJochen Burghardtuse of body-declared variable in loop annotation causes crashID0001997:
**This issue was created automatically from Mantis Issue 1997. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001997:
**This issue was created automatically from Mantis Issue 1997. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001997 | Frama-Clang | Plug-in > clang | public | 2014-11-27 | 2015-04-27 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **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
161.cpp:3:[fclang] failure: Unknown local variable s
[kernel] Current source was: 161.cpp:3
The full backtrace is:
Raised at file "src/kernel/log.ml", line 524, characters 30-31
Called from file "src/kernel/log.ml", line 518, characters 9-16
Re-raised at file "src/kernel/log.ml", line 521, characters 15-16
Called from file "src/frama-clang/convert_acsl.ml", line 317, characters 18-77
Called from file "src/frama-clang/convert_acsl.ml", line 303, characters 13-52
Called from file "src/frama-clang/convert_acsl.ml", line 172, characters 38-72
Called from file "src/frama-clang/convert_acsl.ml", line 272, characters 4-30
Called from file "src/frama-clang/convert_acsl.ml", line 172, characters 38-72
Called from file "src/frama-clang/convert_acsl.ml", line 385, characters 13-38
Called from file "src/frama-clang/convert_acsl.ml", line 363, characters 11-42
Called from file "src/frama-clang/convert_acsl.ml", line 586, characters 14-40
Called from file "list.ml", line 57, characters 20-23
Called from file "src/frama-clang/convert.ml", line 1179, characters 18-70
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 remains if line 3 is changed to "//@ loop assigns s;", and if "s" is declared "static int" (in which case a reference to "s" in a loop annotation makes sense).
## Attachments
- [161.cpp](/uploads/5bfc197761d406d5ad0e3f804e293cad/161.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/640declarations of static variable of class type in function body causes crash2021-03-29T17:24:55ZJochen Burghardtdeclarations of static variable of class type in function body causes crashID0002001:
**This issue was created automatically from Mantis Issue 2001. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002001:
**This issue was created automatically from Mantis Issue 2001. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002001 | Frama-Clang | Plug-in > clang | public | 2014-11-27 | 2015-05-07 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **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
161.cpp:3:[fclang] failure: Unknown local variable s
[kernel] Current source was: 161.cpp:3
The full backtrace is:
Raised at file "src/kernel/log.ml", line 524, characters 30-31
Called from file "src/kernel/log.ml", line 518, characters 9-16
Re-raised at file "src/kernel/log.ml", line 521, characters 15-16
Called from file "src/frama-clang/convert_acsl.ml", line 317, characters 18-77
Called from file "src/frama-clang/convert_acsl.ml", line 303, characters 13-52
Called from file "src/frama-clang/convert_acsl.ml", line 172, characters 38-72
Called from file "src/frama-clang/convert_acsl.ml", line 272, characters 4-30
Called from file "src/frama-clang/convert_acsl.ml", line 172, characters 38-72
Called from file "src/frama-clang/convert_acsl.ml", line 385, characters 13-38
Called from file "src/frama-clang/convert_acsl.ml", line 363, characters 11-42
Called from file "src/frama-clang/convert_acsl.ml", line 586, characters 14-40
Called from file "list.ml", line 57, characters 20-23
Called from file "src/frama-clang/convert.ml", line 1179, characters 18-70
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
(1) the "static" is deleted in line 5, or
(2) "cls" is changed to "int" in line 5.
Could be related to #1997, since the crash messages agree. I dind't check the full call stack, however.
## Attachments
- [173.cpp](/uploads/bc77682336214d038cb4267b460d0df8/173.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/864non-predicate on right-hand size of "|" causes segmentation fault2021-03-29T16:34:53ZJochen Burghardtnon-predicate on right-hand size of "|" causes segmentation faultID0001991:
**This issue was created automatically from Mantis Issue 1991. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001991:
**This issue was created automatically from Mantis Issue 1991. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001991 | 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
Same for "&".
In contrast, "i | (i==i)" is accepted, which might not be ok either, since "i" is not a predicate, and "i | ..." isn't either.
## Attachments
- [155.cpp](/uploads/97f44d774ea3375ac8795a16896f3136/155.cpp)
- [155a.cpp](/uploads/6028e94aafd01c070d1470bd32b6a00c/155a.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/862namespace prefix in annotation causes segmentation fault2021-03-29T16:41:05ZJochen Burghardtnamespace prefix in annotation causes segmentation faultID0001985:
**This issue was created automatically from Mantis Issue 1985. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001985:
**This issue was created automatically from Mantis Issue 1985. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001985 | Frama-Clang | Plug-in > clang | public | 2014-11-24 | 2015-02-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
Segmentation fault (core dumped)
[kernel] user error: Failed to parse C++ file. See Clang messages for more information
## Attachments
- [147.cpp](/uploads/ee910fafdfbabeb2abdb356f31ad4a03/147.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/666indexing of string literal apparently causes memory leak in framaCIRGen2021-02-22T13:40:05ZJochen Burghardtindexing of string literal apparently causes memory leak in framaCIRGenID0001988:
**This issue was created automatically from Mantis Issue 1988. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001988:
**This issue was created automatically from Mantis Issue 1988. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001988 | Frama-Clang | Plug-in > clang | public | 2014-11-24 | 2015-04-02 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **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 :
When running "frama-c 151.cpp" on the attached program, about 1 minute of silence is observed on the terminal output, followed by:
Killed
[kernel] user error: Failed to parse C++ file. See Clang messages for more information
Running "top -d 1" produces the figures shown in file "151.typescript": framaCIRGen acquires about 90MB memory each second until it has 1.8GB after 18 seconds; then the memory remains constant for another 18 seconds; then the process appears to be killed by the Linux kernel due to memory exhaustion.
## Attachments
- [151.cpp](/uploads/22b5baf2a7db1b3084d4da78b008cbaf/151.cpp)
- [151.typescript](/uploads/b4a76f523493de4fe8ab69804480ce6b/151.typescript)
- [156.cpp](/uploads/fb17a0983991ed74ce7fe3d23ce44028/156.cpp)
- [156.typescript](/uploads/1dc0c1b0d4a1e83a9be18b27027d3979/156.typescript)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/890use of template class from namespace causes crash2021-02-22T13:14:18ZJochen Burghardtuse of template class from namespace causes crashID0001971:
**This issue was created automatically from Mantis Issue 1971. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001971:
**This issue was created automatically from Mantis Issue 1971. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001971 | Frama-Clang | Plug-in > clang | public | 2014-11-17 | 2015-02-15 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
The file attached to issue #1970 can be simplified somewhat further while still causing the same crash message (however with a possibly different call stack - I didn't check that):
Now output intermediate result
135a.cpp:3:[fclang] failure: Unknown aggregate type std::vector<...>
[kernel] Current source was: 135a.cpp:3
The full backtrace is:
Raised at file "src/kernel/log.ml", line 524, characters 30-31
Called from file "src/kernel/log.ml", line 518, characters 9-16
Re-raised at file "src/kernel/log.ml", line 521, characters 15-16
Called from file "src/frama-clang/convert_env.ml", line 269, characters 43-71
Called from file "src/frama-clang/convert.ml", line 162, characters 17-69
Called from file "src/frama-clang/convert.ml", line 170, characters 17-52
Called from file "list.ml", line 57, characters 20-23
Called from file "src/frama-clang/convert.ml", line 1283, characters 13-45
Called from file "src/frama-clang/convert.ml", line 1910, characters 8-66
Called from file "list.ml", line 74, characters 24-34
Called from file "src/frama-clang/convert.ml", line 1998, characters 19-78
Called from file "src/frama-clang/convert.ml", line 2262, characters 21-48
Called from file "list.ml", line 74, characters 24-34
Called from file "src/frama-clang/convert.ml", line 2266, characters 4-79
Called from file "src/frama-clang/frama_Clang_register.ml", line 86, characters 13-36
Called from file "src/kernel/file.ml", line 1073, characters 10-43
Called from file "src/kernel/file.ml", line 1117, characters 23-30
Called from file "list.ml", line 74, characters 24-34
Called from file "src/kernel/file.ml", line 1114, characters 6-520
Called from file "src/kernel/file.ml", line 2179, characters 12-30
Called from file "src/kernel/file.ml", line 2264, characters 4-27
Called from file "src/kernel/ast.ml", line 111, characters 2-28
Called from file "src/kernel/ast.ml", line 123, characters 53-71
Called from file "src/kernel/boot.ml", line 29, characters 6-20
Called from file "src/kernel/cmdline.ml", line 761, characters 2-9
Called from file "src/kernel/cmdline.ml", line 216, characters 4-8
Plug-in fclang aborted: internal error.
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Neon-20140301+dev-stance.
Again, the problem disappears if the namespace environment is omitted (i.e. line 2,4 deleted, prefix "std::" deleted in line 6).
It also disappears if "vector" is made an unparametrized class, i.e. if "template<typename _Tp>" is deleted in line 3 and "<int>" is deleted in line 6.
## Attachments
- [135a.cpp](/uploads/6e2f98ce835744c14a137ab678a4f14a/135a.cpp)https://git.frama-c.com/pub/frama-c/-/issues/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/888definition of virtual function in subclass causes crash2021-02-22T13:41:45ZJochen Burghardtdefinition of virtual function in subclass causes crashID0001973:
**This issue was created automatically from Mantis Issue 1973. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001973:
**This issue was created automatically from Mantis Issue 1973. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001973 | Frama-Clang | Plug-in > clang | public | 2014-11-17 | 2015-02-15 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
Now output intermediate result
137.cpp:5:[fclang] failure: No usable assign operator for ::Rectangle
[kernel] Current source was: 137.cpp:5
The full backtrace is:
Raised at file "src/kernel/log.ml", line 524, characters 30-31
Called from file "src/kernel/log.ml", line 518, characters 9-16
Re-raised at file "src/kernel/log.ml", line 521, characters 15-16
Called from file "src/frama-clang/convert.ml", line 1660, characters 30-71
Called from file "src/frama-clang/convert.ml", line 1683, characters 15-39
Called from file "list.ml", line 74, characters 24-34
Called from file "src/frama-clang/convert.ml", line 1686, characters 14-50
Called from file "src/frama-clang/convert.ml", line 1921, characters 21-142
Called from file "list.ml", line 74, characters 24-34
Called from file "src/frama-clang/convert.ml", line 1998, characters 19-78
Called from file "src/frama-clang/convert.ml", line 2262, characters 21-48
Called from file "list.ml", line 74, characters 24-34
Called from file "src/frama-clang/convert.ml", line 2266, characters 4-79
Called from file "src/frama-clang/frama_Clang_register.ml", line 86, characters 13-36
Called from file "src/kernel/file.ml", line 1073, characters 10-43
Called from file "src/kernel/file.ml", line 1117, characters 23-30
Called from file "list.ml", line 74, characters 24-34
Called from file "src/kernel/file.ml", line 1114, characters 6-520
Called from file "src/kernel/file.ml", line 2179, characters 12-30
Called from file "src/kernel/file.ml", line 2264, characters 4-27
Called from file "src/kernel/ast.ml", line 111, characters 2-28
Called from file "src/kernel/ast.ml", line 123, characters 53-71
Called from file "src/kernel/boot.ml", line 29, characters 6-20
Called from file "src/kernel/cmdline.ml", line 761, characters 2-9
Called from file "src/kernel/cmdline.ml", line 216, characters 4-8
Plug-in fclang aborted: internal error.
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Neon-20140301+dev-stance.
The problem disappears if
(1) the "virtual" is removed in line 6, or
(2) a copy of line 6 is inserted after line 2;
the problem remains if
(3) "area" is declared in class "Rectangle", too, but not as "virtual".
## Attachments
- [137.cpp](/uploads/b9c024091e5c2197c3677797a25f89a0/137.cpp)https://git.frama-c.com/pub/frama-c/-/issues/940"catch(...)" causes crash2021-02-22T13:15:30ZJochen Burghardt"catch(...)" causes crashID0001966:
**This issue was created automatically from Mantis Issue 1966. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001966:
**This issue was created automatically from Mantis Issue 1966. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001966 | Frama-Clang | Plug-in > clang | public | 2014-11-13 | 2014-12-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C GIT, precise the release id |
### Description :
output:
Now output intermediate result
[kernel] Current source was: 133.cpp:3
The full backtrace is:
Raised at file "stack.ml", line 31, characters 20-25
Called from file "src/kernel/exn_flow.ml", line 120, characters 37-60
Called from file "list.ml", line 69, characters 12-15
Called from file "src/kernel/exn_flow.ml", line 112, characters 8-389
Called from file "src/kernel/visitor.ml", line 75, characters 14-33
Called from file "cil/src/cil.ml", line 2045, characters 15-31
Called from file "cil/src/cil.ml", line 3094, characters 5-86
Called from file "cil/src/cil.ml", line 2084, characters 13-16
Called from file "cil/src/cil.ml", line 3254, characters 16-40
Called from file "cil/src/cil.ml", line 2060, characters 21-41
Called from file "cil/src/cil.ml", line 3483, characters 14-39
Called from file "cil/src/cil.ml", line 2060, characters 21-41
Called from file "cil/src/cil.ml", line 3445, characters 5-91
Called from file "cil/src/cil.ml", line 3537, characters 16-38
Called from file "cil/src/cil.ml", line 2084, characters 13-16
Called from file "cil/src/cil.ml", line 2129, characters 24-57
Called from file "cil/src/cil.ml", line 3531, characters 5-53
Called from file "cil/src/cil.ml", line 6156, characters 16-36
Called from file "list.ml", line 69, characters 12-15
Called from file "cil/src/cil.ml", line 5746, characters 3-30
Called from file "cil/src/cil.ml", line 6157, characters 2-420
Called from file "cil/src/cil.ml", line 2060, characters 21-41
Called from file "cil/src/cil.ml", line 6190, characters 7-84
Called from file "src/kernel/visitor.ml", line 827, characters 2-45
Called from file "src/kernel/file.ml", line 1617, characters 2-8
Called from file "queue.ml", line 134, characters 6-20
Called from file "src/kernel/file.ml", line 1694, characters 2-36
Called from file "src/kernel/file.ml", line 2264, characters 4-27
Called from file "src/kernel/ast.ml", line 111, characters 2-28
Called from file "src/kernel/ast.ml", line 123, characters 53-71
Called from file "src/kernel/boot.ml", line 29, characters 6-20
Called from file "src/kernel/cmdline.ml", line 761, characters 2-9
Called from file "src/kernel/cmdline.ml", line 216, characters 4-8
Unexpected error (Stack.Empty).
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Neon-20140301+dev-stance.
Could be related to issue #1957?
(Importance: this code is used via #include <vector>.)
## Attachments
- [133.cpp](/uploads/ec10c3fb4d765ca86e6de649c4277911/133.cpp)https://git.frama-c.com/pub/frama-c/-/issues/891struct type inside 'extern "C"' causes crash, except as lhs of typedef2021-03-29T16:16:35ZJochen Burghardtstruct type inside 'extern "C"' causes crash, except as lhs of typedefID0001965:
**This issue was created automatically from Mantis Issue 1965. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001965:
**This issue was created automatically from Mantis Issue 1965. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001965 | Frama-Clang | Plug-in > clang | public | 2014-11-13 | 2015-02-15 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
Now output intermediate result
132.cpp:4:[fclang] failure: Unknown declaration in extern C structure definition
[kernel] Current source was: 132.cpp:4
The full backtrace is:
Raised at file "src/kernel/log.ml", line 524, characters 30-31
Called from file "src/kernel/log.ml", line 518, characters 9-16
Re-raised at file "src/kernel/log.ml", line 521, characters 15-16
Called from file "list.ml", line 74, characters 24-34
Called from file "src/frama-clang/convert.ml", line 2032, characters 10-61
Called from file "src/frama-clang/convert.ml", line 2262, characters 21-48
Called from file "list.ml", line 74, characters 24-34
Called from file "src/frama-clang/convert.ml", line 2266, characters 4-79
Called from file "src/frama-clang/frama_Clang_register.ml", line 86, characters 13-36
Called from file "src/kernel/file.ml", line 1073, characters 10-43
Called from file "src/kernel/file.ml", line 1117, characters 23-30
Called from file "list.ml", line 74, characters 24-34
Called from file "src/kernel/file.ml", line 1114, characters 6-520
Called from file "src/kernel/file.ml", line 2179, characters 12-30
Called from file "src/kernel/file.ml", line 2264, characters 4-27
Called from file "src/kernel/ast.ml", line 111, characters 2-28
Called from file "src/kernel/ast.ml", line 123, characters 53-71
Called from file "src/kernel/boot.ml", line 29, characters 6-20
Called from file "src/kernel/cmdline.ml", line 761, characters 2-9
Called from file "src/kernel/cmdline.ml", line 216, characters 4-8
Plug-in fclang aborted: internal error.
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Neon-20140301+dev-stance.
When activated, each of the lines 5 and 6 causes a similar crash. This problem prohibits use of <stdio.h>.
## Attachments
- [132.cpp](/uploads/c8d869273866f020befb12a0e330ae22/132.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/886throw/catch of struct causes crash2021-03-29T16:21:09ZJochen Burghardtthrow/catch of struct causes crashID0001957:
**This issue was created automatically from Mantis Issue 1957. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001957:
**This issue was created automatically from Mantis Issue 1957. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001957 | Frama-Clang | Plug-in > clang | public | 2014-11-10 | 2015-02-15 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
Now output intermediate result
[kernel] Current source was: 117.cpp:12
The full backtrace is:
Raised at file "hashtbl.ml", line 229, characters 23-32
Called from file "src/kernel/exn_flow.ml", line 492, characters 23-63
Called from file "src/kernel/exn_flow.ml", line 509, characters 55-77
Called from file "list.ml", line 57, characters 20-23
Called from file "src/kernel/exn_flow.ml", line 624, characters 20-60
Called from file "src/kernel/visitor.ml", line 75, characters 14-33
Called from file "cil/src/cil.ml", line 2045, characters 15-31
Called from file "cil/src/cil.ml", line 3094, characters 5-86
Called from file "cil/src/cil.ml", line 2084, characters 13-16
Called from file "cil/src/cil.ml", line 3254, characters 16-40
Called from file "cil/src/cil.ml", line 2060, characters 21-41
Called from file "cil/src/cil.ml", line 3483, characters 14-39
Called from file "cil/src/cil.ml", line 2060, characters 21-41
Called from file "cil/src/cil.ml", line 3445, characters 5-91
Called from file "cil/src/cil.ml", line 3537, characters 16-38
Called from file "cil/src/cil.ml", line 2084, characters 13-16
Called from file "cil/src/cil.ml", line 2129, characters 24-57
Called from file "cil/src/cil.ml", line 3531, characters 5-53
Called from file "cil/src/cil.ml", line 6193, characters 17-37
Called from file "cil/src/cil.ml", line 6200, characters 3-20
Called from file "cil/src/cil.ml", line 2060, characters 21-41
Called from file "cil/src/cil.ml", line 6217, characters 15-39
Called from file "src/kernel/exn_flow.ml", line 687, characters 4-62
Called from file "src/kernel/file.ml", line 1617, characters 2-8
Called from file "queue.ml", line 134, characters 6-20
Called from file "src/kernel/file.ml", line 1694, characters 2-36
Called from file "src/kernel/file.ml", line 2264, characters 4-27
Called from file "src/kernel/ast.ml", line 111, characters 2-28
Called from file "src/kernel/ast.ml", line 123, characters 53-71
Called from file "src/kernel/boot.ml", line 29, characters 6-20
Called from file "src/kernel/cmdline.ml", line 761, characters 2-9
Called from file "src/kernel/cmdline.ml", line 216, characters 4-8
Unexpected error (Not_found).
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Neon-20140301+dev-stance.
The active code is probably minimal causing the crash; the problem remains if any of the commented-out lines is activated.
## Attachments
- [117.cpp](/uploads/033f024cfa988a542749b29f197f174f/117.cpp)Virgile PrevostoVirgile Prevosto