frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2021-02-22T12:56:27Zhttps://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/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/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/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/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/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/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 Maroneze