frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2022-09-28T12:51:12Zhttps://git.frama-c.com/pub/frama-c/-/issues/65WP manual: hyperlink in table of contents sometimes one off2022-09-28T12:51:12ZJens GerlachWP manual: hyperlink in table of contents sometimes one offID0002505:
**This issue was created automatically from Mantis Issue 2505. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002505:
**This issue was created automatically from Mantis Issue 2505. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002505 | Frama-C | Documentation > manuals | public | 2020-04-16 | 2020-05-07 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | maroneze | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 20-Calcium | **Target Version** | - | **Fixed in Version** | - |
### Description :
In the WP manual at http://frama-c.com/download/wp-manual-20.0-Calcium.pdf,
Section 2.4.8 ("Generated Proof Obligations") starts at Page 37.
However, the link in the table of contents points to Page 36.
### Additional Information :
Just a guess: You are probably using the package hyperref. I have read several times (and experienced it myself) that it is a good idea to include this packet at the end.
https://tex.stackexchange.com/questions/1863/which-packages-should-be-loaded-after-hyperref-instead-of-beforeAndre MaronezeAndre Maronezehttps://git.frama-c.com/pub/frama-c/-/issues/90formatting problem in acsl-implementation-18.0-Argon.pdf2021-02-22T13:42:53Zmantis-gitlab-migrationformatting problem in acsl-implementation-18.0-Argon.pdfID0002450:
**This issue was created automatically from Mantis Issue 2450. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002450:
**This issue was created automatically from Mantis Issue 2450. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002450 | Frama-C | Documentation > manuals | public | 2019-06-09 | 2020-02-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | kiniry | **Assigned To** | patrick | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 18-Argon | **Target Version** | - | **Fixed in Version** | Frama-C 20-Calcium |
### Description :
See page 45 of the manual. There is a formatting error pushing at least a paragraph about statement contracts off the lower right hand corner of the page.https://git.frama-c.com/pub/frama-c/-/issues/71Outdated -rte-all option in RTE manual2021-02-22T12:52:26Zmantis-gitlab-migrationOutdated -rte-all option in RTE manualID0002418:
**This issue was created automatically from Mantis Issue 2418. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002418:
**This issue was created automatically from Mantis Issue 2418. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002418 | Frama-C | Documentation > manuals | public | 2018-12-14 | 2020-02-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jaseg | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | low | **Severity** | trivial | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 18-Argon | **Target Version** | Frama-C 20-Calcium | **Fixed in Version** | Frama-C 20-Calcium |
### Description :
The frama-c v18.0 RTE manual[1] linked from the RTE website[0] in ch. 3 claims RTE has options -rte-all and -rte-no-all that the actual command line tool does not seem to recognize. I guess this is just outdated info. Note that the option is also mentioned in the text which I guess would have to be updated as well.
Thanks for the great work,
jaseg
[0] https://frama-c.com/rte.html
[1] https://frama-c.com/download/frama-c-rte-manual.pdf
### Steps To Reproduce :
(this is one of the example command lines from the manual)
> dev~/r/l/src <3 frama-c -rte -rte-select f,g -rte-all -rte-mem
> [kernel] User Error: option `-rte-all' is unknown.
> use `frama-c -help' for more information.
> [kernel] Frama-C aborted: invalid user input.
> dev~/r/l/src <3 frama-c -v
> 18.0 (Argon)https://git.frama-c.com/pub/frama-c/-/issues/233Name of RTE plugin in documentation2021-02-22T13:59:32ZJens GerlachName of RTE plugin in documentationID0002398:
**This issue was created automatically from Mantis Issue 2398. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002398:
**This issue was created automatically from Mantis Issue 2398. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002398 | Frama-C | Documentation > manuals | public | 2018-09-04 | 2018-11-30 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 17-Chlorine | **Target Version** | Frama-C 18-Argon | **Fixed in Version** | Frama-C 18-Argon |
### Description :
The RTE plugin manual has two titles: On the title page it reads "Annotation Generation".
On the third page it reads "Frama-C’s annotation generator plug-in".
Neither title mentions "RTE". Is this intentional?
### Steps To Reproduce :
See http://frama-c.com/download/rte-manual-Chlorine-20180501.pdfhttps://git.frama-c.com/pub/frama-c/-/issues/248Frama-C GUI manual2021-02-22T12:57:24Zmantis-gitlab-migrationFrama-C GUI manualID0002393:
**This issue was created automatically from Mantis Issue 2393. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002393:
**This issue was created automatically from Mantis Issue 2393. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002393 | Frama-C | Documentation > manuals | public | 2018-08-09 | 2018-09-05 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | NewUser | **Assigned To** | maroneze | **Resolution** | no change required |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | N/A |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 17-Chlorine | **Target Version** | - | **Fixed in Version** | - |
### Description :
Is there any detailed (stepwise) manual about GUI of Drama-C?
May be I'm missing some points but Could we edit/write new files within GUI interface? GUI seems to be not very user friendly...https://git.frama-c.com/pub/frama-c/-/issues/284BTS does not allow do select "Frama-C 16 Sulfur" as "Product Version"2021-02-22T12:58:14ZJens GerlachBTS does not allow do select "Frama-C 16 Sulfur" as "Product Version"ID0002343:
**This issue was created automatically from Mantis Issue 2343. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002343:
**This issue was created automatically from Mantis Issue 2343. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002343 | Frama-C | Documentation | public | 2018-01-18 | 2018-01-31 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 16-Sulfur | **Target Version** | - | **Fixed in Version** | Frama-C 16-Sulfur |
### Description :
BTS does not allow do select "Frama-C 16 Sulfur" as "Product Version" ...https://git.frama-c.com/pub/frama-c/-/issues/123explain wp's syntactic restrictions on "inductive" definitions2021-02-22T12:56:27ZJochen Burghardtexplain wp's syntactic restrictions on "inductive" definitionsID0002337:
**This issue was created automatically from Mantis Issue 2337. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002337:
**This issue was created automatically from Mantis Issue 2337. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002337 | Frama-C | Documentation | public | 2017-12-14 | 2019-10-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | text | **Reproducibility** | N/A |
| **Platform** | Sulfur-20171101 | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
In Sect.2.6.3 "Inductive predicates" (p.50) of the manual "acsl-implementation-Sulfur-20171101.pdf", it is announced that "tools might enforce syntactic conditions on the form of inductive definitions". However, in the Wp manual (file "wp-manual-Sulfur-20171101.pdf") the string "inductive" doesn't occur at all. It should be explained there what restrictions Wp enforces on "inductive" definitions; in case it doesn't restrict them at all, this should be mentioned, too. I didn't check other plugin manuals for the occurrence of the string "inductive".
As a side remark: From a user's point of view, the freedom of each plugin to give its own semantics to (details of) ACSL constructs is confusing, and sometimes even annoying. From a software engineer's point of view, admitting too much freedom to plugins gives away the advantages of a integerated framework/plugin architecture. Having different semantics for ACSL details may compromise the interoperability of plugins.https://git.frama-c.com/pub/frama-c/-/issues/320Spelling errors2021-02-22T12:59:16Zmantis-gitlab-migrationSpelling errorsID0002323:
**This issue was created automatically from Mantis Issue 2323. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002323:
**This issue was created automatically from Mantis Issue 2323. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002323 | Frama-C | Documentation | public | 2017-08-11 | 2017-09-01 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | mehdi | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 15-Phosphorus | **Target Version** | - | **Fixed in Version** | Frama-C GIT, precise the release id |
### Description :
Hi,
I've found some spelling errors in Frama-C's source code. Please find attached a patch to fixe them.
## Attachments
- [0008-More-fixes-of-spelling-errors.patch](/uploads/202926e102b518e7e14b24d4d1de7011/0008-More-fixes-of-spelling-errors.patch)
- [0001-Fix-spelling-error-in-binary.patch](/uploads/78cca8ddcb2d7003d2128aae12eb17ce/0001-Fix-spelling-error-in-binary.patch)https://git.frama-c.com/pub/frama-c/-/issues/327Statement contracts and WP2023-07-24T10:25:01ZJens GerlachStatement contracts and WPID0002317:
**This issue was created automatically from Mantis Issue 2317. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002317:
**This issue was created automatically from Mantis Issue 2317. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002317 | Frama-C | Documentation > manuals | public | 2017-07-18 | 2017-07-19 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | text | **Reproducibility** | N/A |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 15-Phosphorus | **Target Version** | - | **Fixed in Version** | - |
### Description :
This is a follow-up on issue https://bts.frama-c.com/view.php?id=2300 which was rather briskly closed.
I can understand that the question on the semantics of statement contracts in WP is not discussed in the ACSL implementation manual. However, in my opinion, it should then be discussed in the WP manual.Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/331suggestions for improvement of Sect.3.6 and 3.7 of the wp manual2023-07-24T10:43:54ZJochen Burghardtsuggestions for improvement of Sect.3.6 and 3.7 of the wp manualID0002313:
**This issue was created automatically from Mantis Issue 2313. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002313:
**This issue was created automatically from Mantis Issue 2313. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002313 | Frama-C | Documentation > manuals | public | 2017-06-15 | 2017-06-23 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | text | **Reproducibility** | N/A |
| **Platform** | wp-manual-Phosphorus-20170501.pd | **OS** | n/a | **OS Version** | - |
| **Product Version** | Frama-C 15-Phosphorus | **Target Version** | - | **Fixed in Version** | - |
### Description :
In the WP manual, section 3.6 "The Typed Memory Model", instead of explaining the "Typed" memory model, refers to an old "Store" memory model and only describes the differences. However, few (and increasingly fewer) users are familiar with that old model, let alone availability issues of old WP manuals. Therefore, the "Typed" model should be described from scratch. Also, the section should initially state that it is about the model named "Typed".
In section 3.7, I found the following senteces hard to understand, and added my questions in "{}":
This detection is more clever than the standard one {That is, the one of the "Typed" model?} since it only takes into account local usage {What is local and global usage of a function? How can an approach being more clever than another one although it is based on less information?} of each function (not global ones).
Additionally, the Caveat memory model of Frama-C performs a local allocation {What is a local allocation? Shouldn't Frama-C's allocation reflect those made by the C compiler, which pushes actual parameters on the local stack in a new stack-frame, and expects formal parameters on the local stack in the current stack frame?} of formal parameters with pointer types that cannot be treated as reference parameters.
This makes explicit the separation hypothesis of memory regions pointed by formals in the Caveat tool. The major benefit of the WP version {Compared to what? To the Caveat tool? To the plain "Typed" model?} is that aliases are taken into account by the Typed memory model, hence, there are no more suspicious aliasing warnings.Loïc CorrensonLoïc Corrensonhttps://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/396Compiling on Windows (cygwin) fails2021-02-22T13:01:11Zmantis-gitlab-migrationCompiling on Windows (cygwin) failsID0002247:
**This issue was created automatically from Mantis Issue 2247. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002247:
**This issue was created automatically from Mantis Issue 2247. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002247 | Frama-C | Documentation > manuals | public | 2016-10-01 | 2016-12-05 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | vlad | **Assigned To** | maroneze | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | Windows | **OS Version** | 7 |
| **Product Version** | Frama-C Aluminium | **Target Version** | - | **Fixed in Version** | - |
### Description :
Windows installation fails when building frama-c as described here: https://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:compiling_from_source
<pre>
$ 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 =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
=-=- 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
FRAMAC_TOP_SRCDIR=C:/Users/User/AppData/Roaming/SPB_Data/.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 FRAMAC_TOP_SRCDIR=C:/Users/User/AppData/Roaming/SPB_Data/.opam/4.02.3+mingw32/build/frama-c-base.20160501 all
### stdout ###
# [...]
### stderr ###
# 4 shift/reduce conflicts.
# 7 shift/reduce conflicts.
# src/libraries/utils/c_bindings.c:1:0: warning: -fPIC ignored for target (all code is position independent)
# /**************************************************************************/
# ^
# src/libraries/utils/c_bindings.c:28:27: fatal error: caml/mlvalues.h: No such file or directory
# compilation terminated.
# make: *** [Makefile:882: src/libraries/utils/c_bindings.o] Error 1
=-=- 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
</pre>https://git.frama-c.com/pub/frama-c/-/issues/138tset issues in manual "acsl-implementation-Aluminium-20160501.pdf"2021-02-22T12:54:36ZJochen Burghardttset issues in manual "acsl-implementation-Aluminium-20160501.pdf"ID0002236:
**This issue was created automatically from Mantis Issue 2236. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002236:
**This issue was created automatically from Mantis Issue 2236. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002236 | Frama-C | Documentation > manuals | public | 2016-06-27 | 2019-07-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | patrick | **Resolution** | fixed |
| **Priority** | normal | **Severity** | text | **Reproducibility** | N/A |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
in fig.2.7 on p.35, the alternative for set comprehension should be
"{ term | binders ..." rather than " tset | binders ... ". The next line's alternative should also use "term" rather than "tset". In the corresponding explanation for set comprehension, probably not "the union of the sets denoted by s" is meant but rather "the set of all terms denoted by s".
When the rule "location-address ::= tset" is shown on p.58 and 79, and "location ::= tset" on p.29 (BTW: I wonder whether both rules should be joined into a single one?), some remark could be given on the semantics of (a singleton containing just) a proper-expression term. For example, "assigns n*n" seems perfectly valid, when "n" is an integer variable - are such clauses forbidden, or do they have a reasonable meaning?
On p.93, in the subsection "Typing rules for sets", rule 4 and 5 appear to deviate from the syntactical form explained at subsection start. There is no \vdash in the antecedent of rule 4, and no comma right of a \vdash in any of the involved 4 lines. In rule 5's antecedent, "b \cup \Lambda" should probably read "b:bool \cup \Lambda". I also didn't understand what "tset \tau" should mean.
In Fig.2.25 on p.72, no initialisation of a model variable is admitted by the grammar (since the rule "parameter ::= type-expr id", appearing on p.49 in Fig.2.12, dosn't allow an initialization), while in example 2.61 on p.73, the model variable "forbidden" is initialized, and apparently by a tset, viz. "\empty".https://git.frama-c.com/pub/frama-c/-/issues/485provide "Magnesium" product version in the BTS2021-02-22T13:03:45ZJens Gerlachprovide "Magnesium" product version in the BTSID0002204:
**This issue was created automatically from Mantis Issue 2204. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002204:
**This issue was created automatically from Mantis Issue 2204. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002204 | Frama-C | Documentation | public | 2016-01-26 | 2016-06-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C Magnesium |
### Description :
Currently it is not possible to submit "magnesium" bugs to the BTS as it still refers only to Neon and Sodium.
(Sorry for posting this here.)https://git.frama-c.com/pub/frama-c/-/issues/482typo in output of 'frama-c -wp-help'2022-09-28T12:24:02ZJens Gerlachtypo in output of 'frama-c -wp-help'ID0002198:
**This issue was created automatically from Mantis Issue 2198. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002198:
**This issue was created automatically from Mantis Issue 2198. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002198 | Frama-C | Documentation | public | 2015-12-09 | 2016-06-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Sodium | **Target Version** | Frama-C Aluminium | **Fixed in Version** | - |
### Description :
In the description of option '-wp-prop' the help option '-wp-help' says
"Accepted categories are: lemmas, ..."
The WP manuals says (and the observed behavior of WP agrees with it)
"Recognized categories are: @lemma,..." (without s).
### Additional Information :
It's a minor typo but I actually ran into it.
Should be easy to fix.
### Steps To Reproduce :
Just run 'frama-c -wp-help'Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/480Bug in example - plugin documentation2021-02-22T13:03:35Zmantis-gitlab-migrationBug in example - plugin documentationID0001979:
**This issue was created automatically from Mantis Issue 1979. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001979:
**This issue was created automatically from Mantis Issue 1979. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001979 | Frama-C | Documentation > manuals | public | 2014-11-21 | 2016-06-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | gavran | **Assigned To** | Matthieu Lemerre | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Linux | **OS** | Debian | **OS Version** | 7 |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | Frama-C Sodium | **Fixed in Version** | Frama-C Sodium |
### Description :
In Plugin development guide (available at frama-c.com/download.html, chapter 2.3.2 code for method vstmt_aux:
- color should be defined without brackets (currently, it is inside [ ] which is duplicating brakets and yields syntax error)https://git.frama-c.com/pub/frama-c/-/issues/479Manuals are not in the distribution2021-02-22T13:03:34Zmantis-gitlab-migrationManuals are not in the distributionID0001822:
**This issue was created automatically from Mantis Issue 1822. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001822:
**This issue was created automatically from Mantis Issue 1822. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001822 | Frama-C | Documentation > manuals | public | 2014-06-30 | 2016-06-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Anne | **Assigned To** | bobot | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | Frama-C Sodium |
### Description :
I am pretty sure that the manuals were distributed with previous version, but there don't come anymore with Neon. Is this on purpose ?
In the Makefile, there is still ``doc/manuals/*.pdf`` in the list of distributed files, but the ``doc/manual`` directory doesn't exist anymore.https://git.frama-c.com/pub/frama-c/-/issues/481wrong link in e-acsl documentation2021-02-22T13:03:36ZJens Gerlachwrong link in e-acsl documentationID0001782:
**This issue was created automatically from Mantis Issue 1782. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001782:
**This issue was created automatically from Mantis Issue 1782. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001782 | Frama-C | Documentation > manuals | public | 2014-05-21 | 2016-06-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | trivial | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | Frama-C Sodium |
### Description :
On page 30 of the e-acsl manual there is a link in entry 13 of the bibliography.
This link does not work.https://git.frama-c.com/pub/frama-c/-/issues/484quality of pdf files2021-02-22T13:03:44ZJens Gerlachquality of pdf filesID0001771:
**This issue was created automatically from Mantis Issue 1771. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001771:
**This issue was created automatically from Mantis Issue 1771. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001771 | Frama-C | Documentation | public | 2014-05-02 | 2016-06-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | low | **Severity** | minor | **Reproducibility** | always |
| **Platform** | OSX | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | Frama-C Magnesium |
### Description :
This might sound very subjective but I always have the feeling that the various pdf files of the Frama-C documentation look a bit blurred.
I do not observe this with my own pdf files that I generate from latex.
It is neither related to Neon nor am I using a retina display.
I wonder whether you are using the "computer modern" family of type faces.
### Steps To Reproduce :
Compare
http://www.fokus.fraunhofer.de/de/sqc/_download_sqc/ACSL-by-Example.pdf
with
http://frama-c.com/download/acsl-implementation-Neon-20140301.pdf