frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2021-02-22T13:01:03Zhttps://git.frama-c.com/pub/frama-c/-/issues/393Ocaml 4.04.0 build error2021-02-22T13:01:03Zmantis-gitlab-migrationOcaml 4.04.0 build errorID0002255:
**This issue was created automatically from Mantis Issue 2255. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002255:
**This issue was created automatically from Mantis Issue 2255. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002255 | Frama-C | Kernel | public | 2016-11-09 | 2016-12-07 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jamesjer | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | x86_64 | **OS** | Linux | **OS Version** | 4.8.6 |
| **Product Version** | Frama-C Aluminium | **Target Version** | - | **Fixed in Version** | - |
### Description :
Building with ocaml 4.04.0 fails:
File "src/kernel_services/plugin_entry_points/db.ml", line 1:
Error: The implementation src/kernel_services/plugin_entry_points/db.ml
does not match the interface src/kernel_services/plugin_entry_points/db.cmi:
...
In module Properties.Interp.To_zone:
Values do not match:
val mk_ctx_func_contrat : (Cil_types.kernel_function -> '_a) ref
is not included in
val mk_ctx_func_contrat :
(Cil_types.kernel_function -> state_opt:bool option -> t_ctx) ref
File "src/kernel_services/plugin_entry_points/db.ml", line 1074, characters 10-29:
Actual declaration
### Additional Information :
See https://bugzilla.redhat.com/show_bug.cgi?id=1392552 for the original report, by Richard W. M. Jones. He supplied a patch which, he says, "fixes compilation, but is generally a bit of a hack. Upstream probably will want to make their own better fix." That patch is attached.
### Steps To Reproduce :
Build with Frama-C Aluminium with ocaml 4.04.0 on an x86_64 Linux machine.
## Attachments
- [frama-c-ocaml-4-04.patch](/uploads/caa49c7fec70d631bd0e90ee7a61dc61/frama-c-ocaml-4-04.patch)https://git.frama-c.com/pub/frama-c/-/issues/392option "-print" prints array upper bound in type before parameter name, rathe...2021-04-16T06:46:54ZJochen Burghardtoption "-print" prints array upper bound in type before parameter name, rather than after itID0002248:
**This issue was created automatically from Mantis Issue 2248. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002248:
**This issue was created automatically from Mantis Issue 2248. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002248 | Frama-C | Kernel | public | 2016-10-06 | 2016-12-08 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | text | **Reproducibility** | always |
| **Platform** | - | **OS** | xubuntu | **OS Version** | - |
| **Product Version** | Frama-C Aluminium | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -print ftest.c" on the attached program doesn't reproduce the input program; insteadt, it prints the "[a]" before the "b", not after it.
## Attachments
- [ftest.c](/uploads/d30107ddbd8fa94ff16f4958ab80029f/ftest.c)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/391wrong example code in value analysis manual, p.35, for message " invalid LHS ...2021-02-22T13:01:00ZJochen Burghardtwrong example code in value analysis manual, p.35, for message " invalid LHS operand for left shift"ID0002257:
**This issue was created automatically from Mantis Issue 2257. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002257:
**This issue was created automatically from Mantis Issue 2257. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002257 | Frama-C | Documentation > manuals | public | 2016-11-21 | 2016-12-08 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | text | **Reproducibility** | N/A |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Aluminium | **Target Version** | - | **Fixed in Version** | - |
### Description :
p.35 (top) of the value analysis manual shows the code from the attached file "lshift_orig.c". However, "frama-c -val lshift_orig.c" does not emit the warning "invalid LHS operand for left shift. assert 0 <= x;" shown in the manual. In fact, x is only written, not read, by the code.
Probably, the code should be like that in file "lshift_new.c". Frama-C emits "lshift_new.c:3:[kernel] warning: invalid LHS operand for left shift. assert 0 ≤ c;" and "lshift_new.c:3:[kernel] warning: signed overflow. assert c<<1 ≤ 2147483647;" when run on that code.
## Attachments
- [lshift_orig.c](/uploads/9b6afc5859b3e4388c1acb15b8dff279/lshift_orig.c)
- [lshift_new.c](/uploads/7fe660e193a41e27c2f9254530e5e91d/lshift_new.c)https://git.frama-c.com/pub/frama-c/-/issues/390Failure to compile on windows using cygwin2021-02-22T13:34:09Zmantis-gitlab-migrationFailure to compile on windows using cygwinID0002251:
**This issue was created automatically from Mantis Issue 2251. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002251:
**This issue was created automatically from Mantis Issue 2251. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002251 | Frama-C | Documentation > manuals | public | 2016-10-14 | 2016-12-08 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dotwa | **Assigned To** | maroneze | **Resolution** | unable to reproduce |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | Windows | **OS Version** | 7 |
| **Product Version** | Frama-C Aluminium | **Target Version** | - | **Fixed in Version** | - |
### Description :
This could be the same issue as :https://bts.frama-c.com/view.php?id=2247 as I get exactly the same error message.
On that page the developer has replied and said it should now work, which if is the same issue is not the case for my computer.
This error message appears when trying to compile frama-c using the instructions for windows provided by the wiki:
$ OPAMYES=yes opam depext -i frama-c
# Detecting depexts using flags: x86 mswindows win32 cygwinports
# The following system packages are needed:
# - gmp
# - gtk2.0
# - gtksourceview2.0
# - libgnomecanvas2
# - pkg-config
installed:gmp
installed:gtk2.0
installed:gtksourceview2.0
installed:libgnomecanvas2
installed:pkg-config
# All required OS packages found.
# Now letting OPAM install the packages
The following actions will be performed:
∗ install frama-c-base 20160501* [required by frama-c]
Why3 can be used by the WP plug-in for running additional automatic solvers
Coq can be used with the WP plug-in for proving interactively proof obligations
∗ install frama-c 20160501
Alt-Ergo Graphical Interface can be used by the WP plug-in
===== ∗ 2 =====
=-=- Gathering sources =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
[frama-c-base: git] Command started
[frama-c-base: git] Command started
[frama-c-base: git] Command started
[frama-c-base: git] Command started
[frama-c-base] git+https://github.com/maroneze/Frama-C-snapshot already up-to-date
=-=- Processing actions -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
[frama-c-base: sh] Command started
[frama-c-base: ./configure] Command started
[frama-c-base: make all] Command started
[ERROR] The compilation of frama-c-base failed at "make -j1
FRAMAC_TOP_SRCDIR=C:/cygwin32/home/User/.opam/4.02.3+mingw32/build/frama-c-base.20160501
all".
[frama-c-base: sh] Command started
[frama-c-base: ./configure] Command started
[frama-c-base: make uninstall] Command started
[frama-c-base: rm] Command started
#=== ERROR while compiling frama-c-base.20160501 ==============================#
# opam-version 1.3.0~dev (98188f141dbeb429258f2b2c00f6240d0af02b84)
# os win32
# command make -j1 FRAMAC_TOP_SRCDIR=C:/cygwin32/home/User/.opam/4.02.3+mingw32/build/frama-c-base.20160501 all
# path C:/cygwin32/home/User/.opam/4.02.3+mingw32/build/frama-c-base.20160501
# exit-code 2
# env-file C:/cygwin32/home/User/.opam/4.02.3+mingw32/build/frama-c-base.20160501\frama-c-base-172-1872ec.env
# stdout-file C:/cygwin32/home/User/.opam/4.02.3+mingw32/build/frama-c-base.20160501\frama-c-base-172-1872ec.out
# stderr-file C:/cygwin32/home/User/.opam/4.02.3+mingw32/build/frama-c-base.20160501\frama-c-base-172-1872ec.err
### stdout ###
# Generating configure
# Generating configure
### stderr ###
# make: autoconf: Command not found
# make[1]: autoconf: Command not found
# C:/cygwin32/home/User/.opam/4.02.3+mingw32/build/frama-c-base.20160501/share/Makefile.dynamic:202: share/Makefile.kernel: No such file or directory
# make[1]: *** [Makefile:2018: configure] Error 127
# make: *** [Makefile:2024: .make-clean] Error 2
=-=- Error report -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
The following actions were aborted
∗ install frama-c 20160501
The following actions failed
λ build frama-c-base 20160501
No changes have been performed
### Steps To Reproduce :
Follow the steps to install Frama-c for windows.
OPAMYES=yes opam depext -i frama-c is the line in the script where the error is fromhttps://git.frama-c.com/pub/frama-c/-/issues/388more prover processes run than expected2021-04-15T08:59:30ZJens Gerlachmore prover processes run than expectedID0002262:
**This issue was created automatically from Mantis Issue 2262. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002262:
**This issue was created automatically from Mantis Issue 2262. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002262 | Frama-C | Plug-in > wp | public | 2016-12-15 | 2016-12-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | sometimes |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | - | **Fixed in Version** | - |
### Description :
When I start WP with '-wp-par 4' (for example) I often observe that more than 4 prover processes are actually running.
### Additional Information :
I am not sure this is related but:
It happens from time to time that a proof obligations that is verified with '-wp-par 1' and given timeout T
is not verified when using a greater number of processes and the same timeout T.
### Steps To Reproduce :
run WP on example with a sufficiently large number of proof obligations that require more than one theorem prover
## Attachments
- ![screen-shot](/uploads/64bc6ecf07003613b00fa43be854d6b3/screen-shot.png)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/387Why3 warning2021-04-15T09:00:01ZJens GerlachWhy3 warningID0002263:
**This issue was created automatically from Mantis Issue 2263. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002263:
**This issue was created automatically from Mantis Issue 2263. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002263 | Frama-C | Plug-in > wp | public | 2016-12-16 | 2016-12-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | - | **Fixed in Version** | - |
### Description :
When running WP I observe the following warning
[Config] reading extra configuration file /Users/jens/.opam/4.04.0/share/frama-c/wp/why3/why3.conf
File "/Users/jens/.opam/4.04.0/share/why3/drivers/smt-libv2.drv", line 34, characters 7-14:
Library file not found: int
The problem occurs both under Linux and macOS.Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/386label Pre in function contracts2022-09-28T13:40:39ZJens Gerlachlabel Pre in function contractsID0002265:
**This issue was created automatically from Mantis Issue 2265. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002265:
**This issue was created automatically from Mantis Issue 2265. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002265 | Frama-C | Kernel > ACSL implementation | public | 2017-01-02 | 2017-01-02 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | - | **Fixed in Version** | - |
### Description :
I have recently noted that we use both 'Pre' and 'Old' in function contracts of "ACSL by Example".
The ACSL description, however, mentions the label 'Pre' only for statement annotations.
Is there a reason to allow both labels in function contracts?
If not, then I would suggest to forbid 'Pre' in function contracts.
## Attachments
- [swap.c](/uploads/21ebefde0c67219b5297aa9a386cedef/swap.c)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/385WP inserts unwanted new lines into Coq proofs2021-04-15T09:00:28ZJens GerlachWP inserts unwanted new lines into Coq proofsID0002266:
**This issue was created automatically from Mantis Issue 2266. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002266:
**This issue was created automatically from Mantis Issue 2266. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002266 | Frama-C | Plug-in > wp | public | 2017-01-02 | 2017-01-02 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | - | **Fixed in Version** | - |
### Description :
I have noticed (since Aluminium) that whenever I work on a Coq proof, then WP adds a newline to all the other Coq proofs in wp0.script (right before "Qed.").
In the long run, it is a bit annoying to have all these empty lines in the coq proofs...Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/384coq 8.5: cannot find Memory.v2021-02-22T13:00:50ZJens Gerlachcoq 8.5: cannot find Memory.vID0002208:
**This issue was created automatically from Mantis Issue 2208. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002208:
**This issue was created automatically from Mantis Issue 2208. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002208 | Frama-C | Plug-in > wp | public | 2016-02-11 | 2017-01-03 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Magnesium | **Target Version** | - | **Fixed in Version** | - |
### Description :
After updating my Frama-C installation through opam to coq.8.5 and why3.0.86.3 I observe the following error. When compiling the attached file with
coqc -R /Users/jens/.opam/system/share/frama-c/wp/coqwp -as "" WP_basics.v
I receive the following error message:
File "./WP_basics.v", line 3, characters 15-21:
Error: Unable to locate library Memory.
With coq.8.4.6 and earlier I did not observe this error.
### Additional Information :
The path '/Users/jens/.opam/system/share/frama-c' points to my Frama-C share.
ls -l /Users/jens/.opam/system/share/frama-c/wp/coqwp/Memory.v
produces
-rw-r--r-- 1 jens staff 10160 11 Feb 10:38 /Users/jens/.opam/system/share/frama-c/wp/coqwp/Memory.v
## Attachments
- [WP_basics.v](/uploads/e9bbf929a84471fcc0ca1d0a5755739b/WP_basics.v)https://git.frama-c.com/pub/frama-c/-/issues/380Fatal error while browsing callgraph.2021-02-22T13:37:54Zmantis-gitlab-migrationFatal error while browsing callgraph.ID0002271:
**This issue was created automatically from Mantis Issue 2271. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002271:
**This issue was created automatically from Mantis Issue 2271. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002271 | Frama-C | Graphical User Interface | public | 2017-01-13 | 2017-01-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Max P. | **Assigned To** | signoles | **Resolution** | won't fix |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | random |
| **Platform** | Cygwin | **OS** | Windows 7 | **OS Version** | x64 SP1 |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | - | **Fixed in Version** | - |
### Description :
After the first callgraph opening the warning is generated:
(frama-c-gui.exe:8512): Pango-WARNING **: couldn't load font "Times-Roman Not-Rotated 14", falling back to "Sans Not-Rotated 14", expect ugly output.
And really the callgraph looks unacceptable. It is impossible to see anything on it in "global view" mode.
In "tree view" mode items are croped in a certain scale. In addition to this when switching in "tree view" lots of the same warnings occurs:
(frama-c-gui.exe:8480): GLib-GObject-WARNING **: value "-1.#IND00" of type 'gdouble' is invalid or out of range for property 'size-points' of type 'gdouble'
Sometimes these warnings becomes too much and it ends with a fatal error (the screenshot is attached).
Last time it happened after the changing of "depth forward".
### Additional Information :
After closing of the error window Frama-C closed and in Сygwin terminal it was printed follows:
This application has requested the Runtime to terminate it in an unusual way.
Please contact the application's support team for more information.
### Steps To Reproduce :
In GUI select "Show callgraph". Change view mode on "tree view". Rotate the mouse wheel to zoom, change depth, etc.
## Attachments
- ![fatal_error](/uploads/5ea06cbd39552c7fbaf19ce9374faec7/fatal_error.png)https://git.frama-c.com/pub/frama-c/-/issues/379The disproportion between block sizes and caption sizes on a callgrath.2021-02-22T13:00:42Zmantis-gitlab-migrationThe disproportion between block sizes and caption sizes on a callgrath.ID0002273:
**This issue was created automatically from Mantis Issue 2273. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002273:
**This issue was created automatically from Mantis Issue 2273. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002273 | Frama-C | Graphical User Interface | public | 2017-01-17 | 2017-01-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Max P. | **Assigned To** | signoles | **Resolution** | no change required |
| **Priority** | normal | **Severity** | tweak | **Reproducibility** | always |
| **Platform** | Cygwin | **OS** | Windows 7 | **OS Version** | x64 SP1 |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | - | **Fixed in Version** | - |
### Description :
Callgraph looks as on attached screenshot.
### Additional Information :
After the first callgraph opening the warning is generated:
(frama-c-gui.exe:8512): Pango-WARNING **: couldn't load font "Times-Roman Not-Rotated 14", falling back to "Sans Not-Rotated 14", expect ugly output.
### Steps To Reproduce :
In GUI select command "Show callgraph".
## Attachments
- ![Global_view_2](/uploads/1b6b6f23c7eca80972a9107e1c51f3b8/Global_view_2.png)https://git.frama-c.com/pub/frama-c/-/issues/378Incorrect code generation with gmp2021-02-22T13:00:41ZKostyantyn VorobyovIncorrect code generation with gmpID0002231:
**This issue was created automatically from Mantis Issue 2231. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002231:
**This issue was created automatically from Mantis Issue 2231. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002231 | Frama-C | Plug-in > E-ACSL | public | 2016-06-14 | 2017-01-18 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | kvorobyov | **Assigned To** | signoles | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | X86-64 | **OS** | Linux | **OS Version** | - |
| **Product Version** | Frama-C Aluminium | **Target Version** | Frama-C Aluminium | **Fixed in Version** | Frama-C 14-Silicon |
### Description :
In some tricky cases involving multiple casts gmp-generated code is incorrect which leads to segmentation faults due to improper use of gmp library.
For instance, in the example (see attached file) the following code is generated:
unsigned long __gen_e_acsl_cast;
mpz_t __gen_e_acsl__2;
...
__gmpz_sub(__gen_e_acsl_sub,(__mpz_struct const *)__gen_e_acsl_cast,
(__mpz_struct const *)(__gen_e_acsl__2));
This results in a segmentation fault because __gmpz_sub expects a mpz_t, not an integer.
### Steps To Reproduce :
The attached file is instrumented with E-ACSL, compiled and executed
## Attachments
- [mcf_slice.c](/uploads/7444bfe912aba62ff524eae88fda8095/mcf_slice.c)https://git.frama-c.com/pub/frama-c/-/issues/377Literal strings in global arrays with compound initializers are not correctly...2021-02-22T14:01:28ZArvid JakobssonLiteral strings in global arrays with compound initializers are not correctly initializedID0001817:
**This issue was created automatically from Mantis Issue 1817. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001817:
**This issue was created automatically from Mantis Issue 1817. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001817 | Frama-C | Plug-in > E-ACSL | public | 2014-06-25 | 2017-01-18 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | arvidj | **Assigned To** | kvorobyov | **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 14-Silicon |
### Description :
Frama-C GIT Commit: b71d80efb3808c286f1a2f17dbf54bc3909824d0
The generated function for initializing global variables "__e_acsl_memory_init" does not handle arrays containing literal strings with compound intializers.
Example:
char *A[2] = {"foo", "bar"};
int main(void) {
/*@ assert \valid(A[0]) ; */
/*@ assert \valid(A[1]) ; */
}
Generated __e_acsl_memory_init:
void __e_acsl_memory_init(void)
{
char *__e_acsl_literal_string;
__store_block((void *)(A),sizeof(char *[2]));
__e_acsl_literal_string = "bar";
__store_block((void *)__e_acsl_literal_string,sizeof("bar"));
__full_init((void *)__e_acsl_literal_string,sizeof("bar"));
__literal_string((void *)__e_acsl_literal_string);
A = (char *)__e_acsl_literal_string;
return;
}
The last assignment is incorrect.
## Attachments
- [usb_urb-drivers-staging-lirc-lirc_imon.ko_false-unreach-call.cil.out.i.pp.i](/uploads/c0863a05b09fb4259e306909b32e8b9f/usb_urb-drivers-staging-lirc-lirc_imon.ko_false-unreach-call.cil.out.i.pp.i)https://git.frama-c.com/pub/frama-c/-/issues/376Assertion failure when unrolling types of struct members2021-02-22T13:00:35ZKostyantyn VorobyovAssertion failure when unrolling types of struct membersID0002191:
**This issue was created automatically from Mantis Issue 2191. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002191:
**This issue was created automatically from Mantis Issue 2191. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002191 | Frama-C | Plug-in > E-ACSL | public | 2015-12-04 | 2017-01-18 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | kvorobyov | **Assigned To** | signoles | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Magnesium | **Target Version** | - | **Fixed in Version** | Frama-C 14-Silicon |
### Description :
/* The following program leads to a failure of an assertion in translate.ml. The failure seems to be due to E-ACSL inability to determine the type of the term _G[0].str. */
struct ST {
char *str;
int num;
};
struct ST _G[] = {
{
.str = "Struct_G[0]",
.num = 99
},
{
.str = "Struct_G[1]",
.num = 147
}
};
int main(int argc, char **argv) {
/*@ assert \valid_read(_G[0].str); */
return 0;
}https://git.frama-c.com/pub/frama-c/-/issues/374Can't install E-ACSL plugin2021-02-22T13:34:08Zmantis-gitlab-migrationCan't install E-ACSL pluginID0002213:
**This issue was created automatically from Mantis Issue 2213. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002213:
**This issue was created automatically from Mantis Issue 2213. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002213 | Frama-C | Plug-in > E-ACSL | public | 2016-02-26 | 2017-01-18 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | George Karpenkov | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Magnesium | **Target Version** | - | **Fixed in Version** | Frama-C 14-Silicon |
### Description :
Hi,
Is E-ACSL 0.5 supposed to work with Frama-C Magnesium?
The installation instructions for E-ACSL still read "Frama-C = Sodium-20150201
(no warranty that this plug-in works with a more recent version of Frama-C)".
I've tried updating Frama-C and E-ACSL through OPAM, but E-ACSL description in OPAM requires the previous version of Frama-C. After changing the E-ACSL metadata I could get it installed, but running "frama-c -e-acsl" reported "option ... is unknown".
I've also tried to install E-ACSL plug-in manually, but running ./configure reports "configure: WARNING: e_acsl disabled because rtegen unknown." after which running "make" does nothing.https://git.frama-c.com/pub/frama-c/-/issues/372It is impossble to change log file without kinds of message changing.2022-09-28T14:06:22Zmantis-gitlab-migrationIt is impossble to change log file without kinds of message changing.ID0002274:
**This issue was created automatically from Mantis Issue 2274. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002274:
**This issue was created automatically from Mantis Issue 2274. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002274 | Frama-C | Kernel | public | 2017-01-19 | 2017-01-24 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Max P. | **Assigned To** | maroneze | **Resolution** | open |
| **Priority** | low | **Severity** | tweak | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | - | **Fixed in Version** | - |
### Description :
I wanted to explore how the analysis settings affect the output messages.
I changed settings and name of log file. But output messages were copied in the file that was pointed firstly.
Only if kinds of messages are changed a new file is created.
### Steps To Reproduce :
In GUI do follows:
1. Set -kernel-log rw:kernel.log
2. Run analysis
3. Verify that a file kernel.log was created.
4. Set -kernel-log rw:kernel2.log
5. Run analysis
6. Verify that a file kernel2.log was not created, but the time of last modification of the kernel.log was changed.
7. Set -kernel-log ruw:kernel2.log
8. Run analysis
9. Verify that a file kernel2.log was created.Andre MaronezeAndre Maronezehttps://git.frama-c.com/pub/frama-c/-/issues/371translation to why3 of int* argument to logic function2021-04-15T08:10:47ZJochen Burghardttranslation to why3 of int* argument to logic functionID0002275:
**This issue was created automatically from Mantis Issue 2275. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002275:
**This issue was created automatically from Mantis Issue 2275. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002275 | Frama-C | Plug-in > wp | public | 2017-02-02 | 2017-02-03 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Silicon-20161101 | **OS** | xubuntu 16.04.1 LTS | **OS Version** | - |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp -wp-prover eprover foo.c" proves lemma "foo" in line 7, although it essentially says that no objects of type "int*" exist at all.
The problem disappears if either
(1) the result type "int" of "deref" is changed to "integer" in line 3,
(2) "deref" is inlined at line 5,
(3) "large" is inlined at line 7, or
(4) "large(s) && !large(s)" is simplified to "\false" in line 7.
Using option "-wp-out", and comparing the files "Axiomatic.why" before and after change (1), see attached files "Axiomatic_int.why" and "Axiomatic_integer.why", reveals that the former has an "axiom Q_TL_deref" while the latter does not. This axiom essentially says that any value fetched from an integer array (i.e. a "map addr int" in why3 language) is already an int (i.e. satisfies "is_sint32" in why3 language), which imho is wrong.
When using "-wp alt-ergo" instead of "-wp eprover", the generated mlw files before and after change (1) literally agree, see attached file "lemma_foo_Alt-Ergo_int.mlw" and "lemma_foo_Alt-Ergo_integer.mlw"; they contain no occurrence of "deref" or "large".
The input given to eprover has been intercepted and boiled down as far as possible, resulting in file "foo_eprover_input.p" which is attached for convenience. Its axiom "q_TL_deref" in line 18 is a boiled-down translation of axiom "Q_TL_deref" from the why3 file, and is wrong as argued above.
## Attachments
- [foo.c](/uploads/820f364a77e732e708ee0a21ae3d0123/foo.c)
- [Axiomatic_int.why](/uploads/10f847d1cf681d6ecde0ea21bab12d96/Axiomatic_int.why)
- [Axiomatic_integer.why](/uploads/3493da1d13894db1a171428f9e5c269e/Axiomatic_integer.why)
- [lemma_foo_Alt-Ergo_int.mlw](/uploads/ffc94494f9b1a25f6bc9ff99c712ec1e/lemma_foo_Alt-Ergo_int.mlw)
- [lemma_foo_Alt-Ergo_integer.mlw](/uploads/ee7e41ba4da81b0485dc5e5cc5d53a89/lemma_foo_Alt-Ergo_integer.mlw)
- [foo_eprover_input.p](/uploads/c00d2b593bcbd384b5bc9781d696e9b7/foo_eprover_input.p)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/369Frama-C sleeps too much when discharging trivial goals2021-04-15T09:08:16Zmantis-gitlab-migrationFrama-C sleeps too much when discharging trivial goalsID0002280:
**This issue was created automatically from Mantis Issue 2280. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002280:
**This issue was created automatically from Mantis Issue 2280. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002280 | Frama-C | Plug-in > wp | public | 2017-02-13 | 2017-02-14 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pkhuong | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | tweak | **Reproducibility** | always |
| **Platform** | Linux/x86_64 | **OS** | Linux | **OS Version** | 4.9.0-1-amd64 #1 |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | - | **Fixed in Version** | - |
### Description :
I have a largish C functions that generates ~70K goals (that I'm refactoring away). Verification with WP and RTE assertions succeeds, but takes ~14 minutes of real time. strace shows the majority of that time is spent executing *no syscall* (i.e., not calling external solvers) except printing the progress on stderr, getrusage, and nanosleeping for half a second. I LD_PRELOADed a shared object to turn usleep into a no-op, and that improved the runtime from 14 minutes to 3 minutes.
Could Frama-C sleep less when Qed does all the work?
### Steps To Reproduce :
frama-c slow_qed.c -cpp-gnu-like -no-asm-contracts -constfold -machdep x86_64 -implicit-function-declaration error -wp -wp-rte -wp-extensional -wp-split -wp-init-const -wp-prop="-trustme,-freeable,-@assigns,-@lemma,-@variant" -wp-prover=alt-ergo,Z3:4.5.0
## Attachments
- [slow_qed.c](/uploads/df95dd235b294d5f24c6ca57181db9d4/slow_qed.c)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/368applicability of Coq proof script depends on order of include files2021-04-15T08:02:31ZJochen Burghardtapplicability of Coq proof script depends on order of include filesID0002282:
**This issue was created automatically from Mantis Issue 2282. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002282:
**This issue was created automatically from Mantis Issue 2282. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002282 | Frama-C | Plug-in > wp | public | 2017-02-16 | 2017-02-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Silicon-20161101 | **OS** | xubuntu | **OS Version** | - |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | - | **Fixed in Version** | - |
### Description :
We run "frama-c -wp -wp-script wp0.script -wp-model Typed+ref -wp-prop HeapMaximum -wp-prover coq make_heap_cpp.c" on the attached files. In the current form, the Coq proof script "wp0.script" works fine and proved the lemma "HeapMaximum" from file "make_heap_cpp.c".
However, when that lemma is moved after the "axiomatic Count", which is completely unrelated, the same command doesn't work any longer. Using "-wp-out" shows that both versions differ in the location where lemma "HeapBounds" is available in Coq; this make it necessary to change the names used in the proof.
The problem originated from lemma "HeapMaximum" being used for the verification of two different function contracts. For software engineering reasons, the order of #include files was different (since different files were preferred to be included in the ".c", rather than already in the ".h" file). This resulted in "lemma HeapMaximum" appearing before and after an "axiomatic", making "wp0.script" work and not work, respectively.
## Attachments
- [make_heap_cpp.c](/uploads/256c2042ed0e2b08fc7901c42cdcbb49/make_heap_cpp.c)
- [wp0.script](/uploads/7277fc9a7ed0386527de3694d96817e5/wp0.script)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/367lemma tacitly omitted from prover assumptions2021-08-05T09:00:11ZJochen Burghardtlemma tacitly omitted from prover assumptionsID0002286:
**This issue was created automatically from Mantis Issue 2286. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002286:
**This issue was created automatically from Mantis Issue 2286. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002286 | Frama-C | Plug-in > wp | public | 2017-02-27 | 2017-02-27 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Silicon-20161101 | **OS** | xubuntu | **OS Version** | - |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp -wp-rte -wp-prop=addIncAdd -wp-prover z3 bug1.c" on the attached file verifies the given goal "addIncAdd" in 40ms. However, when the closing brace is moved from line 35 up to line 30, no proof is found in 10s.
A "diff -r" on the wp-out directories shows that the translation of lemma "incAdd" is put into file "A_addAxioms.why" in the former, but into "Axiomatic2.why" in the latter case.
Intercepting the input if "z3" shows that only in the former case the translation is included in the input of "z3"; in the latter case it is missing.
I couldn't find the reason for just omitting "incAdd": exchanging lemmas "incAdd" and "addAdd" in the C source and comparing the "z3" inputs again shows that still "incAdd" is omitted; so the reason could be in it's name of form, but not in it place in source.
## Attachments
- [bug1.c](/uploads/506733bc64b39e2ab7b3c2d585f33515/bug1.c)
- [why_495d09_Axiomatic2-T-Q_addIncAdd.smt2](/uploads/1b12fd854a0d7471daf0f12f795dc5b4/why_495d09_Axiomatic2-T-Q_addIncAdd.smt2)
- [why_767c25_Axiomatic2-T-Q_addIncAdd.smt2](/uploads/8fbe26071875fc21dea8cfbef1aa6f8d/why_767c25_Axiomatic2-T-Q_addIncAdd.smt2)
- [why_54d12d_Axiomatic2-T-Q_addIncAdd.smt2](/uploads/d92a6c680802a47e1e35e8cd3c5810ad/why_54d12d_Axiomatic2-T-Q_addIncAdd.smt2)Loïc CorrensonLoïc Correnson