frama-c issues
https://git.frama-c.com/pub/frama-c/-/issues
2021-02-22T14:01:23Z
https://git.frama-c.com/pub/frama-c/-/issues/307
predicate overloading causes crash when multiple files are given to wp
2021-02-22T14:01:23Z
Jochen Burghardt
predicate overloading causes crash when multiple files are given to wp
ID0002151:
**This issue was created automatically from Mantis Issue 2151. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002151:
**This issue was created automatically from Mantis Issue 2151. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002151 | Frama-C | Kernel > ACSL implementation | public | 2015-07-30 | 2017-12-06 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | duplicate |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | Sodium-20150201 | **OS** | xubuntu14.04 | **OS Version** | - |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | Frama-C GIT, precise the release id |
### Description :
Running "frama-c -wp 481a.c 481b.c" on the attached files causes a crash with following output:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing 481a.c (with preprocessing)
[kernel] Parsing 481b.c (with preprocessing)
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[wp] warning: Missing RTE guards
[kernel] Current source was: 481b.c:9
The full backtrace is:
Raised at file "map.ml", line 117, characters 16-25
Called from file "list.ml", line 55, characters 20-23
Called from file "src/wp/LogicCompiler.ml", line 776, characters 17-61
Called from file "src/wp/Warning.ml", line 139, characters 6-10
Called from file "src/wp/LogicSemantics.ml", line 813, characters 12-42
Called from file "src/wp/Context.ml", line 31, characters 12-17
Re-raised at file "src/wp/Context.ml", line 34, characters 41-46
Called from file "src/wp/Warning.ml", line 155, characters 14-18
Called from file "src/wp/cfgWP.ml", line 462, characters 23-140
Called from file "src/wp/Context.ml", line 68, characters 14-17
Re-raised at file "src/wp/Context.ml", line 69, characters 43-48
Called from file "src/wp/Context.ml", line 68, characters 14-17
Re-raised at file "src/wp/Context.ml", line 69, characters 43-48
Called from file "src/wp/Context.ml", line 68, characters 14-17
Re-raised at file "src/wp/Context.ml", line 69, characters 43-48
Called from file "src/wp/Context.ml", line 68, characters 14-17
Re-raised at file "src/wp/Context.ml", line 69, characters 43-48
Called from file "list.ml", line 84, characters 24-34
Called from file "src/wp/calculus.ml", line 331, characters 22-64
Called from file "src/wp/calculus.ml", line 341, characters 23-45
Called from file "src/wp/calculus.ml", line 613, characters 20-43
Called from file "src/wp/calculus.ml", line 536, characters 19-40
Called from file "src/wp/calculus.ml", line 586, characters 20-43
Called from file "src/wp/calculus.ml", line 536, characters 19-40
Called from file "src/wp/calculus.ml", line 589, characters 20-43
Called from file "src/wp/calculus.ml", line 536, characters 19-40
Called from file "src/wp/calculus.ml", line 589, characters 20-43
Called from file "src/wp/calculus.ml", line 536, characters 19-40
Called from file "src/wp/calculus.ml", line 579, characters 20-43
Called from file "src/wp/calculus.ml", line 536, characters 19-40
Called from file "src/wp/calculus.ml", line 574, characters 20-43
Called from file "src/wp/calculus.ml", line 536, characters 19-40
Called from file "src/wp/calculus.ml", line 724, characters 40-59
Called from file "set.ml", line 304, characters 38-41
Called from file "map.ml", line 168, characters 20-25
Called from file "map.ml", line 168, characters 10-18
Called from file "map.ml", line 168, characters 10-18
Called from file "src/wp/calculus.ml", line 724, characters 4-64
Called from file "src/wp/calculus.ml", line 770, characters 19-51
Called from file "src/wp/cfgWP.ml", line 1402, characters 39-62
Called from file "src/wp/cfgWP.ml", line 1391, characters 14-837
Called from file "src/wp/Model.ml", line 111, characters 17-20
Re-raised at file "src/wp/Model.ml", line 116, characters 25-28
Called from file "src/wp/Model.ml", line 117, characters 19-36
Called from file "src/wp/register.ml", line 435, characters 15-40
Called from file "src/wp/register.ml", line 574, characters 17-24
Re-raised at file "src/wp/register.ml", line 578, characters 27-29
Called from file "src/wp/register.ml", line 575, characters 17-24
Re-raised at file "src/wp/register.ml", line 579, characters 30-32
Called from file "src/wp/register.ml", line 575, characters 17-24
Re-raised at file "src/wp/register.ml", line 579, characters 30-32
Called from file "queue.ml", line 134, characters 6-20
Called from file "src/kernel/boot.ml", line 37, characters 4-20
Called from file "src/kernel/cmdline.ml", line 763, characters 2-9
Called from file "src/kernel/cmdline.ml", line 216, characters 4-8
Unexpected error (Not_found).
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Sodium-20150201.
## Attachments
- [481a.c](/uploads/bbfbbd240806e1f43941db309a86ecd8/481a.c)
- [481b.c](/uploads/6eb9eab3b5ff4466235f341d5f87e5c4/481b.c)
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/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/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/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
https://git.frama-c.com/pub/frama-c/-/issues/2253
Error during plugin compilation
2021-02-22T13:54:59Z
mantis-gitlab-migration
Error during plugin compilation
ID0000681:
**This issue was created automatically from Mantis Issue 681. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000681:
**This issue was created automatically from Mantis Issue 681. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000681 | Frama-C | Kernel > Makefile | public | 2011-01-21 | 2011-01-24 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | CFaure | **Assigned To** | signoles | **Resolution** | won't fix |
| **Priority** | normal | **Severity** | block | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Boron-20100401 | **Target Version** | - | **Fixed in Version** | - |
### Description :
I made a custom install of Frama-C with
DESTDIR=/home/faure/frama-c/frama-c-install.
I tries to compile a plugin with a Makefile built as described in the manual.
But I got errors and nothing got compiled.
Then I modified the makefile as described in additional information: I mainly added modified the values of FRAMAC_SHARE and FRAMAC_LIBDIR because the paths where wrong.
The make got further but I finally got a link error:
Linking frama-c-Saferiver.byte
Cannot find file /usr/local/lib/frama-c/boot.cmo
make: *** [frama-c-Saferiver.byte] Error 2
### Additional Information :
# Frama-c should be properly installed with "make install
# before any use of this makefile
DESTDIR=/home/faure/frama-c/frama-c-install
FRAMAC_BIN=$(DESTDIR)/usr/local/bin
FRAMAC_SHARE :=$(shell $(FRAMAC_BIN)/frama-c.byte -print-path)
FRAMAC_LIBDIR :=$(shell $(FRAMAC_BIN)/frama-c.byte -print-libpath)
PLUGIN_NAME = Saferiver
PLUGIN_CMO = register
FRAMAC_SHARE := $(DESTDIR)/$(FRAMAC_SHARE)
FRAMAC_LIBDIR := $(DESTDIR)/$(FRAMAC_LIBDIR)
include $(FRAMAC_SHARE)/Makefile.dynamic
https://git.frama-c.com/pub/frama-c/-/issues/2245
Gui crash with a new global variable
2021-02-22T13:54:44Z
Victoria Moya Lamiel
Gui crash with a new global variable
ID0000700:
**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/2221
The procedure entry point freeaddrinfo could not be located in the dynamic li...
2021-02-22T13:54:08Z
mantis-gitlab-migration
The procedure entry point freeaddrinfo could not be located in the dynamic link library WS2_32.dll
ID0000534:
**This issue was created automatically from Mantis Issue 534. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000534:
**This issue was created automatically from Mantis Issue 534. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000534 | Frama-C | Graphical User Interface | public | 2010-07-08 | 2011-03-31 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | chris | **Assigned To** | monate | **Resolution** | suspended |
| **Priority** | normal | **Severity** | block | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Boron-20100401 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Upon double-clicking on the desktop icon of Frama-C on a Win2K box, I get the error:
"The procedure entry point freeaddrinfo could not be located in the dynamic link library WS2_32.dll"
This is a show stopper.
### Additional Information :
You have to take additional measures so that the GUI runs on Win2K. These are described in:
http://support.microsoft.com/kb/822334 (regards FreeAddrInfoW)
http://pressf1.pcworld.co.nz/archive/index.php/t-50226.html (exact same error)
https://git.frama-c.com/pub/frama-c/-/issues/2217
Signature mismatch errors while compiling simple "hello world" plug-in
2021-02-22T13:54:02Z
mantis-gitlab-migration
Signature mismatch errors while compiling simple "hello world" plug-in
ID0000777:
**This issue was created automatically from Mantis Issue 777. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000777:
**This issue was created automatically from Mantis Issue 777. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000777 | Frama-C | Kernel > Makefile | public | 2011-04-07 | 2011-04-07 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | njucslzh | **Assigned To** | signoles | **Resolution** | no change required |
| **Priority** | normal | **Severity** | block | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Boron-20100401 | **Target Version** | - | **Fixed in Version** | Frama-C Carbon-20110201 |
### Description :
ocamlc -c -I . -w Z -warn-error A -annot -g -I "/usr/lib/frama-c" -I /usr/lib/frama-c hello_world.ml
File "hello_world.ml", line 63, characters 5-132:
Error: Signature mismatch:
Modules do not match:
sig val name : string val shortname : string val help : string end
is not included in
sig val name : string val shortname : string val descr : string end
The field `descr' is required but not provided
make: *** [hello_world.cmo] ?? 2
### Additional Information :
OS:Ubuntu 10.10
OCaml:3.11.2
I changed the file /usr/share/frama-c/Makefile.config :
# compilers and others executables
OCAMLC ?=ocamlc
OCAMLOPT ?=ocamlopt
OCAMLDEP ?=ocamldep -slash
OCAMLLEX ?=ocamllex
OCAMLYACC ?=ocamlyacc
OCAMLMKTOP ?=ocamlmktop
OCAMLDOC ?=ocamldoc
OCAMLCP ?=ocamlcp
https://git.frama-c.com/pub/frama-c/-/issues/2210
Unexpected error (Failure("int_of_string")).
2021-02-22T13:53:46Z
John Regher
Unexpected error (Failure("int_of_string")).
ID0000701:
**This issue was created automatically from Mantis Issue 701. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000701:
**This issue was created automatically from Mantis Issue 701. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000701 | Frama-C | Plug-in > wp | public | 2011-02-02 | 2011-04-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | regehr | **Assigned To** | correnson | **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 Carbon-20110201 |
### Description :
Seen on Ubuntu 10.10 on x86. OCaml and related packages are all from Ubuntu, I don't think I've customized anything in particular on this machine.
regehr@home:~/csmith/runtime$ frama-c -wp -wp-rte add.c
[kernel] preprocessing with "gcc -C -E -I. add.c"
[rte] annotating function safe_add
[rte] annotating function unsafe_add
[kernel] The full backtrace is:
Raised at file "src/kernel/command.ml", line 42, characters 10-13
Called from file "src/wp/cfgProof.ml", line 125, characters 4-118
Called from file "list.ml", line 69, characters 12-15
Called from file "list.ml", line 69, characters 12-15
Called from file "list.ml", line 69, characters 12-15
Called from file "list.ml", line 69, characters 12-15
Called from file "src/wp/cfgProof.ml", line 223, characters 1-607
Called from file "src/wp/register.ml", line 322, characters 41-57
Called from file "src/wp/register.ml", line 464, characters 3-32
Called from file "src/wp/register.ml", line 533, characters 8-20
Called from file "src/wp/register.ml", line 570, characters 4-18
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 660, characters 2-9
Called from file "src/kernel/cmdline.ml", line 173, characters 4-8
Unexpected error (Failure("int_of_string")).
Please report as 'crash' at http://bts.frama-c.com/
Note that 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
regehr@home:~/csmith/runtime$ cat add.c
int unsafe_add (int a, int b)
{
return a+b;
}
int safe_add (int si1, int si2)
{
return
(((si1>0) && (si2>0) && (si1 > ((2147483647)-si2))) || ((si1<0) && (si2<0) && (si1 < ((-2147483647-1)-si2)))) ?
((si1)) :
(si1 + si2);
}
https://git.frama-c.com/pub/frama-c/-/issues/2205
Unexpected error (Stack overflow) during WP
2021-02-22T13:53:36Z
Benjamin Monate
Unexpected error (Stack overflow) during WP
ID0000665:
**This issue was created automatically from Mantis Issue 665. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000665:
**This issue was created automatically from Mantis Issue 665. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000665 | Frama-C | Plug-in > wp | public | 2011-01-10 | 2011-04-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | monate | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20101202-beta2 | **Target Version** | Frama-C Carbon-20110201 | **Fixed in Version** | Frama-C Carbon-20110201 |
### Description :
On this file (inspired by bts#654):
frama-c.byte -wp -wp-proof alt-ergo 654.c
crashes with a stack overflow.
===========
typedef unsigned long u64;
struct range {
u64 start;
u64 end;
};
#define min(a,b) ((a < b) ? a : b)
#define max(a,b) ((a > b) ? a : b)
int add_range(struct range *range, int az, int nr_range, u64 start, u64 end);
int add_range_with_merge(struct range *range, int az, int nr_range,
u64 start, u64 end);
void subtract_range(struct range *range, int az, u64 start, u64 end);
/*@ predicate isSorted(struct range* ranges, integer length) =
@ length <= 1 ||
@ (\forall integer idx; 0 <= idx < length-1 ==> ranges[idx].start <= ranges[idx + 1].start);
@
@ logic integer appears{L}(struct range* ranges, integer length, integer istart, integer iend) =
@ length <= 0
@ ? 0
@ : (istart == ranges[0].start && iend == ranges[0].end)
@ ? 1 + appears(ranges + 1, length - 1, istart, iend)
@ : appears(ranges + 1, length - 1, istart, iend);
@*/
/*@ requires az >= 0;
@ requires \valid(range+ (0..az-1));
@
@ assigns *(range+ (0..az-1));
@
@ ensures \forall integer i; 0 <= i < az ==>
@ appears(range, az, range[i].start, range[i].end) == \old(appears(range, az, range[i].start, range[i].end));
@ ensures isSorted(range, az);
@*/
void sort(struct range *range, int az) ;
/*@ logic integer nemptyCount{L}(struct range* ranges, integer length) =
@ length <= 0
@ ? 0
@ : ranges[0].end == 0
@ ? nemptyCount(ranges + 1, length - 1)
@ : 1 + nemptyCount(ranges + 1, length - 1);
@
@ logic integer emptyCount{L}(struct range* ranges, integer length) =
@ length - nemptyCount(ranges, length);
@*/
/*@ requires az >= 0;
@ requires \valid(range+ (0..az-1));
@
@ assigns *(range+ (0..az-1));
@
@ ensures \result == nemptyCount(range, az);
@ ensures isSorted(range, \result);
@ ensures \forall integer i; 0 <= i < \result ==>
@ appears(range, \result, range[i].start, range[i].end) == \old(appears(range, az, range[i].start, range[i].end));
@*/
int clean_range(struct range *range, int az)
{
int i, j, k = az - 1, nr_range = az;
/*@
@
@ loop invariant 0 <= i <= k;
@ loop invariant emptyCount(range, i) == 0;
@ loop invariant emptyCount(range, az) == \at(emptyCount(range, az), Pre);
@ loop invariant az-1-emptyCount(range, az) <= k <= az-1;
@ loop invariant \forall integer idx; (0 <= idx < az) &&
@ \at(range[idx].end != 0, Pre) ==>
@ appears(range, az, \at(range[idx].start, Pre), \at(range[idx].end, Pre))
@ == \at(appears(range, az, \at(range[idx].start, Pre), \at(range[idx].end, Pre)), Pre);
loop variant k - i;
@*/
for (i = 0; i < k; i++) {
if (range[i].end)
continue;
/*@
@
@ loop invariant i <= j <= k;
@ loop invariant \forall integer idx; j < idx < az ==> range[idx].end == 0;
loop variant j;
@*/
for (j = k; j > i; j--) {
if (range[j].end) {
k = j;
break;
}
}
if (j == i)
break;
range[i].start = range[k].start;
range[i].end = range[k].end;
range[k].start = 0;
range[k].end = 0;
k--;
}
/*@
@
@ loop invariant 0 <= i <= emptyCount(range, az);
loop variant i;
@*/
/* count it */
for (i = 0; i < az; i++) {
if (!range[i].end) {
nr_range = i;
break;
}
}
/*@ assert nr_range == emptyCount(range, az);
@*/
sort(range,nr_range);
return nr_range;
}
https://git.frama-c.com/pub/frama-c/-/issues/2158
Value analysis crashes in lib-entry mode with peculiar context
2021-02-22T13:52:25Z
David Delmas
Value analysis crashes in lib-entry mode with peculiar context
ID0000820:
**This issue was created automatically from Mantis Issue 820. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000820:
**This issue was created automatically from Mantis Issue 820. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000820 | Frama-C | Plug-in > Eva | public | 2011-05-11 | 2011-10-10 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | ddelmas | **Assigned To** | pascal | **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 :
A crash occurs with command :
frama-c -val -lib-entry -main F -context-width 1 -context-depth 0 crash_align.c
### Additional Information :
The analysis does not crash with -context-depth 1.
## Attachments
- [crash_align.c](/uploads/27c1eb98ff6f0ccd59f2698b84ba9167/crash_align.c)
https://git.frama-c.com/pub/frama-c/-/issues/2143
Impact analysis does not catch Pdg.Top (returned on variadic calls)
2021-02-22T13:52:06Z
Boris Yakobowski
Impact 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/2142
frama-c always crashes when I install new plugins
2021-02-22T13:52:05Z
mantis-gitlab-migration
frama-c always crashes when I install new plugins
ID0000737:
**This issue was created automatically from Mantis Issue 737. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000737:
**This issue was created automatically from Mantis Issue 737. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000737 | Frama-C | Kernel | public | 2011-02-28 | 2011-10-10 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | smaulat | **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 :
The crash happens when I try to install two "hello" plugins (as explained in the plugin-development-guide-Carbon-20110201.pdf): i.e. two plgins with the same short name.
Once I have tried to do this, frama-c always returns the same error, also when I don't give it any argument.
## Attachments
- [frama-c_crash_20110228_hello.tr](/uploads/50e7703c5f07df04ac9f1e2d5c807587/frama-c_crash_20110228_hello.tr)