frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2021-02-22T13:05:28Zhttps://git.frama-c.com/pub/frama-c/-/issues/544assumes clause and labels2021-02-22T13:05:28ZJens Gerlachassumes clause and labelsID0002040:
**This issue was created automatically from Mantis Issue 2040. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002040:
**This issue was created automatically from Mantis Issue 2040. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002040 | Frama-C | Plug-in > wp | public | 2014-12-27 | 2016-01-26 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | high | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | Frama-C Magnesium |
### Description :
My understanding of assumes clauses is that they refer to the pre-state of a function.
The attached example, however, works differently.
The function push_back has two disjoint behaviors that rely on the predicate "full".
The function push_back_twice is only verified if I add the label "Pre"
to the predicate "full" in the assumes clauses of function push_back.
I think this is a bug.
It should not be necessary to add this explicit label.
### Additional Information :
Concerns versions
Neon-20140301
Neon-20140301+dev-stance
I remember that Kim Völlinger had observed the same(?) problem in Oxygen and
that it was fixed in Fluorine.
## Attachments
- [assumes_label.c](/uploads/c4f41bff0222c51c966f982647981368/assumes_label.c)https://git.frama-c.com/pub/frama-c/-/issues/540predicate definitions should be of type prop2021-02-22T13:05:22ZClaude Marchépredicate definitions should be of type propID0000444:
**This issue was created automatically from Mantis Issue 444. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000444:
**This issue was created automatically from Mantis Issue 444. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000444 | Frama-C | Kernel > ACSL implementation | public | 2010-04-08 | 2016-01-26 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | cmarche | **Assigned To** | virgile | **Resolution** | no change required |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090902 | **Target Version** | - | **Fixed in Version** | - |
### Description :
In a predicate definition like below
//@ predicate f(integer x) = x+1;
it should be checked that the body of the definition denotes a prop and not a termhttps://git.frama-c.com/pub/frama-c/-/issues/534memory leak (endless recursion?) caused by erroneous c program2021-02-22T13:05:10ZJochen Burghardtmemory leak (endless recursion?) caused by erroneous c programID0002184:
**This issue was created automatically from Mantis Issue 2184. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002184:
**This issue was created automatically from Mantis Issue 2184. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002184 | Frama-C | Plug-in > wp | public | 2015-11-02 | 2016-01-26 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | Sodium-20150201 | **OS** | - | **OS Version** | 14.04.1-Ubuntu |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | Frama-C Magnesium |
### Description :
Running "frama-c 10.c" on the attached program causes frama-c to allocate a rapidly increasing amount of memory, until it crashes with the unbuntu-message "Fatal error: out of memory." Apparently, it performs an endless recursion.
The program "10.c" is erroneous and nonsensical, and originates from a "creduce" experiment with a poor test script. However, it may be worth to eliminate the endless recusion, anyway?
## Attachments
- [10.c](/uploads/6b5ba89a77511be850092e7d6514913b/10.c)https://git.frama-c.com/pub/frama-c/-/issues/532"If" statement with only one successor2021-02-22T13:05:08ZHugo Illous"If" statement with only one successorID0002119:
**This issue was created automatically from Mantis Issue 2119. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002119:
**This issue was created automatically from Mantis Issue 2119. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002119 | Frama-C | Kernel | public | 2015-05-20 | 2016-01-26 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | hugo.illous | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Magnesium |
### Description :
When a "If" statements contains in its true block the sequence "do {} while (0);", in the CFG, this statement will have only one successor.
### Steps To Reproduce :
You can simply try with this C program and compute List.length stmt.succs
void f(int n) {
if (n == 0) do {} while (0);
}https://git.frama-c.com/pub/frama-c/-/issues/529overloading of predicate fails2021-02-22T13:05:00ZJens Gerlachoverloading of predicate failsID0002098:
**This issue was created automatically from Mantis Issue 2098. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002098:
**This issue was created automatically from Mantis Issue 2098. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002098 | Frama-C | Kernel > ACSL implementation | public | 2015-03-31 | 2016-01-26 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Sodium | **Target Version** | Frama-C Magnesium | **Fixed in Version** | Frama-C Magnesium |
### Description :
Overloading of ACSL predicates does not work anymore.
### Additional Information :
the problem does NOT occur under Neon.
### Steps To Reproduce :
the attached program reports the following error when called with 'frama-c overloading.c'
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing overloading.c (with preprocessing)
overloading.c:10:[kernel] user error: invalid implicit conversion from 'int' to 'short' in annotation.
[kernel] user error: stopping on file "overloading.c" that has errors. Add '-kernel-msg-key pp'
for preprocessing command.
[kernel] Frama-C aborted: invalid user input.
## Attachments
- [overloading.c](/uploads/9a26b0d025434222fddb2f37e1e99e80/overloading.c)
- [overloading2.c](/uploads/09b42bc4285c4460e2dc291ef3a83c3b/overloading2.c)https://git.frama-c.com/pub/frama-c/-/issues/522provide option "-wp-lemma"2021-02-22T13:04:45ZJens Gerlachprovide option "-wp-lemma"ID0002202:
**This issue was created automatically from Mantis Issue 2202. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002202:
**This issue was created automatically from Mantis Issue 2202. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002202 | Frama-C | Plug-in > wp | public | 2016-01-23 | 2016-02-23 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | - |
### Description :
WP has several options to consider only individual functions, properties, or behaviors during verification.
It would be nice if there were an option "-wp-lemma 'name' " which would allow to consider only the names lemma.https://git.frama-c.com/pub/frama-c/-/issues/504Reals are bad encoded for coq2021-02-22T13:04:23Zmantis-gitlab-migrationReals are bad encoded for coqID0002214:
**This issue was created automatically from Mantis Issue 2214. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002214:
**This issue was created automatically from Mantis Issue 2214. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002214 | Frama-C | Plug-in > wp | public | 2016-03-03 | 2016-06-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | davyg | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | All | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Magnesium | **Target Version** | - | **Fixed in Version** | Frama-C Aluminium |
### Description :
The definition of real_base(Qedlib) in the coq exporter of wp is incorrect :
There is :
Definition real_base e a n :=
match n with
| 0 => 1%R
| Zpos n => (a * pow e (Pos.to_nat n))%R
| Zneg n => (a / pow e (Pos.to_nat n))%R
end.
in stead of
Definition real_base e a n :=
match n with
| 0 => a
| Zpos n => (a * pow e (Pos.to_nat n))%R
| Zneg n => (a / pow e (Pos.to_nat n))%R
end.
### Steps To Reproduce :
I think that any coq proof you try to prove with wp containing real constant should have the errorhttps://git.frama-c.com/pub/frama-c/-/issues/502Values inferred for 32-bit variable do not fit in 32-bit type2021-02-22T13:04:21ZPascal CuoqValues inferred for 32-bit variable do not fit in 32-bit typeID0001968:
**This issue was created automatically from Mantis Issue 1968. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001968:
**This issue was created automatically from Mantis Issue 1968. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001968 | Frama-C | Plug-in > Eva | public | 2014-11-13 | 2016-06-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | valentin.perrelle | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C Aluminium |
### Description :
The values inferred for the variable i below are 64-bit values that wouldn't even fit the 32-bit unsigned int that variable i is.
Program:
int main() {
Frama_C_show_each(sizeof(unsigned int));
unsigned int i = 0;
while (u())
{
i+=2;
}
}
$ frama-c -val t.c
…
[value] Called Frama_C_show_each({4})
…
[value] Values at end of function main:
i ∈ [0..9223372036854775806],0%2https://git.frama-c.com/pub/frama-c/-/issues/501coq fails to compile Cint because Zbits is not found2021-02-22T13:04:18Zmantis-gitlab-migrationcoq fails to compile Cint because Zbits is not foundID0002155:
**This issue was created automatically from Mantis Issue 2155. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002155:
**This issue was created automatically from Mantis Issue 2155. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002155 | Frama-C | Plug-in > wp | public | 2015-09-02 | 2016-06-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | kroeckx | **Assigned To** | patrick | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | Frama-C Aluminium |
### Description :
As described in https://lists.gforge.inria.fr/pipermail/frama-c-discuss/2014-March/004380.html, I get the same error message that Cint can't be compiled because Zbits isn't compiled yet.
I'm getting this on a Debian system.
I attached a patch based on the mail that seems to fix the issue for me.
## Attachments
- [wp.driver.patch](/uploads/a497ab58ae4dc3b1ac4220b14fafbd1d/wp.driver.patch)https://git.frama-c.com/pub/frama-c/-/issues/496Frama-c accepts assigning formal parameters when a range is used2021-02-22T13:04:05Zmantis-gitlab-migrationFrama-c accepts assigning formal parameters when a range is usedID0002217:
**This issue was created automatically from Mantis Issue 2217. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002217:
**This issue was created automatically from Mantis Issue 2217. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002217 | Frama-C | Kernel | public | 2016-03-17 | 2016-06-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Ian | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | Ubuntu | **OS Version** | - |
| **Product Version** | Frama-C Magnesium | **Target Version** | - | **Fixed in Version** | Frama-C Aluminium |
### Description :
When assigning a range, no error is produced when referencing a formal parameter.
### Steps To Reproduce :
test.c:
typedef struct obj {
char buf[5];
} obj;
/*@
assigns x.buf[0..0];
*/
void foo(obj x);
void bar() {
obj tmp;
foo(tmp);
//@ assert \true;
}
Running as given above produces no error (it should).
> frama-c test.c
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing test.c (with preprocessing)
Running the above program with wp causes an error.
> frama-c test.c -wp
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing test.c (with preprocessing)
[wp] warning: Missing RTE guards
test.c:6:[wp] user error: Address of logic value (tmp_0)
[kernel] Plug-in wp aborted: invalid user input.
Changing the specification of foo to “assigns x.buf[0]” results in the expected error.
> frama-c test.c
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing test.c (with preprocessing)
test.c:6:[kernel] user error: can not assign part of a formal parameter: x.buf[0]
[kernel] user error: stopping on file "test.c" that has errors. Add '-kernel-msg-key pp'
for preprocessing command.
[kernel] Frama-C aborted: invalid user input.https://git.frama-c.com/pub/frama-c/-/issues/494missing lower bound of ACSL operator ".." not detected by Magnesium2021-02-22T13:04:01ZJochen Burghardtmissing lower bound of ACSL operator ".." not detected by MagnesiumID0002230:
**This issue was created automatically from Mantis Issue 2230. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002230:
**This issue was created automatically from Mantis Issue 2230. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002230 | Frama-C | Plug-in > wp | public | 2016-06-13 | 2016-06-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | suspended |
| **Priority** | none | **Severity** | feature | **Reproducibility** | always |
| **Platform** | Magnesium | **OS** | xubuntu-14.04 | **OS Version** | - |
| **Product Version** | Frama-C Magnesium | **Target Version** | - | **Fixed in Version** | Frama-C Aluminium |
### Description :
The Frama-C Magnesium parser didn't complain about the missing lower bound of "..".
The Frama-C Aluminium parser does find the syntax error (in fact, this was the way we detected it).
We therefore intend this issue not as a bug report, but merely as another regression test on future Frama-C releases. There is nothing to be fixed now.
## Attachments
- [486.c](/uploads/3fc4fdf16d4ecfe42871670515e0ef32/486.c)
- [max_element.c](/uploads/c5be5280ef02a12d06e4b53b840cb0b9/max_element.c)https://git.frama-c.com/pub/frama-c/-/issues/486doubling of a word2021-02-22T13:03:46ZJens Gerlachdoubling of a wordID0002183:
**This issue was created automatically from Mantis Issue 2183. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002183:
**This issue was created automatically from Mantis Issue 2183. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002183 | Frama-C | Documentation > ACSL | public | 2015-10-30 | 2016-06-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | maroneze | **Resolution** | fixed |
| **Priority** | normal | **Severity** | trivial | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Sodium | **Target Version** | Frama-C Aluminium | **Fixed in Version** | Frama-C Aluminium |
### Description :
On Page 25 of acs-implementation-Sodium-20150201.pdf (Section 2.2.6) there is the sentence
Unlike in C, there is no implicit cast from from an array type to a pointer type.
Please remove one occurrence of "from".
### Additional Information :
I normally use the attached perl script to remove duplicate entries in text files
## Attachments
- [duplicate.pl](/uploads/312364e1f963474ca5c11499489bcc13/duplicate.pl)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/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/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/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.