frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2021-02-22T13:01:49Zhttps://git.frama-c.com/pub/frama-c/-/issues/415Error in use of polyId in the 1.10 grammar2021-02-22T13:01:49ZDavid CokError in use of polyId in the 1.10 grammarID0002212:
**This issue was created automatically from Mantis Issue 2212. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002212:
**This issue was created automatically from Mantis Issue 2212. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002212 | Frama-C | Documentation > ACSL | public | 2016-02-25 | 2016-07-22 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dcok@grammatech.com | **Assigned To** | patrick | **Resolution** | won't fix |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Magnesium | **Target Version** | - | **Fixed in Version** | - |
### Description :
The 1.10 ACSL grammar defines a poly-id as a combination of a simple id, optional label-binders and optional type-var-binders. This is correct for the many places that a poly-id is used as part of a declaration. However, poly-id is also used as a term - either as a standalone variable or as the function name in a function application. Here it is a **use** of the identifier, so the contents of the type list are type expressions (as in Fig. 2.12), not type variable binders. Similarly the labels are instances of labels (including label literals such as Here), and not binders. (The comment about binders also applies to the predicate application production in Fig. 2.2). Something like a poly-id-use is needed:
poly-id-use ::= id ( { label-use ( , label-use )* } )? ( < type-expr (, type-expr )* > )?
where
label-use ::= id | label-literal
label-literal ::= Here | Pre | ...https://git.frama-c.com/pub/frama-c/-/issues/414suggest to make pdf document searchable again2024-02-21T09:26:46ZJochen Burghardtsuggest to make pdf document searchable againID0002008:
**This issue was created automatically from Mantis Issue 2008. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002008:
**This issue was created automatically from Mantis Issue 2008. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002008 | Frama-Clang | Documentation > ACSL | public | 2014-12-01 | 2016-07-27 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | - | **Resolution** | fixed |
| **Priority** | urgent | **Severity** | feature | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
In the current version of e.g. "acsl-implementation-Neon-20140301.pdf", it is not possible to search for a string: although "the" appears on almost every page, my viewer, "xpdf" doesn't find it. Without the search feature, a user needs to waste a lot of time with scanning though the document to find what (s)he is looking for.
I set the priority to "urgent" since I guess that it is easy to allow for string search again.https://git.frama-c.com/pub/frama-c/-/issues/413Implicit casting from integer to real causes failure in WP proof generation2021-04-15T06:54:30Zmantis-gitlab-migrationImplicit casting from integer to real causes failure in WP proof generationID0002241:
**This issue was created automatically from Mantis Issue 2241. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002241:
**This issue was created automatically from Mantis Issue 2241. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002241 | Frama-C | Plug-in > wp | public | 2016-07-29 | 2016-07-29 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jrobbins | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Aluminium | **Target Version** | - | **Fixed in Version** | - |
### Description :
ACSL defines the integer type as a subset of the real type. Therefore, it states, implicit casting from integers to reals is allowed, because one is the subset of another. However, when this is done in practice, the WP plugin will generate goals that provers cannot parse, giving a type error.
### Additional Information :
This is confirmed to occur with the alt-ergo and why3 provers.
Tested on both Frama-C Sodium and Aluminum. Sodium produces slightly different errors than Aluminum, but both produce errors.
### Steps To Reproduce :
== Input file (bug.c):
/*@
axiomatic Bug {
logic integer ibug;
logic real rbug = ibug;
}
*/
/*@
requires i == rbug;
*/
void foo(int i);
void main() {
foo(42);
}
== Command to reproduce
frama-c -wp bug.c
== Output
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing bug.c (with preprocessing)
bug.c:13:[kernel] warning: No code nor implicit assigns clause for function foo, generating default assigns from the prototype
[wp] warning: Missing RTE guards
[wp] 1 goal scheduled
/tmp/wp714796.dir/typed/A_Bug.ergo:7:[wp] user error: Alt-Ergo error:
characters 1-34:typing error: real and int cannot be unified
[wp] [Alt-Ergo] Goal typed_main_call_foo_pre : Failed
characters 1-34:typing error: real and int cannot be unified
[wp] Proved goals: 0 / 1
Alt-Ergo: 0 (failed: 1)
## Attachments
- [bug.c](/uploads/24ea9349eeb21558e55d63d94453b416/bug.c)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/412Incorrect location of warnings emitted by value analysis2021-02-22T13:57:59ZVirgile PrevostoIncorrect location of warnings emitted by value analysisID0000772:
**This issue was created automatically from Mantis Issue 772. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000772:
**This issue was created automatically from Mantis Issue 772. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000772 | Frama-C | Plug-in > Eva | public | 2011-03-30 | 2016-08-02 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | virgile | **Assigned To** | yakobowski | **Resolution** | won't fix |
| **Priority** | low | **Severity** | tweak | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | - |
### Description :
On the code below, frama-c -val -main f t.c will report an out of bound read on line 2. It should be line 3.
------------- t.c
void f (int* x) {
int a = 3 +
*x;
}
-----------------https://git.frama-c.com/pub/frama-c/-/issues/410Logic with read clauses can have their values invalidated by writes to separa...2021-08-05T09:15:39Zmantis-gitlab-migrationLogic with read clauses can have their values invalidated by writes to separated memory locationsID0002244:
**This issue was created automatically from Mantis Issue 2244. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002244:
**This issue was created automatically from Mantis Issue 2244. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002244 | Frama-C | Plug-in > wp | public | 2016-08-08 | 2016-08-08 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jrobbins | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Aluminium | **Target Version** | - | **Fixed in Version** | - |
### Description :
In some cases, axiomatic logic using reads clauses can be true for a certain memory location, and then become unknown once an unrelated memory location is assigned to. You can even prove the memory locations as separate, but it does not fix the issue.
### Additional Information :
This bug is present on both Frama-C versions Sodium and Aluminum.
### Steps To Reproduce :
== File bug.c:
/*@
axiomatic Axiomatic {
logic boolean property_of_buffer(char *buffer) reads *buffer;
}
*/
/*@
assigns *buffer;
ensures property_of_buffer(buffer);
*/
void foo(char *buffer);
/*@
requires property_of_buffer(buffer);
assigns *buffer;
ensures property_of_buffer(buffer);
*/
int bar(char *buffer);
char buf1[1];
char buf2[1];
void main() {
foo(buf1);
bar(buf1);
foo(buf2);
bar(buf1);
}
== Command to run:
frama-c -wp bug.c
== Output:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing bug.c (with preprocessing)
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[wp] warning: Missing RTE guards
[wp] 2 goals scheduled
[wp] [Qed] Goal typed_main_call_bar_pre : Valid
[wp] [alt-ergo] Goal typed_main_call_bar_pre_2 : Unknown (562ms)
[wp] Proved goals: 1 / 2
Qed: 1
alt-ergo: 0 (unknown: 1)
== Expected behavior: For typed_main_call_bar_pre_2 to prove valid.
## Attachments
- [bug.c](/uploads/40ef28c81962575b7520fa0642241586/bug.c)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/409Nested scopes may cause issues with the validity of created pointers2021-04-15T08:57:59Zmantis-gitlab-migrationNested scopes may cause issues with the validity of created pointersID0002245:
**This issue was created automatically from Mantis Issue 2245. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002245:
**This issue was created automatically from Mantis Issue 2245. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002245 | Frama-C | Plug-in > wp | public | 2016-08-17 | 2016-08-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jrobbins | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Aluminium | **Target Version** | - | **Fixed in Version** | - |
### Description :
Upon entering a nested scope (caused by conditional blocks, or even just wrapping parts of code in {}), pointers once known as valid may become unknown in validity. This only seems to occur when more than 1 pointer is being reasoned about in the scope.
### Additional Information :
This bug occurs on both Sodium in Cygwin and Aluminum on Linux.
### Steps To Reproduce :
== Program bug.c:
/*@
ensures \valid(\result);
*/
int* foo();
void main() {
int* x = foo();
{
int y;
//@ assert \valid(x);
//@ assert \valid(&y);
}
}
== Command to run:
frama-c bug.c -wp
== Output:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing bug.c (with preprocessing)
bug.c:6:[kernel] warning: No code nor implicit assigns clause for function foo, generating default assigns from the prototype
[wp] warning: Missing RTE guards
[wp] 2 goals scheduled
[wp] [Alt-Ergo] Goal typed_main_assert : Unknown (51ms)
[wp] Proved goals: 1 / 2
Qed: 1
Alt-Ergo: 0 (unknown: 1)
== Expected output:
Both assertions to pass, since x is ensures to be valid, and the & operator always returns a valid pointer.
== Real output:
The pointer we ensure to be valid could not be proven to be valid.
Moving the definition of y to the outer scope fixes this issue, as well as moving the definition of x inside.
## Attachments
- [bug.c](/uploads/cfc99feea8974ba3cb5097bed4bfb3d3/bug.c)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/408Frama-C does not support standard C digraphs2021-02-22T13:58:41ZDavid CokFrama-C does not support standard C digraphsID0002146:
**This issue was created automatically from Mantis Issue 2146. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002146:
**This issue was created automatically from Mantis Issue 2146. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002146 | Frama-C | Kernel | public | 2015-07-16 | 2016-08-29 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dcok@grammatech.com | **Assigned To** | maroneze | **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 :
Frama-C does not parse a program like
void func() <%
return;
%>
Presumably other standard digraphs and trigraphs are not supported as well.
## Attachments
- [clexer.mll.patch](/uploads/68eac5f1bf97603b7453d8f565aef75f/clexer.mll.patch)https://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/405error in Coq file generation2021-04-15T08:59:05ZAlain Giorgettierror in Coq file generationID0002260:
**This issue was created automatically from Mantis Issue 2260. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002260:
**This issue was created automatically from Mantis Issue 2260. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002260 | Frama-C | Plug-in > wp | public | 2016-12-03 | 2016-12-03 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | giorgetti | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Aluminium | **Target Version** | - | **Fixed in Version** | - |
### Description :
When an ACSL axiomatic in a C file main.c contains a type declaration, say
type t;
the command
frama-c .. -wp main.c -wp-prover coqide ..
generates a wrong line
Parameter fct : Type.
in the file typed_fct/A_coq_.v.
### Additional Information :
Noticed during a meeting with L. CorrensonLoïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/404Unterminated comment while generating division-by-zero assertion2021-02-22T13:01:31ZKostyantyn VorobyovUnterminated comment while generating division-by-zero assertionID0002250:
**This issue was created automatically from Mantis Issue 2250. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002250:
**This issue was created automatically from Mantis Issue 2250. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002250 | Frama-C | Kernel | public | 2016-10-13 | 2016-12-05 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | kvorobyov | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | Linux | **OS** | Gentoo | **OS Version** | - |
| **Product Version** | Frama-C Magnesium | **Target Version** | Frama-C 14-Silicon | **Fixed in Version** | - |
### Description :
For the following code snippet:
...
ret = dividend / *p;
...
RTE generates annotation:
/*@ assert rte: signed_overflow: dividend/*p ≤ 2147483647; */
The above leads to unterminated comment preprocessing error
### Steps To Reproduce :
frama-c -rte -then -print
of the following program:
int zero_division_006_gbl_divisor = 0;
void zero_division_006 () {
int dividend = 1000;
int *p;
int ret;
p = &zero_division_006_gbl_divisor;
ret = dividend / *p;
}
int main(int argc, const char **argv) {
zero_division_006();
return 0;
}
## Attachments
- [a.c](/uploads/fac19dff3e17847ea3277c0a8c3c3fbf/a.c)https://git.frama-c.com/pub/frama-c/-/issues/403workaround for coq-8.5.1 issue?2021-02-22T13:01:28ZJochen Burghardtworkaround for coq-8.5.1 issue?ID0002233:
**This issue was created automatically from Mantis Issue 2233. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002233:
**This issue was created automatically from Mantis Issue 2233. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002233 | Frama-C | Plug-in > wp | public | 2016-06-16 | 2016-12-05 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | none | **Severity** | feature | **Reproducibility** | always |
| **Platform** | Aluminium-20160501 | **OS** | xubuntu16.04 | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
We ran the command
frama-c-gui -cpp-extra-args='-I.' -pp-annot -no-unicode -wp -wp-rte -wp-script wp0.script -wp-model Typed+ref -wp-prop AdjacentDifferenceInverse -wp-coq-timeout 5 -wp-prover coq -wp-par 1 -wp-out adjacent_difference_inverse.wp adi.c
on the attached file "adi.c", using the attached Coq-script "wp0.script".
The goal isn't proven, and when manually starting the Coq Ide, it complains:
Error: The reference Q_UnchangedSection was not found in the current
environment.
However, the lemma "UnchangedSection" is present in lines 28-33 of file "adi.c", and a "Hypothesis Q_UnchangedSection" is present in lines 33-36 of the generated file "adjacent_difference_inverse.wp/typed_ref/Axiomatic.v", which is included in line 33 of file "adjacent_difference_inverse.wp/typed_ref/lemma_AdjacentDifferenceInverse_Coq.v" (i.e. of the file shown in the Coq Ide).
For these reasons, we believe that the behavior is a Coq-8.5.1 problem, not a Frama-c problem. Moreover, the same files cause no problems when Coq-8.5.1 is replaced by Coq-8.4.6.
Nevertheless, in an e-mail to Jens, Loic encouraged us to report the issue here, since Frama-C might provide a workaround for it.
## Attachments
- [adi.c](/uploads/c4c8150d300c94e05ae4078a54bb0388/adi.c)
- [wp0.script](/uploads/7a7bb805cc9c8332faccefd8ebe42e5d/wp0.script)
- [Axiomatic.v](/uploads/9ab08c5dc84284dc5f8412c7ddc95f09/Axiomatic.v)
- [lemma_AdjacentDifferenceInverse_Coq.v](/uploads/d61593407465c9df0f749dc04240e6ea/lemma_AdjacentDifferenceInverse_Coq.v)
- [adi.script](/uploads/9ab0f4bd54640d060c2292833e1bcd01/adi.script)https://git.frama-c.com/pub/frama-c/-/issues/402__attribute__((aligned(0))) tacitly causes sizeof computation to fail2021-02-22T13:37:02ZJochen Burghardt__attribute__((aligned(0))) tacitly causes sizeof computation to failID0002249:
**This issue was created automatically from Mantis Issue 2249. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002249:
**This issue was created automatically from Mantis Issue 2249. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002249 | Frama-C | Kernel | public | 2016-10-13 | 2016-12-05 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | maroneze | **Resolution** | fixed |
| **Priority** | normal | **Severity** | text | **Reproducibility** | always |
| **Platform** | Aluminium-20160501 | **OS** | xbuntu 64bit | **OS Version** | - |
| **Product Version** | Frama-C Aluminium | **Target Version** | - | **Fixed in Version** | Frama-C GIT, precise the release id |
### Description :
Running "frama-c -val aaa.c" on the attached program issues the warnings:
[value] Computing initial state
aaa.c:6:[kernel] warning: division by zero. assert sizeof(struct _st) ≢ 0;
aaa.c:6:[value] Evaluation of initializer '(int)((unsigned int)1000 / sizeof(struct _st))' failed
[value] Initial state computed
When the "aligned(0)" attribute is omitted, the warning disappears. While it is acceptible that the Frama-C value analysis doesn't support all esoteric gcc contructs (like __attribute__), issueing a warning that "alignied(0)" isn't supported would help the user to understand the reasons for the warning.
## Attachments
- [aaa.c](/uploads/da286bc72aa9f2a0fbb3e13ad293ea02/aaa.c)
- [aaa2.c](/uploads/366b803f2d48dc409aec4d71a24cf3fb/aaa2.c)https://git.frama-c.com/pub/frama-c/-/issues/401Annotation wrongly displayed as checked (green bullet) whereas it is false, w...2021-02-22T13:01:21Zmantis-gitlab-migrationAnnotation wrongly displayed as checked (green bullet) whereas it is false, when using the option -rte on command line.ID0002258:
**This issue was created automatically from Mantis Issue 2258. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002258:
**This issue was created automatically from Mantis Issue 2258. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002258 | Frama-C | Plug-in > RTE | public | 2016-11-24 | 2016-12-05 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | julien-cohen | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | PC | **OS** | Linux Ubuntu | **OS Version** | 16.04 LTS |
| **Product Version** | Frama-C Magnesium | **Target Version** | - | **Fixed in Version** | - |
### Description :
I have a program with an incorrect acces outside an array. When lauching frama-c-gui with no options and value analysis, the out-of-bounds access is detected and the corresponding annotation is displayed with an orange bullet. When using the -rte option, two annotations are displayed (for the lower and upper bound of the array), and a green bullet is displayed for both (which is not correct).
/*@ assert rte: index_bound: 0 ≤ cpt; */
/*@ assert rte: index_bound: cpt < 5; */
The console says :
tableau_erreur.c:11:[value] Assertion 'rte,index_bound' got status valid.
### Additional Information :
Posted on http://stackoverflow.com/questions/40763614/unsound-behavior-with-rte-option-in-magnesium/40766174#40766174 .
There are two screen captures there. Someone (anol) replied and gave additional information (see the post).
### Steps To Reproduce :
Here is my program :
int main(){
int t[5] = {1,2,3,4,5};
int cpt =0 ;
int tmp ;
while (cpt<10){
tmp = getchar() ;
if ( t[cpt] > tmp )
{ return 1 ; }
cpt++ ;
}
return 10 ;
}
The problem occurs when launching frama-c-gui -rte and the calue analysis on this program.https://git.frama-c.com/pub/frama-c/-/issues/399expression "b--3" accepted in ACSL (interpreted as "b - -3"), but not in C2021-02-22T13:01:16ZJochen Burghardtexpression "b--3" accepted in ACSL (interpreted as "b - -3"), but not in CID0002240:
**This issue was created automatically from Mantis Issue 2240. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002240:
**This issue was created automatically from Mantis Issue 2240. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002240 | Frama-C | Kernel > ACSL implementation | public | 2016-07-28 | 2016-12-05 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | no change required |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | xubuntu | **OS Version** | - |
| **Product Version** | Frama-C Aluminium | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp aaa.c" on the attached program gives no syntax error, and reports 1/1 goals proven, although the right-hand side expression in line 7 is invalid. Uncommenting line 6, which contains the same expression in C, results in a syntax error, as expected.
## Attachments
- [aaa.c](/uploads/6a6a5f3ec88892032d6934c50957a697/aaa.c)https://git.frama-c.com/pub/frama-c/-/issues/398"Builtin already registered" after Reparse2021-02-22T13:37:10Zmantis-gitlab-migration"Builtin already registered" after ReparseID0002242:
**This issue was created automatically from Mantis Issue 2242. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002242:
**This issue was created automatically from Mantis Issue 2242. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002242 | Frama-C | Plug-in > wp | public | 2016-07-30 | 2016-12-05 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | khar | **Assigned To** | bobot | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | lubuntu | **OS Version** | - |
| **Product Version** | Frama-C Aluminium | **Target Version** | - | **Fixed in Version** | - |
### Description :
When using frama-c-gui to analyze code that uses arrays or pointers to structs, after a Reparse, the GUI fails to perform further analysis.
### Additional Information :
Step 2 (selecting the function "Foo" rather than the file "repro.c") is needed to work around a possibly unrelated bug where the source viewer doesn't update properly after a Reparse. To reproduce that bug, simply click "repro.c" instead of "Foo" in step 2.
### Steps To Reproduce :
$ cat repro.c:
//@ ensures foo[1] == 1;
void Foo(int* foo) {
foo[1] = 1;
}
$ frama-c-gui repro.c
1. Expand "repro.c" on the file panel.
2. Click "Foo" on the file panel.
3. Right-click the "ensures" annotation in the source panel.
4. Click "Prove property by WP".
5. On the toolbar, click the "Reparse source files, and replay analyses" button.
6. Click "repro.c" on the file panel.
7. Right-click the "ensures" annotation in the source panel.
8. Click "Prove property by WP".
Results: an error dialog with the following text:
Current source was: repro.c:2
The full backtrace is:
Raised at file "hashtbl.ml", line 328, characters 23-32
Called from file "src/libraries/project/state_topological.ml", line 62, characters 23-38
Unexpected error (Failure("Builtin already registered for 'shift_sint32'")).
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Aluminium-20160501.
Note that a version and a backtrace alone often do not contain enough
information to understand the bug. Guidelines for reporting bugs are at:
http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelines
## Attachments
- [repro.c](/uploads/5cc283fba4536bd3c0702a8ca68141b5/repro.c)https://git.frama-c.com/pub/frama-c/-/issues/397Switch statements seem to be unsound2021-02-22T13:01:13Zmantis-gitlab-migrationSwitch statements seem to be unsoundID0002246:
**This issue was created automatically from Mantis Issue 2246. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002246:
**This issue was created automatically from Mantis Issue 2246. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002246 | Frama-C | Plug-in > wp | public | 2016-08-19 | 2016-12-05 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | ghulette | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | Linux | **OS Version** | Ubuntu 16.04 |
| **Product Version** | Frama-C Aluminium | **Target Version** | - | **Fixed in Version** | - |
### Description :
// Run the following to see the problem:
// $ frama-c -wp -wp-rte bad.c
//
// Frama-C does not detect the error in the ensures condition. You
// can cause WP to report the error by commenting out the case 0 line,
// or by passing the -simplify-cfg option. Maybe a problem with
// switch statements?
int x;
/*@
requires x != 1;
assigns x;
ensures x != 1;
*/
void bad (int e) {
switch (e) {
case 0: break;
case 1: x = 1; break;
}
}
### Additional Information :
$ frama-c --version
Aluminium-20160501
### Steps To Reproduce :
See comments in description.
## Attachments
- [bad.c](/uploads/c873fd1a6a052a79d2354129467bc6fe/bad.c)https://git.frama-c.com/pub/frama-c/-/issues/396Compiling on Windows (cygwin) fails2021-02-22T13:01:11Zmantis-gitlab-migrationCompiling on Windows (cygwin) failsID0002247:
**This issue was created automatically from Mantis Issue 2247. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002247:
**This issue was created automatically from Mantis Issue 2247. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002247 | Frama-C | Documentation > manuals | public | 2016-10-01 | 2016-12-05 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | vlad | **Assigned To** | maroneze | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | Windows | **OS Version** | 7 |
| **Product Version** | Frama-C Aluminium | **Target Version** | - | **Fixed in Version** | - |
### Description :
Windows installation fails when building frama-c as described here: https://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:compiling_from_source
<pre>
$ OPAMYES=yes opam depext -i frama-c
# Detecting depexts using flags: x86 mswindows win32 cygwinports
# The following system packages are needed:
# - gmp
# - gtk2.0
# - gtksourceview2.0
# - libgnomecanvas2
# - pkg-config
installed:gmp
installed:gtk2.0
installed:gtksourceview2.0
installed:libgnomecanvas2
installed:pkg-config
# All required OS packages found.
# Now letting OPAM install the packages
The following actions will be performed:
∗ install frama-c-base 20160501 [required by frama-c]
Why3 can be used by the WP plug-in for running additional automatic solvers
Coq can be used with the WP plug-in for proving interactively proof obligations
∗ install frama-c 20160501
Alt-Ergo Graphical Interface can be used by the WP plug-in
===== ∗ 2 =====
=-=- Gathering sources =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
=-=- Processing actions -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
[frama-c-base: sh] Command started
[frama-c-base: ./configure] Command started
[frama-c-base: make all] Command started
[ERROR] The compilation of frama-c-base failed at "make
FRAMAC_TOP_SRCDIR=C:/Users/User/AppData/Roaming/SPB_Data/.opam/4.02.3+mingw32/build/frama-c-base.20160501
all".
[frama-c-base: sh] Command started
[frama-c-base: ./configure] Command started
[frama-c-base: make uninstall] Command started
[frama-c-base: rm] Command started
#=== ERROR while compiling frama-c-base.20160501 ==============================#
# opam-version 1.3.0~dev (98188f141dbeb429258f2b2c00f6240d0af02b84)
# os win32
# command make FRAMAC_TOP_SRCDIR=C:/Users/User/AppData/Roaming/SPB_Data/.opam/4.02.3+mingw32/build/frama-c-base.20160501 all
### stdout ###
# [...]
### stderr ###
# 4 shift/reduce conflicts.
# 7 shift/reduce conflicts.
# src/libraries/utils/c_bindings.c:1:0: warning: -fPIC ignored for target (all code is position independent)
# /**************************************************************************/
# ^
# src/libraries/utils/c_bindings.c:28:27: fatal error: caml/mlvalues.h: No such file or directory
# compilation terminated.
# make: *** [Makefile:882: src/libraries/utils/c_bindings.o] Error 1
=-=- Error report -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
The following actions were aborted
∗ install frama-c 20160501
The following actions failed
λ build frama-c-base 20160501
No changes have been performed
</pre>https://git.frama-c.com/pub/frama-c/-/issues/395the documented grammar does not allow completeness clauses in statement contr...2021-02-22T13:37:04ZDavid Cokthe documented grammar does not allow completeness clauses in statement contractsID0002224:
**This issue was created automatically from Mantis Issue 2224. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002224:
**This issue was created automatically from Mantis Issue 2224. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002224 | Frama-C | Documentation > ACSL | public | 2016-04-13 | 2016-12-05 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | DavidCok | **Assigned To** | patrick | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Magnesium | **Target Version** | - | **Fixed in Version** | - |
### Description :
the documented grammar does not allow completeness clauses in statement contracts, but Frama-C wp does. I presume the implemented behavior is what is desired, so then the documentation should be updated.https://git.frama-c.com/pub/frama-c/-/issues/394Frama-C is unsound when employing both alt-ergo and cvc42021-02-22T13:01:06ZJochen BurghardtFrama-C is unsound when employing both alt-ergo and cvc4ID0002237:
**This issue was created automatically from Mantis Issue 2237. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002237:
**This issue was created automatically from Mantis Issue 2237. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002237 | Frama-C | Plug-in > wp | public | 2016-06-30 | 2016-12-05 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | high | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | xubuntu |
| **Product Version** | Frama-C Aluminium | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp -wp-out out -wp-prover alt-ergo -wp-prover cvc4 bug.c" on the attached file "bug.c" proves both lemmas, although they are both obviously false. A look at file "lemma_Two_Alt-Ergo.mlw" shows that Alt-ergo proved in fact One==>Two, while a look at file "Axiomatic.why" indicates that cvc4 proved in fact Two==>One.
Apparently, the order of lemmas is reversed when piping through "why" - the output generated for coq amounts to "prove One" and "prove One==>Two", similar to that for Alt-ergo.
The problem disappeared when the type of the bound variable "x" was changed to "integer".
## Attachments
- [bug.c](/uploads/4c15388a22c29202e6cb9736f3dc73c9/bug.c)
- [lemma_Two_Alt-Ergo.mlw](/uploads/f03a7de730f37671825be7aed7c67b57/lemma_Two_Alt-Ergo.mlw)
- [Axiomatic.why](/uploads/1dcfeb3bf5a2935354dd3cae6d5c5e0a/Axiomatic.why)
- [0001-WP-Fix-definition-order.patch](/uploads/58c12a1488d50b4d416869447762e3e4/0001-WP-Fix-definition-order.patch)https://git.frama-c.com/pub/frama-c/-/issues/393Ocaml 4.04.0 build error2021-02-22T13:01:03Zmantis-gitlab-migrationOcaml 4.04.0 build errorID0002255:
**This issue was created automatically from Mantis Issue 2255. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002255:
**This issue was created automatically from Mantis Issue 2255. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002255 | Frama-C | Kernel | public | 2016-11-09 | 2016-12-07 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jamesjer | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | x86_64 | **OS** | Linux | **OS Version** | 4.8.6 |
| **Product Version** | Frama-C Aluminium | **Target Version** | - | **Fixed in Version** | - |
### Description :
Building with ocaml 4.04.0 fails:
File "src/kernel_services/plugin_entry_points/db.ml", line 1:
Error: The implementation src/kernel_services/plugin_entry_points/db.ml
does not match the interface src/kernel_services/plugin_entry_points/db.cmi:
...
In module Properties.Interp.To_zone:
Values do not match:
val mk_ctx_func_contrat : (Cil_types.kernel_function -> '_a) ref
is not included in
val mk_ctx_func_contrat :
(Cil_types.kernel_function -> state_opt:bool option -> t_ctx) ref
File "src/kernel_services/plugin_entry_points/db.ml", line 1074, characters 10-29:
Actual declaration
### Additional Information :
See https://bugzilla.redhat.com/show_bug.cgi?id=1392552 for the original report, by Richard W. M. Jones. He supplied a patch which, he says, "fixes compilation, but is generally a bit of a hack. Upstream probably will want to make their own better fix." That patch is attached.
### Steps To Reproduce :
Build with Frama-C Aluminium with ocaml 4.04.0 on an x86_64 Linux machine.
## Attachments
- [frama-c-ocaml-4-04.patch](/uploads/caa49c7fec70d631bd0e90ee7a61dc61/frama-c-ocaml-4-04.patch)