frama-c issues
https://git.frama-c.com/pub/frama-c/-/issues
2021-02-22T13:46:43Z
https://git.frama-c.com/pub/frama-c/-/issues/1937
wrong ELF class: ELFCLASS64
2021-02-22T13:46:43Z
mantis-gitlab-migration
wrong ELF class: ELFCLASS64
ID0001294:
**This issue was created automatically from Mantis Issue 1294. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001294:
**This issue was created automatically from Mantis Issue 1294. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001294 | Frama-C | Graphical User Interface | public | 2012-11-02 | 2012-12-06 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | ngong | **Assigned To** | monate | **Resolution** | no change required |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Nitrogen-20111001 | **Target Version** | - | **Fixed in Version** | - |
### Description :
after installing package frama-c on Debian SID 64 bit, the command
frama-c-gui -slevel 10 -val p.c
led to the failure message
frama-c-gui: error while loading shared libraries: libgtksourceview-2.0.so.0: wrong ELF class: ELFCLASS64
and did not show anything else.
I expected to see what is mentioned on page http://frama-c.com/try_out.html
https://git.frama-c.com/pub/frama-c/-/issues/1918
Project menu is empty when Ubuntu/Unity is enabled
2021-02-22T13:46:07Z
Benjamin Monate
Project menu is empty when Ubuntu/Unity is enabled
ID0001182:
**This issue was created automatically from Mantis Issue 1182. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001182:
**This issue was created automatically from Mantis Issue 1182. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001182 | Frama-C | Graphical User Interface | public | 2012-05-25 | 2013-01-25 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | monate | **Assigned To** | monate | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Nitrogen-20111001 | **Target Version** | - | **Fixed in Version** | Frama-C Oxygen-20120901 |
### Description :
When unity is enabled and the main menubar of Frama-C is shown detached from its main window, the dynamic menu entries are not visible.
This can be fixed by setting the environment variable UBUNTU_MENUPROXY to 0.
For example :
UBUNTU_MENUPROXY=0 frama-c-gui
fixes the problem.
No solution is known to fix this on the Frama-C side.
https://git.frama-c.com/pub/frama-c/-/issues/1836
"src/project/project.ml", line 678 Assertion failed
2021-02-22T13:43:43Z
mantis-gitlab-migration
"src/project/project.ml", line 678 Assertion failed
ID0001464:
**This issue was created automatically from Mantis Issue 1464. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001464:
**This issue was created automatically from Mantis Issue 1464. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001464 | Frama-C | Graphical User Interface | public | 2013-07-29 | 2013-08-01 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | barries | **Assigned To** | - | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Boron-20100401 | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
Steps to reproduce:
1. Project -> default -> Duplicate project
2. Save As "test.frama" (any name will do; test.frama attached to issue)
3. Project -> Load project -> "test.frama"
4. Observe Error dialog:
The full backtrace is:
Called from file "src/kernel/journal.ml", line 323, characters 15-26
Re-raised at file "src/kernel/journal.ml", line 338, characters 14-15
Called from file "src/gui/project_manager.ml", line 131, characters 18-34
Called from file "src/lib/extlib.ml", line 176, characters 12-15
Re-raised at file "src/lib/extlib.ml", line 181, characters 10-11
Called from file "src/gui/gtk_helper.ml", line 533, characters 8-385
Unexpected error (File "src/project/project.ml", line 678, characters 24-30: Assertion failed).
Please report as 'crash' at http://bts.frama-c.com
### Additional Information :
I'm a new user and may well be skipping some key step.
## Attachments
- [test.frama](/uploads/5006aaf758fc35d237fb6b231cdd86fc/test.frama)
https://git.frama-c.com/pub/frama-c/-/issues/1757
Selection of [loop variant] properties in GUI
2021-02-22T13:40:26Z
mantis-gitlab-migration
Selection of [loop variant] properties in GUI
ID0000724:
**This issue was created automatically from Mantis Issue 724. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000724:
**This issue was created automatically from Mantis Issue 724. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000724 | Frama-C | Graphical User Interface | public | 2011-02-16 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Anne | **Assigned To** | monate | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
The [loop variant] properties are not correctly identified when asking to compute WP on them.
### Additional Information :
Try for instance : frama-c-gui tests/wp/wp_loop.c -wp-verbose 3
and observe the "Console" window. Then calling Wp on the [loop variant] in [loop_var] function for instance, we get :
[wp] [wpAnnot.get_strategies] for behaviors names: default!
[wp] [wpAnnot.get_strategies] select stmt 148 properties
tests/wp/wp_loop.c:178:[wp] warning: [wpAnnot.get_strategies] no behaviors found
Compare for instance with the [loop assigns] property which works :
[wp] build strategy for 'loop_var', behavior 'default!', property loop_assigns_148, both assigns or not
[wp] [wp-cfg] start computing with the strategy for 'loop_var', behavior 'default!', property loop_assigns_148, both assigns or not
It also works normally for [loop invariant]...
When the WP is computed for the whole function, the [loop variant] is processed normally, and its green V mark is correctly set.
https://git.frama-c.com/pub/frama-c/-/issues/1747
Wrong evaluation of expression in the GUI
2021-02-22T13:40:06Z
Julien Signoles
Wrong evaluation of expression in the GUI
ID0000666:
**This issue was created automatically from Mantis Issue 666. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000666:
**This issue was created automatically from Mantis Issue 666. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000666 | Frama-C | Graphical User Interface | public | 2011-01-11 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | signoles | **Assigned To** | pascal | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20101202-beta2 | **Target Version** | - | **Fixed in Version** | Frama-C Carbon-20110201 |
### Description :
When evaluating an expression in the GUI, the result "After statement" seems to be equal to the result "Before statement" in some cases (e.g. if the statement is a conditional). Of course, that is incorrect in the general cases.
### Steps To Reproduce :
Consider the following program:
==========
int t[2], c;
void main(void) {
t[0] = 0;
t[1] = 0;
if (c) t[0] = 1; else t[0] = 2;
t[1] += t[0];
}
==========
1) Run the GUI with options -val -lib-entry on this program.
2) Left-click at the end of the line containing "if". The information panel indicates that this line modifies t[0]: good.
3) Right-click at the end of the line containing "if" and select "Evaluate expression".
4) Enter "t[0]" as expression.
5) the information panel indicates that t[0] is equal to 0 after this statement. Quite bad, doesn't it?
Note: before statement "t[1] += t[0]", t[0] is 1 or 2: that is ok and that is the expected result after the conditional...
https://git.frama-c.com/pub/frama-c/-/issues/1706
Exception raised if dot not found
2021-02-22T14:03:08Z
Julien Signoles
Exception raised if dot not found
ID0000517:
**This issue was created automatically from Mantis Issue 517. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000517:
**This issue was created automatically from Mantis Issue 517. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000517 | Frama-C | Graphical User Interface | public | 2010-06-22 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | signoles | **Assigned To** | monate | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Boron-20100401 | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
Should check dynamically if dot is executable before trying to run it.
https://git.frama-c.com/pub/frama-c/-/issues/1677
In the GUI, it is impossible to talk about variables generated by Value's -li...
2021-02-22T13:37:43Z
Pascal Cuoq
In the GUI, it is impossible to talk about variables generated by Value's -lib-entry
ID0000470:
**This issue was created automatically from Mantis Issue 470. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000470:
**This issue was created automatically from Mantis Issue 470. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000470 | Frama-C | Graphical User Interface | public | 2010-05-05 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | pascal | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Boron-20100401 | **Target Version** | - | **Fixed in Version** | Frama-C Carbon-20101201-beta1 |
### Description :
"evaluate expression", "occurrences" and "Show defs", for instance, when tried on such a variable, emit the error message "Invalid expression: Logic_interp.Error(_, "Unbound variable star_CompositionPage")"
### Additional Information :
To leave public.
https://git.frama-c.com/pub/frama-c/-/issues/1607
Warning repetition in Messages window
2021-02-22T13:35:48Z
mantis-gitlab-migration
Warning repetition in Messages window
ID0000237:
**This issue was created automatically from Mantis Issue 237. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000237:
**This issue was created automatically from Mantis Issue 237. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000237 | Frama-C | Graphical User Interface | public | 2009-09-10 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pherrmann | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | urgent | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090901 | **Target Version** | Frama-C Beryllium-20090902 | **Fixed in Version** | Frama-C Beryllium-20090902 |
### Description :
The exact same warning is repeated a number of times (10+) in the "Messages" window of the GUI.
### Additional Information :
For the file in attachment : I get several "out of bound read ..." at line 5 after value analysis.
## Attachments
- [oob.c](/uploads/d6f46d358e06b20fbd20e8924e0370ff/oob.c)
https://git.frama-c.com/pub/frama-c/-/issues/1601
Error when linking the viewer
2021-02-22T13:35:41Z
mantis-gitlab-migration
Error when linking the viewer
ID0000236:
**This issue was created automatically from Mantis Issue 236. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000236:
**This issue was created automatically from Mantis Issue 236. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000236 | Frama-C | Graphical User Interface | public | 2009-09-10 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | mehdi | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090901 | **Target Version** | - | **Fixed in Version** | Frama-C Beryllium-20090902 |
### Description :
Hello,
When compiling the viewer with a system installation of ocamlgraph, I get this error:
Linking bin/viewer.byte
File "_none_", line 1, characters 0-1:
Error: Error while linking lib/gui/Syntactic_callgraph.cmo:
Reference to undefined global `DGraphView'
Please find attached a patch that fixes the issue.
Kind regards,
## Attachments
- [0003-Add-dGraphView.cmo-when-linking.patch](/uploads/d5a3ba7e06dc4bc6a70fda430039b968/0003-Add-dGraphView.cmo-when-linking.patch)
https://git.frama-c.com/pub/frama-c/-/issues/1600
Files of a project state not displayed on reload in GUI
2021-02-22T13:35:39Z
mantis-gitlab-migration
Files of a project state not displayed on reload in GUI
ID0000238:
**This issue was created automatically from Mantis Issue 238. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000238:
**This issue was created automatically from Mantis Issue 238. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000238 | Frama-C | Graphical User Interface | public | 2009-09-11 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pherrmann | **Assigned To** | monate | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090901 | **Target Version** | - | **Fixed in Version** | Frama-C Beryllium-20090902 |
### Description :
After creating a project consisting of a single file plus a standard value analysis in frama-c-gui :
- save the state
- quit the gui
- relaunch the gui
- load the state
The files belonging in the project are not displayed in the left tab.
### Additional Information :
The results of the analysis seem to be available after loading a state (in particular the call graph can be displayed).
https://git.frama-c.com/pub/frama-c/-/issues/1534
"-cpp-command ..." parameter lost
2021-02-22T13:34:08Z
mantis-gitlab-migration
"-cpp-command ..." parameter lost
ID0000374:
**This issue was created automatically from Mantis Issue 374. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000374:
**This issue was created automatically from Mantis Issue 374. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000374 | Frama-C | Graphical User Interface | public | 2010-01-18 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pherrmann | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **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 :
(release id 7362)
The kernel parameter "-cpp-command" is lost when creating new projects.
In GUI : set "-cpp-command" parameter (either through command-line, or using "Ctrl-R/kernel/Customizing Normalization") in order to point to Frama-C "libc" directory.
Create a new Projet and select file "need_builtin.c" (attached) : preprocessing is OK.
Check "cpp-command" parameter value with "Ctrl-R" : it has become blank.
Create a new Project and select file "need_builtin.c" : preprocessing fails.
### Additional Information :
The attached archive also contains the journalization file.
## Attachments
- [bugParams.tar.gz](/uploads/53f42ffa4a1a23414664a6a88d243035/bugParams.tar.gz)
https://git.frama-c.com/pub/frama-c/-/issues/1531
'Go to definition' and 'Go to caller' do not update main view of GUI
2021-02-22T13:34:04Z
Virgile Prevosto
'Go to definition' and 'Go to caller' do not update main view of GUI
ID0000242:
**This issue was created automatically from Mantis Issue 242. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000242:
**This issue was created automatically from Mantis Issue 242. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000242 | Frama-C | Graphical User Interface | public | 2009-09-14 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | virgile | **Assigned To** | monate | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090901 | **Target Version** | - | **Fixed in Version** | Frama-C Beryllium-20090902 |
### Description :
In the GUI, Using the menu 'Go to definition' and 'Go to caller' correctly
updates the tree panel (unfolding the appropriate file entry) but does not select the function, and does not update the source view in the middle panel.
### Additional Information :
gtk version: 2.16.1 (Ubuntu 9.04)
lablgtk version: 2.12.0
https://git.frama-c.com/pub/frama-c/-/issues/1451
value analysis warning disappears from 'Messages' window in gui after 'Repars...
2021-02-22T13:31:50Z
Jochen Burghardt
value analysis warning disappears from 'Messages' window in gui after 'Reparse' button clicked
ID0001104:
**This issue was created automatically from Mantis Issue 1104. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001104:
**This issue was created automatically from Mantis Issue 1104. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001104 | Frama-C | Graphical User Interface | public | 2012-02-24 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Nitrogen-20111001 | **Target Version** | - | **Fixed in Version** | Frama-C Oxygen-20120901 |
### Description :
Under Mac OS X Version 10.6.8, I ran "frama-c-gui -val exm02.c" on the attached program. In the "Messages" window of the Frama-C gui, an overflow warning is displayed for line 4, which is ok.
After clicking on the "Reparse" button, that message disappears, although nothing has been changed in the source code. Even after clicking on the "Analyses" button and clicking on the "Execute" button in the popped-up window "Launching analysis", the overflow warning doesn't appear again.
## Attachments
- [exm02.c](/uploads/d06012dc33809c4967f807411658345d/exm02.c)
https://git.frama-c.com/pub/frama-c/-/issues/1437
Opening consolidation graph crashes when 'dot' is missing
2021-02-22T14:03:08Z
Julien Signoles
Opening consolidation graph crashes when 'dot' is missing
ID0001122:
**This issue was created automatically from Mantis Issue 1122. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001122:
**This issue was created automatically from Mantis Issue 1122. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001122 | Frama-C | Graphical User Interface | public | 2012-03-19 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | signoles | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Nitrogen-20111001 | **Target Version** | - | **Fixed in Version** | Frama-C Oxygen-20120901 |
### Description :
All in the title. Was previously fixed for the callgraph.
https://git.frama-c.com/pub/frama-c/-/issues/1251
r11920: Analyses -> Show callgraph requires a main function
2023-05-02T09:30:27Z
Pascal Cuoq
r11920: Analyses -> Show callgraph requires a main function
ID0000723:
**This issue was created automatically from Mantis Issue 723. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000723:
**This issue was created automatically from Mantis Issue 723. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000723 | Frama-C | Graphical User Interface | public | 2011-02-15 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
Launch the GUI on a C file without a main():
bin/viewer.opt tests/idct/idct.c
Select Analyses -> Show callgraph
Result:
[kernel] preprocessing with "gcc -C -E -I. tests/idct/idct.c"
[cg] beginning analysis
[gui] user error: cannot find entry point `main'.
Please use option `-main' for specifying a valid entry point.
Considering that the syntactic callgraph is most useful to find which function is the entry point, this is annoying.
https://git.frama-c.com/pub/frama-c/-/issues/916
Gui unusable if value analysis degenerates
2021-02-22T14:02:21Z
Boris Yakobowski
Gui unusable if value analysis degenerates
ID0000684:
**This issue was created automatically from Mantis Issue 684. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000684:
**This issue was created automatically from Mantis Issue 684. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000684 | Frama-C | Graphical User Interface | public | 2011-01-24 | 2015-01-07 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | yakobowski | **Assigned To** | monate | **Resolution** | duplicate |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20101202-beta2 | **Target Version** | - | **Fixed in Version** | - |
### Description :
If frama-c is started with -val, and the value analysis degenerates, the gui starts, then halts because of the exception of the value analysis. The error message "Degeneration occured:@\nresults are not correct for lines of code that can be reached from the degeneration point." of Eval.force_compute cannot be seen by the user, the gui exits before it is shown.
If frama-c is started without -val on the same code, and the value analysis is started manually, things go better. However the gui is left on a strange state where it is no longer possible to click reactively on the source code, and the right button menu is deactivated.
### Additional Information :
Use the function below to force a degeneration. Ideally we would like to examine
the state of the statement x++, which is before the degeneration.
void main () {
int x = 1;
double d;
x++;
d = Frama_C_cos(1,2);
}
https://git.frama-c.com/pub/frama-c/-/issues/828
typo in gui message
2021-02-22T13:12:51Z
Jochen Burghardt
typo in gui message
ID0001792:
**This issue was created automatically from Mantis Issue 1792. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001792:
**This issue was created automatically from Mantis Issue 1792. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001792 | Frama-Clang | Graphical User Interface | public | 2014-06-02 | 2015-02-18 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | none | **Severity** | text | **Reproducibility** | always |
| **Platform** | - | **OS** | xubuntu-cfe13.10 | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | - |
### Description :
"This si a from clause"
should be "... is ..."
### Steps To Reproduce :
run "frama-c-gui from01.cpp" on the attached program
## Attachments
- [from01.cpp](/uploads/b3ccdf1d92d578e813af78fbdf81676c/from01.cpp)
https://git.frama-c.com/pub/frama-c/-/issues/714
Bullet colors are unreadable for color blind people
2021-02-22T13:24:44Z
David Mentré
Bullet colors are unreadable for color blind people
ID0001485:
**This issue was created automatically from Mantis Issue 1485. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001485:
**This issue was created automatically from Mantis Issue 1485. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001485 | Frama-C | Graphical User Interface | public | 2013-09-26 | 2015-03-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dmentre | **Assigned To** | guillaume-petiot | **Resolution** | fixed |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130601 | **Target Version** | - | **Fixed in Version** | Frama-C Sodium |
### Description :
For color blind people (e.g. "Daltoniens" in French), it is very difficult to make the difference between the red, green and orange bullets (at least, I have no testimony for others).
Possible improvements:
* Change the shape (e.g. circle for green bullet, triangle for orange bullet, ...);
* Use a shading scheme suitable for color blind people (https://trello.com is offering such a scheme for label colors), e.g. "/////" for one color, "\\\\\" for another color, etc.
* A combination of above two schemes.
https://git.frama-c.com/pub/frama-c/-/issues/699
Segmentation fault when launching frama-c-gui with OCaml 4.02.0
2021-02-22T13:09:21Z
mantis-gitlab-migration
Segmentation fault when launching frama-c-gui with OCaml 4.02.0
ID0001919:
**This issue was created automatically from Mantis Issue 1919. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001919:
**This issue was created automatically from Mantis Issue 1919. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001919 | Frama-C | Graphical User Interface | public | 2014-09-03 | 2015-03-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dhekir | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | Frama-C Sodium | **Fixed in Version** | Frama-C Sodium |
### Description :
I'm using OPAM 1.1.1 with OCaml 4.02.0.
I installed Frama-C using OPAM, along with its dependencies, and then tried running frama-c-gui. It segfaults. Using gdb I get the following backtrace:
Program received signal SIGSEGV, Segmentation fault.
0x0000000000beb6e6 in GValue_val ()
(gdb) back
#0 0x0000000000beb6e6 in GValue_val ()
#1 0x0000000000bec4b4 in ml_g_signal_emit_by_name ()
#2 0x0000000000a91016 in camlGtkSignal__fun_1460 ()
#3 0x0000000000aaa16c in camlGtkData__set_bounds_1503 ()
#4 0x0000000000790d0e in camlWp__Gtk_form__spinner_1053 () at src/gui/gtk_form.ml:100
#5 0x00007fffedf7bda8 in camlWp__GuiPanel__wp_panel_2423 () at src/wp/GuiPanel.ml:259
#6 0x00000000007603c8 in camlSecurity_slicing__Design__fun_13880 () at src/gui/design.ml:810
#7 0x0000000000ba2fb1 in camlList__iter_1061 () at list.ml:73
#8 0x0000000000763592 in camlSecurity_slicing__Design__fun_13774 () at src/gui/design.ml:808
#9 0x0000000000764083 in camlSecurity_slicing__Design__fun_14157 () at src/gui/design.ml:1136
#10 0x0000000000bd940b in camlCamlinternalOO__iter_f_1269 () at camlinternalOO.ml:369
#11 0x0000000000bd947d in camlCamlinternalOO__run_initializers_opt_1277 () at camlinternalOO.ml:379
#12 0x000000000076167a in camlSecurity_slicing__Design__fun_14455 () at src/gui/design.ml:1264
#13 0x0000000000a3b8f9 in camlExtlib__try_finally_1226 () at src/lib/extlib.ml:277
#14 0x000000000079403e in camlSecurity_slicing__Gtk_helper__fun_5386 () at src/gui/gtk_helper.ml:735
#15 0x00000000007940a5 in camlSecurity_slicing__Gtk_helper__fun_5383 () at src/gui/gtk_helper.ml:727
#16 0x0000000000765ee4 in camlSecurity_slicing__Design__fun_14460 () at src/gui/design.ml:1283
#17 0x0000000000c22b76 in caml_start_program ()
#18 0x00000037040492a6 in g_main_context_dispatch () from /lib64/libglib-2.0.so.0
#19 0x0000003704049628 in g_main_context_iterate.isra.24 () from /lib64/libglib-2.0.so.0
#20 0x00000037040496dc in g_main_context_iteration () from /lib64/libglib-2.0.so.0
#21 0x0000000000be9eda in ml_g_main_iteration ()
#22 0x0000000000ab06a5 in camlGtkMain__default_main_1163 ()
#23 0x0000000000a28d71 in camlCmdline__catch_toplevel_run_1181 () at src/kernel/cmdline.ml:214
#24 0x00000000006bdd85 in camlBoot__entry () at src/kernel/boot.ml:66
#25 0x00000000006b3f49 in caml_program ()
#26 0x0000000000c22b76 in caml_start_program ()
#27 0x0000000000000000 in ?? ()
It could be related to lablgtk. All dependencies were downloaded using OPAM (including lablgtk 2.16.0) and installed without issues.
First I tried using directly the version from OPAM, but due to the segfault error I then tried downloading the sources and compiling them myself.
When running configure, everything is ok except for "OcamlGraph 1.8.5 > 1.8.4 found: should be compatible, but no warranty. Use it at your own risk!", but I used the patch available in https://bts.frama-c.com/view.php?id=1764, and then I could run make and make install without issues. But once again, when running frama-c-gui it segfaults.
To sum up, either using OPAM or downloading and compiling the sources myself, I get the same result (unsurprisingly).
However, when switching to OCaml 4.01.0 and running "opam install frama-c", the GUI works normally.
Has the Frama-C GUI been confirmed to work with OCaml 4.02.0 already? Should I try manually compiling its dependencies to try and identify the cause of the error?
https://git.frama-c.com/pub/frama-c/-/issues/623
Frama-C GUI crashes under OS X
2021-02-22T13:07:34Z
Jens Gerlach
Frama-C GUI crashes under OS X
ID0002099:
**This issue was created automatically from Mantis Issue 2099. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002099:
**This issue was created automatically from Mantis Issue 2099. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002099 | Frama-C | Graphical User Interface | public | 2015-03-31 | 2015-06-29 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | - |
### Description :
If I start the Frama-C GUI on the attached program with 'frama-c-gui lemma.c',
then the GUI starts normally.
In the 'Source' panel I can see 'lemma.c.
When I try to see the lemma inside the file by clicking on the filename (or the little triangle left of it),
then the GUI crashes.
This does not happen under Linux.
### Additional Information :
frama-c was installed with opam
OS X (10.10.3 (14D127a))
opam --version: 1.2.0
frama-c -version
Version: Sodium-20150201
Compilation date: Tue Mar 31 09:48:58 CEST 2015
## Attachments
- [lemma.c](/uploads/f1e70f11f828611cc31af293e127a3c4/lemma.c)