frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2023-05-16T06:53:50Zhttps://git.frama-c.com/pub/frama-c/-/issues/2646OPAM installation on macOS fails2023-05-16T06:53:50ZvarosiOPAM installation on macOS fails<!--
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
<!--
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
To install correctly using OPAM on macOS Ventura 13.2 on x64 following - https://frama-c.com/html/get-frama-c.html
### Actual behaviour
After running **opam install frama-c**, I got:
```
> <><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
> -> removed conf-gtk2.1
> -> installed conf-gtk2.1
> -> retrieved frama-c.21.1 (cached)
> [ERROR] The compilation of frama-c.21.1 failed at "make -j11".
>
> #=== ERROR while compiling frama-c.21.1 =======================================#
> # context 2.1.4 | macos/x86_64 | ocaml-base-compiler.4.07.1 | https://opam.ocaml.org#0c15cf29
> # path ~/.opam/default/.opam-switch/build/frama-c.21.1
> # command ~/.opam/opam-init/hooks/sandbox.sh build make -j11
> # exit-code 2
> # env-file ~/.opam/log/frama-c-37505-febf41.env
> # output-file ~/.opam/log/frama-c-37505-febf41.out
> ### output ###
> # [...]
> # Ocamlc src/plugins/qed/hcons.cmo
> # Ocamlc src/plugins/qed/listmap.cmo
> # Ocamlc src/plugins/qed/listset.cmo
> # Ocamlc src/plugins/qed/intmap.cmo
> # Ocamlc src/plugins/qed/intset.cmo
> # File "src/plugins/markdown-report/sarif.ml", line 31, characters 17-30:
> # Error: Unbound type constructor Yojson.Safe.t
> # make: *** [src/plugins/markdown-report/sarif.cmo] Error 2
> # make: *** Waiting for unfinished jobs....
> # Ocamlc src/plugins/qed/idxmap.cmo
> # AR src/plugins/e-acsl/lib/libeacsl-dlmalloc.a
> # RANLIB src/plugins/e-acsl/lib/libeacsl-dlmalloc.a
```
### Contextual information
- Frama-C installation mode: Opam
- Frama-C version: not installed previously
- OS name: macOS
- OS version: Ventura 13.2 on x64Andre MaronezeAndre Maronezehttps://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/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.pdfhttps://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/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/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/477Erreur dans la documentation pour plugin contradiction sur nom de fichiers2021-02-22T13:03:31Zmantis-gitlab-migrationErreur dans la documentation pour plugin contradiction sur nom de fichiersID0001731:
**This issue was created automatically from Mantis Issue 1731. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001731:
**This issue was created automatically from Mantis Issue 1731. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001731 | Frama-C | Documentation | public | 2014-04-05 | 2016-06-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | zuy | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | low | **Severity** | text | **Reproducibility** | always |
| **Platform** | All | **OS** | All | **OS Version** | All |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | Frama-C Sodium |
### Description :
Dans la documentation de développement de plugin "plugin-development-guide-N-X" notamment dans la documentation de plugin-development-guide-Neon-20140301 à la page 17, il est fait référence à la création d'un fichier Hello_options.ml mais le module référencé est Hello_register et non Hello_options
### Additional Information :
Changer le fichier Hello_options.ml en fichier Hello_register.ml sera moins couteux que d'aller changer les Hello_register.* dans le code source.
### Steps To Reproduce :
Lire la documentation et essayer de faire le tutoriel, on tombe sur une incohérence si on s'en tient à la lecture et probablement sur des bugs disant module not found si on copie colle pour tester.https://git.frama-c.com/pub/frama-c/-/issues/475Erreur dans la documentation pour plugin erreur de type2021-02-22T13:37:51Zmantis-gitlab-migrationErreur dans la documentation pour plugin erreur de typeID0001732:
**This issue was created automatically from Mantis Issue 1732. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001732:
**This issue was created automatically from Mantis Issue 1732. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001732 | Frama-C | Documentation > manuals | public | 2014-04-05 | 2016-06-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | zuy | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | low | **Severity** | text | **Reproducibility** | always |
| **Platform** | All | **OS** | All | **OS Version** | All |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | Frama-C Sodium |
### Description :
A la page 18 de la documentation de développement d'un plugin, il est question d'ajouter une option au plugin en cours de développement.
L'option en question est la possibilité de spécifier la sortie des écritures standard du plugin.
output_fun est alors censé contenir la fonction qui prend un formateur par défaut et attend un string en entrée pour produire un unit (dans le if) mais la branche else ouvre un fichier crée la fonction en question avec fprintf mais un point-virgule et un appel à close_out rend le type des deux branches incompatible.
### Additional Information :
Une solution à la fois simple et propre serait de rester dans l'optique du découpage du code en module
de la page précédente et de définir dans printer un type nécessaire à ses fonctions
après création du printer on récupère un channel qui est le standard ou celui d'un fichier particulier, on peut alors écrire dedans (si c'est le standard tant mieux on utilise result sinon on utilise fprintf.
puis on ferme (si c'est le standard on ne fait rien sinon ou appel close_out dessus)
### Steps To Reproduce :
Lire la documentationhttps://git.frama-c.com/pub/frama-c/-/issues/472Jessie tutorial binary_search examples fail with Why 2.23 - loop variant must...2021-02-22T14:01:36Zmantis-gitlab-migrationJessie tutorial binary_search examples fail with Why 2.23 - loop variant must be addedID0000365:
**This issue was created automatically from Mantis Issue 365. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000365:
**This issue was created automatically from Mantis Issue 365. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000365 | Frama-C | Documentation > manuals | public | 2010-01-04 | 2016-06-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dwheeler | **Assigned To** | cmarche | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090902 | **Target Version** | - | **Fixed in Version** | Frama-C Carbon-20101201-beta1 |
### Description :
The Jessie tutorial in:
http://frama-c.cea.fr/jessie_tutorial_index.html
sections 2.1 and 2.2 include binary_search examples.
If "Why" is upgraded to Why 2.23, these no longer work,
because there is no loop variant provided.
The single loop invariant must be changed to be:
/*@ loop invariant 0 <= l && u <= n-1;
loop variant u-l; */
In addition, explain loop variants, since they are
absolutely necessary to use Why 2.23.
Also, please note in the documentation that this will NOT work:
//@ loop invariant 0 <= l && u <= n-1;
//@ loop variant u-l;
Basically, make it clear that you're not allowed to have
"//@" in succession, especially since doing this produces a
mysterious and misleading error message. See bug 79.
The example of 2.2 should end up looking like this (the lemma is optional):
/*@ lemma mean: \forall integer x, y; x <= y ==> x <= (x+y)/2 <= y; */
//@ requires n >= 0 && \valid_range(t,0,n-1);
int binary_search(int* t, int n, int v) {
int l = 0, u = n-1, p = -1;
/*@ loop invariant 0 <= l && u <= n-1;
@ loop variant u-l; */
while (l <= u ) {
int m = l + (u - l) / 2; // NOTE this is changed for bounded calculation
if (t[m] < v)
l = m + 1;
else if (t[m] > v)
u = m - 1;
else {
p = m; break;
}
}
return p;
}
### Additional Information :
Fixed in Frama-C SVN (doc/jessie)https://git.frama-c.com/pub/frama-c/-/issues/471Plug-in dev guide: tutorial for kernel integrated plug-in is out-of-date2021-02-22T14:03:32ZJulien SignolesPlug-in dev guide: tutorial for kernel integrated plug-in is out-of-dateID0000419:
**This issue was created automatically from Mantis Issue 419. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000419:
**This issue was created automatically from Mantis Issue 419. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000419 | Frama-C | Documentation > manuals | public | 2010-02-23 | 2016-06-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | signoles | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | low | **Severity** | text | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090902 | **Target Version** | - | **Fixed in Version** | Frama-C Oxygen-20120901 |
### Description :
At least Figure 2.2 and Section 2.2.4 are out-of-date according to Beryllium 2.https://git.frama-c.com/pub/frama-c/-/issues/469Wrong module name for the function prepareCFG and computeCFGInfo in the Frama...2021-02-22T13:03:20Zmantis-gitlab-migrationWrong module name for the function prepareCFG and computeCFGInfo in the Frama-C Carbon html API.ID0000821:
**This issue was created automatically from Mantis Issue 821. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000821:
**This issue was created automatically from Mantis Issue 821. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000821 | Frama-C | Documentation > manuals | public | 2011-05-11 | 2016-06-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | fgarnier | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | N/A |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20110201 | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
Inside the Cil_types.html API documentation page, the function Cil.prepareCFG and Cil.computeCFGInfo are referenced as being part of the module Cil.
Those information are exact for the Boron version of FRAMA-C, however in the
Frama-c Carbon version both functions are located in the module Cfg.
Best regards,
Florent.
### Additional Information :
We are currently operating the migration of an experimental plugin, from
the Boron version to the current version of Carbon. Unfortunately, we didn't
used many function. It is possible that we didn't noticed other ill-referenced functions.
We anyway noticed that the function Ast_info.loc_stmt isn't anymore present
within the Ast_info module, and we weren't able to find an equivalent one elsewhere. Therefore, we wrote our own.https://git.frama-c.com/pub/frama-c/-/issues/468wrong figure reference in plugin development guide2021-02-22T13:03:18ZJochen Burghardtwrong figure reference in plugin development guideID0000884:
**This issue was created automatically from Mantis Issue 884. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000884:
**This issue was created automatically from Mantis Issue 884. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000884 | Frama-C | Documentation > manuals | public | 2011-07-18 | 2016-06-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | text | **Reproducibility** | N/A |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20110201 | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
In file "plugin-development-guide-Carbon-20110201.pdf" on page 28 (sect.3.4), there is a reference to Figure 3.4, which does not exist:
BEGIN QUOTE
More generally, the set of functionalities available for a standard plug-in and for a kernel-integrated plug-in are mostly the same. The differences between a standard plug-in and a kernel-integrated one are listed Figure 3.4.
END QUOTE
Probably, the immediately following Fig.3.2 is meant.https://git.frama-c.com/pub/frama-c/-/issues/467outdated manual titles2021-02-22T13:37:33ZJochen Burghardtoutdated manual titlesID0000991:
**This issue was created automatically from Mantis Issue 991. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000991:
**This issue was created automatically from Mantis Issue 991. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000991 | Frama-C | Documentation > manuals | public | 2011-10-20 | 2016-06-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | text | **Reproducibility** | N/A |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Nitrogen-20111001 | **Target Version** | Frama-C Oxygen-20120901 | **Fixed in Version** | Frama-C Oxygen-20120901 |
### Description :
The title page of the document "acsl-implementation-Nitrogen-20111001.pdf" still says "ACSL Version 1.5 / Implementation in Carbon-20110201+dev" rather than "...Nitrogen...".
The title of "jessie-tutorial-Nitrogen-20111001.pdf" still says "Jessie Plug-In Tutorial / Frama-C version: Carbon /Jessie plug-in version: 2.28" rather than "...Nitrogen...2.29".
(I didn't check the rest.)https://git.frama-c.com/pub/frama-c/-/issues/466In section 5.11.5 of the Plugin developper manual : Reference to modules that...2021-02-22T14:01:34Zmantis-gitlab-migrationIn section 5.11.5 of the Plugin developper manual : Reference to modules that neither appear in the API nor in Frama-c source.ID0001036:
**This issue was created automatically from Mantis Issue 1036. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001036:
**This issue was created automatically from Mantis Issue 1036. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001036 | Frama-C | Documentation > manuals | public | 2011-11-30 | 2016-06-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | fgarnier | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | N/A |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Nitrogen-20111001 | **Target Version** | - | **Fixed in Version** | Frama-C Oxygen-20120901 |
### Description :
In the section 5.11.5, concerning the registration of new internal state, the
manual makes some reference to the modules/functors :
_Project.Computation.Register,
_Computation,
_Cil_computation.
I can't find them, neither in the html api --even when browsing the list of
all modules, nor while browsing both the cil source directory nor the framac
kernel directory.
Maybe the value those modules and functors used to defined have been moved
elsewhere.https://git.frama-c.com/pub/frama-c/-/issues/465suggest to mention option "-value-help" in value analysis manual2021-02-22T13:03:14ZJochen Burghardtsuggest to mention option "-value-help" in value analysis manualID0001067:
**This issue was created automatically from Mantis Issue 1067. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001067:
**This issue was created automatically from Mantis Issue 1067. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001067 | Frama-C | Documentation > manuals | public | 2012-01-19 | 2016-06-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | pascal | **Resolution** | fixed |
| **Priority** | normal | **Severity** | trivial | **Reproducibility** | N/A |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Nitrogen-20111001 | **Target Version** | - | **Fixed in Version** | Frama-C Oxygen-20120901 |
### Description :
In an attempt to find out the list of all options to the value analysis plug-in, I manually collected all tt-Font text near an occurrence of the string "option" in the value analysis manual ("value-analysis-Nitrogen-20111001.pdf"). After that, I learned about the option "-value-help", which produces another option list. Neither list is contained in the other, but they have a large intersection.
I suggest to mention in the manual the option "-value-help" (and: that it explains some options not explained in the manual). Vice versa, the manual should be mentioned in the output of the "-value-help" option.
In the long run, of course, both option lists should be made equal.
## Attachments
- [cmpOpts](/uploads/dd347a3a39625c0c49cc5fe8ff53fcb4/cmpOpts)https://git.frama-c.com/pub/frama-c/-/issues/464Plugin-development-guide section 2.1.22021-02-22T13:03:11Zmantis-gitlab-migrationPlugin-development-guide section 2.1.2ID0001088:
**This issue was created automatically from Mantis Issue 1088. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001088:
**This issue was created automatically from Mantis Issue 1088. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001088 | Frama-C | Documentation > manuals | public | 2012-02-09 | 2016-06-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | boris | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | N/A |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Nitrogen-20111001 | **Target Version** | - | **Fixed in Version** | Frama-C Oxygen-20120901 |
### Description :
Change p. 15 of plugin-development-guide from
( ?? The code below is not mandatory :
to
( ?? The function print below is not mandatory :
### Additional Information :
The code below print is mandatory.https://git.frama-c.com/pub/frama-c/-/issues/463Updated example in plugin-development-guide2021-02-22T13:03:10Zmantis-gitlab-migrationUpdated example in plugin-development-guideID0001089:
**This issue was created automatically from Mantis Issue 1089. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001089:
**This issue was created automatically from Mantis Issue 1089. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001089 | Frama-C | Documentation > manuals | public | 2012-02-09 | 2016-06-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | boris | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | N/A |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Nitrogen-20111001 | **Target Version** | - | **Fixed in Version** | Frama-C Oxygen-20120901 |
### Description :
The file attached is an updated version of example 5.14.7.
### Additional Information :
I'm unable to properly copy the comments in the guide with evince so I left them out.
## Attachments
- [ex-5-14-7.ml](/uploads/e13b056e25f714c2e9daad4e3d0111d5/ex-5-14-7.ml)https://git.frama-c.com/pub/frama-c/-/issues/462some typos etc. in the value-analysis manual2021-02-22T13:55:53ZJochen Burghardtsome typos etc. in the value-analysis manualID0001092:
**This issue was created automatically from Mantis Issue 1092. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001092:
**This issue was created automatically from Mantis Issue 1092. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001092 | Frama-C | Documentation > manuals | public | 2012-02-13 | 2016-06-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | pascal | **Resolution** | fixed |
| **Priority** | normal | **Severity** | text | **Reproducibility** | N/A |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Nitrogen-20111001 | **Target Version** | - | **Fixed in Version** | Frama-C Oxygen-20120901 |
### Description :
During reading the value-analysis manual, I collected some typos and similar issues. They are marked in cyan in the gif images (one per page) in the attached .tar.gz file. Corresponding explanatory text is contained in the file value-analysis-typos.txt.
## Attachments
- [value-analysis.tar.gz](/uploads/9bae7c84cebbee2305df46979f4d4311/value-analysis.tar.gz)https://git.frama-c.com/pub/frama-c/-/issues/460RTE - Documentation on Unary Minus2021-02-22T13:37:38Zmantis-gitlab-migrationRTE - Documentation on Unary MinusID0001620:
**This issue was created automatically from Mantis Issue 1620. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001620:
**This issue was created automatically from Mantis Issue 1620. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001620 | Frama-C | Documentation > manuals | public | 2014-01-19 | 2016-06-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dharma | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130601 | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
Hi,
RTE document (http://frama-c.com/download/rte-manual-Fluorine-20130601.pdf), section 2.1.3, assert is incorrect in that <= should be replaced by < to avoid signed overflow, right?