frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2021-02-22T14:02:04Zhttps://git.frama-c.com/pub/frama-c/-/issues/99622446: unknown sizes of types and value initialization2021-02-22T14:02:04ZPascal Cuoq22446: unknown sizes of types and value initializationID0001416:
**This issue was created automatically from Mantis Issue 1416. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001416:
**This issue was created automatically from Mantis Issue 1416. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001416 | Frama-C | Plug-in > Eva | public | 2013-05-07 | 2014-07-28 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
Commit 22446 transforms a crash when some types have unknown sizes into a clean exit, but there remains a problem with the test below:
Sending src/value/initial_state.ml
Transmitting file data .
Committed revision 22446.
~/ppc $ cat t.c
struct s;
struct larger {
struct s t[2];
int i;
} v;
int main(int c, char **v)
{
return 0;
}
~/ppc $ bin/toplevel.opt -val t.c
[kernel] warning: cannot load 5 plug-ins (incompatible with Fluorine-20130401+dev).
Aorai; Obfuscator; Report; Security_slicing;
Wp
[kernel] preprocessing with "gcc -C -E -I. t.c"
[value] Analyzing a complete application starting at main
[value] Computing initial state
t.c:6:[value] warning: during initialization of variable 'v', size of type 'struct s' cannot be
computed (abstract type 'struct s')
[value] Initial state computed
[value] Values of globals at initialization
[kernel] Current source was: t.c:6
The full backtrace is:
Raised at file "cil/src/cil.ml", line 4250, characters 40-64
Called from file "cil/src/cil.ml", line 4763, characters 17-35
Called from file "src/project/state_builder.ml", line 556, characters 17-22
Called from file "src/misc/bit_utils.ml", line 245, characters 37-66
Called from file "list.ml", line 86, characters 24-34
Called from file "src/misc/bit_utils.ml", line 242, characters 37-1023
Called from file "src/misc/bit_utils.ml", line 432, characters 4-58
Called from file "src/memory_state/offsetmap.ml", line 1726, characters 14-160
Called from file "src/memory_state/offsetmap.ml", line 424, characters 10-34
Called from file "format.ml", line 1166, characters 10-25
Called from file "format.ml", line 1166, characters 10-25
Called from file "src/lib/pretty_utils.ml", line 89, characters 2-121
Called from file "format.ml", line 1166, characters 10-25
Called from file "src/value/eval_funs.ml", line 317, characters 6-176
Called from file "src/value/eval_funs.ml", line 567, characters 11-40
Re-raised at file "src/value/eval_funs.ml", line 583, characters 47-50
Called from file "src/project/state_builder.ml", line 839, characters 9-13
Re-raised at file "src/project/state_builder.ml", line 847, characters 15-18
Called from file "src/value/register.ml", line 82, characters 4-24
Called from file "queue.ml", line 135, characters 6-20
Called from file "src/kernel/boot.ml", line 37, characters 4-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 (Cil.SizeOfError("abstract type 'struct s'", _)).
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Fluorine-20130401+dev.
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
~/ppc $https://git.frama-c.com/pub/frama-c/-/issues/893access to nested union/struct component causes crash2021-03-29T16:12:05ZJochen Burghardtaccess to nested union/struct component causes crashID0001803:
**This issue was created automatically from Mantis Issue 1803. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001803:
**This issue was created automatically from Mantis Issue 1803. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001803 | Frama-Clang | Kernel | public | 2014-06-06 | 2015-02-14 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | xubuntu-cfe13.10 | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | - |
### Description :
If, in the resolved issue #1754, the outermost "struct" is changed to "union" (file "1_4_2us.cpp"), the crash re-appears:
Now output intermediate result
1_4_2us.cpp:2:[fclang] failure: No usable default constructor for _s::_w
[kernel] Current source was: 1_4_2us.cpp:2
The full backtrace is:
Raised at file "src/kernel/log.ml", line 524, characters 30-31
Called from file "src/kernel/log.ml", line 518, characters 9-16
Re-raised at file "src/kernel/log.ml", line 521, characters 15-16
Called from file "convert.ml", line 1367, characters 30-75
Called from file "convert.ml", line 1399, characters 17-43
Called from file "list.ml", line 74, characters 24-34
Called from file "convert.ml", line 1425, characters 23-65
Called from file "convert.ml", line 1802, characters 21-133
Called from file "list.ml", line 74, characters 24-34
Called from file "convert.ml", line 1876, characters 19-78
Called from file "convert.ml", line 2102, characters 21-48
Called from file "list.ml", line 74, characters 24-34
Called from file "convert.ml", line 2106, characters 4-79
Called from file "frama_Clang_register.ml", line 82, characters 13-36
Called from file "src/kernel/file.ml", line 1058, characters 10-43
Called from file "src/kernel/file.ml", line 1102, characters 23-30
Called from file "list.ml", line 74, characters 24-34
Called from file "src/kernel/file.ml", line 1099, characters 6-520
Called from file "src/kernel/file.ml", line 2144, characters 12-30
Called from file "src/kernel/file.ml", line 2229, characters 4-27
Called from file "src/kernel/ast.ml", line 113, characters 2-28
Called from file "src/kernel/ast.ml", line 125, characters 53-71
Called from file "src/kernel/boot.ml", line 29, characters 6-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 fclang aborted: internal error.
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Neon-20140301.
If instead, or additionally, the inner "struct" is changed to "union" (files "1_4_2su.cpp" and "1_4_2uu.cpp"), a strange warning is issued:
Now output intermediate result
1_4_2su.cpp:3:[kernel] warning: Calling undeclared function Frama_C_memcpy. Old style K&R code?
## Attachments
- [1_4_2us.cpp](/uploads/d21782d1d8724590e1a9f532c053ab0f/1_4_2us.cpp)
- [1_4_2su.cpp](/uploads/c40254eb1bf606da7ca5bb1fd976753e/1_4_2su.cpp)
- [1_4_2uu.cpp](/uploads/b8d0faf5f634dc32b476e057713a797c/1_4_2uu.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/2407After ./confugure with --disable-all-staff options and make static, frama-c-M...2021-02-22T14:04:45ZNikolai KosmatovAfter ./confugure with --disable-all-staff options and make static, frama-c-Myplugin.byte crashesID0000309:
**This issue was created automatically from Mantis Issue 309. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000309:
**This issue was created automatically from Mantis Issue 309. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000309 | Frama-C | Kernel > ACSL implementation | public | 2009-10-30 | 2010-04-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Nikolai_Kosmatov | **Assigned To** | virgile | **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 Boron-20100401 |
### Description :
After configuring frama-c with the following options
-----------------------
./configure --disable-constant_propagation --disable-from --disable-gui --disable-impact --disable-inout --disable-ltl_to_acsl --disable-metrics --disable-miel --disable-occurrence --disable-pdg --disable-postdominators --disable-scope --disable-security --disable-semantic_callgraph --disable-slicing --disable-sparecode --disable-syntactic_callgraph --disable-users --disable-value --disable-wp
-----------------------
make
sudo make install
and make static for Myplugin, frama-c-Myplugin.byte crashes with the following output :
------------------------
[kernel] warning: cannot load plug-in Ltl_to_acsl
(incompatible with Beryllium-20090902+dev)
[Myplugin] started...
[kernel] preprocessing with "gcc -w -E -dD -include "/lib/lancPthc.h" merge.c"
[kernel] Unexpected error (Type.StringTbl.Unbound_value("Dynamic.Bool.get \"-warn-unspecified-order\"")).
Please report as 'crash' at http://bts.frama-c.com
------------------------https://git.frama-c.com/pub/frama-c/-/issues/1234aorai causes failed assertion2021-02-22T13:31:22ZJochen Burghardtaorai causes failed assertionID0001289:
**This issue was created automatically from Mantis Issue 1289. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001289:
**This issue was created automatically from Mantis Issue 1289. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001289 | Frama-C | Plug-in > aoraï | public | 2012-10-25 | 2014-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Oxygen-20120901 | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
Running "frama-c ftest.c -aorai-automata ftest.ya" on the attached program causes an unexpectyed error in file cil_datatype.ml; see attached stdout log.
## Attachments
- [ftest.c](/uploads/00b0a24a7ad13eb171b46cdba01964c0/ftest.c)
- [ftest.ya](/uploads/9991a7f542c1b39583bf6d5770b4d0ba/ftest.ya)
- [log.txt](/uploads/79e5a6ac1f6b4465b46a3c7b5078777e/log.txt)https://git.frama-c.com/pub/frama-c/-/issues/2517A pure predicate in an axiomatic with some "unpure" axioms have some strange ...2021-04-15T09:17:42ZFrançois BobotA pure predicate in an axiomatic with some "unpure" axioms have some strange resultsID0000073:
**This issue was created automatically from Mantis Issue 73. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |...ID0000073:
**This issue was created automatically from Mantis Issue 73. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000073 | Frama-C | Plug-in > jessie | public | 2009-04-30 | 2009-06-23 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | bobot | **Assigned To** | cmarche | **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 Beryllium-20090601-beta1 |
### Description :
A pure predicate in an axiomatic with some "unpure" axioms have some strange results. In this case an assertion failed :
myc.c
============================
/*@
axiomatic myaxioms{
predicate myrelation(int p,int q);
logic int mylogic{L}(int * p);
axiom myaxiom{L} :
\forall int * p, q; \at(myrelation(mylogic(p),q),L);
}
@*/
frama-c -jessie-analysis unwanted_label.c.assertion_failed.c :
=========================
Calling Jessie tool in subdir unwanted_label.c.assertion_failed.jessie
File "jc/jc_typing.ml", line 2687, characters 20-20:
Uncaught exception: File "jc/jc_typing.ml", line 2687, characters 20-26: Assertion failed
===========================
### Additional Information :
frama-c : 5186https://git.frama-c.com/pub/frama-c/-/issues/2461Assertion failed at project.ml:5632021-02-22T13:59:26ZDillon ParienteAssertion failed at project.ml:563ID0000179:
**This issue was created automatically from Mantis Issue 179. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000179:
**This issue was created automatically from Mantis Issue 179. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000179 | Frama-C | Kernel | public | 2009-07-09 | 2009-09-24 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dpariente | **Assigned To** | pascal | **Resolution** | unable to reproduce |
| **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 Beryllium-20090901 |
### Description :
Hello,
When launching: frama-c -load state.sav
(state.sav was previously generated and saved through -save command line option),
an error is displayed:
[kernel] error: unexpected error File "src/project/project.ml", line 563, characters 11-17: Assertion failed
[kernel] error: please report as `crash' at http://bts.frama-c.com
A printexc at project.ml:563 instead of "assert false" gives:
***** Stack overflow[values] computing for function MAIN
====== INITIAL STATE ======
====== INITIAL STATE COMPUTED ======
Growing heap to 289522k bytes
Regards,
Dillonhttps://git.frama-c.com/pub/frama-c/-/issues/2444Assertion failed in jc_interp_misc.ml2021-04-15T09:17:42Zmantis-gitlab-migrationAssertion failed in jc_interp_misc.mlID0000080:
**This issue was created automatically from Mantis Issue 80. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |...ID0000080:
**This issue was created automatically from Mantis Issue 80. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000080 | Frama-C | Plug-in > jessie | public | 2009-05-11 | 2009-11-25 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | boris | **Assigned To** | cmarche | **Resolution** | duplicate |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Lithium-20081201 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Jessie crashes on code [1] with error message [2].
Environment: Windows XP, cygwin
---------------------------------------
[1]
/*@ requires \valid(p) && \valid(q);
ensures *p == \old(*q);
ensures *q == \old(*p);
assigns *p, *q;
*/
void Swap(int *p, int *q)
{
int temp;
temp = *p;
*p = *q;
*q = temp;
}
/*@ requires \valid(a+ (0..k));
*/
void foo(int a[], int k) {
Swap(&a[0], &a[k]);
}
[2]
memory (mem-field(int_M),q_21)
in memory set (mem-field(int_M),p_20),
(mem-field(int_M),q_21)
File "jc/jc_interp_misc.ml", line 707, characters 7-7:
Uncaught exception: File "jc/jc_interp_misc.ml", line 707, characters 7-13: Assertion failed
Jessie subprocess failed: jessie -why-opt -split-user-conj -v -locs tst2.cloc tst2.jc
### Additional Information :
This bug is likely related to bug 38 http://bts.frama-c.com/view.php?id=38https://git.frama-c.com/pub/frama-c/-/issues/1186Assertion failure in Ival.scale_div2021-02-22T13:22:35ZBoris YakobowskiAssertion failure in Ival.scale_divID0001584:
**This issue was created automatically from Mantis Issue 1584. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001584:
**This issue was created automatically from Mantis Issue 1584. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001584 | Frama-C | Plug-in > Eva | public | 2013-12-09 | 2014-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | yakobowski | **Assigned To** | pascal | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
(Csmith-found program, reduced by creduce)
To be analyzed with -slevel 4.
Interesting part of the backtrace:
Called from file "src/ai/ival.ml", line 1011, characters 3-123
Called from file "src/ai/ival.ml", line 1166, characters 2-35
Called from file "src/ai/ival.ml", line 2370, characters 20-48
## Attachments
- [small3.i](/uploads/5eae9a679e659d4b5d94d6604e24c457/small3.i)https://git.frama-c.com/pub/frama-c/-/issues/1527assign makes Jessie crash2021-04-15T09:17:33Zmantis-gitlab-migrationassign makes Jessie crashID0000303:
**This issue was created automatically from Mantis Issue 303. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000303:
**This issue was created automatically from Mantis Issue 303. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000303 | Frama-C | Plug-in > jessie | public | 2009-10-26 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | boris | **Assigned To** | cmarche | **Resolution** | duplicate |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090901 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Code [1] makes Jessie crash [2] on Beryllium-20090901.
[1]
/*@ requires \valid(p) && \valid(q);
ensures *p == \old(*q);
ensures *q == \old(*p);
assigns *p, *q;
*/
void Swap(int *p, int *q)
{
int temp;
temp = *p;
*p = *q;
*q = temp;
}
void Foo() {
const int n=10;
int a[n];
int i;
for(i=0; i<n; i++) a[i]=0;
//@ loop assigns a[0..n-1];
for(i=1; i<n; i++) Swap(&a[i], &a[0]);
}
[2]
[kernel] preprocessing with "gcc -C -E -I. -dD tst.c"
tst.c:17:[kernel] warning: Variable-sized local variable a
[jessie] Starting Jessie translation
[kernel] No code for function __builtin_alloca, default assigns generated
[jessie] Producing Jessie files in subdir tst.jessie
[jessie] File tst.jessie/tst.jc written.
[jessie] File tst.jessie/tst.cloc written.
[jessie] Calling Jessie tool in subdir tst.jessie
Generating Why function Swap
Generating Why function Foo
** Jc_interp_misc.transpose_location_list: TODO: parameters **
memory (mem-field(int_M),q_4)
in memory set (mem-field(int_M),p_3),
(mem-field(int_M),q_4)
File "jc/jc_interp_misc.ml", line 733, characters 1-1:
Uncaught exception: File "jc/jc_interp_misc.ml", line 733, characters 1-7: Assertion failed
[jessie] user error: Jessie subprocess failed: jessie -why-opt -split-user-conj -v -locs tst.cloc tst.jc
### Additional Information :
See also bug 80 http://bts.frama-c.com/view.php?id=80https://git.frama-c.com/pub/frama-c/-/issues/1001assigns crash on incorrect locations2021-04-15T08:29:05Zmantis-gitlab-migrationassigns crash on incorrect locationsID0001844:
**This issue was created automatically from Mantis Issue 1844. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001844:
**This issue was created automatically from Mantis Issue 1844. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001844 | Frama-C | Plug-in > wp | public | 2014-07-17 | 2014-07-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | boulme | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | Linux Ubuntu 14.04 LTS | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | - |
### Description :
On the file "crash_assigns.c",
an invalid assign clause makes wp crash with the message:
Current source was: crash_assigns.c:5
The full backtrace is:
Raised at file "hashtbl.ml", line 353, characters 18-27
Called from file "hashtbl.ml", line 361, characters 22-38
Plug-in wp aborted: internal error.
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Neon-20140301.
### Additional Information :
Replacing the invalid assigns clause with a valid one like
assigns t[0..9];
makes the pb disappear...
### Steps To Reproduce :
run frama-c-gui crash_assigns.c
and try to prove assigns clause using wp.
## Attachments
- [crash_assigns.c](/uploads/b195abe901a4302f8d3fab7fb4ce8458/crash_assigns.c)Loïc CorrensonLoïc Corrensonhttps://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/1159AST integrity check failure with kernel-debug2021-02-22T13:21:33ZGuillaume PetiotAST integrity check failure with kernel-debugID0001440:
**This issue was created automatically from Mantis Issue 1440. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001440:
**This issue was created automatically from Mantis Issue 1440. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001440 | Frama-C | Kernel | public | 2013-06-03 | 2014-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | guillaume-petiot | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
a.c:6:[kernel] failure: [AST Integrity Check] initial AST
Following functions and variables are present in global tables but not in AST:
Functions:
__builtin_va_arg(158) __builtin_stdarg_start(162) __builtin_next_arg(310)
__builtin_expect(350) __builtin_va_start(357) __builtin_va_arg(541)
__builtin_stdarg_start(545) __builtin_next_arg(693) __builtin_expect(733)
__builtin_va_start(740)
Fatal error: exception Log.AbortFatal("kernel")
Raised at file "src/kernel/log.ml", line 523, characters 30-31
Called from file "src/kernel/log.ml", line 517, characters 9-16
Re-raised at file "src/kernel/log.ml", line 520, characters 15-16
Called from file "src/kernel/file.ml", line 717, characters 8-413
Called from file "cil/src/cil.ml", line 5887, characters 7-84
Called from file "src/kernel/file.ml", line 1449, characters 36-147
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
Re-raised at file "src/kernel/cmdline.ml", line 226, characters 14-17
Called from file "src/kernel/boot.ml", line 66, characters 2-355
### Steps To Reproduce :
$ frama-c a.c -check -kernel-debug 1
## Attachments
- [a.c](/uploads/206b5b7c43303793821044d13c13132b/a.c)https://git.frama-c.com/pub/frama-c/-/issues/113Auto-generated assigns clause for a void* argument crashes wp2021-02-22T13:34:40Zmantis-gitlab-migrationAuto-generated assigns clause for a void* argument crashes wpID0002385:
**This issue was created automatically from Mantis Issue 2385. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002385:
**This issue was created automatically from Mantis Issue 2385. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002385 | Frama-C | Plug-in > wp | public | 2018-07-05 | 2019-10-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | schollet | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
When using an unspecified function with an void* argument from an external file, the default generated assigns clause for that argument crashes frama-c and WP miss-attributes the error to the user.
Specifically, for an unspecified function foo(void* p), the auto generated assigns clause states that the function assigns *((char *)p+(0 .. )), which is then picked up by WP as an invalid user input.
Version : Frama-C 17 Chlorine
### Additional Information :
The command run :
frama-c -wp test2.c
Error log :
[kernel] Parsing test2.c (with preprocessing)
[kernel:annot:missing-spec] test2.c:7: Warning:
Neither code nor specification for function foo, generating default assigns from the prototype
[wp] Warning: Missing RTE guards
[wp] test2.c:11: User Error: Invalid infinite range i_0+(0..)
[kernel] Plug-in wp aborted: invalid user input.
The auto-generated assigns clause (found with frama-c-gui):
/*@ assigns *((char *)thing + (0 ..));
assigns *((char *)thing + (0 ..)) \from *((char *)thing + (0 ..));
*/
Removing the assigns clause for create stops WP from crashing
### Steps To Reproduce :
run `frama-c -wp test2.c` with those 3 provided files
OR:
Write a function and its specification with at least an assigns clause.
Write in it a call to another function.
Write in another file that 2nd function which takes as an argument an void*.
Write the header and include it in the first file.
For the header and the 2nd file, do not write any specification for the function.
run frama-c -wp on the first file
## Attachments
- [assigns.tar.gz](/uploads/7d8c7280dce8dde42f8cce1f86cbef35/assigns.tar.gz)https://git.frama-c.com/pub/frama-c/-/issues/398"Builtin already registered" after Reparse2021-02-22T13:37:10Zmantis-gitlab-migration"Builtin already registered" after ReparseID0002242:
**This issue was created automatically from Mantis Issue 2242. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002242:
**This issue was created automatically from Mantis Issue 2242. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002242 | Frama-C | Plug-in > wp | public | 2016-07-30 | 2016-12-05 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | khar | **Assigned To** | bobot | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | lubuntu | **OS Version** | - |
| **Product Version** | Frama-C Aluminium | **Target Version** | - | **Fixed in Version** | - |
### Description :
When using frama-c-gui to analyze code that uses arrays or pointers to structs, after a Reparse, the GUI fails to perform further analysis.
### Additional Information :
Step 2 (selecting the function "Foo" rather than the file "repro.c") is needed to work around a possibly unrelated bug where the source viewer doesn't update properly after a Reparse. To reproduce that bug, simply click "repro.c" instead of "Foo" in step 2.
### Steps To Reproduce :
$ cat repro.c:
//@ ensures foo[1] == 1;
void Foo(int* foo) {
foo[1] = 1;
}
$ frama-c-gui repro.c
1. Expand "repro.c" on the file panel.
2. Click "Foo" on the file panel.
3. Right-click the "ensures" annotation in the source panel.
4. Click "Prove property by WP".
5. On the toolbar, click the "Reparse source files, and replay analyses" button.
6. Click "repro.c" on the file panel.
7. Right-click the "ensures" annotation in the source panel.
8. Click "Prove property by WP".
Results: an error dialog with the following text:
Current source was: repro.c:2
The full backtrace is:
Raised at file "hashtbl.ml", line 328, characters 23-32
Called from file "src/libraries/project/state_topological.ml", line 62, characters 23-38
Unexpected error (Failure("Builtin already registered for 'shift_sint32'")).
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_guidelines
## Attachments
- [repro.c](/uploads/5cc283fba4536bd3c0702a8ca68141b5/repro.c)https://git.frama-c.com/pub/frama-c/-/issues/440cannot deal with many files2021-02-22T13:38:02Zmantis-gitlab-migrationcannot deal with many filesID0000778:
**This issue was created automatically from Mantis Issue 778. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000778:
**This issue was created automatically from Mantis Issue 778. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000778 | Frama-C | Documentation | public | 2011-04-08 | 2016-06-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | njucslzh | **Assigned To** | monate | **Resolution** | no change required |
| **Priority** | normal | **Severity** | block | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20110201 | **Target Version** | - | **Fixed in Version** | - |
### Description :
When I have many files which are in a project to analysis , it always cannot correctly preprocess them. Errors as follow:
[gui] warning: Frama-C images not found. Is FRAMAC_SHARE correctly set?
[kernel] preprocessing with "gcc -C -E -I. /home/lzh/cvs-1.11.4/src/zlib.c"
[kernel] user error: failed to run: gcc -C -E -I. -o '/tmp/zlib.c788cad.i' '/home/lzh/cvs-1.11.4/src/zlib.c'
you may set the CPP environment variable to select the proper preprocessor command or use the option "-cpp-command".
[kernel] user error: skipping file "/home/lzh/cvs-1.11.4/src/zlib.c" that has errors.
### Additional Information :
For toy program with two or three simply files, I just change c files to i files directly , it works well. But in practical , this don't work. Can you show me how to preprocess and merge the Source Code files? It is described too little in user manual .https://git.frama-c.com/pub/frama-c/-/issues/84Can't build from source using opam2021-02-22T13:34:34Zmantis-gitlab-migrationCan't build from source using opamID0002466:
**This issue was created automatically from Mantis Issue 2466. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002466:
**This issue was created automatically from Mantis Issue 2466. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002466 | Frama-C | Opam | public | 2019-07-25 | 2020-02-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | sshankar | **Assigned To** | maroneze | **Resolution** | fixed |
| **Priority** | normal | **Severity** | block | **Reproducibility** | always |
| **Platform** | - | **OS** | Ubuntu | **OS Version** | 18.04 |
| **Product Version** | Frama-C 18-Argon | **Target Version** | - | **Fixed in Version** | Frama-C 20-Calcium |
### Description :
Argon doesn't build, presumably due to config related bugs in opam/opam. I am guessing its due to inconsistency with opam semantics of "|" (used under conflicts in $FRAMAC/opam/opam).
### Additional Information :
If possible, I'd appreciate a patch I could do locally instead of waiting for the official fix. Thanks.
### Steps To Reproduce :
When I try to install it using the prescribed method
opam init
eval `opam config env`
opam install depext
opam depext frama-c
opam install --deps-only frama-c
cd ~/src (where argon is)
opam pin add --kind=path frama-c frama-c-18.0-Argon/
I get the following error (and no frama-c):
frama-c needs to be installed.
[ERROR] why3-base (< 0.88 | >= 1.0.0) & coq < 8.4.6 & lablgtk < 2.18.2 &
frama-c-e-acsl & frama-c-base is not a valid conjunction
[NOTE] Pinning command successful, but your installed packages may be out of
sync.https://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/1761Cash in value analysis of sliced project2021-02-22T14:03:42ZPatrick BaudinCash in value analysis of sliced projectID0000791:
**This issue was created automatically from Mantis Issue 791. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000791:
**This issue was created automatically from Mantis Issue 791. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000791 | Frama-C | Plug-in > Eva | public | 2011-04-13 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | patrick | **Assigned To** | pascal | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
Unexpected error (File "src/kernel/cilE.ml", line 268, characters 68-74: Assertion failed).
### Additional Information :
Revision: 12829
Command:
frama-c bug.c -slice-return send -then-on 'Slicing export' -val
file bug.c
/*@ assigns *p \from \empty;
assigns \result ; */
int scanf (char const *, int * p);
/*@ assigns \nothing ; */
int send (int x) {
return x;
}
void main(void) {
int input;
scanf("%d",&input);
send (input);
}https://git.frama-c.com/pub/frama-c/-/issues/940"catch(...)" causes crash2021-02-22T13:15:30ZJochen Burghardt"catch(...)" causes crashID0001966:
**This issue was created automatically from Mantis Issue 1966. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001966:
**This issue was created automatically from Mantis Issue 1966. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001966 | Frama-Clang | Plug-in > clang | public | 2014-11-13 | 2014-12-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C GIT, precise the release id |
### Description :
output:
Now output intermediate result
[kernel] Current source was: 133.cpp:3
The full backtrace is:
Raised at file "stack.ml", line 31, characters 20-25
Called from file "src/kernel/exn_flow.ml", line 120, characters 37-60
Called from file "list.ml", line 69, characters 12-15
Called from file "src/kernel/exn_flow.ml", line 112, characters 8-389
Called from file "src/kernel/visitor.ml", line 75, characters 14-33
Called from file "cil/src/cil.ml", line 2045, characters 15-31
Called from file "cil/src/cil.ml", line 3094, characters 5-86
Called from file "cil/src/cil.ml", line 2084, characters 13-16
Called from file "cil/src/cil.ml", line 3254, characters 16-40
Called from file "cil/src/cil.ml", line 2060, characters 21-41
Called from file "cil/src/cil.ml", line 3483, characters 14-39
Called from file "cil/src/cil.ml", line 2060, characters 21-41
Called from file "cil/src/cil.ml", line 3445, characters 5-91
Called from file "cil/src/cil.ml", line 3537, characters 16-38
Called from file "cil/src/cil.ml", line 2084, characters 13-16
Called from file "cil/src/cil.ml", line 2129, characters 24-57
Called from file "cil/src/cil.ml", line 3531, characters 5-53
Called from file "cil/src/cil.ml", line 6156, characters 16-36
Called from file "list.ml", line 69, characters 12-15
Called from file "cil/src/cil.ml", line 5746, characters 3-30
Called from file "cil/src/cil.ml", line 6157, characters 2-420
Called from file "cil/src/cil.ml", line 2060, characters 21-41
Called from file "cil/src/cil.ml", line 6190, characters 7-84
Called from file "src/kernel/visitor.ml", line 827, characters 2-45
Called from file "src/kernel/file.ml", line 1617, characters 2-8
Called from file "queue.ml", line 134, characters 6-20
Called from file "src/kernel/file.ml", line 1694, characters 2-36
Called from file "src/kernel/file.ml", line 2264, characters 4-27
Called from file "src/kernel/ast.ml", line 111, characters 2-28
Called from file "src/kernel/ast.ml", line 123, characters 53-71
Called from file "src/kernel/boot.ml", line 29, characters 6-20
Called from file "src/kernel/cmdline.ml", line 761, characters 2-9
Called from file "src/kernel/cmdline.ml", line 216, characters 4-8
Unexpected error (Stack.Empty).
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Neon-20140301+dev-stance.
Could be related to issue #1957?
(Importance: this code is used via #include <vector>.)
## Attachments
- [133.cpp](/uploads/ec10c3fb4d765ca86e6de649c4277911/133.cpp)https://git.frama-c.com/pub/frama-c/-/issues/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 Prevosto