frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2021-02-22T12:58:03Zhttps://git.frama-c.com/pub/frama-c/-/issues/273"assigns" in statement contract causes abort or crash2021-02-22T12:58:03ZJochen Burghardt"assigns" in statement contract causes abort or crashID0002361:
**This issue was created automatically from Mantis Issue 2361. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002361:
**This issue was created automatically from Mantis Issue 2361. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002361 | Frama-C | Plug-in > clang | public | 2018-02-12 | 2018-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | Sulfur-20171101 | **OS** | - | **OS Version** | Ubuntu 17.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c remove_cpp.cpp" on the attached program outputs
"framaCIRGen: ACSLStatementAnnotation.cpp:248: Parser::Base::ReadResult Acsl::StatementAnnotation::readToken(Acsl::Parser::State&, Acsl::Parser::Arguments&): Assertion `false' failed."
and then aborts. If the "ensures" clause in line 5 is removed, Frama-C outputs instead:
"*** Error in `framaCIRGen': double free or corruption (out): 0x0000559f983d0160 ***"
and then aborts, too. If in addition "a[0..9]" is removed from the "assigns" claus in line 4, Frama-C crashes (Segmentation fault) without printing any error message before. For the latter reason, I've set the severity to "crash".
## Attachments
- [remove_cpp.cpp](/uploads/2af0af96279845d9332c5293876e6c3e/remove_cpp.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/179Can't use e-acsl on a dynamic library containing all the instrumentations2023-03-22T03:49:51Zmantis-gitlab-migrationCan't use e-acsl on a dynamic library containing all the instrumentationsID0002422:
**This issue was created automatically from Mantis Issue 2422. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002422:
**This issue was created automatically from Mantis Issue 2422. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002422 | Frama-C | Plug-in > E-ACSL | public | 2019-01-22 | 2019-01-23 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | rmalak | **Assigned To** | signoles | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | x86_64 | **OS** | Linux 4.19 Ocaml 4.07.0 | **OS Version** | Debian Sid |
| **Product Version** | Frama-C 18-Argon | **Target Version** | Frama-C 19-Potassium | **Fixed in Version** | - |
### Description :
Hi !
main.c contains the entry point : the main function and is not instrumented by frama-c
it calls instrumented func.c (e-acsl.func.c containing the __e_acsl_memory_init call) compiled as a dynamic library libe-acsl.func.so
then the e-acsl code segfault at
e_acsl_segment_tracking.h:815
### Additional Information :
Why the hell am I doing this ? :)
Contiki-NG is an IoT OS. It can be build as a firmware for several IoT devices, as a ELF for Linux x86/x86_64, and as a shared library loaded by the Java Cooja network simulator (with some JNI).
Before experimenting with dlopen in C and JNI in Java, which is going to fail because of the __executable_start symbol at ./share/frama-c/e-acsl/segment_model/e_acsl_shadow_layout.h:47
(this will the subject of another future post)
I would like to be able, as a first step, to use a e-acsl instrumented dynamic library used by a non-instrumented program (containing main or not).
I am open to a solution that eventually needs some change inside the C E-ACSL code.
### Steps To Reproduce :
$ make
rm -vf *.*o ./loader ./main *e-acsl*
frama-c -main func -variadic-no-translation -machdep gcc_x86_64 -c11 -cpp-extra-args="-std=c99 -D_DEFAULT_SOURCE -D__NO_CTYPE -D__FC_MACHDEP_X86_64" -no-frama-c-stdlib func.c -e-acsl-prepare -rte -warn-signed-overflow -warn-unsigned-overflow -warn-signed-downcast -warn-unsigned-downcast -rte-div -rte-float-to-int -rte-mem -rte-pointer-call -rte-shift -rte-no-trivial-annotations -then -e-acsl -e-acsl-full-mmodel -then-last -print -ocode e-acsl.func.c
[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl_gmp_api.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing)
[kernel] Parsing func.c (with preprocessing)
[rte] annotating function __bswap_16
[rte] annotating function __bswap_32
[rte] annotating function __bswap_64
[rte] annotating function __uint16_identity
[rte] annotating function __uint32_identity
[rte] annotating function __uint64_identity
[rte] annotating function func
[e-acsl] beginning translation.
[kernel:annot:missing-spec] :0: Warning:
Neither code nor specification for function __builtin_bswap16, generating default assigns from the prototype
[kernel:annot:missing-spec] :0: Warning:
Neither code nor specification for function __builtin_bswap32, generating default assigns from the prototype
[kernel:annot:missing-spec] :0: Warning:
Neither code nor specification for function __builtin_bswap64, generating default assigns from the prototype
[kernel:annot:missing-spec] /usr/include/stdio.h:332: Warning:
Neither code nor specification for function printf, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl".
gcc -shared -fPIC -DE_ACSL_SEGMENT_MMODEL -DE_ACSL_STACK_SIZE=32 -DE_ACSL_HEAP_SIZE=128 -std=c99 -m64 -O0 -g -fno-builtin -fno-merge-constants -Wall -Wno-long-long -Wno-attributes -Wno-nonnull -Wno-undef -Wno-unused -Wno-unused-function -Wno-unused-result -Wno-unused-value -Wno-unused-function -Wno-unused-variable -Wno-unused-but-set-variable -Wno-implicit-function-declaration -Wno-empty-body -I/home/jean/local-frama-c/share/frama-c/e-acsl/ -o libe-acsl.func.so e-acsl.func.c /home/jean/local-frama-c/share/frama-c/e-acsl/e_acsl_rtl.c /home/jean/local-frama-c/share/frama-c/../../lib/libeacsl-dlmalloc.a /home/jean/local-frama-c/share/frama-c/../../lib/libeacsl-gmp.a -lm
gcc -o main main.c -L. -le-acsl.func
LD_LIBRARY_PATH=:./ ./main
Segmentation fault
make: *** [Makefile:11: e-acsl-main-shared] Error 139
## Attachments
- [e-acsl-is-fun.tar](/uploads/c1c5ac773627666455f1b0a93e66da53/e-acsl-is-fun.tar)Julien SignolesJulien Signoleshttps://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/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/286direct initialisation of bool by nullptr2021-02-22T13:36:06ZJens Gerlachdirect initialisation of bool by nullptrID0002347:
**This issue was created automatically from Mantis Issue 2347. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002347:
**This issue was created automatically from Mantis Issue 2347. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002347 | Frama-C | Plug-in > clang | public | 2018-01-22 | 2018-01-23 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | - |
### Description :
The attached program "nullptr_crash.cpp" compiles without warnings with g++-7.2 in C++11 mode.
Clang-5.0 issues a warning (and if I understood the standard correctly, it shouldn't, because the example uses "direct initialisation").
Frama-Clang crashes on the example.
The second example "nullptr_bool.cpp" which uses "copy initialisation" only warns about implicit conversion...
## Attachments
- [nullptr_crash.cpp](/uploads/7975ccda4df20b073580f91557d4e559/nullptr_crash.cpp)
- [nullptr_bool.cpp](/uploads/cecfd360ef834b1bcbf7a7a9606df04f/nullptr_bool.cpp)
- [nullptr_no_crash.cpp](/uploads/7bfd118ea401a367676355d8352849c2/nullptr_no_crash.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/281Frama-Clang crashes on error in contract2021-02-22T13:36:01ZJens GerlachFrama-Clang crashes on error in contractID0002352:
**This issue was created automatically from Mantis Issue 2352. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002352:
**This issue was created automatically from Mantis Issue 2352. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002352 | Frama-C | Plug-in > clang | public | 2018-01-31 | 2018-01-31 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 16-Sulfur | **Target Version** | - | **Fixed in Version** | - |
### Description :
The attached example uses mistakenly the assignment operator = instead of == in the ensures clause.
Frama-Clang crashes on this example.
frama-c -wp -wp-rte assignment_in_contract.cpp
[kernel] Parsing assignment_in_contract.cpp (external front-end)
framaCIRGen: ACSLTermOrPredicate.cpp:7096: Parser::Base::ReadResult Acsl::TermOrPredicate::readToken(Acsl::Parser::State&, Acsl::Parser::Arguments&): Assertion `false' failed.
Aborted (core dumped)
[kernel] user error: Failed to parse C++ file. See Clang messages for more information
[kernel] user error: stopping on file "assignment_in_contract.cpp" that has errors.
[kernel] Frama-C aborted: invalid user input.
A message along the lines of normal Frama-C
"user error: Assignment operators not allowed in annotations."
would be more helpful.
## Attachments
- [assignment_in_contract.cpp](/uploads/f0d2dd6918d688ca68e2c4996617c929/assignment_in_contract.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/274"Here" as predicate label in statement contract causes Segmentation fault2021-02-22T12:58:03ZJochen Burghardt"Here" as predicate label in statement contract causes Segmentation faultID0002360:
**This issue was created automatically from Mantis Issue 2360. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002360:
**This issue was created automatically from Mantis Issue 2360. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002360 | Frama-C | Plug-in > clang | public | 2018-02-12 | 2018-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | Sulfur-20171101 | **OS** | - | **OS Version** | Ubuntu 17.10 |
| **Product Version** | Frama-C 16-Sulfur | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp rotate_cpp.cpp" on the attached program outputs an error message "rotate_cpp.cpp:5:23: expecting a label argument", and then crashes due to a Segmentation fault. The problem disappears when the statement contract in line 5 is changed into an assertion.
## Attachments
- [rotate_cpp.cpp](/uploads/56cddcc4aad61f74882ab6f0a55106cf/rotate_cpp.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/646loop invariant referring to body-local variable causes crash, when body is en...2021-03-29T17:09:18ZJochen Burghardtloop invariant referring to body-local variable causes crash, when body is enclosed in curly braces "{...}"ID0002107:
**This issue was created automatically from Mantis Issue 2107. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002107:
**This issue was created automatically from Mantis Issue 2107. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002107 | Frama-Clang | Plug-in > clang | public | 2015-04-27 | 2015-04-27 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | Sodium-20150201 | **OS** | - | **OS Version** | xubuntu14.04 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing 470.cpp (external front-end)
Now output intermediate result
470.cpp:3:[fclang] failure: Unknown local variable s
[kernel] Current source was: 470.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 "convert_acsl.ml", line 329, characters 18-77
Called from file "convert_acsl.ml", line 315, characters 13-52
Called from file "convert_acsl.ml", line 184, characters 38-72
Called from file "convert_acsl.ml", line 284, characters 4-30
Called from file "convert_acsl.ml", line 184, characters 38-72
Called from file "convert_acsl.ml", line 397, characters 13-38
Called from file "convert_acsl.ml", line 375, characters 11-42
Called from file "convert_acsl.ml", line 603, characters 14-40
Called from file "list.ml", line 55, characters 20-23
Called from file "convert.ml", line 1248, characters 18-70
Called from file "convert.ml", line 1344, characters 20-46
Called from file "list.ml", line 84, characters 24-34
Called from file "convert.ml", line 1334, characters 17-40
Called from file "convert.ml", line 2508, characters 21-44
Called from file "convert.ml", line 2642, characters 21-41
Called from file "list.ml", line 84, characters 24-34
Called from file "convert.ml", line 2645, characters 4-74
Called from file "frama_Clang_register.ml", line 120, characters 13-36
Called from file "src/kernel/file.ml", line 1248, characters 8-41
Called from file "src/kernel/file.ml", line 1296, characters 23-30
Called from file "list.ml", line 84, characters 24-34
Called from file "src/kernel/file.ml", line 1293, characters 6-864
Called from file "src/kernel/file.ml", line 2287, characters 12-30
Called from file "src/kernel/file.ml", line 2372, characters 4-27
Called from file "src/kernel/ast.ml", line 111, characters 2-28
Called from file "src/kernel/ast.ml", line 123, characters 53-71
Called from file "src/kernel/boot.ml", line 29, characters 6-20
Called from file "src/kernel/cmdline.ml", line 763, characters 2-9
Called from file "src/kernel/cmdline.ml", line 216, characters 4-8
Plug-in fclang aborted: internal error.
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Sodium-20150201.
The crash doesn't happen when
(1) the braces "{" and "}" in line 5 and 7 are deleted,
(2) "s" is replaced by "0" in the invariant in line 3,
(3) the declaration of "s" in line 6 is deleted,
(4) the file is renamed to "470.c".
In each of these cases, an appropriate error message is printed.
### Additional Information :
My output of "clang --version" is:
Ubuntu clang version 3.4-1ubuntu3 (tags/RELEASE_34/final) (based on LLVM 3.4)
Target: x86_64-pc-linux-gnu
Thread model: posix
## Attachments
- [470.cpp](/uploads/25f4766330a52880d319ebc21f807ac9/470.cpp)Virgile PrevostoVirgile Prevostohttps://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/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/853placement new causes crash2021-02-22T13:13:28ZJochen Burghardtplacement new causes crashID0001960:
**This issue was created automatically from Mantis Issue 1960. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001960:
**This issue was created automatically from Mantis Issue 1960. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001960 | Frama-Clang | Plug-in > clang | public | 2014-11-10 | 2015-02-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **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
124.cpp:5:[fclang] failure: Wrong number of arguments in function call (expected 2, got 0)
[kernel] Current source was: 124.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 601, characters 19-79
Called from file "src/frama-clang/convert.ml", line 875, characters 31-57
Called from file "src/frama-clang/convert.ml", line 1132, characters 20-53
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.
## Attachments
- [124.cpp](/uploads/71566326db9e49039b74bf124e12fee7/124.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/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/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/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/1023WP crash when type casting in lemma2021-04-15T15:42:55Zmantis-gitlab-migrationWP crash when type casting in lemmaID0001804:
**This issue was created automatically from Mantis Issue 1804. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001804:
**This issue was created automatically from Mantis Issue 1804. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001804 | Frama-C | Plug-in > wp | public | 2014-06-06 | 2014-06-06 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Ian | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | Ubuntu | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | - |
### Description :
When using Typed+cast, a cast in a lemma can cause wp to crash.
In the below example, removing the lemma will cause the assert to validate.
### Steps To Reproduce :
Create file ptr_cast.c :
/*@
lemma valid_pointers:
\forall int **ptr; sizeof(int *) >= sizeof(int) ==> \valid(ptr) ==> \valid((int *) ptr);
*/
void f(int **ptr){
//@ assert sizeof(int *) >= sizeof(int) ==> \valid(ptr) ==> \valid((int *) ptr);
}
Run :
frama-c -cpp-command 'gcc -C -E' -pp-annot -wp -wp-model Typed+cast ptr_cast.c
Receive output :
[kernel] preprocessing with "gcc -C -E -dD ptr_cast.c"
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
ptr_cast.c:4:[wp] warning: Cast with incompatible pointers types (source: int**) (target: sint32*)
[wp] failure: Context 'Warning' non-initialized.
[kernel] Current source was: ptr_cast.c: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/wp/Warning.ml", line 117, characters 10-31
Called from file "src/wp/MemTyped.ml", line 799, characters 3-111
Called from file "src/wp/MemVar.ml", line 374, characters 23-51
Called from file "src/wp/Cvalues.ml", line 433, characters 30-42
Called from file "src/wp/LogicSemantics.ml", line 768, characters 12-27
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 358, characters 20-35
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 "src/wp/Lang.ml", line 869, characters 33-38
Re-raised at file "src/wp/Lang.ml", line 870, characters 40-43
Called from file "src/wp/LogicSemantics.ml", line 684, characters 11-54
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 326, characters 14-25
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/LogicCompiler.ml", line 401, characters 24-83
Called from file "src/wp/LogicCompiler.ml", line 673, characters 6-97
Called from file "src/wp/LogicCompiler.ml", line 690, characters 19-41
Called from file "src/wp/cfgWP.ml", line 1294, characters 31-42
Called from file "map.ml", line 169, characters 20-25
Called from file "src/wp/cfgWP.ml", line 1369, characters 14-54
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_guidelinesAllan BlanchardAllan Blanchard