frama-c issues
https://git.frama-c.com/pub/frama-c/-/issues
2021-04-15T09:17:42Z
https://git.frama-c.com/pub/frama-c/-/issues/2517
A pure predicate in an axiomatic with some "unpure" axioms have some strange ...
2021-04-15T09:17:42Z
François Bobot
A pure predicate in an axiomatic with some "unpure" axioms have some strange results
ID0000073:
**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 : 5186
https://git.frama-c.com/pub/frama-c/-/issues/2508
Compilation error if options --with-jessie-static --with-ltl_to_acsl-static a...
2021-02-22T14:00:22Z
mantis-gitlab-migration
Compilation error if options --with-jessie-static --with-ltl_to_acsl-static are present.
ID0000111:
**This issue was created automatically from Mantis Issue 111. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000111:
**This issue was created automatically from Mantis Issue 111. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000111 | Frama-C | Kernel | public | 2009-06-02 | 2009-06-23 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | nstouls | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | block | **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 :
With ocamlc 3.10.2
If the configure script is launched with following options :
--with-jessie-static --with-ltl_to_acsl-static
then this error occurs during compilation:
Ocamlc src/lib/dynlink_common_interface.cmo
The implementation src/lib/dynlink_common_interface.ml
does not match the interface src/lib/dynlink_common_interface.cmi:
The field `is_native' is required but not provided
make: *** [src/lib/dynlink_common_interface.cmo] Erreur 2
Removing configure options resolves the problem.
https://git.frama-c.com/pub/frama-c/-/issues/2481
crash for untyped_metrics example plugin
2021-02-22T13:59:50Z
Stephane Duprat
crash for untyped_metrics example plugin
ID0000163:
**This issue was created automatically from Mantis Issue 163. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000163:
**This issue was created automatically from Mantis Issue 163. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000163 | Frama-C | Kernel | public | 2009-06-25 | 2009-09-02 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | sduprat | **Assigned To** | monate | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090601-beta1 | **Target Version** | - | **Fixed in Version** | Frama-C Beryllium-20090901 |
### Description :
when running this plugin :
> frama-c -count-for tmp1.c
> [kernel] error: unexpected error Not_found
> [kernel] error: please report as `crash' at http://bts.frama-c.com
https://git.frama-c.com/pub/frama-c/-/issues/2478
crash when unbound variable
2021-02-22T13:59:47Z
mantis-gitlab-migration
crash when unbound variable
ID0000190:
**This issue was created automatically from Mantis Issue 190. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000190:
**This issue was created automatically from Mantis Issue 190. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000190 | Frama-C | Plug-in > slicing | public | 2009-07-15 | 2009-09-02 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | lukaszc | **Assigned To** | patrick | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Beryllium-20090901 |
### Description :
"frama-c -slice-rd y -pp-annot test.c" results in a crash
------------
test.c
------------
int x(int y, int z)
{
/*@ slice pragma expr y == 1; */
//@ assert y == 1;
//@ assert y + z == 3;
return 2*y*z1();
}
int main()
{
x(1,2);
return 0;
}
int z1()
{
return 1;
}
https://git.frama-c.com/pub/frama-c/-/issues/2461
Assertion failed at project.ml:563
2021-02-22T13:59:26Z
Dillon Pariente
Assertion failed at project.ml:563
ID0000179:
**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,
Dillon
https://git.frama-c.com/pub/frama-c/-/issues/2457
Problem with the "-main" option
2021-02-22T13:59:21Z
mantis-gitlab-migration
Problem with the "-main" option
ID0000279:
**This issue was created automatically from Mantis Issue 279. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000279:
**This issue was created automatically from Mantis Issue 279. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000279 | Frama-C | Kernel | public | 2009-10-09 | 2009-10-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | cbenkimoun | **Assigned To** | monate | **Resolution** | no change required |
| **Priority** | normal | **Severity** | block | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090902 | **Target Version** | - | **Fixed in Version** | Frama-C Beryllium-20090902 |
### Description :
I've just installed Frama-c on my computer.
I try to run the first.c example which is available on your web site.
I've got an error concerning the -main option.
Here is the output:
"
[kernel] preprocessing with "C:\Cygwin\bin\gcc-3.exe -CC -E -I toto.c"
# 1 "toto.c"
# 1 "<built-in>"
# 1 "<command line>"
# 1 "toto.c"
int S=0;
int T[5];
int main (void)
{
int i;
int *p = &T[0] ;
for (i=0; i<5; i++)
{ S = S+i; *p++ = S; }
return S;
}
[kernel] user error: Could not find entry point: main
"
I don't know what to do because there is a "main" function in my example.
I tried the -lib-entry option as well but without success...
Could you please help me?
Many thanks.
Cyril.
### Additional Information :
Running on Windows Vista.
Using cygwin gcc (PPC = "C:\Cygwin\bin\gcc-3.exe -CC -E -I"
https://git.frama-c.com/pub/frama-c/-/issues/2444
Assertion failed in jc_interp_misc.ml
2021-04-15T09:17:42Z
mantis-gitlab-migration
Assertion failed in jc_interp_misc.ml
ID0000080:
**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=38
https://git.frama-c.com/pub/frama-c/-/issues/2437
(* TODO: parameters *)
2021-04-15T09:17:40Z
Sylvie Boldo
(* TODO: parameters *)
ID0000112:
**This issue was created automatically from Mantis Issue 112. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000112:
**This issue was created automatically from Mantis Issue 112. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000112 | Frama-C | Plug-in > jessie | public | 2009-06-02 | 2009-12-03 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | sboldo | **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** | - |
### Description :
hello,
I am in trunk, svn version 5349.
I fell into an
assert false) (* TODO: parameters *)
which is at line 718 of jc/jc_interp_misc.ml
The C file is attached. It tackles loops with floating-point matrices.
Regards,
Sylvie Boldo
## Attachments
- [int_matrix.c](/uploads/684d06b33caba66a5c5c7b153c5f0bbb/int_matrix.c)
https://git.frama-c.com/pub/frama-c/-/issues/2436
Jessie internal error
2021-04-15T09:17:38Z
mantis-gitlab-migration
Jessie internal error
ID0000199:
**This issue was created automatically from Mantis Issue 199. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000199:
**This issue was created automatically from Mantis Issue 199. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000199 | Frama-C | Plug-in > jessie | public | 2009-07-22 | 2009-12-03 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | lukaszc | **Assigned To** | cmarche | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090601-beta1 | **Target Version** | - | **Fixed in Version** | - |
### Description :
I've obtained the following output:
[kernel] error: unexpected error File "src/jessie/interp.ml", line 1764, characters 18-24: Assertion failed
[kernel] error: please report as `crash' at http://bts.frama-c.com
### Additional Information :
It does not crash anymore but still complains about a cast from char* to int.
This is normal since "a" is a string, it should be 'a'
I agree that Frama-C front-end should complain earlier...
https://git.frama-c.com/pub/frama-c/-/issues/2425
share/Makefile.kernel: No such file or directory
2021-02-22T14:04:47Z
mantis-gitlab-migration
share/Makefile.kernel: No such file or directory
ID0000408:
**This issue was created automatically from Mantis Issue 408. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000408:
**This issue was created automatically from Mantis Issue 408. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000408 | Frama-C | Kernel > Makefile | public | 2010-02-16 | 2010-02-18 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | javert42 | **Assigned To** | signoles | **Resolution** | no change required |
| **Priority** | normal | **Severity** | block | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090902 | **Target Version** | - | **Fixed in Version** | - |
### Description :
running 'make' gives the following errors:
share/Makefile.dynamic:55: share/Makefile.kernel: No such file or directory
Makefile:1853: .depend: No such file or directory
Copying to lib/dgraph.cmi
cp: cannot stat `ocamlgraph/dgraph/dgraph.cmi': No such file or directory
make: *** [lib/dgraph.cmi] Error 1
https://git.frama-c.com/pub/frama-c/-/issues/2424
cp: cannot stat `ocamlgraph/dgraph/dgraph.cmi': No such file or directory
2021-02-22T14:04:47Z
mantis-gitlab-migration
cp: cannot stat `ocamlgraph/dgraph/dgraph.cmi': No such file or directory
ID0000409:
**This issue was created automatically from Mantis Issue 409. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000409:
**This issue was created automatically from Mantis Issue 409. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000409 | Frama-C | Kernel > Makefile | public | 2010-02-16 | 2010-02-18 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | javert42 | **Assigned To** | signoles | **Resolution** | no change required |
| **Priority** | normal | **Severity** | block | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090902 | **Target Version** | - | **Fixed in Version** | - |
### Description :
frama-c-Beryllium-20090902-why-2.21
Running make gives the following error:
share/Makefile.dynamic:55: share/Makefile.kernel: No such file or directory
Makefile:1853: .depend: No such file or directory
Copying to lib/dgraph.cmi
cp: cannot stat `ocamlgraph/dgraph/dgraph.cmi': No such file or directory
make: *** [lib/dgraph.cmi] Error 1
### Additional Information :
dgraph.cmi does not exist in ocamlgraph/dgraph
dgraph.cmi does not exist anywhere in ocamlgraph.tar.gz
https://git.frama-c.com/pub/frama-c/-/issues/2407
After ./confugure with --disable-all-staff options and make static, frama-c-M...
2021-02-22T14:04:45Z
Nikolai Kosmatov
After ./confugure with --disable-all-staff options and make static, frama-c-Myplugin.byte crashes
ID0000309:
**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/2392
File "src/kernel/cilE.ml", line 372, characters 13-19: Assertion failed
2021-02-22T13:58:05Z
mantis-gitlab-migration
File "src/kernel/cilE.ml", line 372, characters 13-19: Assertion failed
ID0000385:
**This issue was created automatically from Mantis Issue 385. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000385:
**This issue was created automatically from Mantis Issue 385. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000385 | Frama-C | Kernel | public | 2010-02-01 | 2010-04-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | tari3x | **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 :
The attached file crashes Frama-C with the above error. Steps to reproduce:
- load the file in frama-c-gui
- tick Imact->Slicing after impact
- click somewhere on an equality sign in the code
- click "Set Selected"
## Attachments
- [client.i](/uploads/0a9c28d714a2f10e0ca19bc55a5a7322/client.i)
https://git.frama-c.com/pub/frama-c/-/issues/2391
Failure("Function 'From.find_deps_no_transitivity' not registered yet")
2021-02-22T13:58:03Z
mantis-gitlab-migration
Failure("Function 'From.find_deps_no_transitivity' not registered yet")
ID0000392:
**This issue was created automatically from Mantis Issue 392. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000392:
**This issue was created automatically from Mantis Issue 392. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000392 | Frama-C | Plug-in > Eva | public | 2010-02-03 | 2010-04-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | djs52 | **Assigned To** | pascal | **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 :
Attempting value analysis on a large code base, using -mem-exec to exclude some difficult functions. Running frama-c -val -mem-exec ... seems to complete without error; frama-c-gui with the same options fails with
Unexpected error (Failure("Function 'From.find_deps_no_transitivity' not registered yet"))
https://git.frama-c.com/pub/frama-c/-/issues/2386
Dgraph.DGraphModel.read_dot
2021-02-22T13:57:57Z
Sylvie Boldo
Dgraph.DGraphModel.read_dot
ID0000431:
**This issue was created automatically from Mantis Issue 431. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000431:
**This issue was created automatically from Mantis Issue 431. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000431 | Frama-C | Kernel | public | 2010-03-19 | 2010-04-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | sboldo | **Assigned To** | signoles | **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 :
Hello,
I try to compile the latest svn version (8087) but I can't. I have the following message:
File "src/gui/property_navigator.ml", line 50, characters 18-45:
Error: Unbound value Dgraph.DGraphModel.read_dot
make: *** [src/gui/property_navigator.cmo] Error 2
What my .configure gives is as attached file.
Probably a Makefile problem...
Regards,
Sylvie Boldo
## Attachments
- [toto](/uploads/41db4ba05d9983a1154e110b0d9b1be7/toto)
https://git.frama-c.com/pub/frama-c/-/issues/2377
Jessie translation fails with double assignment
2021-04-15T09:17:21Z
Victoria Moya Lamiel
Jessie translation fails with double assignment
ID0000450:
**This issue was created automatically from Mantis Issue 450. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000450:
**This issue was created automatically from Mantis Issue 450. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000450 | Frama-C | Plug-in > jessie | public | 2010-04-13 | 2010-04-19 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | vmoyalam | **Assigned To** | cmarche | **Resolution** | unable to reproduce |
| **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 :
Jessie crashes on the attached file.
WHY version : 2.21
command : "frama-c -jessie test4.c".
### Additional Information :
It seems there is a problem with double assignment.
Command-line output :
[kernel] preprocessing with "gcc -C -E -I. -dD test4.c"
[jessie] Starting Jessie translation
test4.c:13:[jessie] failure: Unexpected failure.
Please submit bug report (Ref. "interp.ml:1798:18").
[kernel] Plugin jessie aborted because of an internal error.
Please report with 'crash' at http://bts.frama-c.com
## Attachments
- [test4.c](/uploads/3184950f1379cfe6d9dfd2999f7d563d/test4.c)
https://git.frama-c.com/pub/frama-c/-/issues/2370
volatile annotation breaks type checker
2021-04-15T09:17:19Z
mantis-gitlab-migration
volatile annotation breaks type checker
ID0000480:
**This issue was created automatically from Mantis Issue 480. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000480:
**This issue was created automatically from Mantis Issue 480. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000480 | Frama-C | Plug-in > jessie | public | 2010-05-12 | 2010-05-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | tomahawkins | **Assigned To** | cmarche | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Boron-20100401 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Adding a volatile annotation on some variables breaks the type checker. (Why 2.26) For example:
#include <stdint.h>
// This works.
//int32_t a;
// This doesn't.
volatile int32_t a;
void f(double b) {
a = (int32_t) b;
}
Yields:
e0082888@e0082888-laptop:~$ frama-c -jessie test.c
[kernel] preprocessing with "gcc -C -E -I. -dD test.c"
[jessie] Starting Jessie translation
[jessie] Producing Jessie files in subdir test.jessie
[jessie] File test.jessie/test.jc written.
[jessie] File test.jessie/test.cloc written.
[jessie] Calling Jessie tool in subdir test.jessie
File "test.jc", line 34, characters 41-55: typing error: bad cast to integer
[jessie] user error: Jessie subprocess failed: jessie -why-opt -split-user-conj -v -locs test.cloc test.jc
Claude Marché
Claude Marché
https://git.frama-c.com/pub/frama-c/-/issues/2368
Segmentation fault: plugin reading from Cil_types
2021-02-22T13:57:25Z
mantis-gitlab-migration
Segmentation fault: plugin reading from Cil_types
ID0000481:
**This issue was created automatically from Mantis Issue 481. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000481:
**This issue was created automatically from Mantis Issue 481. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000481 | Frama-C | Kernel | public | 2010-05-17 | 2010-05-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | tomahawkins | **Assigned To** | signoles | **Resolution** | no change required |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | Ubuntu Linux x86 10.04 | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Boron-20100401 | **Target Version** | - | **Fixed in Version** | - |
### Description :
A plugin that reads data from the Cil_types module, trips a segmentation fault.
The plugin reads all data from the Cil_types module. Are there any values in Cil_types that are invalid to read, and which would cause a segfault when referenced?
Attached in the plugin (dump_cil.ml), the Makefile to build and install the pluging, and a test file (plugin_segfaults.c) that demonstrates C syntax that works and syntax that segfaults.
## Attachments
- [dump_cil.ml](/uploads/0bfe6c9ea6268fa512807fdce430eb7b/dump_cil.ml)
- [Makefile](/uploads/ab42f3de07a524bf5d522f26ce035b5c/Makefile)
- [plugin_segfaults.c](/uploads/b7438400154254b45333b8a2f174649d/plugin_segfaults.c)
https://git.frama-c.com/pub/frama-c/-/issues/2328
Jessie translation unexpected failure
2021-04-15T09:17:24Z
Victoria Moya Lamiel
Jessie translation unexpected failure
ID0000410:
**This issue was created automatically from Mantis Issue 410. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000410:
**This issue was created automatically from Mantis Issue 410. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000410 | Frama-C | Plug-in > jessie | public | 2010-02-17 | 2010-12-09 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | vmoyalam | **Assigned To** | cmarche | **Resolution** | duplicate |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090902 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Jessie crashes on the attached file.
WHY version : 2.21
command : "frama-c -jessie test.c".
### Additional Information :
It seems there is a problem with structure comparisons.
Command-line output :
[kernel] preprocessing with "gcc -C -E -I. -dD test.c"
[jessie] Starting Jessie translation
test.c:14:[jessie] failure: Unexpected failure.
Please submit bug report (Ref. "interp.ml:631:14").
[kernel] Plugin jessie aborted because of an internal error.
Please report with 'crash' at http://bts.frama-c.com
## Attachments
- [test.c](/uploads/f198f20d8a427daa21da709b89e888a4/test.c)
https://git.frama-c.com/pub/frama-c/-/issues/2325
error in analyzing xen 4.0.0 code
2021-02-22T13:56:34Z
mantis-gitlab-migration
error in analyzing xen 4.0.0 code
ID0000516:
**This issue was created automatically from Mantis Issue 516. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000516:
**This issue was created automatically from Mantis Issue 516. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000516 | Frama-C | Plug-in > Eva | public | 2010-06-19 | 2010-12-10 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | amkhalid | **Assigned To** | pascal | **Resolution** | unable to reproduce |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
[kernel] Parsing stage early
[kernel] Parsing stage extending
[kernel] Parsing stage extended
[kernel] Parsing stage exiting
[kernel] Parsing stage loading
[kernel] Parsing stage configuring
[kernel] preprocessing with "gcc -C -E -I. -I/home/ak729/xen-4.0.0/xen/include/ /home/ak729/xen-4.0.0/xen/common/kernel.c"
/home/ak729/xen-4.0.0/xen/include/public/domctl.h:51:[kernel] user error: syntax error
[kernel] The full backtrace is:
[kernel] Raised at file "cil/src/frontc/frontc.ml", line 209, characters 9-28
[kernel] Called from file "cil/src/frontc/frontc.ml", line 124, characters 13-38
[kernel] Called from file "cil/src/frontc/frontc.ml", line 263, characters 13-32
[kernel] Called from file "src/kernel/file.ml", line 546, characters 27-46
[kernel] Called from file "src/kernel/file.ml", line 582, characters 16-23
[kernel] Re-raised at file "src/kernel/file.ml", line 585, characters 52-55
[kernel] Called from file "list.ml", line 74, characters 24-34
[kernel] Called from file "src/kernel/file.ml", line 579, characters 6-314
[kernel] Called from file "src/kernel/file.ml", line 1027, characters 12-30
[kernel] Called from file "src/kernel/file.ml", line 1108, characters 4-27
[kernel] Called from file "src/kernel/ast.ml", line 57, characters 29-45
[kernel] Called from file "src/project/computation.ml", line 108, characters 17-21
[kernel] Called from file "src/kernel/file.ml", line 1147, characters 12-22
[kernel] Called from file "src/project/project.ml", line 432, characters 12-15
[kernel] Re-raised at file "src/project/project.ml", line 437, characters 10-11
[kernel] Called from file "src/kernel/boot.ml", line 44, characters 33-47
[kernel] Called from file "src/kernel/cmdline.ml", line 170, characters 4-8
[kernel]
[kernel] Unexpected error (Parsing.Parse_error).
[kernel] Please report as 'crash' at http://bts.frama-c.com