frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2021-02-22T13:03:31Zhttps://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/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?https://git.frama-c.com/pub/frama-c/-/issues/433Fraunhofer FIRST -> Fraunhofer FOKUS2021-02-22T13:02:21ZJens GerlachFraunhofer FIRST -> Fraunhofer FOKUSID0001334:
**This issue was created automatically from Mantis Issue 1334. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001334:
**This issue was created automatically from Mantis Issue 1334. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001334 | Frama-C | Documentation | public | 2012-12-17 | 2016-06-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | patrick | **Resolution** | fixed |
| **Priority** | normal | **Severity** | text | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Oxygen-20120901 | **Target Version** | - | **Fixed in Version** | Frama-C Fluorine-20130401 |
### Description :
Fraunhofer FIRST has been merged into Fraunhofer FOKUS.
Please change URL on http://frama-c.com/wp.html to
www.fokus.fraunhofer.dehttps://git.frama-c.com/pub/frama-c/-/issues/432new link to ACSL by Example2021-02-22T13:02:20ZJens Gerlachnew link to ACSL by ExampleID0001335:
**This issue was created automatically from Mantis Issue 1335. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001335:
**This issue was created automatically from Mantis Issue 1335. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001335 | Frama-C | Documentation | public | 2012-12-17 | 2016-06-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | patrick | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Oxygen-20120901 | **Target Version** | - | **Fixed in Version** | Frama-C Fluorine-20130401 |
### Description :
Due to the merge of Fraunhofer FIRST with Fraunhofer FOKUS there is a new URL for the "ACSL by Example" documents.
I suggest to add the new URL
http://www.fokus.fraunhofer.de/de/quest/_download_quest/_projekte/acsl_by_example.pdf
on
http://frama-c.com/wp.htmlhttps://git.frama-c.com/pub/frama-c/-/issues/407Non working example in the documentation2021-02-22T13:37:00Zmantis-gitlab-migrationNon working example in the documentationID0001098:
**This issue was created automatically from Mantis Issue 1098. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001098:
**This issue was created automatically from Mantis Issue 1098. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001098 | Frama-C | Documentation | public | 2012-02-17 | 2016-08-31 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | ploc | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Nitrogen-20111001 | **Target Version** | Frama-C Sodium | **Fixed in Version** | Frama-C Sodium |
### Description :
In logic_typing.ml the example to illustrate the definition of a new keyword is not typable.
The correct version is :
let foo_typer ~typing_context ~loc bhv ps =
match ps with
| p::[] ->
bhv.b_extended
<- ("FOO",42, [Logic_const.new_predicate (typing_context.type_predicate (typing_context.post_state [Normal]) p)]) ::bhv.b_extended
| _ -> typing_context.error loc "expecting a predicate after keyword FOO"
let () = register_behavior_extension "FOO" foo_typerhttps://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/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/436Cute boolean options too cute for their own good2021-02-22T13:02:29ZPascal CuoqCute boolean options too cute for their own goodID0001085:
**This issue was created automatically from Mantis Issue 1085. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001085:
**This issue was created automatically from Mantis Issue 1085. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001085 | Frama-C | Documentation | public | 2012-02-08 | 2016-06-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Oxygen-20120901 |
### Description :
$ bin/toplevel.opt -kernel-help
Description: General options provided by the Frama-C kernel
Most options of the form '-option-name' and without any parameter
have an opposite with the name '-no-option-name'.
***** LIST OF AVAILABLE OPTIONS:
*** ANALYSIS OPTIONS
...
-safe-arrays for arrays that are fields inside structs, assume that
accesses are in bounds (set by default)
...
There is no way to know that the option to unset this option is -unsafe-arrayshttps://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/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/437gui and doc2021-02-22T13:57:53ZMuriel Rogergui and docID0001014:
**This issue was created automatically from Mantis Issue 1014. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001014:
**This issue was created automatically from Mantis Issue 1014. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001014 | Frama-C | Documentation | public | 2011-11-10 | 2016-06-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | muriel | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Nitrogen-20111001 | **Target Version** | - | **Fixed in Version** | Frama-C Oxygen-20120901 |
### Description :
generation of documentation (via make doc) has permanently fail when gui is not installed :
File "src/occurrence/register_gui.ml", line 23, characters 0-18:
Error: Unbound module Pretty_source
1 error(s) encounteredhttps://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/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/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/440cannot deal with many files2021-02-22T13:38:02Zmantis-gitlab-migrationcannot deal with many filesID0000778:
**This issue was created automatically from Mantis Issue 778. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000778:
**This issue was created automatically from Mantis Issue 778. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000778 | Frama-C | Documentation | public | 2011-04-08 | 2016-06-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | njucslzh | **Assigned To** | monate | **Resolution** | no change required |
| **Priority** | normal | **Severity** | block | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20110201 | **Target Version** | - | **Fixed in Version** | - |
### Description :
When I have many files which are in a project to analysis , it always cannot correctly preprocess them. Errors as follow:
[gui] warning: Frama-C images not found. Is FRAMAC_SHARE correctly set?
[kernel] preprocessing with "gcc -C -E -I. /home/lzh/cvs-1.11.4/src/zlib.c"
[kernel] user error: failed to run: gcc -C -E -I. -o '/tmp/zlib.c788cad.i' '/home/lzh/cvs-1.11.4/src/zlib.c'
you may set the CPP environment variable to select the proper preprocessor command or use the option "-cpp-command".
[kernel] user error: skipping file "/home/lzh/cvs-1.11.4/src/zlib.c" that has errors.
### Additional Information :
For toy program with two or three simply files, I just change c files to i files directly , it works well. But in practical , this don't work. Can you show me how to preprocess and merge the Source Code files? It is described too little in user manual .https://git.frama-c.com/pub/frama-c/-/issues/441mismatch between configure check and INSTALL requirements for ocamlgraph version2021-02-22T14:00:33ZJulien Signolesmismatch between configure check and INSTALL requirements for ocamlgraph versionID0000757:
**This issue was created automatically from Mantis Issue 757. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000757:
**This issue was created automatically from Mantis Issue 757. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000757 | Frama-C | Documentation | public | 2011-03-17 | 2016-06-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | signoles | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | tweak | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20110201 | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
configure checks an exact version number for ocamlgraph, while INSTALL says >=.
### Additional Information :
Don't know what is the best thing to do:
- allowing >= is better, but requires that ocamlgraph is stable enough (forward compatibility). Not sure that it is the case yet :-(.
- allowing only = is simpler, but much less flexible for users.https://git.frama-c.com/pub/frama-c/-/issues/442Patch for Cross Compiling OCaml-3.12.0(for arm-linux)2021-02-22T13:02:37Zmantis-gitlab-migrationPatch for Cross Compiling OCaml-3.12.0(for arm-linux)ID0000631:
**This issue was created automatically from Mantis Issue 631. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000631:
**This issue was created automatically from Mantis Issue 631. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000631 | Frama-C | Documentation | public | 2010-11-25 | 2016-06-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Frank-Chen | **Assigned To** | signoles | **Resolution** | no change required |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
The patch I am uploading is from Eric Cooper(ecc@cmu.edu,http://www.cs.cmu.edu/~ecc/).He sent it to me a month ago.With the patch , I succeeded in making a OCaml-cross-compiler-3.12.0(with a new EABI based arm-linux-gcc-4.3.2),and when I used it to cross-compile mldonkey-3.0.2,mlnet was also generated successfully(you have to configrue with "./configure --enable-ocamlver=3.12.0 --host=arm-linux" and build some .o files with the "compile_by_hand.sh" I am also uploading).But Because this OCaml-cross-compiler-3.12 seems to only support the new EABI but my target machine just supports the old ABI(and the gcc cross compiler of my machine just supports soft float-point), I can't run it on my target machine and don't know whether the mlnet can run perfectly in a new EABI based machine.So I 'd like to upload the patch here and all of you can test it.Maybe someone who want to do a cross-compiling will find it useful.
By the way ,does this kind of version of OCaml which supports soft float-point and the Old ABI(not the new EABI) exist?It seems that OCaml 3.12 adds soft float-point and EABI support together,but I just need soft float-point and the Old ABI.
Best Regards!
Frank-Chen
## Attachments
- [cross-compiler-for-arm-target.patch](/uploads/068b76e2937191decde9dec773884cdf/cross-compiler-for-arm-target.patch)
- [README.cross](/uploads/a9a7684367b4eb08069863d3e15f62c1/README.cross)
- [compile_by_hand.sh](/uploads/cf6e415fcbf8a46c91bdd530c9b04203/compile_by_hand.sh)https://git.frama-c.com/pub/frama-c/-/issues/443Implementation <-> Documentation Inconsistency2021-02-22T13:02:38Zmantis-gitlab-migrationImplementation <-> Documentation InconsistencyID0000595:
**This issue was created automatically from Mantis Issue 595. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000595:
**This issue was created automatically from Mantis Issue 595. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000595 | Frama-C | Documentation | public | 2010-10-04 | 2016-06-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | kalyan | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | N/A |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Boron-20100401 | **Target Version** | Frama-C Carbon-20101201-beta1 | **Fixed in Version** | Frama-C Carbon-20101201-beta1 |
### Description :
I see that the Plug-in development guide is not accurate (or consistent with the implementation, if I should put it this way). It makes it difficult for beginners to work with plugin-development, especially using visitors. For example, Section 4.14.3 (Action Performed) and compare it with the implementation, you don't see any DoChildrenPost () and you don't see any JustCopyPost () in the guide. It would be great if you update the plugin-development guide as and when you make changes in the implementation.