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/263frama-c/jessie crashes with Unexpected error (Cil.SizeOfError("Undefined size...2021-04-20T17:20:20Zmantis-gitlab-migrationframa-c/jessie crashes with Unexpected error (Cil.SizeOfError("Undefined sizeof on a function.", _)).ID0002376:
**This issue was created automatically from Mantis Issue 2376. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002376:
**This issue was created automatically from Mantis Issue 2376. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002376 | Frama-C | Plug-in > jessie | public | 2018-05-29 | 2018-05-29 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | foo | **Assigned To** | cmarche | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 16-Sulfur | **Target Version** | - | **Fixed in Version** | - |
### Description :
Hi all,
I'm very new to the frama-c and why ecosystem. I hope it's really a bug with frama-c and not jessie.
The C input is:
#include<stdlib.h>
int main(void) {
char *p =malloc(5);
p[0] = 4;
return 3;
}
I'd like to verify that the write to p[0] goes toa valid address.
$ Frama-c -val -jessie t.c
[kernel] Parsing t.c (with preprocessing)
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
[value:initial-state] Values of globals at initialization
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__fc_mblen_state ∈ [--..--]
__fc_mbtowc_state ∈ [--..--]
__fc_wctomb_state ∈ [--..--]
t.c:4:[value] allocating variable __malloc_main_l4
t.c:5:[value] warning: out of bounds write. assert \valid(p + 0);
[value] done for function main
[value] ====== VALUES COMPUTED ======
[value:final-states] Values at end of function main:
__fc_heap_status ∈ [--..--]
p ∈ {{ &__malloc_main_l4[0] }}
__retres ∈ {3}
__malloc_main_l4[0] ∈ {4}
[1..4] ∈ UNINITIALIZED
[jessie] Starting Jessie translation
[jessie] warning: \separated is not supported by Jessie. This predicate will be ignored
[kernel] Current source was: FRAMAC_SHARE/libc/stdlib.h:389
The full backtrace is:
Raised at file "src/kernel_services/ast_queries/cil.ml", line 5238, characters 9-67
Called from file "common.ml", line 329, characters 27-46
Called from file "norm.ml", line 1551, characters 11-55
Called from file "norm.ml", line 1571, characters 37-71
Called from file "norm.ml", line 1614, characters 22-47
Called from file "norm.ml", line 1685, characters 19-43
Called from file "src/kernel_services/ast_queries/cil.ml", line 2239, characters 15-31
Called from file "src/kernel_services/ast_queries/cil.ml" (inlined), line 3543, characters 17-35
Called from file "src/kernel_services/ast_queries/cil.ml", line 3572, characters 12-19
Called from file "src/kernel_services/ast_queries/cil.ml", line 2278, characters 13-16
Called from file "src/kernel_services/ast_queries/cil.ml", line 3576, characters 23-50
Called from file "src/kernel_services/ast_queries/cil.ml", line 2254, characters 21-41
Called from file "src/kernel_services/ast_queries/cil.ml", line 3613, characters 14-38
Called from file "src/kernel_services/ast_queries/cil.ml", line 2254, characters 21-41
Called from file "src/kernel_services/ast_queries/cil.ml", line 3602, characters 5-80
Called from file "src/kernel_services/ast_queries/cil.ml", line 3840, characters 16-37
Called from file "src/kernel_services/ast_queries/cil.ml", line 2278, characters 13-16
Called from file "src/kernel_services/ast_queries/cil.ml", line 2323, characters 24-57
Called from file "src/kernel_services/ast_queries/cil.ml", line 3808, characters 5-53
Called from file "src/kernel_services/ast_queries/cil.ml" (inlined), line 6463, characters 17-37
Called from file "src/kernel_services/ast_queries/cil.ml", line 6468, characters 24-33
Called from file "src/kernel_services/ast_queries/cil.ml", line 6470, characters 3-20
Called from file "src/kernel_services/ast_queries/cil.ml", line 2254, characters 21-41
Called from file "src/kernel_services/ast_queries/cil.ml", line 6487, characters 15-39
Called from file "common.ml", line 580, characters 2-13
Called from file "norm.ml", line 1959, characters 2-26
Called from file "register.ml", line 158, characters 4-23
Called from file "register.ml", line 278, characters 6-12
Called from file "src/kernel_services/plugin_entry_points/journal.ml", line 442, characters 19-22
Re-raised at file "src/kernel_services/plugin_entry_points/journal.ml", line 457, characters 10-17
Called from file "queue.ml", line 105, characters 6-15
Called from file "src/kernel_internals/runtime/boot.ml", line 37, characters 4-20
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 789, characters 2-9
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 819, characters 18-64
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 228, characters 4-8
Unexpected error (Cil.SizeOfError("Undefined sizeof on a function.", _)).
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Sulfur-20171101.
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
[kernel] writing journal in file `./.frama-c/frama_c_journal.ml'.
### Additional Information :
I'm using
frama-c Sulfur-20171101
why 2.40
Why3 0.88.3
ocaml 4.06.1
## Attachments
- [frama_c_journal.ml](/uploads/d55e08324ce8dc26fa7317cab9a5d1be/frama_c_journal.ml)Claude MarchéClaude Marchéhttps://git.frama-c.com/pub/frama-c/-/issues/1179Frama-C Kernel on a specific C file (unexpected error, assertion failed)2022-10-21T11:21:18ZDavid MentréFrama-C Kernel on a specific C file (unexpected error, assertion failed)ID0001475:
**This issue was created automatically from Mantis Issue 1475. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001475:
**This issue was created automatically from Mantis Issue 1475. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001475 | Frama-C | Kernel | public | 2013-09-03 | 2014-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dmentre | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130601 | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
When Frama-C is launched on attached file, I get an exception.
$ frama-c q4_error_static_fun.c
[kernel] preprocessing with "gcc -C -E -I. questions/q4_error_static_fun.c"
[kernel] failure: Some globals contain dangling references after link:
F4:f5;
[kernel] Current source was: questions/q4_error_static_fun.c:35
The full backtrace is:
Raised at file "cil/src/mergecil.ml", line 2842, characters 2-167
Called from file "cil/src/mergecil.ml", line 2903, characters 16-37
Called from file "src/kernel/file.ml", line 1082, characters 20-56
Called from file "src/kernel/file.ml", line 1936, characters 12-30
Called from file "src/kernel/file.ml", line 2020, characters 4-27
Called from file "src/kernel/ast.ml", line 103, characters 2-28
Called from file "src/kernel/ast.ml", line 114, characters 53-71
Called from file "src/kernel/boot.ml", line 29, characters 6-20
Called from file "src/kernel/cmdline.ml", line 732, characters 2-9
Called from file "src/kernel/cmdline.ml", line 212, characters 4-8
Unexpected error (File "cil/src/mergecil.ml", line 2842, characters 2-8: Assertion failed).
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Fluorine-20130601.
## Attachments
- [q4_error_static_fun.c](/uploads/101d5f158fda1dda3691b247e573920d/q4_error_static_fun.c)https://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/240frama-clang fails to compile2022-09-28T11:04:53Zmantis-gitlab-migrationframa-clang fails to compileID0002402:
**This issue was created automatically from Mantis Issue 2402. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002402:
**This issue was created automatically from Mantis Issue 2402. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002402 | Frama-C | Plug-in > clang | public | 2018-10-01 | 2018-10-03 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | barafael | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | block | **Reproducibility** | always |
| **Platform** | Ubuntu | **OS** | Linux | **OS Version** | 18.04 LTS |
| **Product Version** | Frama-C 17-Chlorine | **Target Version** | - | **Fixed in Version** | - |
### Description :
When trying to compile frama-clang, I encounter
Error: Unbounded constructor ASinteger
in file convert_acsl.ml.
ASidentifier is also missing.
### Steps To Reproduce :
Get sources for frama-clang-0.0.6, configure, makeVirgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/520FRama C Nitrogen Nitrogen-201110012021-02-22T14:01:40Zmantis-gitlab-migrationFRama C Nitrogen Nitrogen-20111001ID0002210:
**This issue was created automatically from Mantis Issue 2210. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002210:
**This issue was created automatically from Mantis Issue 2210. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002210 | Frama-C | Plug-in > pdg | public | 2016-02-22 | 2016-02-25 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | lammyday | **Assigned To** | yakobowski | **Resolution** | unable to reproduce |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | sometimes |
| **Platform** | - | **OS** | Linux | **OS Version** | Ubuntu 14.04 |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | - |
### Description :
Frama-c pdg crashed of an unexpected error(out of memeory) after a warning that it could not find a final state, or a final state was unreachable.
### Additional Information :
Error meesages from crash:
main.c:2313:[pdg] warning: no final state. Probably unreachable...
[pdg] done for function main
[kernel] The full backtrace is:
Raised by primitive operation at file "src/kernel/log.ml", line 197, characters 16-31
Called from file "format.ml", line 299, characters 4-28
Called from file "format.ml", line 428, characters 6-72
Called from file "format.ml", line 435, characters 6-24
Called from file "format.ml", line 1148, characters 10-28
Called from file "external/hptmap.ml", line 201, characters 3-15
Called from file "external/hptmap.ml", line 201, characters 3-15
Called from file "external/hptmap.ml", line 201, characters 3-15
Called from file "external/hptmap.ml", line 201, characters 3-15
Called from file "list.ml", line 69, characters 12-15
Called from file "src/pdg_types/pdgTypes.ml", line 584, characters 6-33
Called from file "format.ml", line 1157, characters 10-25
Called from file "format.ml", line 1157, characters 10-25
Called from file "src/pdg/register.ml", line 140, characters 8-63
Called from file "queue.ml", line 134, characters 6-20
Called from file "src/pdg/register.ml", line 145, characters 4-68
Called from file "queue.ml", line 134, characters 6-20
Called from file "src/kernel/boot.ml", line 36, characters 4-20
Called from file "src/kernel/cmdline.ml", line 723, characters 2-9
Called from file "src/kernel/cmdline.ml", line 200, characters 4-8
Unexpected error (Out of memory).
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Nitrogen-20111001.
Note that a version and a backtrace alone often does not have 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
### Steps To Reproduce :
execute:
"frama-c -pdg -dot-pdg graph -pdg-print main.i -main main -val-ignore-recursive-calls"
on the make gnu utility with git version: 036760a9fdb11849b6a43feec7ce294e7f77db2a
this is obtainable from this url:
http://git.savannah.gnu.org/cgit/make.git/snapshot/make-036760a9fdb11849b6a43feec7ce294e7f77db2a.tar.gzhttps://git.frama-c.com/pub/frama-c/-/issues/523FRama C Nitrogen Nitrogen-20111001 crash during pdg construction2021-02-22T14:01:40Zmantis-gitlab-migrationFRama C Nitrogen Nitrogen-20111001 crash during pdg constructionID0002211:
**This issue was created automatically from Mantis Issue 2211. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002211:
**This issue was created automatically from Mantis Issue 2211. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002211 | Frama-C | Plug-in > pdg | public | 2016-02-22 | 2016-02-22 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | lammyday | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | Linux | **OS Version** | Ubunutu 14.04 |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | - |
### Description :
Crash during pdg construction, due to unexpected error - (File "external/hptmap.ml)
### Additional Information :
Error Message:
[value] computing for function error <- readline <- do_define <- eval <-
eval_makefile.
Called from read.c:2391.
[value] Done for function error
[kernel] The full backtrace is:
Called from file "src/lib/binary_cache.ml", line 366, characters 14-21
Called from file "external/hptmap.ml", line 1107, characters 18-41
Called from file "src/memory_state/lmap.ml", line 818, characters 10-35
Called from file "src/value/current_table.ml", line 75, characters 9-57
Called from file "src/value/eval_stmts.ml", line 1136, characters 6-69
Called from file "cil/src/ext/dataflow.ml", line 305, characters 12-27
Called from file "cil/src/ext/dataflow.ml", line 497, characters 8-21
Called from file "cil/src/ext/dataflow.ml", line 501, characters 9-22
Called from file "src/value/eval_funs.ml", line 117, characters 14-37
Called from file "src/value/eval_funs.ml", line 478, characters 10-65
Called from file "src/value/eval_stmts.ml", line 866, characters 14-73
Called from file "src/value/eval_stmts.ml", line 885, characters 10-114
Called from file "src/value/eval_stmts.ml", line 918, characters 38-62
Called from file "list.ml", line 74, characters 24-34
Called from file "src/value/eval_stmts.ml", line 974, characters 26-79
Called from file "cil/src/ext/dataflow.ml", line 320, characters 29-47
Called from file "cil/src/ext/dataflow.ml", line 497, characters 8-21
Called from file "cil/src/ext/dataflow.ml", line 501, characters 9-22
Called from file "src/value/eval_funs.ml", line 117, characters 14-37
Called from file "src/value/eval_funs.ml", line 478, characters 10-65
Called from file "src/value/eval_stmts.ml", line 866, characters 14-73
Called from file "src/value/eval_stmts.ml", line 885, characters 10-114
Called from file "src/value/eval_stmts.ml", line 918, characters 38-62
Called from file "list.ml", line 74, characters 24-34
Called from file "src/value/eval_stmts.ml", line 974, characters 26-79
Called from file "cil/src/ext/dataflow.ml", line 320, characters 29-47
Called from file "cil/src/ext/dataflow.ml", line 497, characters 8-21
Called from file "cil/src/ext/dataflow.ml", line 501, characters 9-22
Called from file "src/value/eval_funs.ml", line 117, characters 14-37
Called from file "src/value/eval_funs.ml", line 478, characters 10-65
Called from file "src/value/eval_stmts.ml", line 866, characters 14-73
Called from file "src/value/eval_stmts.ml", line 885, characters 10-114
Called from file "src/value/eval_stmts.ml", line 918, characters 38-62
Called from file "list.ml", line 74, characters 24-34
Called from file "src/value/eval_stmts.ml", line 974, characters 26-79
Called from file "cil/src/ext/dataflow.ml", line 320, characters 29-47
Called from file "cil/src/ext/dataflow.ml", line 497, characters 8-21
Called from file "cil/src/ext/dataflow.ml", line 501, characters 9-22
Called from file "src/value/eval_funs.ml", line 117, characters 14-37
Called from file "src/value/eval_funs.ml", line 452, characters 6-69
Called from file "src/value/eval_funs.ml", line 556, characters 11-44
Re-raised at file "src/value/eval_funs.ml", line 572, characters 47-50
Called from file "src/project/state_builder.ml", line 1076, characters 9-13
Re-raised at file "src/project/state_builder.ml", line 1080, characters 15-18
Called from file "src/semantic_callgraph/register.ml", line 84, characters 7-24
Called from file "src/project/state_builder.ml", line 490, characters 17-21
Called from file "src/semantic_callgraph/register.ml", line 196, characters 51-65
Called from file "src/pdg/register.ml", line 145, characters 4-68
Called from file "queue.ml", line 134, characters 6-20
Called from file "src/kernel/boot.ml", line 36, characters 4-20
Called from file "src/kernel/cmdline.ml", line 723, characters 2-9
Called from file "src/kernel/cmdline.ml", line 200, characters 4-8
Unexpected error (File "external/hptmap.ml", line 1105, characters 14-20: Assertion failed).
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Nitrogen-20111001.
Note that a version and a backtrace alone often does not have 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
### Steps To Reproduce :
execute:
frama-c -pdg -dot-pdg graph -pdg-print read.i -main eval_makefile -val-ignore-recursive-calls
on gnu make utility repository:
5acda13ace0ae4443ed04c4f8a62512b00a2b656
obtainable at urs:
http://git.savannah.gnu.org/cgit/make.git/snapshot/make-5acda13ace0ae4443ed04c4f8a62512b00a2b656.tar.gzhttps://git.frama-c.com/pub/frama-c/-/issues/1530Frama-C stops with unexpected failure (Ref. "norm.ml:1105:8")2021-04-15T09:17:33Zmantis-gitlab-migrationFrama-C stops with unexpected failure (Ref. "norm.ml:1105:8")ID0000299:
**This issue was created automatically from Mantis Issue 299. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000299:
**This issue was created automatically from Mantis Issue 299. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000299 | Frama-C | Plug-in > jessie | public | 2009-10-21 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jschuhmacher | **Assigned To** | cmarche | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090902 | **Target Version** | - | **Fixed in Version** | Frama-C Carbon-20101202-beta2 |
### Description :
While trying to check a file from the Minix3 kernel frama-c stops with an unexpected failure. A log is attached.
## Attachments
- [jessie.log](/uploads/fe41743dd9783c3f0ee0c320358d0864/jessie.log)
- [system.c](/uploads/aa5a9dc971e05892b8af27fea29eb379/system.c)https://git.frama-c.com/pub/frama-c/-/issues/344Functions that claim to return a struct but don't cause a crash2021-02-22T12:59:51Zmantis-gitlab-migrationFunctions that claim to return a struct but don't cause a crashID0002235:
**This issue was created automatically from Mantis Issue 2235. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002235:
**This issue was created automatically from Mantis Issue 2235. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002235 | Frama-C | Kernel | public | 2016-06-21 | 2017-05-31 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jrobbins | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Aluminium | **Target Version** | - | **Fixed in Version** | Frama-C 15-Phosphorus |
### Description :
If a function returns a struct in its declaration, but it's method body does not return anything, Frama-C will warn about not finding a return value, and then crash.
While the kernel does warn you this is an issue, no invalid operation on the user's part should cause a crash. Instead, it should cause a user error.
### Additional Information :
Tested with Aluminum on Linux 64-bit.
### Steps To Reproduce :
== File bug.c:
struct s {
int i;
};
struct s foo() {}
== Run command:
frama-c bug.c
== Output:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing bug.c (with preprocessing)
bug2.c:5:[kernel] warning: Body of function foo falls-through and cannot find an appropriate return value
bug2.c:5:[kernel] failure: Found return without value in function foo
[kernel] Current source was: bug.c:5
The full backtrace is:
Raised at file "src/kernel_services/plugin_entry_points/log.ml", line 583, characters 30-31
Called from file "src/kernel_services/plugin_entry_points/log.ml", line 577, characters 9-16
Re-raised at file "src/kernel_services/plugin_entry_points/log.ml", line 580, characters 15-16
Called from file "src/kernel_internals/typing/oneret.ml", line 246, characters 8-87
Called from file "src/kernel_internals/typing/oneret.ml", line 354, characters 22-54
Called from file "src/kernel_internals/typing/oneret.ml", line 361, characters 13-35
Called from file "src/kernel_services/ast_queries/file.ml", line 891, characters 6-26
Called from file "list.ml", line 73, characters 12-15
Called from file "src/kernel_services/ast_queries/file.ml", line 1143, characters 5-43
Called from file "src/kernel_services/ast_queries/file.ml", line 1579, characters 2-22
Called from file "src/kernel_services/ast_queries/file.ml", line 1666, characters 4-27
Called from file "src/kernel_services/ast_data/ast.ml", line 111, characters 2-28
Called from file "src/kernel_services/ast_data/ast.ml", line 123, characters 53-71
Called from file "src/kernel_internals/runtime/boot.ml", line 29, characters 6-20
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 787, characters 2-9
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 817, characters 18-64
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 228, characters 4-8
Frama-C aborted: internal error.
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Aluminium-20160501.
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/2218Goto outside of a block with assigns property2021-02-22T14:04:24Zmantis-gitlab-migrationGoto outside of a block with assigns propertyID0000776:
**This issue was created automatically from Mantis Issue 776. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000776:
**This issue was created automatically from Mantis Issue 776. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000776 | Frama-C | Kernel | public | 2011-04-04 | 2011-04-05 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Anne | **Assigned To** | - | **Resolution** | duplicate |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
I not really sure of the title, but I get:
$ frama-c toto.c
[kernel] preprocessing with "gcc -C -E -I. toto.c"
Erreur de segmentation
with the following file :
---------------------------------------------------
int X;
void f (int c) {
//@ assigns X;
if (c) {
X++;
if (X > 0) goto L;
X++;
}
L: ;
}https://git.frama-c.com/pub/frama-c/-/issues/2245Gui crash with a new global variable2021-02-22T13:54:44ZVictoria Moya LamielGui crash with a new global variableID0000700:
**This issue was created automatically from Mantis Issue 700. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000700:
**This issue was created automatically from Mantis Issue 700. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000700 | Frama-C | Graphical User Interface | public | 2011-02-01 | 2011-02-07 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | vmoyalam | **Assigned To** | monate | **Resolution** | no change required |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20101202-beta2 | **Target Version** | - | **Fixed in Version** | Frama-C Carbon-20101202-beta2 |
### Description :
Adding a new global variable as follows :
let typ = (TInt(IInt,[]));
and loc = {Lexing.dummy_pos with
Lexing.pos_lnum=1; Lexing.pos_fname=file} in
let var = Cil.makeGlobalVar ~logic:false ~generated:false se_var_name typ;
and iv = {init=Some(Cil.makeZeroInit ~loc:(loc,loc) typ)} in
var.vdecl <- (loc,loc);
var.vdescr <- Some("side_effect variable for FDC analysis");
try
Globals.Vars.add var iv;
with Globals.Vars.AlreadyExists (_,_)->
Printf.printf "Error adding Global %s" var.vname
makes Frma-C crash, raising a Not Found exception, with the following command :
frama-c-gui -testGlobal ../VAL/LOT/testBug.c
where "-testGlobal" is our plug-in adding a global variable.
There is no crash using the command "frama-c", the problem only appears using the interface (with "frama-c-gui").
### Additional Information :
I do not know is the cause is related to a lack of information at the moment of the creation of the global variable.
The full backtrace is:
Raised at file "hashtbl.ml", line 229, characters 23-32
Called from file "src/gui/filetree.ml", line 375, characters 6-51
Called from file "hashtbl.ml", line 145, characters 8-13
Called from file "hashtbl.ml", line 148, characters 4-19
Called from file "src/project/state_builder.ml", line 625, characters 15-30
Called from file "src/value/register_gui.ml", line 385, characters 2-15
Called from file "list.ml", line 69, characters 12-15
Called from file "src/gui/design.ml", line 1054, characters 4-36
Called from file "camlinternalOO.ml", line 374, characters 12-17
Called from file "camlinternalOO.ml", line 384, characters 24-40
Called from file "src/gui/design.ml", line 1170, characters 15-33
Called from file "src/lib/extlib.ml", line 186, characters 12-15
Re-raised at file "src/lib/extlib.ml", line 191, characters 10-11
Called from file "src/gui/gtk_helper.ml", line 717, characters 8-350
Unexpected error (Not_found).
You will find the "testGlobal" plugin and the "testBug" C file in the attached tar file.
## Attachments
- [testGlobal.tar](/uploads/165ffc930ccef808c99ba450c8f285c2/testGlobal.tar)https://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/2143Impact analysis does not catch Pdg.Top (returned on variadic calls)2021-02-22T13:52:06ZBoris YakobowskiImpact analysis does not catch Pdg.Top (returned on variadic calls)ID0000768:
**This issue was created automatically from Mantis Issue 768. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000768:
**This issue was created automatically from Mantis Issue 768. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000768 | Frama-C | Plug-in > impact analysis | public | 2011-03-29 | 2011-10-10 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | yakobowski | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20110201 | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
Querying the impact analysis of 'i++' in the following code results in a crash
int f(int, ...);
int main () {
int i=0;
i++;
f(i);
}https://git.frama-c.com/pub/frama-c/-/issues/1386incompatible types for a correct spec2021-02-22T13:29:30ZJulien Signolesincompatible types for a correct specID0001027:
**This issue was created automatically from Mantis Issue 1027. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001027:
**This issue was created automatically from Mantis Issue 1027. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001027 | Frama-C | Kernel > ACSL implementation | public | 2011-11-25 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | signoles | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Nitrogen-20111001 | **Target Version** | - | **Fixed in Version** | Frama-C Oxygen-20120901 |
### Description :
On the attached file, we get:
$ frama-c -jessie max_ok.c
<snip>
File "max_ok.jc", line 53, characters 11-17: typing error: incompatible types: intP[..] and integer
Note that the WP plug-in proves this program correct wrt its spec.
## Attachments
- [max_ok.c](/uploads/6e0308bc9a71173bd3e8ca7fb989bc33/max_ok.c)https://git.frama-c.com/pub/frama-c/-/issues/1536Incorrect 'assert false' in value analysis2021-02-22T13:34:10ZBoris YakobowskiIncorrect 'assert false' in value analysisID0000388:
**This issue was created automatically from Mantis Issue 388. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000388:
**This issue was created automatically from Mantis Issue 388. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000388 | Frama-C | Plug-in > Eva | public | 2010-02-01 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | yakobowski | **Assigned To** | monate | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C Boron-20100401 |
### Description :
This might be related to variadic calls, but I'm not really sure.
The crash is triggered by the following code:
typedef void *va_list;
#define va_start(AP, LASTARG) \
(AP = ((va_list) __builtin_next_arg (LASTARG)))
void main(const char *pszMessage,...) {
va_list vlParameters;
va_start(vlParameters,pszMessage);
}
### Additional Information :
SVN 7571https://git.frama-c.com/pub/frama-c/-/issues/1329incorrect AST generated2021-02-22T13:44:14ZPascal Cuoqincorrect AST generatedID0000911:
**This issue was created automatically from Mantis Issue 911. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000911:
**This issue was created automatically from Mantis Issue 911. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000911 | Frama-C | Kernel | public | 2011-08-04 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | block | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20110201 | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
short S;
int f(int x, int y)
{
return x+y;
}
int main (void) {
return f(1, S++);
}
Mini:~/ppc $ bin/toplevel.opt t.c -check
[kernel] preprocessing with "gcc -C -E -I. t.c"
t.c:11:[kernel] failure: [AST Integrity Check] initial AST
in call tmp_0 = f(1,tmp);, arg tmp has type short instead of int
[kernel] error occurring when exiting Frama-C: stopping exit procedure.
The full backtrace is:
Raised at file "src/kernel/log.ml", line 509, characters 30-31
Called from file "src/kernel/log.ml", line 503, characters 9-16
Re-raised at file "src/kernel/log.ml", line 506, characters 15-16
Called from file "src/kernel/file.ml", line 639, characters 16-240
Called from file "cil/src/cil.ml", line 1410, characters 15-31
Called from file "cil/src/cil.ml", line 2258, characters 5-62
Called from file "cil/src/cil.ml", line 2384, characters 14-21
Called from file "cil/src/cil.ml", line 1356, characters 21-41
Called from file "cil/src/cil.ml", line 2302, characters 5-86
Called from file "cil/src/cil.ml", line 2331, characters 14-35
Called from file "cil/src/cil.ml", line 1379, characters 13-16
Called from file "cil/src/cil.ml", line 2329, characters 4-844
Called from file "cil/src/cil.ml", line 1356, characters 21-41
Called from file "cil/src/cil.ml", line 2302, characters 5-86
Called from file "cil/src/cil.ml", line 1379, characters 13-16
Called from file "cil/src/cil.ml", line 2436, characters 16-40
Called from file "cil/src/cil.ml", line 1356, characters 21-41
Called from file "cil/src/cil.ml", line 2649, characters 14-39
Called from file "cil/src/cil.ml", line 1356, characters 21-41
Called from file "cil/src/cil.ml", line 2624, characters 5-101
Called from file "cil/src/cil.ml", line 2700, characters 16-38
Called from file "cil/src/cil.ml", line 1379, characters 13-16
Called from file "cil/src/cil.ml", line 1424, characters 24-57
Called from file "cil/src/cil.ml", line 2694, characters 5-63
Called from file "cil/src/cil.ml", line 8221, characters 16-36
Called from file "list.ml", line 69, characters 12-15
Called from file "cil/src/cil.ml", line 8178, characters 3-30
Called from file "cil/src/cil.ml", line 8222, characters 2-368
Called from file "cil/src/cil.ml", line 1356, characters 21-41
Called from file "cil/src/cil.ml", line 8253, characters 7-84
Called from file "src/kernel/file.ml", line 1159, characters 35-147
Called from file "src/kernel/file.ml", line 1380, characters 4-27
Called from file "src/kernel/ast.ml", line 60, characters 2-28
Called from file "src/kernel/ast.ml", line 67, characters 53-71
Called from file "queue.ml", line 134, characters 6-20
Called from file "src/kernel/cmdline.ml", line 174, characters 6-23
Frama-C aborted because of internal error.
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Carbon-20110201+dev.
Note that a version and a backtrace alone often does not have 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
Mini:~/ppc $
### Tags :
csmithhttps://git.frama-c.com/pub/frama-c/-/issues/1971Incorrect cil merging in presence of ACSL annotations2021-02-22T13:47:36ZBoris YakobowskiIncorrect cil merging in presence of ACSL annotationsID0000672:
**This issue was created automatically from Mantis Issue 672. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000672:
**This issue was created automatically from Mantis Issue 672. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000672 | Frama-C | Kernel | public | 2011-01-17 | 2012-09-19 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | yakobowski | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20101202-beta2 | **Target Version** | - | **Fixed in Version** | Frama-C Oxygen-20120901 |
### Description :
Launching Frama-C on the three attached files with the -check option causes a crash with the error
builtin.h:6:[kernel] failure: [AST Integrity Check]
initial ASTlogic variable Frama_C_entropy_source(728) is not declared
### Additional Information :
Command-line:
frama-c builtin.h builtin.c main.c -check
Three different files seem to be needed. The error also depends on the order the files are passed on the command line.
## Attachments
- [files.tgz](/uploads/ac8cda89035e915909e82790250a3e23/files.tgz)https://git.frama-c.com/pub/frama-c/-/issues/1255Incorrect handling of nearly-empty switch clauses with -simplify-cfg2021-02-22T13:24:55ZBoris YakobowskiIncorrect handling of nearly-empty switch clauses with -simplify-cfgID0000720:
**This issue was created automatically from Mantis Issue 720. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000720:
**This issue was created automatically from Mantis Issue 720. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000720 | Frama-C | Kernel | public | 2011-02-13 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | yakobowski | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20110201 | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
Frama-c chokes on the following code with option -simplify-cfg
void main()
{
switch(0) {
case 0:
break;
}
}
This can be seen either by starting the value analysis, or with -check.https://git.frama-c.com/pub/frama-c/-/issues/1303Incorrect loop unrolling in presence of switch2023-11-21T14:40:58ZBoris YakobowskiIncorrect loop unrolling in presence of switchID0000861:
**This issue was created automatically from Mantis Issue 861. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000861:
**This issue was created automatically from Mantis Issue 861. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000861 | Frama-C | Kernel | public | 2011-06-09 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | yakobowski | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | high | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20110201 | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
Syntactic loop unrolling of loops containing while is completely wrong.
Can be checked with -print or -check on the code below.
void main () {
/*@ loop pragma UNROLL_LOOP 4; */
for (int i=0;i<4;i++) {
switch (i) {
case 1: break;
case 2: break;
case 3: break;
case 4: break;
default:
}
}
}https://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 Prevosto