frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2023-06-21T09:50:07Zhttps://git.frama-c.com/pub/frama-c/-/issues/2661frama-c-gui 27.0 segmentation fault in MacOS Ventura 13.42023-06-21T09:50:07ZDavid Sananframa-c-gui 27.0 segmentation fault in MacOS Ventura 13.4I have installed the latest Frama-C version (27.0) in MacOS Ventura 13.4 on M1 and M2 Macbooks. The installation process is smooth, including Ivette installation.
Once everything is installed when trying to run the GUI I get the followi...I have installed the latest Frama-C version (27.0) in MacOS Ventura 13.4 on M1 and M2 Macbooks. The installation process is smooth, including Ivette installation.
Once everything is installed when trying to run the GUI I get the following
```
[gui] Warning: creating config directory `.config/frama-c/gui'
(frama-c-gui:13363): Gtk-WARNING **: 12:57:42.276: Drawing a gadget with negative dimensions. Did you forget to allocate a size? (node tab owner GtkNotebook)
(frama-c-gui:13363): Gtk-WARNING **: 12:57:42.276: Drawing a gadget with negative dimensions. Did you forget to allocate a size? (node arrow owner GtkNotebook)
(frama-c-gui:13363): Gtk-WARNING **: 12:57:42.277: Drawing a gadget with negative dimensions. Did you forget to allocate a size? (node arrow owner GtkNotebook)
[1] 13363 segmentation fault frama-c-gui
```
I get this behaviour on both computers.
Is there any workaround for this? I tried copying the GUI config file from Linux without any success.
It works well in Linux, though. And the new interface is very neat thank you!
Thanks and best regards,
David.Andre MaronezeAndre Maronezehttps://git.frama-c.com/pub/frama-c/-/issues/2637libgnomecanvas disabled in brew2023-06-21T08:15:31ZLaura Titololibgnomecanvas disabled in brewTrying to install frama-c in a Mac machine, when executing
`brew libgnomecanvas`
an error occurs since the library is currently disabled.
The libgnomecanvas repository seems archived since November 29, 2022 (https://formulae.brew.sh/for...Trying to install frama-c in a Mac machine, when executing
`brew libgnomecanvas`
an error occurs since the library is currently disabled.
The libgnomecanvas repository seems archived since November 29, 2022 (https://formulae.brew.sh/formula/libgnomecanvas. https://gitlab.gnome.org/Archive/libgnomecanvas).https://git.frama-c.com/pub/frama-c/-/issues/2587Crash on Startup of frama-c-gui on WSL2022-01-18T09:06:14ZmoemodeCrash on Startup of frama-c-gui on WSL### Steps to reproduce the issue
Install frama-c on Windows 11 WSL according to install instructions. Then launch frama-c-gui
### Expected behaviour
frama-c-gui opens the gui
### Actual behaviour
![frama_err](/uploads/88a88cea9d4899...### Steps to reproduce the issue
Install frama-c on Windows 11 WSL according to install instructions. Then launch frama-c-gui
### Expected behaviour
frama-c-gui opens the gui
### Actual behaviour
![frama_err](/uploads/88a88cea9d4899909f2ee7ef74c73099/frama_err.png)
[frama_c_journal.ml](/uploads/a75256b6f842241a1e7ffb7ab0919b00/frama_c_journal.ml)
### Contextual information
- Frama-C installation mode: Opam as described on [Website](https://frama-c.com/html/get-frama-c.html)
- Frama-C version: 24.0 (Chromium)
- OS name: Windows
- OS version: 11Andre MaronezeAndre Maronezehttps://git.frama-c.com/pub/frama-c/-/issues/2586** (frama-c-gui:11256): CRITICAL **2021-12-14T13:30:19Zankit247** (frama-c-gui:11256): CRITICAL **<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the iss...<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- you installed Frama-C as prescribed in the [instructions](INSTALL.md).
If the issue applies to a specific Frama-C plug-in, please prefix the title
by the plug-in name: [Eva], [WP], [E-ACSL]…
-->
### Steps to reproduce the issue
$ frama-c-gui foo.c Gdk-Message: 00:28:20.600: Unable to load arrow from the cursor theme ** (frama-c-gui:11388): CRITICAL **: 00:28:32.491: GSourceFunc: callback raised an exception
<!--
Please indicate here steps to follow to get a [minimal, complete, and verifiable example](https://stackoverflow.com/help/mcve) which reproduces the issue.
-->
### Expected behaviour
Getting error opening GUI for Frama-c
<!--
-->
### Actual behaviour
Should open the GUI
<!--
-->
### Contextual information
- Frama-C installation mode: **Opam**
- Frama-C version: **24.0**
- Plug-in used: **eva**
- OS name: Windows 11 (UBUNTU as WSLg)
- OS version: ubuntu 20.04 LTS
### Additional information (optional)
Usig command **frama-c -eva -main SumHadCoefficients foo.c**, not getting any error, also analysis result is getting dumped on terminal. But using gui gives error
![framac_gui_error_eva](/uploads/79eef02f4cce41c37a7ea764844fbe78/framac_gui_error_eva.png)
While running command frama-c-gui foo.c gives followin error
![framac_gui_error](/uploads/18d90850585b150c1ce9c3992a069e8c/framac_gui_error.png)
<!--
-->Andre MaronezeAndre Maronezehttps://git.frama-c.com/pub/frama-c/-/issues/2496Order of the functions in gui2021-02-22T14:00:09Zmantis-gitlab-migrationOrder of the functions in guiID0000157:
**This issue was created automatically from Mantis Issue 157. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000157:
**This issue was created automatically from Mantis Issue 157. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000157 | Frama-C | Graphical User Interface | public | 2009-06-18 | 2009-06-25 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Anne | **Assigned To** | monate | **Resolution** | won't fix |
| **Priority** | low | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
The function list in the gui sidebar is in reverse order compared to the list of the functions in the C code.https://git.frama-c.com/pub/frama-c/-/issues/2474Incorrect linking order for the viewer2021-02-22T13:59:42Zmantis-gitlab-migrationIncorrect linking order for the viewerID0000225:
**This issue was created automatically from Mantis Issue 225. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000225:
**This issue was created automatically from Mantis Issue 225. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000225 | Frama-C | Graphical User Interface | public | 2009-09-01 | 2009-09-09 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | mehdi | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090601-beta1 | **Target Version** | - | **Fixed in Version** | Frama-C Beryllium-20090901 |
### Description :
Hi,
When compiling the viewer using a system-installation of ocamlgraph, the compilation fails with the following error:
ocamlc.opt -w Ael -warn-error A -annot -I src/misc -I src/ai -I src/memory_state -I src/toplevel -I src/slicing_types -I src/pdg_types -I src/kernel -I src/logic -I src/lib -I src/project -I src/buckx -I external -I cil/src -I cil/src/ext -I cil/src/frontc -I cil/src/logic -I cil/ocamlutil -I lib/plugins -I lib -I +ocamlgraph -g -I src/gui -I +lablgtk2 -I +ocamlgraph -linkall -custom -o bin/viewer.byte nums.cma unix.cma bigarray.cma str.cma dynlink.cma src/buckx/mybigarray.o src/buckx/buckx_c.o graph.cma /usr/lib/ocaml/ocamlgraph/viewGraph.cmo /usr/lib/ocaml/ocamlgraph/viewGraph_select.cmo /usr/lib/ocaml/ocamlgraph/viewGraph_utils.cmo lablgtk.cma lablgnomecanvas.cma lablgtksourceview.cma /usr/lib/ocaml/ocamlgraph/viewGraph.cmo /usr/lib/ocaml/ocamlgraph/viewGraph_select.cmo /usr/lib/ocaml/ocamlgraph/viewGraph_utils.cmo
[...]
File "_none_", line 1, characters 0-1:
Error: Error while linking /usr/lib/ocaml/ocamlgraph/viewGraph.cmo:
Reference to undefined global `GnoCanvas'
As you can see, viewGraph.cmo (and friends) are specified twice when linking and between the two groups there is lablgnomecanvas.cma which is needed by viewGraph.cmo.
Please find attached a patch that fixes this issue.
Kind regards,
## Attachments
- [0002-Do-not-add-GRAPH_GUICMO-to-BYTE_GUI_LIBS.patch](/uploads/2a2f35dda8b3eb544d3cb94fe4af1e7b/0002-Do-not-add-GRAPH_GUICMO-to-BYTE_GUI_LIBS.patch)https://git.frama-c.com/pub/frama-c/-/issues/2367How to update frama-c-gui2021-02-22T13:57:24Zmantis-gitlab-migrationHow to update frama-c-guiID0000483:
**This issue was created automatically from Mantis Issue 483. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000483:
**This issue was created automatically from Mantis Issue 483. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000483 | Frama-C | Graphical User Interface | public | 2010-05-17 | 2010-05-18 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | luoting | **Assigned To** | signoles | **Resolution** | no change required |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Hi ,Signoles
I once installed frama-c (version 20081201)by Synaptic ,and you said the version was a bit old. So I downloaded the frama-c (version Boron-20100401)source file and full installed it (./configure&&make&&sudo make install).However ,I find frama-c is version Boron-20100401 ,while frama-c-gui is still version 20081201.Why ? How to update frama-c-gui?
Thanks!
### Additional Information :
I have not removed the frama-c (version 20081201) before install the new version.https://git.frama-c.com/pub/frama-c/-/issues/2346Suggest to close a section if each obligation is proven by *some* prover2021-02-22T13:56:58ZJochen BurghardtSuggest to close a section if each obligation is proven by *some* proverID0000602:
**This issue was created automatically from Mantis Issue 602. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000602:
**This issue was created automatically from Mantis Issue 602. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000602 | Frama-C | Graphical User Interface | public | 2010-10-12 | 2010-10-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | monate | **Resolution** | not fixable |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Boron-20100401 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Currently, a section (like e.g. "fctxxx default behaviour" is automatically closed when *one* prover was able to prove all its contained obligations. However, often no single prover can prove them all, but each of them can be proved by some prover (i.e. in each line a green bullet appears, although not in the same column).
As a result, the user has to check all lines by himself, which is tedious (and even error-prone) when sections are large and the process of finding an adequate and verifiable specification involves many edit->vcg->prove cycles.
Therefor, I suggest to close a section once the statistics count has reached 100% of proven obligations (i.e. n/n). A "summary column" could be introduced showing a green bullet for single a obligation if it was proven by some prover, and a green check-mark for a section if its statistics count is 100%. For "very large" programs, it might even be desirable to have an icon summarizing all sections, i.e. the whole program, in a corresponding way.https://git.frama-c.com/pub/frama-c/-/issues/2337newbie trying to make operable2021-02-22T13:56:49Zmantis-gitlab-migrationnewbie trying to make operableID0000592:
**This issue was created automatically from Mantis Issue 592. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000592:
**This issue was created automatically from Mantis Issue 592. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000592 | Frama-C | Graphical User Interface | public | 2010-09-23 | 2010-12-03 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | blackdiamond | **Assigned To** | monate | **Resolution** | no change required |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Boron-20100401 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Hi :
I have installed the Boron Frama-C windows with Cygwin 2.721 setup version.
Also I installed the gcc and so.
After trying to load a c program in the frame dialog, an error appear with the next:
"gcc" not recognized as an internal or external command, program or executable lot file
Also, the message:
"Note that no C preprocessor is installed by Frama-C itself.
We encourage you to install cygwin from http://cygwin.org and to
launch Frama-C tools from a shell which contains "gcc" and the "bin"
directory of Frama-C in its path."
I have added the PATH of Frama-C/bin but it still does not work.
DO I need to set windows environment in order to enable Frama gets the gcc??
What steps are missed in order to make operable Frama-C ?
Thanks in Advance
### Additional Information :
Also, I have the environment with Frama-C installed.
HOMEPATH=\Documents and Settings\sal
CAML_LD_LIBRARY_PATH=C:\Frama-C\lib\stublibs
MANPATH=/usr/local/man:/usr/share/man:/usr/man:
APPDATA=C:\Documents and Settings\sal\Datos de programa
HOSTNAME=ACER1
TERM=cygwin
PROCESSOR_IDENTIFIER=x86 Family 6 Model 28 Stepping 2, GenuineIntel
FRAMAC_SHARE=C:\Frama-C\share\frama-c
WINDIR=C:\WINDOWS
OLDPWD=/usr/bin
USERDOMAIN=ACER1
OS=Windows_NT
ALLUSERSPROFILE=C:\Documents and Settings\All Users
USER=sal
!::=::\
TEMP=/cygdrive/c/DOCUME~1/sal/CONFIG~1/Temp
COMMONPROGRAMFILES=C:\Archivos de programa\Archivos comunes
WHYLIB='C:\Frama-C\lib\why'
VXIPNPPATH=C:\VXIpnp\
FRAMAC_LIB=C:\Frama-C\lib\frama-c
USERNAME=sal
PROCESSOR_LEVEL=6
PATH=/usr/local/bin:/usr/bin:/bin:/cygdrive/c/WINDOWS/system32:/cygdrive/c/WINDOWS:/cygdrive/c/WINDOWS/System32/Wbem:/cygdrive/c/Archivos de programa/Microsoft USB Flash Drive Manager/:/cygdrive/c/VXIpnp/WinNT/Bin:/cygdrive/c/Archivos de programa/GtkSharp/2.12/bin:/cygdrive/c/Archivos de programa/doxygen/bin:/cygdrive/c/Archivos de programa/Graphviz2.26.3/bin:/cygdrive/c/MCC18/mpasm:/cygdrive/c/MCC18/bin:/cygdrive/c/Archivos de programa/Microsoft USB Flash Drive Manager/:C:/Frama-C/bin
FP_NO_HOST_CHECK=NO
PWD=/cygdrive/c/Documents and Settings/sal
SYSTEMDRIVE=C:
LANG=C.UTF-8
USERPROFILE=C:\Documents and Settings\sal
CLIENTNAME=Console
PS1=\[\e]0;\w\a\]\n\[\e[32m\]\u@\h \[\e[33m\]\w\[\e[0m\]\n\$
LOGONSERVER=\\ACER1
PROCESSOR_ARCHITECTURE=x86
!C:=C:\cygwin\bin
ERGOLIB=C:\Frama-C\lib\alt-ergo
SHLVL=1
QUCSDIR=C:\Archivos de programa\Qucs
OCAMLLIB=C:\Frama-C\lib
HOME=/cygdrive/c/Documents and Settings/sal
PATHEXT=.COM;.EXE;.BAT;.CMD;.VBS;.VBE;.JS;.JSE;.WSF;.WSH
HOMEDRIVE=C:
FRAMAC_PLUGIN=C:\Frama-C\lib\frama-c\plugins
PROMPT=$P$G
MCC_INCLUDE=C:\MCC18\h;
COMSPEC=C:\WINDOWS\system32\cmd.exe
TMP=/cygdrive/c/DOCUME~1/sal/CONFIG~1/Temp
SYSTEMROOT=C:\WINDOWS
ASCODIR=C:\Archivos de programa\Qucs
PRINTER=CutePDF Printer
CVS_RSH=/bin/ssh
PROCESSOR_REVISION=1c02
tvdumpflags=8
INFOPATH=/usr/local/info:/usr/share/info:/usr/info:
PROGRAMFILES=C:\Archivos de programa
NUMBER_OF_PROCESSORS=2
SESSIONNAME=Console
COMPUTERNAME=ACER1
_=/usr/bin/envhttps://git.frama-c.com/pub/frama-c/-/issues/2281Stoping external process (why)2021-02-22T13:55:31Zmantis-gitlab-migrationStoping external process (why)ID0000569:
**This issue was created automatically from Mantis Issue 569. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000569:
**This issue was created automatically from Mantis Issue 569. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000569 | Frama-C | Graphical User Interface | public | 2010-08-23 | 2010-12-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Anne | **Assigned To** | monate | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Carbon-20101201-beta1 |
### Description :
For instance, when proving a property with WP, WHY processes are running.
When the user stop the computation (STOP button), is it possible to also stop those external processes ?https://git.frama-c.com/pub/frama-c/-/issues/2266Text on GUI buttons not readable on Windows (locale-dependant?)2021-02-22T13:55:11Zmantis-gitlab-migrationText on GUI buttons not readable on Windows (locale-dependant?)ID0000596:
**This issue was created automatically from Mantis Issue 596. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000596:
**This issue was created automatically from Mantis Issue 596. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000596 | Frama-C | Graphical User Interface | public | 2010-10-06 | 2010-12-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dmorneau | **Assigned To** | monate | **Resolution** | won't fix |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Boron-20100401 | **Target Version** | - | **Fixed in Version** | Frama-C Carbon-20101202-beta2 |
### Description :
The GUI always gives me garbage ("boxes") instead of characters on some components on Windows. A screenshot is included.
Environment: Windows Vista (Japanese version)
This bug unfortunately makes the software very hard to use since it affects the file selection dialog (and all dialogs in general).
### Additional Information :
I suspect this bug may be limited to non-English locales. I noticed that the "about" dialog has a localized title (it's literally saying "about", in Japanese, in the included screenshot). Probably, the "OK", "Cancel", etc. buttons as well as some folder names such as "My Documents" are also localized into Japanese, but the font used for the GUI does not support Japanese characters, thus turning the text into garbage.
Perhaps there is a way to disable this internationalization (in GTK, I assume) or use a unicode font?
## Attachments
- ![framac](/uploads/e36459b7655209e6772f2958022d5e30/framac.jpg)https://git.frama-c.com/pub/frama-c/-/issues/2249An erorr appears when executing right-click on the source-file name(left side...2021-02-22T14:03:36Zmantis-gitlab-migrationAn erorr appears when executing right-click on the source-file name(left side of the screen).ID0000508:
**This issue was created automatically from Mantis Issue 508. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000508:
**This issue was created automatically from Mantis Issue 508. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000508 | Frama-C | Graphical User Interface | public | 2010-06-14 | 2011-01-28 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | adytzul_ac | **Assigned To** | signoles | **Resolution** | unable to reproduce |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | random |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Boron-20100401 | **Target Version** | - | **Fixed in Version** | - |
### Description :
The full backtrace is:
Raised at file "src/pdg_types/pdgTypes.ml", line 548, characters 22-25
Called from file "src/pdg_types/pdgTypes.ml", line 554, characters 32-48
Called from file "src/security_slicing/components.ml", line 393, characters 2-80
Called from file "list.ml", line 74, characters 24-34
Called from file "list.ml", line 74, characters 24-34
Called from file "src/security_slicing/components.ml", line 601, characters 22-53
Called from file "src/security_slicing/components.ml", line 676, characters 14-69
Called from file "src/lib/type.ml", line 746, characters 40-45
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/impact/register_gui.ml", line 117, characters 15-37
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 (PdgTypes.Pdg.Top).
Please report as 'crash' at http://bts.frama-c.com
## Attachments
- [main.c](/uploads/cfcb446045cce03adbefbcea7c5c3715/main.c)
- ![error_2](/uploads/0df923cdc34eef798552c3264fdfa575/error_2.JPG)https://git.frama-c.com/pub/frama-c/-/issues/2245Gui crash with a new global variable2021-02-22T13:54:44ZVictoria Moya LamielGui crash with a new global variableID0000700:
**This issue was created automatically from Mantis Issue 700. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000700:
**This issue was created automatically from Mantis Issue 700. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000700 | Frama-C | Graphical User Interface | public | 2011-02-01 | 2011-02-07 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | vmoyalam | **Assigned To** | monate | **Resolution** | no change required |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20101202-beta2 | **Target Version** | - | **Fixed in Version** | Frama-C Carbon-20101202-beta2 |
### Description :
Adding a new global variable as follows :
let typ = (TInt(IInt,[]));
and loc = {Lexing.dummy_pos with
Lexing.pos_lnum=1; Lexing.pos_fname=file} in
let var = Cil.makeGlobalVar ~logic:false ~generated:false se_var_name typ;
and iv = {init=Some(Cil.makeZeroInit ~loc:(loc,loc) typ)} in
var.vdecl <- (loc,loc);
var.vdescr <- Some("side_effect variable for FDC analysis");
try
Globals.Vars.add var iv;
with Globals.Vars.AlreadyExists (_,_)->
Printf.printf "Error adding Global %s" var.vname
makes Frma-C crash, raising a Not Found exception, with the following command :
frama-c-gui -testGlobal ../VAL/LOT/testBug.c
where "-testGlobal" is our plug-in adding a global variable.
There is no crash using the command "frama-c", the problem only appears using the interface (with "frama-c-gui").
### Additional Information :
I do not know is the cause is related to a lack of information at the moment of the creation of the global variable.
The full backtrace is:
Raised at file "hashtbl.ml", line 229, characters 23-32
Called from file "src/gui/filetree.ml", line 375, characters 6-51
Called from file "hashtbl.ml", line 145, characters 8-13
Called from file "hashtbl.ml", line 148, characters 4-19
Called from file "src/project/state_builder.ml", line 625, characters 15-30
Called from file "src/value/register_gui.ml", line 385, characters 2-15
Called from file "list.ml", line 69, characters 12-15
Called from file "src/gui/design.ml", line 1054, characters 4-36
Called from file "camlinternalOO.ml", line 374, characters 12-17
Called from file "camlinternalOO.ml", line 384, characters 24-40
Called from file "src/gui/design.ml", line 1170, characters 15-33
Called from file "src/lib/extlib.ml", line 186, characters 12-15
Re-raised at file "src/lib/extlib.ml", line 191, characters 10-11
Called from file "src/gui/gtk_helper.ml", line 717, characters 8-350
Unexpected error (Not_found).
You will find the "testGlobal" plugin and the "testBug" C file in the attached tar file.
## Attachments
- [testGlobal.tar](/uploads/165ffc930ccef808c99ba450c8f285c2/testGlobal.tar)https://git.frama-c.com/pub/frama-c/-/issues/2221The procedure entry point freeaddrinfo could not be located in the dynamic li...2021-02-22T13:54:08Zmantis-gitlab-migrationThe procedure entry point freeaddrinfo could not be located in the dynamic link library WS2_32.dllID0000534:
**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/2216Needs for some refresh of the property status into the source code2021-02-22T13:54:01ZPatrick BaudinNeeds for some refresh of the property status into the source codeID0000792:
**This issue was created automatically from Mantis Issue 792. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000792:
**This issue was created automatically from Mantis Issue 792. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000792 | Frama-C | Graphical User Interface | public | 2011-04-13 | 2011-04-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | patrick | **Assigned To** | monate | **Resolution** | duplicate |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
When running some long wp calculus required by the command line,
unfolding of the source file freeze the status of the properties into the source code.
The status isn't updated when ending the wp proofs.
### Additional Information :
Command:
> frama-c-gui -wp valinit.c
When the GUI opens the Frama-C window, unfold the source file valinit.c before the end of WP.
## Attachments
- [valinit.c](/uploads/a77921a132027baf85b9fe1af7c4fd4c/valinit.c)https://git.frama-c.com/pub/frama-c/-/issues/2091Highlighting of PVDecl encompasses first Cil-added statement2021-02-22T13:50:50ZRichard BonichonHighlighting of PVDecl encompasses first Cil-added statementID0001042:
**This issue was created automatically from Mantis Issue 1042. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001042:
**This issue was created automatically from Mantis Issue 1042. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001042 | Frama-C | Graphical User Interface | public | 2011-12-09 | 2011-12-10 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | rbonichon | **Assigned To** | monate | **Resolution** | no change required |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | Frama-C GIT, precise the release id | **Fixed in Version** | - |
### Description :
Whenever highlighting a function declaration in the GUI (ie. a PVDecl construct) whose first statement has been added by Cil, the highlighting affects not only the function name and args until the opening '{' but also the first statement of the function.
It does not seem to happen for functions whose first statement is equivalent to the original Cabs statement.
### Steps To Reproduce :
See the attache gzipped archive which contains a minimal Frama-C plugin with an example to exhibit the problematic behavior.
## Attachments
- [minimal.tgz](/uploads/dbeceb12db03da6f0acc101532b09571/minimal.tgz)https://git.frama-c.com/pub/frama-c/-/issues/2090frama-c-gui hangs on start2021-02-22T13:50:48Zmantis-gitlab-migrationframa-c-gui hangs on startID0001043:
**This issue was created automatically from Mantis Issue 1043. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001043:
**This issue was created automatically from Mantis Issue 1043. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001043 | Frama-C | Graphical User Interface | public | 2011-12-09 | 2011-12-11 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | oliverks | **Assigned To** | monate | **Resolution** | no change required |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Nitrogen-20111001 | **Target Version** | - | **Fixed in Version** | - |
### Description :
I installed Frama-C Nitrogen on Mac OS X 10.6.8. Whenever I try to start frama-c-gui it just hangs. No graphical screen comes up and no error messages are reported.
If I run frama-c-gui -verbose 9 this is what I see
okingsmith:analysis oliverks$ frama-c-gui -verbose 9
[kernel] creating project "default"
[kernel] its unique name is "default"
[kernel] parsing command line options of stage "early".
[kernel] parsing command line options of stage "extending".
[kernel] dynamic plug-ins are now also searched inside directory `/usr/local/Frama-C/lib/frama-c/plugins'
[kernel] dynamic plug-ins are now also searched inside directory `/usr/local/Frama-C/lib/frama-c/plugins/gui'
[kernel] loading plug-in Security_slicing
[kernel] loading plug-in Wp
[kernel] loading plug-in Aorai
[kernel] loading plug-in Report
This is as far as it seems to get.
Oliverhttps://git.frama-c.com/pub/frama-c/-/issues/2068Unused global variable names not striked out in gui when assigns clause for e...2021-02-22T13:50:14ZJochen BurghardtUnused global variable names not striked out in gui when assigns clause for external function is usedID0001105:
**This issue was created automatically from Mantis Issue 1105. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001105:
**This issue was created automatically from Mantis Issue 1105. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001105 | Frama-C | Graphical User Interface | public | 2012-02-24 | 2012-02-24 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | monate | **Resolution** | no change required |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Nitrogen-20111001 | **Target Version** | - | **Fixed in Version** | - |
### Description :
I ran "frama-c-gui -val computeBug.c" on the attached program. Although the variable "a" is never used, its name is not striked out in the translation-unit overview window of the gui.
On the other hand, both variable names "a" and "b" are striked out when either
(1) the "@" is removed in line 4, or
(2) the ";" is replaced by a trivial procedure body "{}" in line 5, or
(3) the call to "write()" is commented out in line 9.
## Attachments
- [computeBug.c](/uploads/e60bce36639c274507c8d0e9f34354b9/computeBug.c)https://git.frama-c.com/pub/frama-c/-/issues/2046Look for "frama-c-gui.config" in HOME __before__ USERPROFILE2021-02-22T13:49:40Zmantis-gitlab-migrationLook for "frama-c-gui.config" in HOME __before__ USERPROFILEID0001185:
**This issue was created automatically from Mantis Issue 1185. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001185:
**This issue was created automatically from Mantis Issue 1185. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001185 | Frama-C | Graphical User Interface | public | 2012-05-29 | 2012-05-31 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Anne | **Assigned To** | monate | **Resolution** | unable to reproduce |
| **Priority** | normal | **Severity** | tweak | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Nitrogen-20111001 | **Target Version** | - | **Fixed in Version** | - |
### Description :
May I suggest to first look for HOME __before__ USERPROFILE in src/gui/gtk_helper.ml
because under cygwin, I get the following warning :
cygwin warning:
MS-DOS style path detected: C:\Users\Anne/frama-c-gui.config
Preferred POSIX equivalent is: /cygdrive/c/Users/Anne/frama-c-gui.config
because :
$ echo $USERPROFILE
C:\Users\Anne
but I also have :
$ echo $HOME
/home/Annehttps://git.frama-c.com/pub/frama-c/-/issues/2000Rename frama-c-gui.config2021-02-22T13:48:20Zmantis-gitlab-migrationRename frama-c-gui.configID0001102:
**This issue was created automatically from Mantis Issue 1102. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001102:
**This issue was created automatically from Mantis Issue 1102. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001102 | Frama-C | Graphical User Interface | public | 2012-02-21 | 2012-09-19 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | boris | **Assigned To** | monate | **Resolution** | fixed |
| **Priority** | normal | **Severity** | tweak | **Reproducibility** | N/A |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Nitrogen-20111001 | **Target Version** | - | **Fixed in Version** | Frama-C Oxygen-20120901 |
### Description :
Rename frama-c-gui.config to .frama-c-gui.config so it it's hidden as all other config-files.