frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2024-02-16T10:24:26Zhttps://git.frama-c.com/pub/frama-c/-/issues/569WP output of loop variant's goal doesn't have location of loop variant2024-02-16T10:24:26Zmantis-gitlab-migrationWP output of loop variant's goal doesn't have location of loop variantID0002190:
**This issue was created automatically from Mantis Issue 2190. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002190:
**This issue was created automatically from Mantis Issue 2190. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002190 | Frama-C | Plug-in > wp | public | 2015-12-03 | 2016-01-26 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | gaggarwal | **Assigned To** | correnson | **Resolution** | won't fix |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | - |
### Description :
Consider the following example:
1) void main() {
2) int i;
3) /*@ loop invariant 0 <= i <= 5;
4) @ loop variant 5-i;
5) @*/
6) for(i=0;i<5;i++);
7) }
Output generated by wp for loop variant is following:
Goal Decreasing of Loop variant at loop (file /SpecDemo/src/test6.c, line 6):
Assume {
(* Domain *)
......
Prove: true.
Prover Qed returns Valid
Goal Positivity of Loop variant at loop (file /SpecDemo/src/test6.c, line 6):
Assume {
(* Domain *)
.......
Prove: true.
Prover Qed returns Valid
Notice that both goals have location of loop i.e. (file /SpecDemo/src/test6.c, line 6) and not of loop variant. Even though a loop can have only one loop variant and it is not very hard to figure out which loop variant it is, it will be really helpful if we can include location of loop variant too.https://git.frama-c.com/pub/frama-c/-/issues/570Unprovable inequality involving (unsigned) -12021-02-22T13:39:14Zmantis-gitlab-migrationUnprovable inequality involving (unsigned) -1ID0002127:
**This issue was created automatically from Mantis Issue 2127. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002127:
**This issue was created automatically from Mantis Issue 2127. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002127 | Frama-C | Plug-in > wp | public | 2015-06-04 | 2016-01-26 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | loic | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Linux | **OS** | Ubuntu | **OS Version** | 12.04.5 LTS |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Magnesium |
### Description :
Nitrogen-20111001
alt-ergo 0.94
The following assertion cannot be proven.
void arithmetic_testcase(unsigned i) {
/*@ assert i <= (unsigned) -10 ==> i + 9 <= (unsigned) -1; */
}
### Steps To Reproduce :
frama-c -wp -wp-ret for the code above (also as attachment).
## Attachments
- [arithmetic_testcase.c](/uploads/23e6a21720bcbac1cbefa9b6bfa47303/arithmetic_testcase.c)https://git.frama-c.com/pub/frama-c/-/issues/571WP crashes on generation of PO for assigns clause (assertion failure in MemVa...2021-02-22T14:01:52ZVirgile PrevostoWP crashes on generation of PO for assigns clause (assertion failure in MemVar.ml)ID0002126:
**This issue was created automatically from Mantis Issue 2126. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002126:
**This issue was created automatically from Mantis Issue 2126. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002126 | Frama-C | Plug-in > wp | public | 2015-06-02 | 2016-01-26 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | virgile | **Assigned To** | correnson | **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 Magnesium |
### Description :
On the example source below, frama-c -wp reduced.i crashes with the following error:
File "src/wp/MemVar.ml", line 491, characters 54-60: Assertion failed
Apparently (by inferring why the offending function in MemVar got called), the p1+0 in the assigns for fn1 leads WP to think that p1 should be instantiated with an array (in particular, if you remove the +0, everything is fine).
-- reduced.i
/*@ assigns *(p1); */
int fn1(char *p1);
/*@
assigns \nothing;
*/
void fn2(void) {
char pcr_index;
fn1(&pcr_index);
}https://git.frama-c.com/pub/frama-c/-/issues/572suggest to issue a warning on (<)-comparisons between pointers, unless both a...2021-02-22T14:01:45ZJochen Burghardtsuggest to issue a warning on (<)-comparisons between pointers, unless both are non-nullID0000875:
**This issue was created automatically from Mantis Issue 875. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000875:
**This issue was created automatically from Mantis Issue 875. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000875 | Frama-C | Plug-in > Eva | public | 2011-06-29 | 2016-01-26 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20110201 | **Target Version** | - | **Fixed in Version** | Frama-C Magnesium |
### Description :
In the attached program, Frama-C could issue a warning for the comparison (NULL<p) in line 11; similar for (NULL<=p) in line 21.
Astree warns "ALARM(C): comparing pointers on different memory blocks {NULL} and {a}" in this case.
Gcc doesn't warn at all; it generates the same code for (NULL<p) in line 11 as for (NULL!=p) in line 16, and translates (NULL<=p) in line 21 as (true); i.e. gcc tacitly assumes that pointer adresses are not negative. The hex constants in the printf-s serve to recognize the branches in the translated machine code program.
The C99 standard (http://www.open-std.org/jtc1/sc22/wg14/www/docs/n1539.pdf) seems to say in sect.5 that (NULL<p) is undefined. Therefor, any behavior of the value-analysis plugin is admissible.
However, when pointers are compared (p<q), the programmer usually intends both p and q to be non-null. If in fact one of them may be null, this is probably a bug . Value-analysis could help to find such bugs.
## Attachments
- [memory_framac.c](/uploads/f7afdc1411ad0657ad58e63f9ea192cd/memory_framac.c)https://git.frama-c.com/pub/frama-c/-/issues/574expression "term!=term" is considered always a predicate, rather than (in som...2021-03-15T17:05:04ZJochen Burghardtexpression "term!=term" is considered always a predicate, rather than (in some contexts) a termID0002197:
**This issue was created automatically from Mantis Issue 2197. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002197:
**This issue was created automatically from Mantis Issue 2197. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002197 | Frama-C | Kernel > ACSL implementation | public | 2015-12-07 | 2015-12-07 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | Sodium-20150201 | **OS** | - | **OS Version** | xubuntu14.04 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c 485.c -no-unicode" on the attached program results in an error message
485.c:2:[kernel] user error: comparison of incompatible types: integer and boolean in annotation.
However, according to the manual "acsl-implementation-Sodium-20150201.pdf", p.16-17, fig.2.1, 2.2, the ACSL grammar allows for a derivation
pred ------> term rel-op term ------> 2 > ( term ) ------> 2 > ( term bin-op term ) ------> 2 > ( id != id ) ------> 2 > (x != x)
The remark on consecutive comparison operators (p.18) shouldn't apply due to the additional parantheses around "x!=x".
### Additional Information :
(The file was boiled down from a file generated by a first version of "acslsmith", an adaption of "csmith".)
## Attachments
- [485.c](/uploads/b362c071921e344811aef78b676cdf05/485.c)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/575ambiguity with consecutive comparison and ternary expressions2021-02-22T13:06:12ZDavid Cokambiguity with consecutive comparison and ternary expressionsID0002195:
**This issue was created automatically from Mantis Issue 2195. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002195:
**This issue was created automatically from Mantis Issue 2195. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002195 | Frama-C | Kernel > ACSL implementation | public | 2015-12-05 | 2015-12-06 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dcok@grammatech.com | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | major | **Reproducibility** | N/A |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | - |
### Description :
The ACSL grammar allows two forms of ternary expressions for predicates:
term ? pred : pred
pred ? pred : pred
But the interpretation of consecutive comparisons depends on whether the expression is in term or predicate position. Thus the predicate
(i == j < k) ? (\true==>\\true) ? (\true==>\false)
is fundamentally ambiguous in the grammar. If the condition is a predicate, it is equivalent to
((i == j) && (j < k)) ? ...
As a term it is equivalent to
((i == j) < k) ?
Depending on the types of i, j, and k,
it may not typecheck correctly as either a term or predicate - but does, for example, if all three are ints. However, it would be really bad design if the grammar parser depended on the types of expressions.
Is this construct deemed illegal, or is it resolved in favor of one form or the other?Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/576No syntax to apply lambda expressions2021-02-22T13:06:12ZDavid CokNo syntax to apply lambda expressionsID0002196:
**This issue was created automatically from Mantis Issue 2196. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002196:
**This issue was created automatically from Mantis Issue 2196. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002196 | Frama-C | Kernel > ACSL implementation | public | 2015-12-05 | 2015-12-05 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dcok@grammatech.com | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | N/A |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | - |
### Description :
ACSL 1.9 allows writing lambda expressions. They can be used in extended quantifiers. But there is no syntax to use them anywhere else, such as to apply a lambda expression to a sequence of arguments.Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/577Recursive calls in value analysis2021-02-22T13:39:19Zmantis-gitlab-migrationRecursive calls in value analysisID0002185:
**This issue was created automatically from Mantis Issue 2185. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002185:
**This issue was created automatically from Mantis Issue 2185. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002185 | Frama-C | Plug-in > Eva | public | 2015-11-03 | 2015-12-04 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | lammyday | **Assigned To** | yakobowski | **Resolution** | won't fix |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | Linux | **OS Version** | ubuntu 13.04 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Frama-c pdg could not generate pdg graphs for program containing recursive calls.
### Additional Information :
See implicit.c file here:
http://git.savannah.gnu.org/cgit/make.git/tree/implicit.c?id=2860d3b247e70a34246936fb085aeec951ea49b1
you can download the full GNU make version repository here:
http://git.savannah.gnu.org/cgit/make.git/commit/?id=2860d3b247e70a34246936fb085aeec951ea49b1
### Steps To Reproduce :
Running "frama-c -pdg -dot-pdg graph -pdg-print implicit.i -main pattern_search"
for the GNU make version repository 2860d3b2 gives the following errors:
implicit.c:700:[value] warning: recursive call during value analysis (pattern_search <- pattern_search)
Use -val-ignore-recursive-calls to ignore (beware this will make the analysis
unsound)
[kernel] State_builder.aborted because of unimplemented feature.
Please send a feature request at http://bts.frama-c.com with:
'recursive calls in value analysis'https://git.frama-c.com/pub/frama-c/-/issues/578Frama-C runs out of memory on small C program (combinatorial explosion in ana...2021-04-15T07:34:42ZJochen BurghardtFrama-C runs out of memory on small C program (combinatorial explosion in analysis of "main"?)ID0002189:
**This issue was created automatically from Mantis Issue 2189. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002189:
**This issue was created automatically from Mantis Issue 2189. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002189 | Frama-C | Plug-in > wp | public | 2015-12-03 | 2015-12-03 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | tweak | **Reproducibility** | always |
| **Platform** | Sodium-20150201 | **OS** | - | **OS Version** | xubuntu14.04 |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp -wp-rte -wp-prover none 10g.c" on the attached program causes Frama-C to run out of memory after allocation of 3 GBytes memory (deliberately restricted by "ulimit -v 3000000" to avoid swapping/paging).
This phenomenon disappears e.g. if
* "main" is renamed to "foo" in line 28,
* both "p1" and "p2" are made "static" in line 23,24, or
* field "e0" or "e1" is removed from the "struct S" definition in line 9,14, and its use in line 33/34 is also removed.
Probably, there is some combinatorial explosion effect in the analysis. While this isn't a real bug, it may be worthwile to look after it, since the circumstances under which it can be observed are quite strange.
## Attachments
- [10g.c](/uploads/bd7968263c9a1d7ed8fbd893f14eef3f/10g.c)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/579bit_test axiomatization doesn't imply == equality from bit-by-bit equality fo...2021-04-15T06:57:41ZJochen Burghardtbit_test axiomatization doesn't imply == equality from bit-by-bit equality for e.g. uint32ID0002188:
**This issue was created automatically from Mantis Issue 2188. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002188:
**This issue was created automatically from Mantis Issue 2188. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002188 | Frama-C | Plug-in > wp | public | 2015-11-30 | 2015-11-30 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Sodium-20150201 | **OS** | - | **OS Version** | xubuntu14.04 |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | - |
### Description :
I ran "frama-c -wp -wp-out wp-out -wp-model Typed+ref -wp-driver jb.drv 484.c" on the attached program (and the attached driver file), and alt-ergo couldn't prove the lemma in line 10-15.
Looking at the background theory in (also attached) file "lemma_l_Alt-Ergo.mlw", it seems that in fact it doesn't imply the goal: axioms about "bit_test" occur only in lines 600 to 819; the only axioms that speak about something different from bit_test in their conclusion are (with line numbers):
604 axiom bit_test_def1 : relates to bit_testb, which isn't used further
612 axiom bit_test_extraction1 : relates to land(lsl(1,...))
622 axiom bit_test_extraction_bis_eq : implies only LSB=1
701 axiom lsl1_extraction : implies equality of bit position, not of values
757 axiom to_sint8_extraction_sup : implies negativity, not equality
773 axiom to_sint16_extraction_sup : similar
789 axiom to_sint32_extraction_sup : similar
805 axiom to_sint64_extraction_sup : similar
Axioms about lsl appear only in lines 608 to 1019; axioms speaking about something different from "lsl" and "bit_test" in their conclusion are:
616 axiom lsl_1_0 : (lsl(1, 0) = 1)
672 axiom land_1_lsl_1 : is about <, not about =
833 axiom is_uint8_lsl1_inf : about lsl(1,...) fitting into a uint8
837 axiom is_uint8_lsl1_sup : about lsl(1,...) not fitting into a uint8
853 axiom is_uint16_lsl1_inf : similar
857 axiom is_uint16_lsl1_sup : similar
873 axiom is_uint32_lsl1_inf : similar
877 axiom is_uint32_lsl1_sup : similar
893 axiom is_uint64_lsl1_inf : similar
897 axiom is_uint64_lsl1_sup : similar
921 axiom is_sint8_lsl1 : (lsl(1, 7) = 128)
923 axiom is_sint8_lsl1_inf : about lsl(1,...) fitting into an sint8
927 axiom is_sint8_lsl1_sup : about lsl(1,...) not fitting into an sint8
951 axiom is_sint16_lsl1 : (lsl(1, 15) = 32768)
953 axiom is_sint16_lsl1_inf : similar
957 axiom is_sint16_lsl1_sup : similar
981 axiom is_sint32_lsl1 : (lsl(1, 31) = 2147483648)
983 axiom is_sint32_lsl1_inf : similar
987 axiom is_sint32_lsl1_sup : similar
1011 axiom is_sint64_lsl1 : (lsl(1, 63) = 9223372036854775808)
1013 axiom is_sint64_lsl1_inf : similar
1017 axiom is_sint64_lsl1_sup : similar
Alltogether, I think there is no way to infer some equality relation from the agreement of bit_test (or land(lsl(...))) results.
I'm not sure whether I used the driver-file mechanism in an appropriate way; this might be the cause for my problem.
## Attachments
- [484.c](/uploads/a8645270645bbbcae0fa2802bc761c15/484.c)
- [jb.drv](/uploads/e5776c86ccbf4fec7dd49143e9b4625d/jb.drv)
- [lemma_l_Alt-Ergo.mlw](/uploads/869a0eda0b87de7cf6a05c199a23f624/lemma_l_Alt-Ergo.mlw)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/581Nested VLA are not supported2022-09-28T14:37:05ZPascal CuoqNested VLA are not supportedID0001718:
**This issue was created automatically from Mantis Issue 1718. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001718:
**This issue was created automatically from Mantis Issue 1718. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001718 | Frama-C | Kernel | public | 2014-03-25 | 2015-11-04 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Note that I have never seen this feature actually used, but it appears to be supported by GCC and Clang.
To reiterate, I have never seen code that does int t[a][a];
This report is only for the sake of completeness.
### Steps To Reproduce :
```
~/gitlab/frama-c $ bin/toplevel.opt -print t.c
[kernel] warning: cannot load plug-in `Aorai' (incompatible with Neon-20140301+dev).
[kernel] warning: cannot load plug-in `Obfuscator' (incompatible with Neon-20140301+dev).
[kernel] warning: cannot load plug-in `Report' (incompatible with Neon-20140301+dev).
[kernel] warning: cannot load plug-in `Security_slicing' (incompatible with Neon-20140301+dev).
[kernel] warning: cannot load plug-in `Wp' (incompatible with Neon-20140301+dev).
[kernel] preprocessing with "gcc -C -E -I. t.c"
t.c:4:[kernel] user error: Length of array is not a constant: a
t.c:4:[kernel] warning: Variable-sized local variable t
[kernel] user error: skipping file "t.c" that has errors.
[kernel] Frama-C aborted: invalid user input.
~/gitlab/frama-c $ cat t.c
int main(int c, char **v)
{
int a = 3;
int t[a][a];
t[a-1][a-1] = 1;
}
~/gitlab/frama-c $ gcc -pedantic -std=c99 t.c
~/gitlab/frama-c $
```Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/582Plug-in wp aborted: internal error, Raised at file "src/wp/register.ml", line...2021-04-14T15:32:57Zmantis-gitlab-migrationPlug-in wp aborted: internal error, Raised at file "src/wp/register.ml", line 579ID0002182:
**This issue was created automatically from Mantis Issue 2182. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002182:
**This issue was created automatically from Mantis Issue 2182. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002182 | Frama-C | Plug-in > wp | public | 2015-10-27 | 2015-10-27 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | lorenz | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | - |
### Description :
The following (minimized) example file crashes the wp plugin of frama-c:
#> frama-c -wp min3.c
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing min3.c (with preprocessing)
/tmp/ppannotc0c3e2.c:1:0: warning: "__STDC_VERSION__" redefined
#define __STDC_VERSION__ 201112L
^
<built-in>: note: this is the location of the previous definition
/tmp/ppannotc0c3e2.c:2:0: warning: "__STDC_UTF_16__" redefined
#define __STDC_UTF_16__ 1
^
<built-in>: note: this is the location of the previous definition
/tmp/ppannotc0c3e2.c:3:0: warning: "__STDC_UTF_32__" redefined
#define __STDC_UTF_32__ 1
^
<built-in>: note: this is the location of the previous definition
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[wp] warning: Missing RTE guards
[wp] failure: *** Label Label 'L' not-found
[kernel] Current source was: min3.c:16
The full backtrace is:
Raised at file "src/wp/register.ml", line 579, characters 30-32
Called from file "queue.ml", line 134, characters 6-20
Called from file "src/kernel/boot.ml", line 37, characters 4-20
Called from file "src/kernel/cmdline.ml", line 763, characters 2-9
Called from file "src/kernel/cmdline.ml", line 216, characters 4-8
Plug-in wp aborted: internal error.
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Sodium-20150201.
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
#>
### Steps To Reproduce :
frama-c -wp min3.c
## Attachments
- [min3.c](/uploads/31cca83763f8d99e4ce71ae17158d08f/min3.c)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/584Unable to prove things that are provable, gets confused2021-04-15T08:45:52Zmantis-gitlab-migrationUnable to prove things that are provable, gets confusedID0002179:
**This issue was created automatically from Mantis Issue 2179. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002179:
**This issue was created automatically from Mantis Issue 2179. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002179 | Frama-C | Plug-in > wp | public | 2015-10-18 | 2015-10-18 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | kroeckx | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | - |
### Description :
Hi,
In the attached file as is using wp -wp-model Typed,cast test-final.c, the last assert can't be proven, resulting in the ensures and assigns to be valid under hypotheses. This is a minimal version that still shows the problem.
However, there are several ways to make it be able to prove it and as far as I can see should have no effect on it. The different ways are:
- Removing any of the following 3 lines:
p[n] = 0x80; /* there is always room for one */
HASH_BLOCK_DATA_ORDER(c, p, 1);
c->num = 0;
- Removing the first assert
- Removing the requires \valid_read(c->data+(0 .. c->num-1));
I assume it gets confused because the \valid_read() overlaps with the \valid(c). It's not really needed. (In the full version the \valid_read() should more be something like \initialized.)
## Attachments
- [test-final.c](/uploads/d2b5913be633bcbecc3fbfb5a5fd886c/test-final.c)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/588mixed virtual/nonvirtual base class causes error2021-02-22T13:39:25ZJochen Burghardtmixed virtual/nonvirtual base class causes errorID0002077:
**This issue was created automatically from Mantis Issue 2077. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002077:
**This issue was created automatically from Mantis Issue 2077. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002077 | Frama-Clang | Plug-in > clang | public | 2015-02-09 | 2015-10-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | fvedrine | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | Neon-20140301+dev-STANCE-Jan2015 | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing 462.cpp (external front-end)
Now output intermediate result
462.cpp:5:[kernel] failure: Cannot resolve variable __frama_c_arg_0
[kernel] user error: stopping on file "462.cpp" that has errors.
If "virtual" is deleted in line 4, the error disappears; similarly if "virtual" is inserted in line 3.
Since in Stroustrup's book no mixed virtual/nonvirtual base class is discussed, the example in file "462.cpp" may not be of any relevance. However, the clang++ compiler accepts that file without any problems.
## Attachments
- [462.cpp](/uploads/6c5857ed398e1a937d5fade5314a5a1e/462.cpp)Franck VedrineFranck Vedrinehttps://git.frama-c.com/pub/frama-c/-/issues/590ACSL typing fails when performing unification of type variables2021-03-29T18:04:28ZPatrick BaudinACSL typing fails when performing unification of type variablesID0002170:
**This issue was created automatically from Mantis Issue 2170. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002170:
**This issue was created automatically from Mantis Issue 2170. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002170 | Frama-C | Kernel > ACSL implementation | public | 2015-09-24 | 2015-09-24 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | patrick | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Frama-C fails while typing the given ACSL axiomatic.
### Additional Information :
Typing is succesful when axiom "a" is replaced by:
@ axiom a: P(aList,Nil);
### Steps To Reproduce :
```
> cat list.i
//@ type List<A> = Nil | Cons(A,List<A>);
/*@ axiomatic L {
@ predicate P<B>(List<B> l1, List<B> l2);
@ logic List<integer> aList{L} ;
@ axiom a: P(Nil, aList);
@ }
@*/
> frama-c list.i
...
../tests/list.i:8:[kernel] user error: invalid implicit conversion from ℤ to A#4
```Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/591set of set2021-02-22T13:06:36ZPatrick Baudinset of setID0000575:
**This issue was created automatically from Mantis Issue 575. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000575:
**This issue was created automatically from Mantis Issue 575. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000575 | Frama-C | Kernel > ACSL implementation | public | 2010-08-25 | 2015-09-24 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | patrick | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Boron-20100401 | **Target Version** | - | **Fixed in Version** | - |
### Description :
For exemple, there is not way to build the set containing the empty set without using comprehension set construct.
The proposition is to extend the actual ACSL grammar in order to allow "{" term "}" as set expression.https://git.frama-c.com/pub/frama-c/-/issues/592incomplete Alt-Ergo obligation files generated in presence of lemma "forall i...2021-04-15T08:44:57ZJochen Burghardtincomplete Alt-Ergo obligation files generated in presence of lemma "forall int x; ..." with "x" not occurring in "..."ID0002169:
**This issue was created automatically from Mantis Issue 2169. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002169:
**This issue was created automatically from Mantis Issue 2169. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002169 | Frama-C | Plug-in > wp | public | 2015-09-21 | 2015-09-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Sodium-20150201 | **OS** | - | **OS Version** | xubuntu14.04 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp 483.c -wp-out wp-out" on the attached file generates an Alt-Ergo obligation file "foo_assert_Alt-Ergo.mlw" which contains neither the lemma "xxx" nor the proof goal for the assertion in line 5. Apparently, Frama-C/Wp tacitly crashes during translating the lemma.
The problem disappears ifin line 2 "int" is changed to "integer", or "\false" is changed to some formula containing "x".
## Attachments
- [483.c](/uploads/b7743ec7ca8f15e3df9b2238386f8533/483.c)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/593suggest command-line option to avoid sophisticated expression transformations...2021-04-15T08:43:45ZJochen Burghardtsuggest command-line option to avoid sophisticated expression transformations, in particular for Coq obligationsID0002168:
**This issue was created automatically from Mantis Issue 2168. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002168:
**This issue was created automatically from Mantis Issue 2168. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002168 | Frama-C | Plug-in > wp | public | 2015-09-21 | 2015-09-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | Sodium-20150201 | **OS** | - | **OS Version** | xubuntu14.04 |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp 482b.c" on the attached file, the assertion "zzz" can't be proven by Alt-Ergo, although it should be an immediate consequence of assertion "yyy" and axiom "xxx". Looking at the file "bar_assert_zzz_Alt-Ergo.mlw" shows that some sophisticated expression transformations have been applied to the goal, but not to the axiom:
763 axiom Q_xxx:
764 forall lg_0,pos_0 : int.
765 (forall i : int. (pos_0 <= i) -> (i < (lg_0 + pos_0)) -> P_Tst(i)) ->
766 P_Prp(1 - lg_0)
772 goal bar_assert_zzz:
787 (forall i_1 : int. (i_1 < i) -> (x <= i_1) -> P_Tst(i_1)) ->
788 P_Prp(1 + x - i)
It is not a problem of Frama-C/Wp, but a problem of Alt-Ergo: it just should apply the lemma "xxx" with instantiation { pos_0:=x, lg_0 := i-x } to obtain line 788 from line 787.
However, when trying to prove the "zzz" assertion manually using Coq, Wp's transformation causes additional confusion. It would be desirable if the was a command-line switch to generate proof obligations as close to the source code as possible, i.e. to avoid the transformation.
As a side note, if the "assert" in line 20 is replaced by the statement-contract "ensures" in line 18, the transformation disappears, the goal is fairly good readable, and Alt-Ergo find the proof.
## Attachments
- [482b.c](/uploads/2c17baa4edc565f1b208267d133e0f42/482b.c)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/594Relocable buckx2022-08-09T08:54:52Zmantis-gitlab-migrationRelocable buckxID0002165:
**This issue was created automatically from Mantis Issue 2165. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002165:
**This issue was created automatically from Mantis Issue 2165. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002165 | Frama-C | Kernel > Makefile | public | 2015-09-16 | 2015-09-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | ploc | **Assigned To** | signoles | **Resolution** | duplicate |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | N/A |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Please add, as a default option, the relocation for buckx_c files:
GEN_BUCKX_CFLAGS="-fPIC"https://git.frama-c.com/pub/frama-c/-/issues/595assertion failure using memset on a char2021-04-15T08:43:01Zmantis-gitlab-migrationassertion failure using memset on a charID0002160:
**This issue was created automatically from Mantis Issue 2160. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002160:
**This issue was created automatically from Mantis Issue 2160. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002160 | Frama-C | Plug-in > wp | public | 2015-09-14 | 2015-09-15 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | kroeckx | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | - |
### Description :
When trying to analyse the this:
#include <string.h>
int main()
{
char a;
memset(&a, 0, 1);
}
Using wp I get:
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[wp] warning: No definition for 'memchr' interpreted as reads nothing
[wp] warning: No definition for 'strlen' interpreted as reads nothing
[wp] warning: No definition for 'memset' interpreted as reads nothing
[wp] warning: No definition for 'strchr' interpreted as reads nothing
[wp] warning: No definition for 'strcmp' interpreted as reads nothing
[wp] warning: No definition for 'strncmp' interpreted as reads nothing
[wp] warning: No definition for 'wcscmp' interpreted as reads nothing
[wp] warning: No definition for 'wcslen' interpreted as reads nothing
[wp] warning: No definition for 'wcsncmp' interpreted as reads nothing
[wp] warning: Missing RTE guards
[kernel] Current source was: test.c:6
The full backtrace is:
Raised at file "src/wp/MemVar.ml", line 474, characters 54-66
Called from file "src/wp/MemVar.ml", line 519, characters 16-38
Called from file "src/wp/MemVar.ml", line 543, characters 9-38
Called from file "list.ml", line 55, characters 20-23
Called from file "src/wp/Lang.ml", line 735, characters 25-40
Called from file "src/wp/Warning.ml", line 139, characters 6-10
Called from file "src/wp/LogicSemantics.ml", line 813, characters 12-42
Called from file "src/wp/Context.ml", line 31, characters 12-17
Re-raised at file "src/wp/Context.ml", line 34, characters 41-46
Called from file "list.ml", line 55, characters 20-23
Called from file "src/wp/Context.ml", line 68, characters 14-17
Re-raised at file "src/wp/Context.ml", line 69, characters 43-48
Called from file "src/wp/Context.ml", line 68, characters 14-17
Re-raised at file "src/wp/Context.ml", line 69, characters 43-48
Called from file "src/wp/Context.ml", line 68, characters 14-17
Re-raised at file "src/wp/Context.ml", line 69, characters 43-48
Called from file "src/wp/Context.ml", line 68, characters 14-17
Re-raised at file "src/wp/Context.ml", line 69, characters 43-48
Called from file "src/wp/cfgWP.ml", line 1087, characters 18-60
Called from file "src/wp/Warning.ml", line 155, characters 14-18
Called from file "src/wp/cfgWP.ml", line 1118, characters 23-207
Called from file "src/wp/Context.ml", line 68, characters 14-17
Re-raised at file "src/wp/Context.ml", line 69, characters 43-48
Called from file "src/wp/Context.ml", line 68, characters 14-17
Re-raised at file "src/wp/Context.ml", line 69, characters 43-48
Called from file "src/wp/Context.ml", line 68, characters 14-17
Re-raised at file "src/wp/Context.ml", line 69, characters 43-48
Called from file "src/wp/Context.ml", line 68, characters 14-17
Re-raised at file "src/wp/Context.ml", line 69, characters 43-48
Called from file "src/wp/calculus.ml", line 448, characters 14-224
Called from file "src/wp/calculus.ml", line 595, characters 10-57
Called from file "src/wp/calculus.ml", line 536, characters 19-40
Called from file "src/wp/calculus.ml", line 579, characters 20-43
Called from file "src/wp/calculus.ml", line 536, characters 19-40
Called from file "src/wp/calculus.ml", line 574, characters 20-43
Called from file "src/wp/calculus.ml", line 536, characters 19-40
Called from file "src/wp/calculus.ml", line 724, characters 40-59
Called from file "set.ml", line 304, characters 38-41
Called from file "map.ml", line 168, characters 20-25
Called from file "map.ml", line 168, characters 10-18
Called from file "map.ml", line 168, characters 10-18
Called from file "src/wp/calculus.ml", line 724, characters 4-64
Called from file "src/wp/calculus.ml", line 770, characters 19-51
Called from file "src/wp/cfgWP.ml", line 1402, characters 39-62
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/wp/cfgWP.ml", line 1391, characters 14-837
Called from file "src/wp/Model.ml", line 111, characters 17-20
Re-raised at file "src/wp/Model.ml", line 116, characters 25-28
Called from file "src/wp/Model.ml", line 117, characters 19-36
Called from file "src/wp/register.ml", line 435, characters 15-40
Called from file "src/wp/register.ml", line 574, characters 17-24
Re-raised at file "src/wp/register.ml", line 578, characters 27-29
Called from file "src/wp/register.ml", line 575, characters 17-24
Re-raised at file "src/wp/register.ml", line 579, characters 30-32
Called from file "src/wp/register.ml", line 575, characters 17-24
Re-raised at file "src/wp/register.ml", line 579, characters 30-32
Called from file "queue.ml", line 134, characters 6-20
Called from file "src/kernel/boot.ml", line 37, characters 4-20
Called from file "src/kernel/cmdline.ml", line 763, characters 2-9
Called from file "src/kernel/cmdline.ml", line 216, characters 4-8
Unexpected error (File "src/wp/MemVar.ml", line 474, characters 54-60: Assertion failed).
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Sodium-20150201.
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_guidelinesLoïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/597typo in grammar2021-02-22T13:06:42ZDavid Coktypo in grammarID0001784:
**This issue was created automatically from Mantis Issue 1784. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001784:
**This issue was created automatically from Mantis Issue 1784. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001784 | Frama-C | Documentation > ACSL | public | 2014-05-25 | 2015-09-09 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | DavidCok | **Assigned To** | patrick | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | Frama-C Sodium |
### Description :
The ACSL Neon documentation, in Fig 2.12, uses 'lemma-def' but defines 'lemma-decl'.
Presumably these should both be 'lemma-def'https://git.frama-c.com/pub/frama-c/-/issues/598Slow in proof obligation generation2021-04-15T08:41:46Zmantis-gitlab-migrationSlow in proof obligation generationID0002156:
**This issue was created automatically from Mantis Issue 2156. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002156:
**This issue was created automatically from Mantis Issue 2156. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002156 | Frama-C | Plug-in > wp | public | 2015-09-03 | 2015-09-07 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | juki21c | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | Both Ubuntu and OS X | **OS Version** | - |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | - |
### Description :
I experienced that Frama-C/WP was very slow in generating the proof obligations only (skipping invoking any provers). For the attached files, code6.c takes about 1 min. code10.c takes about 15 min. code12.c abnormally terminates Frama-C with a stack overflow error.
### Steps To Reproduce :
> frama-c -wp -wp-prover why3ide -pp-annot -wp-gen -wp-out out code6.c
> frama-c -wp -wp-prover why3ide -pp-annot -wp-gen -wp-out out code10.c
> frama-c -wp -wp-prover why3ide -pp-annot -wp-gen -wp-out out code12.c
## Attachments
- [code.zip](/uploads/f899faa93ff0631830e910686ea4ef7d/code.zip)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/599invalid statement contract ("assigns") verified with CVC4 under strange circu...2021-02-22T13:29:19ZJochen Burghardtinvalid statement contract ("assigns") verified with CVC4 under strange circumstancesID0002110:
**This issue was created automatically from Mantis Issue 2110. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002110:
**This issue was created automatically from Mantis Issue 2110. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002110 | Frama-Clang | Plug-in > wp | public | 2015-04-30 | 2015-09-07 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Sodium-20150201 | **OS** | - | **OS Version** | xubuntu14.04 |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp-prover cvc4 -wp 473.c" on the attached file (referred to as version "(0)" in the modification discussion below) results in verifying all proof obligations, including the statement contract in line 27, which is obviously false, since "myRead" also assigns "fd->pos" (line 13) and definitely changes it (line 15). I can't see a contradiction from which line 27 could be proven.
CVC4 still proves all obligations if one of the following changes is made:
(+1) myRead's "assigns" clauses in line 13 and 14 are joined into a single one, viz. "assigns fd->pos,*a;"
(+2) all "requires" clauses in line 10-12 and 20-22 are commented-in simultaneously
CVC4 fails to prove the statement contract in line 27 if one of the following changes is made:
(-1) myRead's "assigns" clauses in line 13 and 14 are swapped,
(-2) myRead's "assigns" clauses in line 13 and 14 are joined into a single "assigns *a,fd->pos;"
(-3) the "ensures" clauses in line 15 is deleted
(-4) the "ensures" clauses in line 23 (i.e. the whole contract) is deleted
(-5) the type of "a" is changed from "struct A*" to "int*" in line 17 and 25
From (+1) vs. (-2), as well as from (0) vs. (-1), it seems that the order of the memory location specifiers in myRead's "assigns" clause does matter.
In (0) vs. (-4), the "ensures" clause of "myMain" apparently influences its body code.
## Attachments
- [473.c](/uploads/11dc1d524233fc5202f6d678f181dca2/473.c)
- [wp-out.tar.gz](/uploads/ab1dd06676ca947a179dfe9d25490319/wp-out.tar.gz)
- [myMain_0b.why](/uploads/7dbe248cc0d0ba6fe57db28b2ffe6d19/myMain_0b.why)
- [myMain_0b1.smt2](/uploads/d3a0414d7a30295360902d885a8b6107/myMain_0b1.smt2)
- [myMain_0b2.smt2](/uploads/0835c74f12ab3e7a82f4a7d6ad984ac0/myMain_0b2.smt2)
- [myMain_0.smt2](/uploads/22b46ceffb1f126b776507e741a9134c/myMain_0.smt2)
- [myMain_-4.smt2](/uploads/7c12b3f5df33a42109d0215a16cc65c9/myMain_-4.smt2)
- [myMain_0.why](/uploads/e153c4b48d2e88354dae40eea92a4613/myMain_0.why)
- [myMain_-4.why](/uploads/45ab78b845a9d3f96afb1065a32e9184/myMain_-4.why)https://git.frama-c.com/pub/frama-c/-/issues/601bound variable names in Coq file depend on unrelated function later in C sour...2021-04-15T06:45:00ZJochen Burghardtbound variable names in Coq file depend on unrelated function later in C source codeID0002153:
**This issue was created automatically from Mantis Issue 2153. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002153:
**This issue was created automatically from Mantis Issue 2153. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002153 | Frama-C | Plug-in > wp | public | 2015-08-31 | 2015-09-03 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Sodium-20150201 | **OS** | - | **OS Version** | xubuntu14.04 |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -pp-annot -wp -wp-split -kernel-msg-key pp -wp-model Typed+ref -wp-driver ../BitTest.driver -cpp-command 'gcc -C -E' -wp-timeout 2 -wp-coq-timeout 5 -wp-prover cvc4 -wp-prover coq 0.c -wp-out 0.wp" on the attached file "0.c", and the corresponding command on "1.c", generate Coq proof obligation files "0.wp/typed_ref_BitTest/Bitstream_WriteThenRead_assert_left.coq" and "1.wp/typed_ref_BitTest/Bitstream_WriteThenRead_assert_left.coq" that differ in bound variable names.
However, "0.c" initially just includes "1.c" and the defines a function "Bitstream_ReadThenWrite" that is unrelated to the code in "1.c"; for this reason, it shouldn't influence the proof obligation of "Bitstream_WriteThenRead_assert_left". The influence apparently depends on the name of the trailing extra-function in "0.c": if it is named "Bitstream_XeadThenWrite", then the problem disappears. Frama-C handles functions in alphabetical order, as can be seen by its stdout messages.
## Attachments
- [0.c](/uploads/5e9c47840cfd6d001d24d36f3d401dfa/0.c)
- [1.c](/uploads/456c5e464671fb845a75362f43ec8bb3/1.c)
- [BitTest.driver](/uploads/fb98b62b3dcf8b0dad1d87be5184dfd7/BitTest.driver)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/602With struct containing arrays, option -unspecified-access is too strict2021-04-28T09:34:03ZPascal CuoqWith struct containing arrays, option -unspecified-access is too strictID0002152:
**This issue was created automatically from Mantis Issue 2152. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002152:
**This issue was created automatically from Mantis Issue 2152. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002152 | Frama-C | Kernel | public | 2015-08-21 | 2015-08-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
The program given below is correct, but:
$ frama-c -val t.c -unspecified-access
...
t.c:4:[kernel] warning: Unspecified sequence with side effect:
/* s.t[1] <- s.t */
s.t[1] = (char)0;
/* s.t[2] <- s.t */
s.t[2] = s.t[1];
[value] Analyzing a complete application starting at main
...
t.c:4:[kernel] warning: undefined multiple accesses in expression. assert \separated(&s.t[1], &s.t);
[value] Recording results for main
[value] done for function main
t.c:4:[value] Assertion 'Value,separation' got final status invalid.
...
I expected this program would be accepted without a warning about multiple accesses in expressions.
### Additional Information :
The struct is necessary for the bug to appear. With a toplevel array t, the assignment t[2] = t[1] = 0; does not cause a warning.
### Steps To Reproduce :
```c
struct s { char t[3]; } s;
int main() {
s.t[2] = s.t[1] = 0;
return 0;
}
```Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/604suggest to warn about ensures clauses containing only \old variables2021-02-22T13:06:57ZJochen Burghardtsuggest to warn about ensures clauses containing only \old variablesID0001017:
**This issue was created automatically from Mantis Issue 1017. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001017:
**This issue was created automatically from Mantis Issue 1017. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001017 | Frama-C | Kernel > ACSL implementation | public | 2011-11-10 | 2015-08-03 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | no change required |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Nitrogen-20111001 | **Target Version** | - | **Fixed in Version** | - |
### Description :
A novice student wrote "ensures 0<=\old(n)<10;" when he actually meant "requires 0<=n<10;" in his solution to an Acsl exercise.
As this kind of error can be detected easily (ensures clauses should contain at least one identifier outside of \old), I suggest to add a warning in these cases.
See attached file for an own minimal example.
## Attachments
- [ftest.c](/uploads/843b644ab8a3c44a7e6e286c4b05969e/ftest.c)https://git.frama-c.com/pub/frama-c/-/issues/608Slicing does not preserve some ACSL constructs2021-02-22T14:01:48ZJulien SignolesSlicing does not preserve some ACSL constructsID0000690:
**This issue was created automatically from Mantis Issue 690. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000690:
**This issue was created automatically from Mantis Issue 690. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000690 | Frama-C | Plug-in > slicing | public | 2011-01-26 | 2015-08-03 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | signoles | **Assigned To** | yakobowski | **Resolution** | not fixable |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20101202-beta2 | **Target Version** | - | **Fixed in Version** | - |
### Description :
The slicer does not keep ACSL annotations if it does not understand them. This behavior may prevent to prove properties of the sliced program.
### Steps To Reproduce :
Consider the following program:
==== a.c
int t[10];
void main(void) {
/*@ loop invariant 0 <= i <= 10;
@ loop invariant \forall integer k; 0 <= k < i ==> t[k] == 0;
@ */
for(int i = 0; i < 10; i++) t[i] = 0;
/*@ assert t[0] == 0; */
}
====
Run it with:
$ frama-c -slice-assert main -slice-print a.c
The printed program forget the second loop invariant. Thus, for instance, plug-in WP cannot prove the final assertion anymore.
/* Generated by Frama-C */
int t[10] ;
void main(void)
{
{ int i ; i = 0;
/*@ loop invariant (0 ? i) ? (i ? 10); */
while (i < 10) { t[i] = 0; i ++; }
}
/*@ assert (t[0] ? 0); */ ;
return;
}https://git.frama-c.com/pub/frama-c/-/issues/609Control dependencies between labelled instructuctions and the corresponding ...2022-09-28T14:07:01Zmantis-gitlab-migrationControl dependencies between labelled instructuctions and the corresponding goto statementID0001992:
**This issue was created automatically from Mantis Issue 1992. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001992:
**This issue was created automatically from Mantis Issue 1992. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001992 | Frama-C | Plug-in > pdg | public | 2014-11-25 | 2015-08-03 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | nguenaomer | **Assigned To** | maroneze | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | X68 | **OS** | Linux | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130601 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Issue1: Does the pdg of frama-c include the transitive closure of standard control and data dependency relation?
Issue2: I think that there is an error in the PDG (or only the dot version).
The PDG of the function below states that the "while_0_break" statement control the "goto while_0_break" when using the -simplify-cfg option. To me, it should be the converse. The same with Neon.
Note that Issue1 and Issue2 are related.
### Steps To Reproduce :
I executed the following commamds with the C code below
$frama-c -pdg example2.c -main transfer_func -pdg-dot pdg2 -simplify-cfg
$dot -Tpng -o pdg2.transfer_func.png pdg2.transfer_func.dot
int x1,x2 ;
void transfer_func(int time) {
int prod =1 ;
int k =1 ;
while (k<=10) {
if (time/k > prod) break ;
prod *= k;
k++ ;
}
x1++;
x2++;
}
Enclosed is the pdg.
## Attachments
- ![pdg2.transfer_func](/uploads/89e7e73de0bccff6146ec1bca3678b43/pdg2.transfer_func.png)Andre MaronezeAndre Maronezehttps://git.frama-c.com/pub/frama-c/-/issues/611implicit conversion of terms to predicates2021-02-22T13:39:30ZDavid Cokimplicit conversion of terms to predicatesID0002148:
**This issue was created automatically from Mantis Issue 2148. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002148:
**This issue was created automatically from Mantis Issue 2148. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002148 | Frama-C | Kernel > ACSL implementation | public | 2015-07-17 | 2015-07-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dcok@grammatech.com | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | - |
### Description :
ACSL distinguishes carefully between terms and predicates. For example, a predicate (e.g. \valid(...) ) cannot be placed in a term position, such as the argument of a cast.
However, clauses such as 'requires 1;' are accepted by Frama-C, even though the 1.9 grammar nowhere permits terms to be implicitly converted to predicates. Integer-typed terms maybe implicitly converted to boolean terms, but there is no indication that terms are converted to predicates.
Is this an oversight in the grammar? or does Frama-C accept more than the grammar as a convenience?Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/612Error when struct has no members2021-04-14T15:50:21Zmantis-gitlab-migrationError when struct has no membersID0002145:
**This issue was created automatically from Mantis Issue 2145. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002145:
**This issue was created automatically from Mantis Issue 2145. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002145 | Frama-C | Plug-in > wp | public | 2015-07-15 | 2015-07-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Ian | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | Ubuntu | **OS Version** | - |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | - |
### Description :
WP produces an invalid ergo file when there is a struct which contains no members. The failure was present using alt-ergo, why3:alt-ergo, and why3:z3-4.4.0
### Steps To Reproduce :
Create empty_struct.c:
struct a{};
void foo() {
struct a i,j;
//@ assert i == j;
}
run:
> frama-c empty_struct.c -wp -wp-out struct_out
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing empty_struct.c (with preprocessing)
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[wp] warning: Missing RTE guards
[wp] 1 goal scheduled
struct_out/typed/S_a.ergo:5:[wp] user error: Alt-Ergo error:
characters 14-15:syntax error
[wp] [Alt-Ergo] Goal typed_foo_assert : Failed
Error: characters 14-15:syntax error
[wp] Proved goals: 0 / 1
Alt-Ergo: 0 (failed: 1)
> frama-c empty_struct.c -wp -wp-out struct_out -wp-prover why3:alt-ergo
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing empty_struct.c (with preprocessing)
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[wp] warning: Missing RTE guards
[wp] 1 goal scheduled
------------------------------------------------------------
--- Why3 (stderr) :
------------------------------------------------------------
[Config] reading extra configuration file /usr/local/share/frama-c/wp/why3/why3.conf
/usr/local/lib/why3/plugins/hypothesis_selection can't be loaded : Dynlink error : cannot find file /usr/local/lib/why3/plugins/hypothesis_selection.cmxs in search path
File "struct_out/typed/S_a.why", line 13, characters 13-14:
syntax error
------------------------------------------------------------
[wp] [alt-ergo] Goal typed_foo_assert : Failed
Error: Why3 exits with status [1]
[wp] Proved goals: 0 / 1
alt-ergo: 0 (failed: 1)
> frama-c empty_struct.c -wp -wp-out struct_out -wp-prover why3:z3-4.4.0
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing empty_struct.c (with preprocessing)
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[wp] warning: Missing RTE guards
[wp] 1 goal scheduled
------------------------------------------------------------
--- Why3 (stderr) :
------------------------------------------------------------
[Config] reading extra configuration file /usr/local/share/frama-c/wp/why3/why3.conf
/usr/local/lib/why3/plugins/hypothesis_selection can't be loaded : Dynlink error : cannot find file /usr/local/lib/why3/plugins/hypothesis_selection.cmxs in search path
File "struct_out/typed/S_a.why", line 13, characters 13-14:
syntax error
------------------------------------------------------------
[wp] [z3-4.4.0] Goal typed_foo_assert : Failed
Error: Why3 exits with status [1]
[wp] Proved goals: 0 / 1
z3-4.4.0: 0 (failed: 1)
## Attachments
- [empty_struct.c](/uploads/10b5a1fe20023bf3f990705bc2c1048d/empty_struct.c)
- [S_a.ergo](/uploads/1467997d82e0c98a27a1272083c9f126/S_a.ergo)
- [S_a.why](/uploads/0262536de1d48f1a1a041741a72a0edd/S_a.why)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/616Frama-C problem with macro substitution in annotations2021-03-29T17:50:08ZDavid CokFrama-C problem with macro substitution in annotationsID0002147:
**This issue was created automatically from Mantis Issue 2147. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002147:
**This issue was created automatically from Mantis Issue 2147. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002147 | Frama-C | Kernel > ACSL implementation | public | 2015-07-16 | 2015-07-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dcok@grammatech.com | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | - |
### Description :
This piece of code should parse with frama-c, but does not:
#define MACRO 3
void m() {
char buf[MACRO+1];
//@ assert \valid(buf+(0..MACRO));
}
Upon execution, frama-c gives back "[kernel] user error: unbound logic variable MACRO in annotation.".
This piece of code, however, executes as it should:
#define MACRO 3
void m() {
char buf[MACRO+1];
//@ assert \valid(buf+(0.. MACRO));
}
This code is also okay:
#define MACRO 3
void m() {
char buf[MACRO+1];
//@ assert \valid(buf+(0..(MACRO)));
}
It seems that frama-c refuses to substitute defines directly after a .. operator.Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/617deficient axioms2021-02-22T13:07:23ZDavid Cokdeficient axiomsID0002138:
**This issue was created automatically from Mantis Issue 2138. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002138:
**This issue was created automatically from Mantis Issue 2138. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002138 | Frama-C | Plug-in > wp | public | 2015-06-29 | 2015-06-29 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | DavidCok | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | Windows | **OS Version** | 7 |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | - |
### Description :
The proof of the following with -WP and alt-ergo fails:
/*@
requires (int)(x+y) == x+y;
ensures \result == x+y;
*/
int f(int x, int y) {
return x+y;
}
On inspecting the intermediate artifacts, we identified the problem as inadequate axioms. Two solutions requiring changes in axioms worked for us.
However, I don't know if either change would have wider ramifications.
1)
axiom is_to_sint32 :
(forall x:int [is_sint32(to_sint32(x))]. is_sint32(to_sint32(x)))
The effect of the triggers in this axiom is simply to allow is_sint32(to_sint32(x)) to be reduced to true. In fact the more common need is to know that to_sint32(x) satisfies is_sint32. The proof above goes through if the trigger is changed to
axiom is_to_sint32 :
(forall x:int [to_sint32(x)]. is_sint32(to_sint32(x)))
2)
axiom id_sint32 :
(forall x:int [to_sint32(x)]. ((((-2147483648) <= x) and
(x < 2147483648)) -> (to_sint32(x) = x)))
This axiom is much more useful if it is written as an equivalence instead of an implication. Doing so also enables the proof of the program above to go through.https://git.frama-c.com/pub/frama-c/-/issues/618Sessions and WP do not interact properly2021-02-22T13:07:24Zmantis-gitlab-migrationSessions and WP do not interact properlyID0002044:
**This issue was created automatically from Mantis Issue 2044. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002044:
**This issue was created automatically from Mantis Issue 2044. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002044 | Frama-C | Plug-in > wp | public | 2015-01-06 | 2015-06-29 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | ploc | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | - |
### Description :
Bonjour, quelques problèmes avec le -save et le -load des sessions conjugés avec WP/Why3 et l'option no-let !!!!
1. Si on utilise pas -wp-out les fichiers temporaires de wp sont supprimés et lors du prochain appel de frama-c avec le -load, il se plaint de l'absence des fichiers
2. Si on specifie -wp-out, avec le -load, Frama-C retrouve les fichiers générés mais il ne semble pas retrouver tout ce dont il a besoin.
3. Enfin lors de l'utilisation de coq comme prover lors d'un run (avec -load et -save), au prochain appel avec toujours -load et -save, frama-c appelle systématiquement coq, y compris si on specifie -wp-prover altergo par exemple.
### Steps To Reproduce :
Pour les points 1 et 2:
Par exemple, pour le fichier C suivant:
$ cat essai.c
struct greycounter_mem {_Bool _first; };
/*@ requires \valid(self);
@ ensures ((*self)._first ==1);
@ assigns *self;*/
void greycounter_reset (struct greycounter_mem *self) {
self->_first = 1;;
return;
}
Le script suivant active les différents problemes:
#!bin/bash
src=essai.c
# Error 1: temporary wp folder with no-let option and why3 solver (eg. altergo or CVC4)
frama-c -save session -wp-prop "@ensures" -wp-prover why3:altergo -wp-no-let $src
frama-c -load session -save session -wp-prop "@assigns" $src
# Error 2: no-let with why3:cvc4
frama-c -save session -wp-prop "@ensures" -wp-prover CVC4 $src -wp-no-let -wp-out wp
frama-c -load session -save session -wp-prop "@assigns" $src
# Here it works
frama-c -save session -wp-prop "@ensures" -wp-prover CVC4 $src -wp-out wp
frama-c -load session -save session -wp-prop "@assigns" $srchttps://git.frama-c.com/pub/frama-c/-/issues/620unable to use lemma separated_region2021-04-15T09:10:25ZJens Gerlachunable to use lemma separated_regionID0002041:
**This issue was created automatically from Mantis Issue 2041. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002041:
**This issue was created automatically from Mantis Issue 2041. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002041 | Frama-C | Plug-in > wp | public | 2014-12-28 | 2015-06-29 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | - |
### Description :
I am using two Frama-C installation:
1.) Neon-20140301 installed through opam under OS X
2.) Neon-20140301+dev-stance manually installed under Linix
In both installations the lemma separated_region in file FRAMAC_SHARE/wp/coqwp/Memory.v
is unaccessible because it is put in comments.
I suspect that this is the reason why I cannot prove that a local struct variable is separated from one
that a function receives as an argument.
What is the reason that this lemma is not available?Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/622normalization of "assigns" in statement contract doens't cope with introduced...2021-03-30T07:28:00ZJochen Burghardtnormalization of "assigns" in statement contract doens't cope with introduced auxiliary variablesID0002102:
**This issue was created automatically from Mantis Issue 2102. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002102:
**This issue was created automatically from Mantis Issue 2102. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002102 | Frama-Clang | Plug-in > wp | public | 2015-04-09 | 2015-06-29 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | sometimes |
| **Platform** | Sodium-20150201 (opam) | **OS** | xubuntu14.04 | **OS Version** | - |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp 468.c" on the attached program generates an unprovable obligation (viz. "false" in Alt-Ergo's .mlw file) for the "assert" (statement contract) in line 7.
Running "frama-c-gui -wp 468.c" shows that the code normalization introduced an auxiliary variable "tmp", which is assigned, too (cf. attached image "468.gif"). However the "assigns" clause wasn't extended accordingly; so in the normalized version, the statement contract is indeed false.
A workaround, found by our student Timon Lapawczyk, is to enclose the statement in line 8 into braces, which makes the contract refer to a compound statement with "tmp" a hidden variable inside it. In this case, the statement contract is proven without problems.
## Attachments
- [468.c](/uploads/3ffd2a021e987a1ea908721495c6fa87/468.c)
- ![468](/uploads/5d29ccc3dc630b3c4df7845d74ead155/468.gif)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/623Frama-C GUI crashes under OS X2021-02-22T13:07:34ZJens GerlachFrama-C GUI crashes under OS XID0002099:
**This issue was created automatically from Mantis Issue 2099. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002099:
**This issue was created automatically from Mantis Issue 2099. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002099 | Frama-C | Graphical User Interface | public | 2015-03-31 | 2015-06-29 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | - |
### Description :
If I start the Frama-C GUI on the attached program with 'frama-c-gui lemma.c',
then the GUI starts normally.
In the 'Source' panel I can see 'lemma.c.
When I try to see the lemma inside the file by clicking on the filename (or the little triangle left of it),
then the GUI crashes.
This does not happen under Linux.
### Additional Information :
frama-c was installed with opam
OS X (10.10.3 (14D127a))
opam --version: 1.2.0
frama-c -version
Version: Sodium-20150201
Compilation date: Tue Mar 31 09:48:58 CEST 2015
## Attachments
- [lemma.c](/uploads/f1e70f11f828611cc31af293e127a3c4/lemma.c)https://git.frama-c.com/pub/frama-c/-/issues/624do ... while{ } loop and -wp-invariants option2021-02-22T13:23:13ZLionel Blatterdo ... while{ } loop and -wp-invariants optionID0002118:
**This issue was created automatically from Mantis Issue 2118. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002118:
**This issue was created automatically from Mantis Issue 2118. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002118 | Frama-C | Plug-in > wp | public | 2015-05-19 | 2015-06-29 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | blatterl | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Linux | **OS** | Fedora | **OS Version** | Version 17 |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | - |
### Description :
When I use the WP plug-in on the do ... while{ } loop below with the -wp-invariants option, WP proves all goals.
But the ensures properties ("ensures n == 0 ==> \result == 0") of the function, including the do ... while{ } loop seems not valid to me.
I get the same result if I replace the post condition "\result == 0" by anything.
What is the exact semantics of the -wp-invariants option ?
/*@ ensures n == 0 ==> \result == 0; */
int fonction(int n, int a){
int i = 0;
int b = 0;
/*@ loop invariant b == i*a; */
do {
b = b+a;
i = i+1;
} while (i < n);
/*@ assert n== 0 ==> b==a; */
return b;
}
### Steps To Reproduce :
frama-c -wp -wp-invariants file.c
with file.c containing the above snippet.https://git.frama-c.com/pub/frama-c/-/issues/625validity of obligation from statement contract depends on whether the stateme...2021-08-05T09:27:25ZJochen Burghardtvalidity of obligation from statement contract depends on whether the statement is enclosed in block {}ID0002123:
**This issue was created automatically from Mantis Issue 2123. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002123:
**This issue was created automatically from Mantis Issue 2123. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002123 | Frama-C | Plug-in > wp | public | 2015-06-01 | 2015-06-29 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Sodium-20150201 | **OS** | - | **OS Version** | xubuntu14.04 |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp 480.c" on the attached program produces one unproven Alt-Ergo obligation (see file "in_block_foo_stmt_post_Alt-Ergo.mlw").
If the block parentheses in line 16 and 23 are removed, the corresponding obligation (file "not_in_block_foo_stmt_post_Alt-Ergo.mlw") is proven.
The differences between both obligations files are:
772c772
< forall t_2,t_1 : (addr,int) farray.
---
> forall t_1 : (addr,int) farray.
780c780
< (1 = L_deref(t_2, a))
---
> (1 = L_deref(t_1, a))
So, enclosing the statement in a block apparently creates an unrelated memory state.
## Attachments
- [480.c](/uploads/55316dd19dad2a676e3bd65c099feb68/480.c)
- [in_block_foo_stmt_post_Alt-Ergo.mlw](/uploads/a9e4708fc1538ad58d7a2b081be33aa2/in_block_foo_stmt_post_Alt-Ergo.mlw)
- [not_in_block_foo_stmt_post_Alt-Ergo.mlw](/uploads/825bcad7efb1e4837cdba3c38b5efd31/not_in_block_foo_stmt_post_Alt-Ergo.mlw)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/626requires in beahviors do not behave as expected2021-02-22T13:54:03ZDavid Cokrequires in beahviors do not behave as expectedID0002133:
**This issue was created automatically from Mantis Issue 2133. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002133:
**This issue was created automatically from Mantis Issue 2133. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002133 | Frama-C | Plug-in > wp | public | 2015-06-12 | 2015-06-29 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | DavidCok | **Assigned To** | correnson | **Resolution** | won't fix |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | Windows | **OS Version** | 7 |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | - |
### Description :
See the code below. The second case proves the assignment temp=p[0] OK, the first case does not (with -wp-rte enabled), using Frama-C with default alt-ergo. The corresponding proof obligations are shown below the code. The difference between the two cases is that the requires clause is pulled out in front in the second case.
The proof in the second case includes as an assumption the stated requires clause. And it proves OK even if the requires clause is
requires (num == 2) ==> (\valid(p) && \valid(p+1));
However the first proof has no assumptions corresponding to the requires clause.
This appears to me to be a bug in WP but the language of the proof obligations is unfamiliar to me - so I'd be glad to have this case explained.
/*@
@
@ behavior b2:
@ assumes num == 2;
@ requires \valid(p) && \valid(p+1);
@ ensures p[1] == \old(p[0]) && p[0] == \old(p[1]);
*/
void swap(int* p, int num) {
int temp;
switch (num) {
case 2:
temp = p[0];
p[0] = p[1];
p[1] = temp;
break;
default:
}
}
/*@
@ requires \valid(p) && \valid(p+1);
@ behavior b2:
@ assumes num == 2;
@ ensures p[1] == \old(p[0]) && p[0] == \old(p[1]);
*/
void swap2(int* p, int num) {
int temp;
switch (num) {
case 2:
temp = p[0];
p[0] = p[1];
p[1] = temp;
break;
default:
}
}
FramacWp: Function swap
FramacWp: ------------------------------------------------------------
FramacWp:
FramacWp: Goal Assertion 'rte,mem_access' (file C/cygwin/home/sb/trunk/nasa-speedy/EditorTest/src/behaviorBug.c, line 14):
FramacWp: Tags: Case 2.
FramacWp: Assume { (* Heap *) Have: (linked Malloc_0). }
FramacWp: Prove: (valid_rd Malloc_0 (shift p_1 0) 1).
FramacWp: Prover Alt-Ergo returns Unknown (1s)
FramacWp:
FramacWp: ------------------------------------------------------------
FramacWp: Function swap2
FramacWp: ------------------------------------------------------------
FramacWp:
FramacWp: Goal Assertion 'rte,mem_access' (file C/cygwin/home/sb/trunk/nasa-speedy/EditorTest/src/behaviorBug.c, line 33):
FramacWp: Tags: Case 2.
FramacWp: Assume {
FramacWp: (* Heap *)
FramacWp: Have: (linked Malloc_0).
FramacWp: (* Pre-condition (file C/cygwin/home/sb/trunk/nasa-speedy/EditorTest/src/behaviorBug.c, line 24) in 'swap2' *)
FramacWp: (* Pre-condition: *)
FramacWp: Have: (valid_rw Malloc_0 p_1 1) /\ (valid_rw Malloc_0 (shift p_1 1) 1).
FramacWp: }
FramacWp: Prove: (valid_rd Malloc_0 (shift p_1 0) 1).
FramacWp: Prover Alt-Ergo returns Valid (16)
### Steps To Reproduce :https://git.frama-c.com/pub/frama-c/-/issues/627Range of remainder of two positive integers, wrong and missing assertions.2021-02-22T13:07:39Zmantis-gitlab-migrationRange of remainder of two positive integers, wrong and missing assertions.ID0002129:
**This issue was created automatically from Mantis Issue 2129. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002129:
**This issue was created automatically from Mantis Issue 2129. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002129 | Frama-C | Plug-in > wp | public | 2015-06-04 | 2015-06-29 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | loic | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | Linux | **OS** | Ubuntu | **OS Version** | 12.04.5 LTS |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Nitrogen-20111001
alt-ergo 0.94
False negative and false positive int the following code.
/*@ requires 0 <= n; */
void modulo_testcase_0(unsigned n) {
/*@ ghost unsigned q = n / 2; */
/*@ ghost unsigned r = n % 2; */
/*@ assert 0 <= n; */ /* OK */
/*@ assert n == 2*q + r; */ /* OK */
/*@ assert 0 <= q; */ /* OK */
/*@ assert 0 <= r < 1; */ /* NOK, cannot be proven */
}
/*@ requires 0 <= n && 0 < d; */
void modulo_testcase_1(int n, int d) {
/*@ assert n <= d * (n / d); */ /* NOK, cannot be proven */
/*@ ghost int q = n / d; */ /* OK */
/*@ ghost int r = n % d; */ /* OK */
/*@ assert 0 <= r < 1; */ /* NOK, r < d is true */
/*@ assert n <= d * (n / d); */ /* OK */
}
### Steps To Reproduce :
frama-c -wp -wp-rte on the code above (also as attachment).
## Attachments
- [modulo_testcase.c](/uploads/b725efd4758f124867c970e99d059011/modulo_testcase.c)https://git.frama-c.com/pub/frama-c/-/issues/628*off == off_cpy cannot be proven just after the assignment *off = off_cpy2021-02-22T13:07:41Zmantis-gitlab-migration*off == off_cpy cannot be proven just after the assignment *off = off_cpyID0002130:
**This issue was created automatically from Mantis Issue 2130. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002130:
**This issue was created automatically from Mantis Issue 2130. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002130 | Frama-C | Plug-in > wp | public | 2015-06-04 | 2015-06-29 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | loic | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | Linux | **OS** | Ubuntu | **OS Version** | 12.04.5 LTS |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Nitrogen-20111001
alt-ergo 0.94
#include <stddef.h>
/*
* Can memory zones be declared disjoint? For instance:
* \disjoint(off, buf + *off)
*
* wp does not accept and thus gracefully skips the following try:
* @ requires \forall size_t i;
* 0 <= i < sizeof(*off) ==> (char *) off != buf + (*off + i);
*/
/*@
@ requires \valid(off) && \valid(buf + *off);
@ assigns *off, buf[*off];
@ ensures *off == \old(*off) + 1;
@ ensures buf[\old(*off)] == '\0';
@*/
void alias_testcase_0(char *const buf, size_t *const off) {
size_t off_cpy = *off; /* restricted pointers cannot be required */
buf[off_cpy++] = '\0';
/*@ assert off_cpy - 1 == \at(*off, Pre); */ /* OK */
/*@ assert buf[off_cpy - 1] == '\0'; */ /* OK */
*off = off_cpy;
/*@ assert *off == off_cpy; */ /* NOK, cannot be proven */
/*@ assert buf[\at(*off, Pre)] == '\0'; */ /* NOK, cannot be proven */
}
### Steps To Reproduce :
frama-c -wp -wp-rte on the code above (also as attachment).
## Attachments
- [alias_testcase.c](/uploads/65a0be19399d07141588a8edf1eeb1c0/alias_testcase.c)https://git.frama-c.com/pub/frama-c/-/issues/630Weak and Strong Invariants are not supported2021-02-22T13:07:41Zmantis-gitlab-migrationWeak and Strong Invariants are not supportedID0002134:
**This issue was created automatically from Mantis Issue 2134. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002134:
**This issue was created automatically from Mantis Issue 2134. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002134 | Frama-C | Kernel > ACSL implementation | public | 2015-06-12 | 2015-06-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | gaggarwal | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | - |
### Description :
ACSL manual version 1.8, in Figure 2.23 explains grammar of data-invariant and type-invariant. Section 2.11(Data invariants) explains the difference between between strong and weak invariants.
I tried running the example manual have for strong invariant in the same section. But it seems like weak and strong invariants are not supported and ACSL parser is not able to parse the invariants with inv-strength.
### Steps To Reproduce :
I used example ACSL manual version 1.8 have :
int a;
//@ global invariant a_is_positive: a >= 0 ;
typedef double temperature;
/*@ strong type invariant temp_in_celsius(temperature t) =
@ t >= -273.15 ;
@*/
struct S {
int f;
};
//@ type invariant S_f_is_positive(struct S s) = s.f >= 0 ;
Ran "frama-c -wp file.c" command and got following kernel error:
file.c:5:[kernel] user error: unexpected token 'type'Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/631*i == *j cannot be proven from i == j2021-02-22T13:07:43Zmantis-gitlab-migration*i == *j cannot be proven from i == jID0002128:
**This issue was created automatically from Mantis Issue 2128. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002128:
**This issue was created automatically from Mantis Issue 2128. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002128 | Frama-C | Plug-in > wp | public | 2015-06-04 | 2015-06-08 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | loic | **Assigned To** | virgile | **Resolution** | unable to reproduce |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Linux | **OS** | Ubuntu | **OS Version** | 12.04.5 LTS |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Sodium |
### Description :
Nitrogen-20111001
alt-ergo 0.94
The following assertion cannot be proven.
void pointer_testcase(int *i, int *j) {
/*@ assert i == j ==> *i == *j; */
}
### Steps To Reproduce :
frama-c -wp -wp-rte on the code above (also as attachment).
## Attachments
- [pointer_testcase.c](/uploads/ec0d97eb74499b149912f74f57f48a94/pointer_testcase.c)https://git.frama-c.com/pub/frama-c/-/issues/632E-ACSL: executes "__store_block()" but never "__delete_block()"!2021-02-22T14:01:28Zmantis-gitlab-migrationE-ACSL: executes "__store_block()" but never "__delete_block()"!ID0001636:
**This issue was created automatically from Mantis Issue 1636. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001636:
**This issue was created automatically from Mantis Issue 1636. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001636 | Frama-C | Plug-in > E-ACSL | public | 2014-01-30 | 2015-06-08 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | ThomasJ | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130601 | **Target Version** | Frama-C Sodium | **Fixed in Version** | Frama-C Sodium |
### Description :
E-ACSL translation of a simple printf like:
printf("###");
results in the following code:
char *__e_acsl_literal_string;
__e_acsl_literal_string = "###";
__store_block((void *)__e_acsl_literal_string,sizeof("###"));
__full_init((void *)__e_acsl_literal_string);
__literal_string((void *)__e_acsl_literal_string);
printf(__e_acsl_literal_string);
The "__store_block()" function allocates memory, but there is no "__delete_block()" function in order to deallocate the memory!
Consider a periodic execution of printf()...
On my ARM processor with 1024KByte Flash and 160KByte RAM, this malloc without free will end up in the following error:
"assertion "new_leaf != NULL" failed: file "e-acsl/memory_model/e_acsl_bittree.c", line 256, function: __add_element"
malloc without free! :O
### Steps To Reproduce :
E-ACSL translation of:
int main(void)
{
int x = 0;
/*@ assert x == 0; */
while(1)
{
printf("###");
}
return 0;
}https://git.frama-c.com/pub/frama-c/-/issues/633Literal strings can be added multiple times in memory2021-02-22T14:01:51ZArvid JakobssonLiteral strings can be added multiple times in memoryID0001837:
**This issue was created automatically from Mantis Issue 1837. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001837:
**This issue was created automatically from Mantis Issue 1837. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001837 | Frama-C | Plug-in > E-ACSL | public | 2014-07-16 | 2015-06-08 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | arvidj | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Sodium |
### Description :
Consider the following example:
int i = 4;
while (i--) {
char *s = "toto";
/@ assert \valid(s) ; */
printf(s);
}
Each time the body of the while-loop is executed, the block corresponding to "toto" is added to the memory store, however this string has always the same address.
## Attachments
- [bug-1837-literal-strings.c](/uploads/4765106fd263bda0285e8ccba836efe9/bug-1837-literal-strings.c)https://git.frama-c.com/pub/frama-c/-/issues/634Redefintion of variables in same scope is allowed in annotations2022-09-28T11:49:38Zmantis-gitlab-migrationRedefintion of variables in same scope is allowed in annotationsID0002125:
**This issue was created automatically from Mantis Issue 2125. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002125:
**This issue was created automatically from Mantis Issue 2125. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002125 | Frama-C | Kernel > ACSL implementation | public | 2015-06-01 | 2015-06-02 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | gaggarwal | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Consider an example:
```
/*@
predicate is_valid(int* n, int n) =
(0 <= n) ;
*/
```
Frama-C doesn't throw any exception for the above predicate, even though variable "n" is defined twice in the same scope and it uses n as of Type int and allows comparison 0 <= n.
If I change the above predicate to following:
```
/*@
predicate is_valid_int_range(int n, int* n) =
(0 <= n) ;
*/
```
Frama-c complains "[kernel] user error: comparison of incompatible types: ℤ and int * in annotation" for comparison 0 <= n in above example, which means that it treats n of type int*.
Similarly, redefinition of variable in same scope is allowed in quantifier expressions like:
```
loop invariant \forall int k, char k; 0 <= k && k< i ==> a[k] == b[k];
```
In C language it is not allowed to redefine variable in same scope. Is this an intentional behavior? And if so that is the purpose behind it? I don't see this matter is discussed in ACSL document.Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/635WP crashes on generation of PO for assigns clause (assertion failure in MemVa...2021-02-22T14:01:52ZVirgile PrevostoWP crashes on generation of PO for assigns clause (assertion failure in MemVar.ml)ID0002124:
**This issue was created automatically from Mantis Issue 2124. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002124:
**This issue was created automatically from Mantis Issue 2124. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002124 | Frama-Clang | Plug-in > wp | public | 2015-06-01 | 2015-06-02 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | virgile | **Assigned To** | correnson | **Resolution** | duplicate |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
On the example source below, frama-c -wp reduced.i crashes with the following error:
File "src/wp/MemVar.ml", line 491, characters 54-60: Assertion failed
Apparently (by inferring why the offending function in MemVar got called), the p1+0 in the assigns for fn1 leads WP to think that p1 should be instantiated with an array (in particular, if you remove the +0, everything is fine).
-- reduced.i
/*@ assigns *(p1); */
int fn1(char *p1);
/*@
assigns \nothing;
*/
void fn2(void) {
char pcr_index;
fn1(&pcr_index);
}https://git.frama-c.com/pub/frama-c/-/issues/636float constant in contract causes crash2021-03-29T17:27:14ZJochen Burghardtfloat constant in contract causes crashID0001981:
**This issue was created automatically from Mantis Issue 1981. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001981:
**This issue was created automatically from Mantis Issue 1981. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001981 | Frama-Clang | Plug-in > clang | public | 2014-11-24 | 2015-05-11 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
Now output intermediate result
Could not parse floating point number ""
[kernel] Current source was: 143.cpp:3
The full backtrace is:
Called from file "cil/src/logic/logic_utils.ml", line 288, characters 16-65
Called from file "cil/src/logic/logic_typing.ml", line 2116, characters 17-60
Called from file "cil/src/logic/logic_typing.ml", line 2000, characters 14-60
Called from file "cil/src/logic/logic_typing.ml", line 2630, characters 15-26
Called from file "cil/src/logic/logic_typing.ml", line 3172, characters 56-76
Called from file "list.ml", line 57, characters 20-23
Called from file "cil/src/logic/logic_typing.ml", line 3304, characters 15-129
Called from file "list.ml", line 57, characters 20-23
Called from file "cil/src/logic/logic_typing.ml", line 3291, characters 12-1023
Called from file "cil/src/frontc/cabshelper.ml", line 58, characters 17-23
Called from file "cil/src/frontc/cabs2cil.ml", line 7411, characters 2-370
Called from file "cil/src/frontc/cabs2cil.ml", line 7702, characters 22-80
Called from file "list.ml", line 74, characters 24-34
Called from file "cil/src/frontc/cabs2cil.ml", line 7719, characters 15-54
Called from file "cil/src/frontc/cabs2cil.ml", line 9145, characters 12-35
Called from file "list.ml", line 69, characters 12-15
Called from file "cil/src/frontc/cabs2cil.ml", line 9150, characters 2-26
Called from file "src/frama-clang/frama_Clang_register.ml", line 89, characters 12-34
Called from file "src/kernel/file.ml", line 1073, characters 10-43
Called from file "src/kernel/file.ml", line 1117, characters 23-30
Called from file "list.ml", line 74, characters 24-34
Called from file "src/kernel/file.ml", line 1114, characters 6-520
Called from file "src/kernel/file.ml", line 2179, characters 12-30
Called from file "src/kernel/file.ml", line 2264, characters 4-27
Called from file "src/kernel/ast.ml", line 111, characters 2-28
Called from file "src/kernel/ast.ml", line 123, characters 53-71
Called from file "src/kernel/boot.ml", line 29, characters 6-20
Called from file "src/kernel/cmdline.ml", line 761, characters 2-9
Called from file "src/kernel/cmdline.ml", line 216, characters 4-8
Unexpected error (File "src/lib/floating_point.ml", line 204, characters 7-13: Assertion failed).
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Neon-20140301+dev-stance.
## Attachments
- [143.cpp](/uploads/64a8df8b99e6b641a9b44ed842186bc2/143.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/637failure: invalid implicit conversion from void to int2021-02-22T14:01:44ZPascal Cuoqfailure: invalid implicit conversion from void to intID0001503:
**This issue was created automatically from Mantis Issue 1503. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001503:
**This issue was created automatically from Mantis Issue 1503. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001503 | Frama-C | Kernel | public | 2013-10-18 | 2015-05-10 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
The program below appears to conform to the C99 standard:
$ cat r.c
void f()
{
0 ? 0 * 0 ? 0 : 0 : 0;
}
$ gcc -c -std=c99 -pedantic r.c
But the Frama-C front-end refuses to parse it:
$ frama-c r.c
[kernel] preprocessing with "gcc -C -E -I. r.c"
r.c:3:[kernel] failure: invalid implicit conversion from void to int
[kernel] user error: skipping file "r.c" that has errors.
[kernel] Frama-C aborted: invalid user input.
### Additional Information :
This may be the first of a non-singleton series of programs misdiagnosed with the "invalid conversion from void to int" diagnostic. The original error is in the Linux kernel. It seems better to submit only reduced programs even if the real problem is still there after the first fix, than to submit the entire code.
The entire file causing the problem is attached to this issue, but I can do reduction again after the 0 ? 0 * 0 ? 0 : 0 : 0; problem is fixed.https://git.frama-c.com/pub/frama-c/-/issues/638access to static struct fields unsupported in annotation2021-02-22T13:39:53ZJochen Burghardtaccess to static struct fields unsupported in annotationID0002116:
**This issue was created automatically from Mantis Issue 2116. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002116:
**This issue was created automatically from Mantis Issue 2116. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002116 | Frama-Clang | Plug-in > clang | public | 2015-05-07 | 2015-05-07 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Sodium-20150201 | **OS** | - | **OS Version** | xubuntu14.04 |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing 479.cpp (external front-end)
479.cpp:9:18: Unsupported Field Access to s in struct Cl
Now output intermediate result
(Despite the error message, provers are called, when command-line option "-wp" is used.)
The error disappears if (line 8 is activated and) line 9 is deactivated.
## Attachments
- [479.cpp](/uploads/abca3d8bf2819f8cdb4b49d9f829011c/479.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/639declaration of static class-type variable in function body causes crash2021-03-29T17:24:54ZJochen Burghardtdeclaration of static class-type variable in function body causes crashID0002109:
**This issue was created automatically from Mantis Issue 2109. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002109:
**This issue was created automatically from Mantis Issue 2109. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002109 | Frama-Clang | Plug-in > clang | public | 2015-04-27 | 2015-05-07 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Sodium-20150201 | **OS** | - | **OS Version** | xubuntu14.04 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing 472.cpp (external front-end)
Now output intermediate result
472.cpp:5:[fclang] failure: Unknown local variable a
[kernel] Current source was: 472.cpp:5
The full backtrace is:
Raised at file "src/kernel/log.ml", line 524, characters 30-31
Called from file "src/kernel/log.ml", line 518, characters 9-16
Re-raised at file "src/kernel/log.ml", line 521, characters 15-16
Called from file "convert.ml", line 256, characters 8-39
Called from file "convert.ml", line 441, characters 33-55
Called from file "convert.ml", line 485, characters 29-52
Called from file "convert.ml", line 894, characters 29-54
Called from file "list.ml", line 84, characters 24-34
Called from file "convert.ml", line 891, characters 4-213
Called from file "convert.ml", line 910, characters 24-55
Called from file "convert.ml", line 972, characters 31-71
Called from file "convert.ml", line 1201, characters 20-53
Called from file "convert.ml", line 1344, characters 20-46
Called from file "list.ml", line 84, characters 24-34
Called from file "convert.ml", line 1334, characters 17-40
Called from file "convert.ml", line 2508, characters 21-44
Called from file "convert.ml", line 2642, characters 21-41
Called from file "list.ml", line 84, characters 24-34
Called from file "convert.ml", line 2645, characters 4-74
Called from file "frama_Clang_register.ml", line 120, characters 13-36
Called from file "src/kernel/file.ml", line 1248, characters 8-41
Called from file "src/kernel/file.ml", line 1296, characters 23-30
Called from file "list.ml", line 84, characters 24-34
Called from file "src/kernel/file.ml", line 1293, characters 6-864
Called from file "src/kernel/file.ml", line 2287, characters 12-30
Called from file "src/kernel/file.ml", line 2372, characters 4-27
Called from file "src/kernel/ast.ml", line 111, characters 2-28
Called from file "src/kernel/ast.ml", line 123, characters 53-71
Called from file "src/kernel/boot.ml", line 29, characters 6-20
Called from file "src/kernel/cmdline.ml", line 763, characters 2-9
Called from file "src/kernel/cmdline.ml", line 216, characters 4-8
Plug-in fclang aborted: internal error.
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Sodium-20150201.
The crash disappears if:
(1) the type of "a" is changed from "A" to "int" in line 5, or
(2) the "static" is removed in line 5.
### Additional Information :
Ubuntu clang version 3.4-1ubuntu3 (tags/RELEASE_34/final) (based on LLVM 3.4)
## Attachments
- [472.cpp](/uploads/3d558269abe175d97792e6b3cef32c24/472.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/640declarations of static variable of class type in function body causes crash2021-03-29T17:24:55ZJochen Burghardtdeclarations of static variable of class type in function body causes crashID0002001:
**This issue was created automatically from Mantis Issue 2001. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002001:
**This issue was created automatically from Mantis Issue 2001. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002001 | Frama-Clang | Plug-in > clang | public | 2014-11-27 | 2015-05-07 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
Now output intermediate result
161.cpp:3:[fclang] failure: Unknown local variable s
[kernel] Current source was: 161.cpp:3
The full backtrace is:
Raised at file "src/kernel/log.ml", line 524, characters 30-31
Called from file "src/kernel/log.ml", line 518, characters 9-16
Re-raised at file "src/kernel/log.ml", line 521, characters 15-16
Called from file "src/frama-clang/convert_acsl.ml", line 317, characters 18-77
Called from file "src/frama-clang/convert_acsl.ml", line 303, characters 13-52
Called from file "src/frama-clang/convert_acsl.ml", line 172, characters 38-72
Called from file "src/frama-clang/convert_acsl.ml", line 272, characters 4-30
Called from file "src/frama-clang/convert_acsl.ml", line 172, characters 38-72
Called from file "src/frama-clang/convert_acsl.ml", line 385, characters 13-38
Called from file "src/frama-clang/convert_acsl.ml", line 363, characters 11-42
Called from file "src/frama-clang/convert_acsl.ml", line 586, characters 14-40
Called from file "list.ml", line 57, characters 20-23
Called from file "src/frama-clang/convert.ml", line 1179, characters 18-70
Called from file "src/frama-clang/convert.ml", line 1275, characters 20-46
Called from file "list.ml", line 74, characters 24-34
Called from file "src/frama-clang/convert.ml", line 1265, characters 17-40
Called from file "src/frama-clang/convert.ml", line 2151, characters 21-44
Called from file "src/frama-clang/convert.ml", line 2262, characters 21-48
Called from file "list.ml", line 74, characters 24-34
Called from file "src/frama-clang/convert.ml", line 2266, characters 4-79
Called from file "src/frama-clang/frama_Clang_register.ml", line 86, characters 13-36
Called from file "src/kernel/file.ml", line 1073, characters 10-43
Called from file "src/kernel/file.ml", line 1117, characters 23-30
Called from file "list.ml", line 74, characters 24-34
Called from file "src/kernel/file.ml", line 1114, characters 6-520
Called from file "src/kernel/file.ml", line 2179, characters 12-30
Called from file "src/kernel/file.ml", line 2264, characters 4-27
Called from file "src/kernel/ast.ml", line 111, characters 2-28
Called from file "src/kernel/ast.ml", line 123, characters 53-71
Called from file "src/kernel/boot.ml", line 29, characters 6-20
Called from file "src/kernel/cmdline.ml", line 761, characters 2-9
Called from file "src/kernel/cmdline.ml", line 216, characters 4-8
Plug-in fclang aborted: internal error.
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Neon-20140301+dev-stance.
The problem disappears if
(1) the "static" is deleted in line 5, or
(2) "cls" is changed to "int" in line 5.
Could be related to #1997, since the crash messages agree. I dind't check the full call stack, however.
## Attachments
- [173.cpp](/uploads/bc77682336214d038cb4267b460d0df8/173.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/641no label accepted in "assigns \nothing"2021-02-22T13:07:56ZJochen Burghardtno label accepted in "assigns \nothing"ID0002113:
**This issue was created automatically from Mantis Issue 2113. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002113:
**This issue was created automatically from Mantis Issue 2113. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002113 | Frama-Clang | Kernel | public | 2015-05-04 | 2015-05-04 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | no change required |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Sodium-20150201 | **OS** | - | **OS Version** | xubuntu14.04 |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c 478.c" on the attached program yields the output:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing 478.c (with preprocessing)
478.c:6:[kernel] user error: unexpected token '\nothing'
[kernel] user error: stopping on file "478.c" that has errors. Add '-kernel-msg-key pp'
for preprocessing command.
[kernel] Frama-C aborted: invalid user input.
Some modifications, using / omitting a label, using "\nothing" / a variable name have been tried, and the result is documented in the respetive line of the file. It seems that "\nothing" is accepted by the parser only immediately after "assigns", such that not even a label is accepted in between.
## Attachments
- [478.c](/uploads/589fcbdd46108b9edbc78f9b7106b8f7/478.c)https://git.frama-c.com/pub/frama-c/-/issues/642can't prove (trivial) validity of memory access of "p->a"2021-02-22T13:07:57ZJochen Burghardtcan't prove (trivial) validity of memory access of "p->a"ID0002112:
**This issue was created automatically from Mantis Issue 2112. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002112:
**This issue was created automatically from Mantis Issue 2112. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002112 | Frama-Clang | Plug-in > clang | public | 2015-05-04 | 2015-05-04 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Sodium-20150201 | **OS** | - | **OS Version** | xubuntu14.04 |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp -wp-rte 477.cpp" on the attached program leaves an obligation "typed_main_assert_rte_mem_access" unproven by Alt-Ergo. It goal formula in file "main_assert_rte_mem_access_Alt-Ergo.mlw" reads:
576 goal main_assert_rte_mem_access:
577 forall t_1,t : int farray.
578 linked(t) ->
579 valid_rw(t_1, shiftfield_F__Z1X_a(shift__Z1X(global(L_x_111), 0)), 1)
When "t" is changed to "t_1" in line 578, the formaula is proven. This looks as if an "assigns" clause is missing for some operator. However, there is no user-defined operator involved here, so the necessary "assigns" clause should be generated by Frama-C.
## Attachments
- [477.cpp](/uploads/cabf9f2eb5e5c7118db6400bf14d3275/477.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/643insufficient preconditions given to verify constructor call from global varia...2021-02-22T14:02:18ZJochen Burghardtinsufficient preconditions given to verify constructor call from global variable initializationID0002003:
**This issue was created automatically from Mantis Issue 2003. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002003:
**This issue was created automatically from Mantis Issue 2003. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002003 | Frama-Clang | Plug-in > clang | public | 2014-12-01 | 2015-05-04 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
The predonditions of the cls() constructor aren't verified for the call originating from the declaration in line 9. The goal in the .mlw file is just "forall i : int. is_sint32(i) -> (0 <> i)", i.e. the fact that i (that is x in the C++ source) has the value 2 isn't given as precondition.
In contrast, when cls() is called explicitly in main(), the actual value of x is given - the .mlw file's goal for line 13 reads: "... -> (0 <> (safe_comp_div(1, 2)))". Note that here the effect of the line-9 cls()-call is ignored in x-value computation; in fact, already the cls()-call in line 12 will crash with zero-divide.
This issues is probably closely related to #2002.
## Attachments
- [178.cpp](/uploads/5a04d189eb4a14ee24fb23392f9ea5b5/178.cpp)
- [476.cpp](/uploads/383651d9a385b7199be6833e66e52491/476.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/644different signatures for "linked" in definition and use in generated Alt-Ergo...2021-03-29T17:11:27ZJochen Burghardtdifferent signatures for "linked" in definition and use in generated Alt-Ergo mlw fileID0002111:
**This issue was created automatically from Mantis Issue 2111. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002111:
**This issue was created automatically from Mantis Issue 2111. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002111 | Frama-Clang | Plug-in > clang | public | 2015-05-04 | 2015-05-04 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Sodium-20150201 | **OS** | - | **OS Version** | xubuntu14.04 |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp -wp-rte -wp-out wp-out 475.cpp" generated the file "_Z3fooR1X_assert_rte_mem_access_Alt-Ergo.mlw" which seems to contain different signatures of "linked":
...
493 logic linked : (int,int) farray -> prop
...
766 forall t : int farray.
767 forall t_1 : (addr,int) farray.
768 forall a : addr.
769 let a_1 = shiftfield_F__Z1X_x(a) : addr in
770 linked(t) ->
...
"linked" is declared as taking an argument of type "(int,int) farray", but at its single use it is given an argument of type "int farray".
I'm not sure whether this is ok (maybe Alt-Ergo provides overloading?) or indicates an error. Alt-Ergo doesn't complain, anyway.
## Attachments
- [475.cpp](/uploads/013ed2b11f15bf97426688f7c8b9ee1b/475.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/646loop invariant referring to body-local variable causes crash, when body is en...2021-03-29T17:09:18ZJochen Burghardtloop invariant referring to body-local variable causes crash, when body is enclosed in curly braces "{...}"ID0002107:
**This issue was created automatically from Mantis Issue 2107. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002107:
**This issue was created automatically from Mantis Issue 2107. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002107 | Frama-Clang | Plug-in > clang | public | 2015-04-27 | 2015-04-27 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | Sodium-20150201 | **OS** | - | **OS Version** | xubuntu14.04 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing 470.cpp (external front-end)
Now output intermediate result
470.cpp:3:[fclang] failure: Unknown local variable s
[kernel] Current source was: 470.cpp:3
The full backtrace is:
Raised at file "src/kernel/log.ml", line 524, characters 30-31
Called from file "src/kernel/log.ml", line 518, characters 9-16
Re-raised at file "src/kernel/log.ml", line 521, characters 15-16
Called from file "convert_acsl.ml", line 329, characters 18-77
Called from file "convert_acsl.ml", line 315, characters 13-52
Called from file "convert_acsl.ml", line 184, characters 38-72
Called from file "convert_acsl.ml", line 284, characters 4-30
Called from file "convert_acsl.ml", line 184, characters 38-72
Called from file "convert_acsl.ml", line 397, characters 13-38
Called from file "convert_acsl.ml", line 375, characters 11-42
Called from file "convert_acsl.ml", line 603, characters 14-40
Called from file "list.ml", line 55, characters 20-23
Called from file "convert.ml", line 1248, characters 18-70
Called from file "convert.ml", line 1344, characters 20-46
Called from file "list.ml", line 84, characters 24-34
Called from file "convert.ml", line 1334, characters 17-40
Called from file "convert.ml", line 2508, characters 21-44
Called from file "convert.ml", line 2642, characters 21-41
Called from file "list.ml", line 84, characters 24-34
Called from file "convert.ml", line 2645, characters 4-74
Called from file "frama_Clang_register.ml", line 120, characters 13-36
Called from file "src/kernel/file.ml", line 1248, characters 8-41
Called from file "src/kernel/file.ml", line 1296, characters 23-30
Called from file "list.ml", line 84, characters 24-34
Called from file "src/kernel/file.ml", line 1293, characters 6-864
Called from file "src/kernel/file.ml", line 2287, characters 12-30
Called from file "src/kernel/file.ml", line 2372, characters 4-27
Called from file "src/kernel/ast.ml", line 111, characters 2-28
Called from file "src/kernel/ast.ml", line 123, characters 53-71
Called from file "src/kernel/boot.ml", line 29, characters 6-20
Called from file "src/kernel/cmdline.ml", line 763, characters 2-9
Called from file "src/kernel/cmdline.ml", line 216, characters 4-8
Plug-in fclang aborted: internal error.
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Sodium-20150201.
The crash doesn't happen when
(1) the braces "{" and "}" in line 5 and 7 are deleted,
(2) "s" is replaced by "0" in the invariant in line 3,
(3) the declaration of "s" in line 6 is deleted,
(4) the file is renamed to "470.c".
In each of these cases, an appropriate error message is printed.
### Additional Information :
My output of "clang --version" is:
Ubuntu clang version 3.4-1ubuntu3 (tags/RELEASE_34/final) (based on LLVM 3.4)
Target: x86_64-pc-linux-gnu
Thread model: posix
## Attachments
- [470.cpp](/uploads/25f4766330a52880d319ebc21f807ac9/470.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/647variable declared in loop initializer is unknown in loop body "assert"2021-02-22T13:54:40ZJochen Burghardtvariable declared in loop initializer is unknown in loop body "assert"ID0002108:
**This issue was created automatically from Mantis Issue 2108. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002108:
**This issue was created automatically from Mantis Issue 2108. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002108 | Frama-Clang | Plug-in > clang | public | 2015-04-27 | 2015-04-27 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Sodium-20150201 | **OS** | - | **OS Version** | xubuntu14.04 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing 471.cpp (external front-end)
471.cpp:5:17: unknown identifier 'i'
Now output intermediate result
The error message disappears if
(1) the "assert" in line 5 is deleted (i.e. "i" is known in the "loop assigns" clause in line 3), or
(2) the declaration of "i" is moved before line 3.
### Additional Information :
Ubuntu clang version 3.4-1ubuntu3 (tags/RELEASE_34/final) (based on LLVM 3.4)
## Attachments
- [471.cpp](/uploads/e8841adebbb2c9c95ac3128188b487e6/471.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/648use of body-declared variable in loop annotation causes crash2021-02-22T14:01:53ZJochen Burghardtuse of body-declared variable in loop annotation causes crashID0001997:
**This issue was created automatically from Mantis Issue 1997. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001997:
**This issue was created automatically from Mantis Issue 1997. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001997 | Frama-Clang | Plug-in > clang | public | 2014-11-27 | 2015-04-27 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
Now output intermediate result
161.cpp:3:[fclang] failure: Unknown local variable s
[kernel] Current source was: 161.cpp:3
The full backtrace is:
Raised at file "src/kernel/log.ml", line 524, characters 30-31
Called from file "src/kernel/log.ml", line 518, characters 9-16
Re-raised at file "src/kernel/log.ml", line 521, characters 15-16
Called from file "src/frama-clang/convert_acsl.ml", line 317, characters 18-77
Called from file "src/frama-clang/convert_acsl.ml", line 303, characters 13-52
Called from file "src/frama-clang/convert_acsl.ml", line 172, characters 38-72
Called from file "src/frama-clang/convert_acsl.ml", line 272, characters 4-30
Called from file "src/frama-clang/convert_acsl.ml", line 172, characters 38-72
Called from file "src/frama-clang/convert_acsl.ml", line 385, characters 13-38
Called from file "src/frama-clang/convert_acsl.ml", line 363, characters 11-42
Called from file "src/frama-clang/convert_acsl.ml", line 586, characters 14-40
Called from file "list.ml", line 57, characters 20-23
Called from file "src/frama-clang/convert.ml", line 1179, characters 18-70
Called from file "src/frama-clang/convert.ml", line 1275, characters 20-46
Called from file "list.ml", line 74, characters 24-34
Called from file "src/frama-clang/convert.ml", line 1265, characters 17-40
Called from file "src/frama-clang/convert.ml", line 2151, characters 21-44
Called from file "src/frama-clang/convert.ml", line 2262, characters 21-48
Called from file "list.ml", line 74, characters 24-34
Called from file "src/frama-clang/convert.ml", line 2266, characters 4-79
Called from file "src/frama-clang/frama_Clang_register.ml", line 86, characters 13-36
Called from file "src/kernel/file.ml", line 1073, characters 10-43
Called from file "src/kernel/file.ml", line 1117, characters 23-30
Called from file "list.ml", line 74, characters 24-34
Called from file "src/kernel/file.ml", line 1114, characters 6-520
Called from file "src/kernel/file.ml", line 2179, characters 12-30
Called from file "src/kernel/file.ml", line 2264, characters 4-27
Called from file "src/kernel/ast.ml", line 111, characters 2-28
Called from file "src/kernel/ast.ml", line 123, characters 53-71
Called from file "src/kernel/boot.ml", line 29, characters 6-20
Called from file "src/kernel/cmdline.ml", line 761, characters 2-9
Called from file "src/kernel/cmdline.ml", line 216, characters 4-8
Plug-in fclang aborted: internal error.
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Neon-20140301+dev-stance.
The problem remains if line 3 is changed to "//@ loop assigns s;", and if "s" is declared "static int" (in which case a reference to "s" in a loop annotation makes sense).
## Attachments
- [161.cpp](/uploads/5bfc197761d406d5ad0e3f804e293cad/161.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/649declaration of local variable of class type results in unprovable assigns clause2021-02-22T13:08:04ZJochen Burghardtdeclaration of local variable of class type results in unprovable assigns clauseID0002106:
**This issue was created automatically from Mantis Issue 2106. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002106:
**This issue was created automatically from Mantis Issue 2106. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002106 | Frama-Clang | Plug-in > clang | public | 2015-04-27 | 2015-04-27 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Sodium-20150201 | **OS** | - | **OS Version** | xubuntu14.04 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
The assigns clause in line 4 of the attached program results in two Alt-Ergo obligations (such as "goal _Z3foo_assign_normal: forall t : int farray. not linked(t)" in obligation file "_Z3foo_assign_normal_Alt-Ergo.mlw"), none of which is provable.
However, from a C++ programmer's point of view, the clause should be valid.
Probably, some Frama-Cxx-internal variables are assigned by the implicit constructor "A()", and hence by "foo()", but there is no clue how to refer to them. Maybe they should be added automatically by Frama-Cxx to the set of assigned locations.
## Attachments
- [469.cpp](/uploads/a03e4e3a40b48a76922e10de413446fb/469.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/650template parameter type can't used in typedef2021-02-22T13:08:05ZJochen Burghardttemplate parameter type can't used in typedefID0001972:
**This issue was created automatically from Mantis Issue 1972. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001972:
**This issue was created automatically from Mantis Issue 1972. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001972 | Frama-Clang | Plug-in > clang | public | 2014-11-17 | 2015-04-27 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
Now output intermediate result
136.cpp:6:[kernel] failure: Cannot find type _ZN6traitsIiE2stE2tp (kind:type)
The problem disappears if the surrounding "struct st {" and "};" is deleted in line 3, and "st::" is deleted in line 6.
BTW: A call of "c++filt -n _ZN6traitsIiE2stE2tp" yields "traits<int>::st(tp)", while I would have expected "traits<int>::st::tp".
(Importance: this code is used via #include <vector>.)
Other issues that involve both typedef and templates were/are #1705, #1580, #1531. One of them might be related to the problem here.
## Attachments
- [136.cpp](/uploads/7681db01d5299465de8a20e5ebe39490/136.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/651postcondition of destructor unconsidered2021-02-22T14:01:54ZJochen Burghardtpostcondition of destructor unconsideredID0002103:
**This issue was created automatically from Mantis Issue 2103. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002103:
**This issue was created automatically from Mantis Issue 2103. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002103 | Frama-Clang | Plug-in > clang | public | 2015-04-09 | 2015-04-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | duplicate |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Sodium-20150201 | **OS** | xubuntu14.04 | **OS Version** | - |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | - |
### Description :
The "ensures" in line 9 can't be proven. The goal given to Alt-Ergo reads:
759 goal _Z3foo_post:
760 forall i : int.
761 forall t : int farray.
762 linked(t) ->
763 is_sint32(i) ->
764 (3 = i)
which apparently doesn't reflect the fact that before "foo" exists, the destructor "~A" is called for variable "aa", and assigns 3 to "x".
There are two more unproven goals, viz. in file "_Z3foo_assign_exit_Alt-Ergo.mlw":
493 logic linked : (int,int) farray -> prop
...
554 (* ---------------------------------------------------------- *)
555 (* --- Assigns (file 466.cpp, line 9) in '_Z3foo' --- *)
556 (* ---------------------------------------------------------- *)
557
558 goal _Z3foo_assign_exit: forall t : int farray. not linked(t)
where the prodicate "linked" doesn't appear anywhere outside the shown lines, and hence the goal is unprovable, and in file "_Z3foo_assign_normal_Alt-Ergo.mlw", which is literally identical to the above, except for the goal's name.
## Attachments
- [466.cpp](/uploads/564031d9eacadce7745391f86f6b4e12/466.cpp)https://git.frama-c.com/pub/frama-c/-/issues/652syntax error in contract causes rest to be tacitly ignored2021-02-22T14:01:54ZJochen Burghardtsyntax error in contract causes rest to be tacitly ignoredID0001821:
**This issue was created automatically from Mantis Issue 1821. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001821:
**This issue was created automatically from Mantis Issue 1821. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001821 | Frama-Clang | Plug-in > clang | public | 2014-06-27 | 2015-04-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | xubuntu-cfe13.10 (64 bit) | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c-gui -wp -wp-rte Fault2.cpp" on the attached program causes a message "Fault2.cpp:4:2: expecting function spec" on stderr (that's ok), but doesn't prevent the gui to appear (that's at least different to the behavior on a renamed version "Fault2.c").
More important, no error or warning message is visible in the gui (I checked the tabs "Information", "Messages", "Console", "Properties", "WP Goals"), and the contract rest after the error is tacitly ignored.
## Attachments
- [Fault2.cpp](/uploads/2ea7598b48027d199c2e89b9df46f36c/Fault2.cpp)https://git.frama-c.com/pub/frama-c/-/issues/653using "delete" causes warning for "free"2021-02-22T14:01:55ZJochen Burghardtusing "delete" causes warning for "free"ID0001946:
**This issue was created automatically from Mantis Issue 1946. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001946:
**This issue was created automatically from Mantis Issue 1946. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001946 | Frama-Clang | Plug-in > clang | public | 2014-10-30 | 2015-04-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | xubuntu-cfe13.10 | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
Now output intermediate result
072.cpp:3:[kernel] warning: Calling undeclared function free. Old style K&R code?
[kernel] warning: Assuming declared function free can't throw any exception
Similar to issue #1596, but now for "delete"/"free" rather than "new"/"malloc", cf. the note #4424 there.
## Attachments
- [072.cpp](/uploads/076e092452147592d1b383b325ade662/072.cpp)https://git.frama-c.com/pub/frama-c/-/issues/654"__is_trivial" causes abort2021-02-22T13:08:13ZJochen Burghardt"__is_trivial" causes abortID0001967:
**This issue was created automatically from Mantis Issue 1967. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001967:
**This issue was created automatically from Mantis Issue 1967. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001967 | Frama-Clang | Plug-in > clang | public | 2014-11-13 | 2015-04-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **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 :
output:
Unsupported expressions:UnaryTypeTraitExpr 0x253e888 <134.cpp:2:10, col:26> '_Bool'
Aborting
[kernel] user error: Failed to parse C++ file. See Clang messages for more information
(Importance: this code is used via #include <vector>.)
## Attachments
- [134.cpp](/uploads/fc0e0514a33ec9a94e33e11fd592e5b0/134.cpp)https://git.frama-c.com/pub/frama-c/-/issues/655double index causes error2021-02-22T13:26:10ZJochen Burghardtdouble index causes errorID0001987:
**This issue was created automatically from Mantis Issue 1987. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001987:
**This issue was created automatically from Mantis Issue 1987. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001987 | Frama-Clang | Plug-in > clang | public | 2014-11-24 | 2015-04-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
Now output intermediate result
150.cpp:5:[kernel] user error: Cast over a non-scalar type int *[4]
When renamed to "150.c", the file is handled pretty well by Frama-C.
## Attachments
- [150.cpp](/uploads/aebbefedb6dddb821eed8858253fd454/150.cpp)https://git.frama-c.com/pub/frama-c/-/issues/656extra "//" comment within "//@" annotation causes abort2021-02-22T13:08:15ZJochen Burghardtextra "//" comment within "//@" annotation causes abortID0002013:
**This issue was created automatically from Mantis Issue 2013. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002013:
**This issue was created automatically from Mantis Issue 2013. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002013 | Frama-Clang | Plug-in > clang | public | 2014-12-04 | 2015-04-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
framaCIRGen: src/frama-clang/ACSLToken.h:563: Acsl::DLexer::AbstractToken Acsl::DLexer::Token::getFullToken() const: Assertion `_type != 0' failed.
Aborted (core dumped)
[kernel] user error: Failed to parse C++ file. See Clang messages for more information
The problem disappears if "// comment" is deleted in line 2, or if the file is renamed to "190.c".
## Attachments
- [190.cpp](/uploads/6e7ae2cf72d87f620e534fcf2c6a03dd/190.cpp)https://git.frama-c.com/pub/frama-c/-/issues/657logic function with typedef'd result type causes crash2021-02-22T13:08:16ZJochen Burghardtlogic function with typedef'd result type causes crashID0002056:
**This issue was created automatically from Mantis Issue 2056. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002056:
**This issue was created automatically from Mantis Issue 2056. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002056 | Frama-Clang | Plug-in > clang | public | 2015-01-22 | 2015-04-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | Neon-20140301+dev-STANCE-Jan2015 | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing 437.cpp (external front-end)
Now output intermediate result
437.cpp:6:[fclang] failure: predicate definition with a term as body
[kernel] Current source was: 437.cpp:6
The full backtrace is:
Raised at file "src/kernel/log.ml", line 524, characters 30-31
Called from file "src/kernel/log.ml", line 518, characters 9-16
Re-raised at file "src/kernel/log.ml", line 521, characters 15-16
Called from file "src/frama-clang/convert_acsl.ml", line 622, characters 12-76
Called from file "src/frama-clang/convert.ml", line 2233, characters 18-54
Called from file "list.ml", line 74, characters 24-34
Called from file "src/frama-clang/convert.ml", line 2241, characters 19-78
Called from file "src/frama-clang/convert.ml", line 2554, characters 21-48
Called from file "list.ml", line 74, characters 24-34
Called from file "src/frama-clang/convert.ml", line 2558, characters 4-79
Called from file "src/frama-clang/frama_Clang_register.ml", line 86, characters 13-36
Called from file "src/kernel/file.ml", line 1248, characters 8-41
Called from file "src/kernel/file.ml", line 1296, characters 23-30
Called from file "list.ml", line 74, characters 24-34
Called from file "src/kernel/file.ml", line 1293, characters 6-864
Called from file "src/kernel/file.ml", line 2287, characters 12-30
Called from file "src/kernel/file.ml", line 2372, characters 4-27
Called from file "src/kernel/ast.ml", line 111, characters 2-28
Called from file "src/kernel/ast.ml", line 123, characters 53-71
Called from file "src/kernel/boot.ml", line 29, characters 6-20
Called from file "src/kernel/cmdline.ml", line 761, characters 2-9
Called from file "src/kernel/cmdline.ml", line 216, characters 4-8
Plug-in fclang aborted: internal error.
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Neon-20140301+dev-STANCE.
The problem disappears if the return type is changed to "int" in line 6.
Line 7 just demonstrates that the same expression is accepted in C++ code.
## Attachments
- [437.cpp](/uploads/b80e0c84f1ccd4254f37a850575ad463/437.cpp)https://git.frama-c.com/pub/frama-c/-/issues/658method can't be used in member initializer before its declaration2021-02-22T13:08:18ZJochen Burghardtmethod can't be used in member initializer before its declarationID0002064:
**This issue was created automatically from Mantis Issue 2064. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002064:
**This issue was created automatically from Mantis Issue 2064. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002064 | Frama-Clang | Plug-in > clang | public | 2015-01-26 | 2015-04-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Neon-20140301+dev-STANCE-Jan2015 | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing 443.cpp (external front-end)
Now output intermediate result
443.cpp:7:[kernel] warning: Calling undeclared function _ZNK5PointE1x. Old style K&R code?
The error message is not observed for any of the variants in lines 4 to 6 (currently commented-out). It also disappears if the definition of x() is moved before line 4.
## Attachments
- [443.cpp](/uploads/a5451bc00dc4425f63032528113647d7/443.cpp)https://git.frama-c.com/pub/frama-c/-/issues/659class expression causes abort in presence of user-defined destructor2021-03-29T17:06:09ZJochen Burghardtclass expression causes abort in presence of user-defined destructorID0002004:
**This issue was created automatically from Mantis Issue 2004. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002004:
**This issue was created automatically from Mantis Issue 2004. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002004 | Frama-Clang | Plug-in > clang | public | 2014-12-01 | 2015-04-15 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
Unsupported expressions:ExprWithCleanups 0x17e7dc0 <179.cpp:8:6, col:17> '_Bool'
`-CXXMemberCallExpr 0x17e7d98 <col:6, col:17> '_Bool'
`-MemberExpr 0x17e7d68 <col:6, col:12> '<bound member function type>' .test 0x1799820
`-CXXBindTemporaryExpr 0x17e7d48 <col:6, col:10> 'struct cls' (CXXTemporary 0x17e7d40)
`-CXXTemporaryObjectExpr 0x17e7d00 <col:6, col:10> 'struct cls' 'void (void)' zeroing
Aborting
[kernel] user error: Failed to parse C++ file. See Clang messages for more information
The problem disappears if the destructor definition in line 3 is deleted.
## Attachments
- [179.cpp](/uploads/4356f9770e055afebc91022a33e22f7c/179.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/660CLASSNAME::PREDICATENAME not recognized as predicate (or even as term)2021-02-22T13:39:56ZJochen BurghardtCLASSNAME::PREDICATENAME not recognized as predicate (or even as term)ID0001944:
**This issue was created automatically from Mantis Issue 1944. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001944:
**This issue was created automatically from Mantis Issue 1944. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001944 | Frama-Clang | Plug-in > clang | public | 2014-10-30 | 2015-04-15 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | xubuntu-cfe13.10 | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
113.cpp:13:28: expecting a term or predicate
113.cpp:13:28: the term is not a predicate
Now output intermediate result
Note that the 2nd message claims a term while the 1st denies a term; no message should appear.
If the prefix "Queue::" is omitted in line 10 before "IsValid", no message is issued, while "unknown identifier 'IsValid'" should be reported.
If the definition of Queue() and its contract are moved inside the class, no message is issued, which is ok.
Probably related to issue #1606.
## Attachments
- [113.cpp](/uploads/4926913e5616dc5c301dabd76eac5c74/113.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/664use of "CLASSNAME::VARIABLENAME" in assigns clase causes abort2021-02-22T13:08:27ZJochen Burghardtuse of "CLASSNAME::VARIABLENAME" in assigns clase causes abortID0002074:
**This issue was created automatically from Mantis Issue 2074. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002074:
**This issue was created automatically from Mantis Issue 2074. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002074 | Frama-Clang | Plug-in > clang | public | 2015-02-05 | 2015-04-09 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Neon-20140301+dev-STANCE-Jan2015 | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing 455.cpp (external front-end)
framaCIRGen: SemaLookup.cpp:1622: bool clang::Sema::LookupQualifiedName(clang::LookupResult &, clang::DeclContext *, bool): Assertion `(!isa<TagDecl>(LookupCtx) || LookupCtx->isDependentContext() || cast<TagDecl>(LookupCtx)->isCompleteDefinition() || cast<TagDecl>(LookupCtx)->isBeingDefined()) && "Declaration context must already be complete!"' failed.
Aborted (core dumped)
[kernel] user error: Failed to parse C++ file. See Clang messages for more information
Cf. #1944 for a similar problem in an "ensures" clause.
If the prefix "Employee::" is deleted in the assigns clause in line 11, a warning is issued instead:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing 455.cpp (external front-end)
Now output intermediate result
455.cpp:12:[kernel] user error: Cannot find field dept
[kernel] user error: stopping on file "455.cpp" that has errors.
As a consequence of both behaviors, it is impossible to write an "assigns" clause for a subclass method that refers to a member of a superclass.
## Attachments
- [455.cpp](/uploads/2b4202f07be66f6e527f8c274d7e5300/455.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/666indexing of string literal apparently causes memory leak in framaCIRGen2021-02-22T13:40:05ZJochen Burghardtindexing of string literal apparently causes memory leak in framaCIRGenID0001988:
**This issue was created automatically from Mantis Issue 1988. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001988:
**This issue was created automatically from Mantis Issue 1988. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001988 | Frama-Clang | Plug-in > clang | public | 2014-11-24 | 2015-04-02 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
When running "frama-c 151.cpp" on the attached program, about 1 minute of silence is observed on the terminal output, followed by:
Killed
[kernel] user error: Failed to parse C++ file. See Clang messages for more information
Running "top -d 1" produces the figures shown in file "151.typescript": framaCIRGen acquires about 90MB memory each second until it has 1.8GB after 18 seconds; then the memory remains constant for another 18 seconds; then the process appears to be killed by the Linux kernel due to memory exhaustion.
## Attachments
- [151.cpp](/uploads/22b5baf2a7db1b3084d4da78b008cbaf/151.cpp)
- [151.typescript](/uploads/b4a76f523493de4fe8ab69804480ce6b/151.typescript)
- [156.cpp](/uploads/fb17a0983991ed74ce7fe3d23ce44028/156.cpp)
- [156.typescript](/uploads/1dc0c1b0d4a1e83a9be18b27027d3979/156.typescript)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/667"=" in contract causes abort rather than syntax error message2021-02-22T13:08:31ZJochen Burghardt"=" in contract causes abort rather than syntax error messageID0001964:
**This issue was created automatically from Mantis Issue 1964. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001964:
**This issue was created automatically from Mantis Issue 1964. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001964 | Frama-Clang | Plug-in > clang | public | 2014-11-13 | 2015-04-02 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **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 :
output:
framaCIRGen: src/frama-clang/ACSLTermOrPredicate.cpp:7053: Parser::ReadResult Acsl::TermOrPredicate::readToken(Parser::State &, Parser::Arguments &): Assertion `false' failed.
Aborted (core dumped)
[kernel] user error: Failed to parse C++ file. See Clang messages for more information
## Attachments
- [130.cpp](/uploads/e09ffb81bdc68a67486b3af38d8eddc9/130.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/668path to non-existing directory given to framaCIRGen2021-02-22T13:26:29ZJochen Burghardtpath to non-existing directory given to framaCIRGenID0001954:
**This issue was created automatically from Mantis Issue 1954. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001954:
**This issue was created automatically from Mantis Issue 1954. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001954 | Frama-Clang | Plug-in > clang | public | 2014-11-06 | 2015-04-02 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe131.1 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
When investigating issue #1953, in order to find out the appropriate command-line arguments for framaCIRGen, I called "frama-c -cxx-clang-command=echo 000.cpp" and got the output
-target i386-unknown-linux-gnu -I /usr/local/share/libc++ -I /usr/local/share/frama-c/libc -I /usr/local/share/frama-c --stop-annot-error 000a.cpp -o /tmp/clang_astb9af51ast
(before frama-c crashed due to lack of stdin input).
However, the first include path, "/usr/local/share/libc++", points to a non-existing directory. This need not be a problem, but it could be. In particular, some include files could be missing that are expected to reside in /usr/local/share/libc++.
### Additional Information :
No need to attach the trivial file 000.cpp here; any file will do.Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/670value analysis assumes dynamic_cast between unrelated classes to succeed, rat...2021-02-22T13:08:36ZJochen Burghardtvalue analysis assumes dynamic_cast between unrelated classes to succeed, rather than to yield NULLID0002076:
**This issue was created automatically from Mantis Issue 2076. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002076:
**This issue was created automatically from Mantis Issue 2076. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002076 | Frama-Clang | Plug-in > clang | public | 2015-02-09 | 2015-04-01 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Neon-20140301+dev-STANCE-Jan2015 | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -val 461.cpp" on the attached program yields the output (excerpt):
461.cpp:10:[value] Assertion got status valid.
However, running "clang++ 461.cpp && ./a.out" reveals that the assertion in line 12 (identical to that in line 11) is in fact invalid:
a.out: 461.cpp:11: int main(): Assertion `bp!=0' failed.
Compiling "g++ 461.cpp" even yields a compile-time warning:
461.cpp: In function ‘int main()’:
461.cpp:9:37: warning: dynamic_cast of ‘A aaa’ to ‘struct B*’ can never succeed [enabled by default]
B* const bp = dynamic_cast<B*>(&aaa);
^
## Attachments
- [461.cpp](/uploads/20b05a3ffead132fae7718ee75d4dece/461.cpp)
- [461_bis.cpp](/uploads/07b4979e4c6b1bdf3d7b1eb9d20722fe/461_bis.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/673virtual base class causes error2021-02-22T13:08:41ZJochen Burghardtvirtual base class causes errorID0002075:
**This issue was created automatically from Mantis Issue 2075. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002075:
**This issue was created automatically from Mantis Issue 2075. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002075 | Frama-Clang | Plug-in > clang | public | 2015-02-05 | 2015-03-30 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | fvedrine | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Neon-20140301+dev-STANCE-Jan2015 | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing 454.cpp (external front-end)
Now output intermediate result
454.cpp:7:[kernel] user error: Cannot find field _frama_c__Z1A
[kernel] user error: stopping on file "454.cpp" that has errors.
The error message disappears if the contructor definition in line 7 is deleted, or if the "virtual" is deleted in line 4.
## Attachments
- [454.cpp](/uploads/4a7365082cdfd5d01d0cea781a1c31b2/454.cpp)Franck VedrineFranck Vedrinehttps://git.frama-c.com/pub/frama-c/-/issues/674method call in initializer of global constant causes segmentation fault2021-02-22T13:08:42ZJochen Burghardtmethod call in initializer of global constant causes segmentation faultID0002005:
**This issue was created automatically from Mantis Issue 2005. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002005:
**This issue was created automatically from Mantis Issue 2005. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002005 | Frama-Clang | Plug-in > clang | public | 2014-12-01 | 2015-03-26 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | fvedrine | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
Segmentation fault (core dumped)
[kernel] user error: Failed to parse C++ file. See Clang messages for more information
If the "const" is removed from line 8, the output changes to:
Now output intermediate result
182.cpp:8:[kernel] warning: Call to _ZN3clsE1a in constant. Ignoring this call and returning 0.
If line 8 is embedded in the body of main(), the problem disappears (with and without "const").
## Attachments
- [182.cpp](/uploads/488e6187dc8b8a423989ecada7a407e0/182.cpp)Franck VedrineFranck Vedrinehttps://git.frama-c.com/pub/frama-c/-/issues/677for a pointer int *p, the expression "(p+1)-p" evaluates to 4 in ACSL rather ...2021-02-22T13:54:40ZJochen Burghardtfor a pointer int *p, the expression "(p+1)-p" evaluates to 4 in ACSL rather than to 1 (as in C)ID0002079:
**This issue was created automatically from Mantis Issue 2079. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002079:
**This issue was created automatically from Mantis Issue 2079. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002079 | Frama-Clang | Plug-in > wp | public | 2015-02-19 | 2015-03-20 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | urgent | **Severity** | major | **Reproducibility** | always |
| **Platform** | Neon-20140301+dev-STANCE-Jan2015 | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp 463.c" on the attached program, the assertion "(p+1)-p == 4" in line 7 is proven by qed (I didn't succeed finding command-line options to disable qed and let Alt-Ergo decide.) However, compiling and running the program shows that the literally identical assertion in line 8 fails; which is in accordance with the C Standard (e.g. item 9. in sect. 6.5.6 of the C99 Standard 2007 http://www.open-std.org/jtc1/sc22/wg14/www/docs/n1256.pdf , p.95-->83).
When both assertions are changed to "(p+1)-p == 1", Frama-C verification fails (with the goal "false" given to Alt-Ergo; I didn't succeed obtaining an unsimplified version), while compiling and running succeeds.
### Tags :
wp
## Attachments
- [463.c](/uploads/f0f3ed2f5f5ed67591630665e928345d/463.c)https://git.frama-c.com/pub/frama-c/-/issues/682CVC4 results are not displayed in the GUI2021-02-22T13:08:57ZJens GerlachCVC4 results are not displayed in the GUIID0001688:
**This issue was created automatically from Mantis Issue 1688. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001688:
**This issue was created automatically from Mantis Issue 1688. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001688 | Frama-C | Plug-in > wp | public | 2014-03-12 | 2015-03-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | high | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C Sodium |
### Description :
When using the CVC4 prover the verification results are not automatically displayed in the GUI.
### Additional Information :
The problem was observed with Frama-C Neon.
## Attachments
- ![frama-c-gui](/uploads/947420837a3939ef2f99b9141387b822/frama-c-gui.gif)
- [gui01.c](/uploads/fbec4c1ec851421b393af44be48d6dc6/gui01.c)https://git.frama-c.com/pub/frama-c/-/issues/683predicate-def and logic-predicate-def2021-02-22T14:01:57ZDavid Cokpredicate-def and logic-predicate-defID0001788:
**This issue was created automatically from Mantis Issue 1788. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001788:
**This issue was created automatically from Mantis Issue 1788. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001788 | Frama-C | Documentation > ACSL | public | 2014-05-28 | 2015-03-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | DavidCok | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | Frama-C Sodium |
### Description :
The ACSL grammar contains symbols for both predicate-def and logic-predicate-def.
The latter is defined but not used. Consistency would say they both should be 'logic-predicate-def'.https://git.frama-c.com/pub/frama-c/-/issues/696Value abort because of Zero-sized location2021-02-22T14:01:58Zmantis-gitlab-migrationValue abort because of Zero-sized locationID0001907:
**This issue was created automatically from Mantis Issue 1907. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001907:
**This issue was created automatically from Mantis Issue 1907. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001907 | Frama-C | Plug-in > Eva | public | 2014-08-08 | 2015-03-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Anne | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Sodium |
### Description :
Value usually support structure types holding an array field with an undefined size, but in the attached case, it aborts with:
user error: Zero-sized location S_buf[0].chunk (type 'int []').
Probably empty struct.
Aborting
* Notice that the size of `buf` is defined since it is only a pointer.
* If `buf` is defined instead of just declared `extern`, the problem disappear.
### Steps To Reproduce :
$ frama-c -val struct.c
## Attachments
- [struct.c](/uploads/11636cf3c288cbc978ed3b2746cda980/struct.c)https://git.frama-c.com/pub/frama-c/-/issues/699Segmentation fault when launching frama-c-gui with OCaml 4.02.02021-02-22T13:09:21Zmantis-gitlab-migrationSegmentation fault when launching frama-c-gui with OCaml 4.02.0ID0001919:
**This issue was created automatically from Mantis Issue 1919. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001919:
**This issue was created automatically from Mantis Issue 1919. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001919 | Frama-C | Graphical User Interface | public | 2014-09-03 | 2015-03-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dhekir | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | Frama-C Sodium | **Fixed in Version** | Frama-C Sodium |
### Description :
I'm using OPAM 1.1.1 with OCaml 4.02.0.
I installed Frama-C using OPAM, along with its dependencies, and then tried running frama-c-gui. It segfaults. Using gdb I get the following backtrace:
Program received signal SIGSEGV, Segmentation fault.
0x0000000000beb6e6 in GValue_val ()
(gdb) back
#0 0x0000000000beb6e6 in GValue_val ()
#1 0x0000000000bec4b4 in ml_g_signal_emit_by_name ()
#2 0x0000000000a91016 in camlGtkSignal__fun_1460 ()
#3 0x0000000000aaa16c in camlGtkData__set_bounds_1503 ()
#4 0x0000000000790d0e in camlWp__Gtk_form__spinner_1053 () at src/gui/gtk_form.ml:100
#5 0x00007fffedf7bda8 in camlWp__GuiPanel__wp_panel_2423 () at src/wp/GuiPanel.ml:259
#6 0x00000000007603c8 in camlSecurity_slicing__Design__fun_13880 () at src/gui/design.ml:810
#7 0x0000000000ba2fb1 in camlList__iter_1061 () at list.ml:73
#8 0x0000000000763592 in camlSecurity_slicing__Design__fun_13774 () at src/gui/design.ml:808
#9 0x0000000000764083 in camlSecurity_slicing__Design__fun_14157 () at src/gui/design.ml:1136
#10 0x0000000000bd940b in camlCamlinternalOO__iter_f_1269 () at camlinternalOO.ml:369
#11 0x0000000000bd947d in camlCamlinternalOO__run_initializers_opt_1277 () at camlinternalOO.ml:379
#12 0x000000000076167a in camlSecurity_slicing__Design__fun_14455 () at src/gui/design.ml:1264
#13 0x0000000000a3b8f9 in camlExtlib__try_finally_1226 () at src/lib/extlib.ml:277
#14 0x000000000079403e in camlSecurity_slicing__Gtk_helper__fun_5386 () at src/gui/gtk_helper.ml:735
#15 0x00000000007940a5 in camlSecurity_slicing__Gtk_helper__fun_5383 () at src/gui/gtk_helper.ml:727
#16 0x0000000000765ee4 in camlSecurity_slicing__Design__fun_14460 () at src/gui/design.ml:1283
#17 0x0000000000c22b76 in caml_start_program ()
#18 0x00000037040492a6 in g_main_context_dispatch () from /lib64/libglib-2.0.so.0
#19 0x0000003704049628 in g_main_context_iterate.isra.24 () from /lib64/libglib-2.0.so.0
#20 0x00000037040496dc in g_main_context_iteration () from /lib64/libglib-2.0.so.0
#21 0x0000000000be9eda in ml_g_main_iteration ()
#22 0x0000000000ab06a5 in camlGtkMain__default_main_1163 ()
#23 0x0000000000a28d71 in camlCmdline__catch_toplevel_run_1181 () at src/kernel/cmdline.ml:214
#24 0x00000000006bdd85 in camlBoot__entry () at src/kernel/boot.ml:66
#25 0x00000000006b3f49 in caml_program ()
#26 0x0000000000c22b76 in caml_start_program ()
#27 0x0000000000000000 in ?? ()
It could be related to lablgtk. All dependencies were downloaded using OPAM (including lablgtk 2.16.0) and installed without issues.
First I tried using directly the version from OPAM, but due to the segfault error I then tried downloading the sources and compiling them myself.
When running configure, everything is ok except for "OcamlGraph 1.8.5 > 1.8.4 found: should be compatible, but no warranty. Use it at your own risk!", but I used the patch available in https://bts.frama-c.com/view.php?id=1764, and then I could run make and make install without issues. But once again, when running frama-c-gui it segfaults.
To sum up, either using OPAM or downloading and compiling the sources myself, I get the same result (unsurprisingly).
However, when switching to OCaml 4.01.0 and running "opam install frama-c", the GUI works normally.
Has the Frama-C GUI been confirmed to work with OCaml 4.02.0 already? Should I try manually compiling its dependencies to try and identify the cause of the error?https://git.frama-c.com/pub/frama-c/-/issues/701WP-Plugin crashes due to an internal error2021-02-22T13:09:24Zmantis-gitlab-migrationWP-Plugin crashes due to an internal errorID0001922:
**This issue was created automatically from Mantis Issue 1922. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001922:
**This issue was created automatically from Mantis Issue 1922. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001922 | Frama-C | Plug-in > wp | public | 2014-09-12 | 2015-03-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | lapawczykt | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | urgent | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | xubuntu | **OS Version** | 14.04 |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | Frama-C Sodium |
### Description :
When the attached file is called with the command line, that reads as follows:
frama-c.byte -pp-annot -no-unicode -wp -wp-no-bits -wp-rte -wp-script 'wp0.script' -wp-model Typed+ref -wp-out foo.wp foo.c
Frama-C produces the following output:
[kernel] preprocessing with "gcc -C -E -I. -dD foo.c"
Adhesion_Factor.c:1:0: warning: "__STDC__" redefined [enabled by default]
/* =============================================================================
^
foo.c:1:0: note: this is the location of the previous definition
# 1 "Adhesion_Factor.c"
^
Adhesion_Factor.c:1:0: warning: "__STDC_HOSTED__" redefined [enabled by default]
/* =============================================================================
^
foo.c:1:0: note: this is the location of the previous definition
# 1 "Adhesion_Factor.c"
^
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[rte] annotating function TrackToTrain_Packet_071
[rte] annotating function TrackToTrain_Packet_071_Encoder
[wp] Collecting variable usage
[wp] Computing [100 goals...]
[wp] failure: Non-assignable term (P_Telegram+(0 .. I_Cur_Dim-1))
[kernel] Current source was: Adhesion_Factor.c:59
The full backtrace is:
Raised at file "src/kernel/log.ml", line 524, characters 30-31
Called from file "src/kernel/log.ml", line 518, characters 9-16
Re-raised at file "src/kernel/log.ml", line 521, characters 15-16
Called from file "list.ml", line 55, characters 20-23
Called from file "set.ml", line 304, characters 38-41
Called from file "map.ml", line 168, characters 20-25
Called from file "map.ml", line 168, characters 10-18
Called from file "map.ml", line 168, characters 10-18
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "queue.ml", line 134, characters 6-20
Called from file "src/kernel/boot.ml", line 37, characters 4-20
Called from file "src/kernel/cmdline.ml", line 735, characters 2-9
Called from file "src/kernel/cmdline.ml", line 214, characters 4-8
Plug-in wp aborted: internal error.
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Neon-20140301.
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
### Additional Information :
The attached foo.c is the preprocessed version of a file out of the openETCS project. All used predicates are already included in the file.
## Attachments
- [foo.c](/uploads/4ca8b0f3f57e9d34ae71f1281023f171/foo.c)https://git.frama-c.com/pub/frama-c/-/issues/711Frama-C does not work with versions of Why3 newer than 0.832021-02-22T13:40:40Zmantis-gitlab-migrationFrama-C does not work with versions of Why3 newer than 0.83ID0002067:
**This issue was created automatically from Mantis Issue 2067. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002067:
**This issue was created automatically from Mantis Issue 2067. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002067 | Frama-C | Plug-in > wp | public | 2015-01-27 | 2015-03-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | thinkmoore | **Assigned To** | bobot | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | Mac OS X | **OS Version** | Yosemite |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | Frama-C Sodium | **Fixed in Version** | Frama-C Sodium |
### Description :
Why3 appears to have changed their command line interface with release 0.84, causing Frama-C to issue commands it no longer understands.
### Steps To Reproduce :
Install Why3 >= 0.84 and attempt to discharge a wp goal using a why3 solver, i.e. -wp-prover z3https://git.frama-c.com/pub/frama-c/-/issues/714Bullet colors are unreadable for color blind people2021-02-22T13:24:44ZDavid MentréBullet colors are unreadable for color blind peopleID0001485:
**This issue was created automatically from Mantis Issue 1485. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001485:
**This issue was created automatically from Mantis Issue 1485. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001485 | Frama-C | Graphical User Interface | public | 2013-09-26 | 2015-03-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dmentre | **Assigned To** | guillaume-petiot | **Resolution** | fixed |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130601 | **Target Version** | - | **Fixed in Version** | Frama-C Sodium |
### Description :
For color blind people (e.g. "Daltoniens" in French), it is very difficult to make the difference between the red, green and orange bullets (at least, I have no testimony for others).
Possible improvements:
* Change the shape (e.g. circle for green bullet, triangle for orange bullet, ...);
* Use a shading scheme suitable for color blind people (https://trello.com is offering such a scheme for label colors), e.g. "/////" for one color, "\\\\\" for another color, etc.
* A combination of above two schemes.https://git.frama-c.com/pub/frama-c/-/issues/741body of atomic cond belonging to an assume reproduced in sequence containing ...2021-02-22T13:52:03ZNicky Williamsbody of atomic cond belonging to an assume reproduced in sequence containing the assumeID0002020:
**This issue was created automatically from Mantis Issue 2020. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002020:
**This issue was created automatically from Mantis Issue 2020. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002020 | Frama-C | Plug-in > pathcrawler | public | 2014-12-05 | 2015-03-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | nicky | **Assigned To** | muriel | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | Frama-C GIT, precise the release id | **Fixed in Version** | Frama-C Sodium |
### Description :
The ast_node.pl file generated for assert assume contains the following lines:
...
ast_node(n(24), seq, [409,n(37),n(33),422,n(48),n(44)]). % assert_assume.c: l.16
...
ast_node(n(44), assume, [atomic_cond(n(53))]). % assert_assume.c: l.17
...
atomic_cond(n(53), [n(54), 429]).
...
ast_node(n(54), seq, [422,n(48)]). % assert_assume.c: l.17
### Steps To Reproduce :
cd pathcrawler/tests/AssertAssume
frama-c -pc -pc-analyzer -lib-entry -main assert_assume assert_assume.chttps://git.frama-c.com/pub/frama-c/-/issues/746Capitalized filename in Dynamic.load_module2021-02-22T13:10:33Zmantis-gitlab-migrationCapitalized filename in Dynamic.load_moduleID0001276:
**This issue was created automatically from Mantis Issue 1276. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001276:
**This issue was created automatically from Mantis Issue 1276. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001276 | Frama-C | Kernel | public | 2012-09-20 | 2015-03-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Anne | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Oxygen-20120901 | **Target Version** | - | **Fixed in Version** | Frama-C Sodium |
### Description :
When calling
Dynamic.load_module "share/lib/file"
if fails because it is looking for [./share/lib/File.cmxs] instead of [./share/lib/file.cmxs].
I guess there is a bad String.capitalize there.
(Warning: it seems that there is the same problem in the following function 'load_script')https://git.frama-c.com/pub/frama-c/-/issues/748Crah with the option -ulevel2021-02-22T14:02:27Zmantis-gitlab-migrationCrah with the option -ulevelID0001768:
**This issue was created automatically from Mantis Issue 1768. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001768:
**This issue was created automatically from Mantis Issue 1768. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001768 | Frama-C | Plug-in > slicing | public | 2014-04-30 | 2015-03-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | nguenaomer | **Assigned To** | patrick | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | PC | **OS** | Ubuntu | **OS Version** | 13.04 |
| **Product Version** | Frama-C Fluorine-20130601 | **Target Version** | - | **Fixed in Version** | Frama-C Sodium |
### Description :
When I execute
$frama-c fsm.c -main main -slice-pragma main -ulevel 10 -then-on 'Slicing export' -print
frama-c get crash with the following part of the log:
[slicing] making slicing project 'Slicing'...
[slicing] interpreting slicing requests from the command line...
[kernel] Current source was: fsm.c:46
The full backtrace is:
Raised at file "src/logic/logic_interp.ml", line 796, characters 6-39
Called from file "list.ml", line 75, characters 12-15
### Additional Information :
the program produce an output with the option -slevel
### Steps To Reproduce :
Here is fsm.c:
int choix ;
int state = 1;
int cumul =0 ;
int step =0;
//initialisation
/*@
ensures \result==0 || \result==1 || \result==2 ;
*/
int choisir() ;
void lecture() {
choix = choisir() ;
}
void fsm_transition() {
switch (state) {
case 1:
if (choix == 2) {
cumul = cumul +2 ;
state = 2 ;
}
else
cumul++;
break ;
case 2:
if ((step==50) && (choix==1))
state = 3 ;
else
cumul++ ;
break ;
case 3: if ((choix==0) && (cumul==10)) state = 1;
default: break ;
}
}
int main() {
while (step>=0){
lecture() ;
fsm_transition() ;
if (state == 3) {
/*@ slice pragma ctrl ;*/
break ;
}
step ++ ;
}
return 0 ;
}https://git.frama-c.com/pub/frama-c/-/issues/749Frama-C/WP "forgets" a proven assertion2021-02-22T14:02:03ZJens GerlachFrama-C/WP "forgets" a proven assertionID0001751:
**This issue was created automatically from Mantis Issue 1751. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001751:
**This issue was created automatically from Mantis Issue 1751. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001751 | Frama-C | Plug-in > wp | public | 2014-04-11 | 2015-03-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | patrick | **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 Sodium |
### Description :
In the following function
void strange_after_shift(unsigned int x)
{
unsigned int y = x & 1;
//@ assert y == 0 || y == 1;
//@ assert 0 <= y <= 1;
}
the first assertion is discharged by Qed but the second assertion (which should also hold)
is not discharged with Alt-Ergo.
Moreover, when I try to prove it with Coq, then I cannot see any hypothesis that represents the first assertion.
## Attachments
- [strange_after_shift.c](/uploads/bb5449fe82a2bd2c11222cda38be2a40/strange_after_shift.c)https://git.frama-c.com/pub/frama-c/-/issues/753typo in wp output: "interruped"-->"interrupted"2021-02-22T14:02:05ZJochen Burghardttypo in wp output: "interruped"-->"interrupted"ID0001832:
**This issue was created automatically from Mantis Issue 1832. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001832:
**This issue was created automatically from Mantis Issue 1832. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001832 | Frama-C | Plug-in > wp | public | 2014-07-14 | 2015-03-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | trivial | **Reproducibility** | always |
| **Platform** | - | **OS** | xubuntu-cfe13.10 | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Sodium |
### Description :
Complete output was:
frama-c -wp-prover alt-ergo,cvc4 -wp -wp-rte gui01.c
[kernel] preprocessing with "gcc -C -E -I. gui01.c"
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[rte] annotating function main
[wp] 1 goal scheduled
[wp] [Alt-Ergo] Goal typed_main_assert : Unknown
[wp] [cvc4] Goal typed_main_assert : Timeout
[wp] Proved goals: 0 / 1
Alt-Ergo: 0 (unknown: 1)
cvc4: 0 (interruped: 1)https://git.frama-c.com/pub/frama-c/-/issues/754Frame Validity2021-02-22T14:02:04ZLoïc CorrensonFrame ValidityID0001828:
**This issue was created automatically from Mantis Issue 1828. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001828:
**This issue was created automatically from Mantis Issue 1828. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001828 | Frama-C | Plug-in > wp | public | 2014-07-08 | 2015-03-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | correnson | **Assigned To** | patrick | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Sodium |
### Description :
//@ requires \valid(one);
void f(int *one){
int two;
//@ assert one != &two;
}
int *zero;
//@ requires \valid(zero) && \valid(one);
void frame(int *one, int arg){
int two;
//@ assert formal: \separated(one,&arg,&two);
//@ assert global: \separated(zero,&arg,&two);
}
## Attachments
- [bts1828_frame.i](/uploads/75bda1142495f914b1db21ba625d707e/bts1828_frame.i)https://git.frama-c.com/pub/frama-c/-/issues/757Crash on invalid -val-split-return-function option2021-02-22T13:10:55Zmantis-gitlab-migrationCrash on invalid -val-split-return-function optionID0001857:
**This issue was created automatically from Mantis Issue 1857. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001857:
**This issue was created automatically from Mantis Issue 1857. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001857 | Frama-C | Plug-in > Eva | public | 2014-07-25 | 2015-03-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Anne | **Assigned To** | yakobowski | **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 :
The Failure is caught when parsing the -val-split-return-function option, but not the Invalid_argument one, hence the crash.
### Steps To Reproduce :
With any C file such as :
int main (void) {
return 0;
}
$ frama-c test.c -val -val-split-return-function main:3x
[kernel] Current source was: test.c:2
The full backtrace is:
Called from file "list.ml", line 55, characters 20-23
Called from file "src/value/value_parameters.ml", line 422, characters 20-48
...
Unexpected error (Invalid_argument("Z.of_string_base: invalid number")).
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Neon-20140301+dev.https://git.frama-c.com/pub/frama-c/-/issues/759bogus syntax error with doxygen2021-02-22T13:47:19Zmantis-gitlab-migrationbogus syntax error with doxygenID0001853:
**This issue was created automatically from Mantis Issue 1853. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001853:
**This issue was created automatically from Mantis Issue 1853. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001853 | Frama-C | Kernel | public | 2014-07-23 | 2015-03-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | billyPilgrim | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | linux | **OS** | ubuntu 12.04 LTS | **OS Version** | 12.04 LTS |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | Frama-C Sodium |
### Description :
I have several header files that contain:
/*@}
strings beginning comments. This will cause frama-c to stop due to a syntax error. It can be fixed by inserting a space between the '*' and the '@'. I don't know if that will result in ill-formed doxygen (I didn't create the file and am not a doxygen user), but the parser does choke on it.
### Steps To Reproduce :
create a header file and put in a comment, starting in column 1
/*@} End of pub_func */
and it will fail.
replace with:
/* @} End of pub_func */
and all is well.https://git.frama-c.com/pub/frama-c/-/issues/760Non terminating call to stncpy2021-02-22T13:11:00Zmantis-gitlab-migrationNon terminating call to stncpyID0001908:
**This issue was created automatically from Mantis Issue 1908. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001908:
**This issue was created automatically from Mantis Issue 1908. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001908 | Frama-C | Plug-in > Eva | public | 2014-08-08 | 2015-03-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Anne | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Sodium |
### Description :
I get a NON TERMINATING FUNCTION on the attached example due to a call to strncpy, but I don't really understand why...
I added a \from part to the assigns property to remove the :
warning: no \from part for clause 'assigns
But it was not the problem.
The message are:
no state left in which to evaluate postcondition
I didn't even found a workaround :-(
### Steps To Reproduce :
$ frama-c -val strncpy.c -cpp-extra-args="-I$(frama-c -print-share-path)/libc" -
val-builtin strlen:Frama_C_strlen
## Attachments
- [strncpy.c](/uploads/5250990c20a0d23f092bb3e01b8e02e2/strncpy.c)https://git.frama-c.com/pub/frama-c/-/issues/761Crash when merging contracts for duplicated functions with different formal p...2021-02-22T13:11:01ZBernard BotellaCrash when merging contracts for duplicated functions with different formal parameters namesID0001901:
**This issue was created automatically from Mantis Issue 1901. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001901:
**This issue was created automatically from Mantis Issue 1901. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001901 | Frama-C | Kernel | public | 2014-07-30 | 2015-03-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | bb | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C Sodium |
### Description :
frama-c monstrdup.c /usr/local/share/frama-c/libc/string.h /usr/local/share/frama-c/libc/string.c -cpp-extra-args='-I/usr/local/share/frama-c/libc/' -check
produces
preprocessing with "gcc -C -E -I. -I/usr/local/share/frama-c/libc/ monstrdup.c"
[kernel] preprocessing with "gcc -C -E -I. -I/usr/local/share/frama-c/libc/ FRAMAC_SHARE/libc/string.h"
[kernel] preprocessing with "gcc -C -E -I. -I/usr/local/share/frama-c/libc/ FRAMAC_SHARE/libc/string.c"
FRAMAC_SHARE/libc/string.c:44:[kernel] warning: def'n of func strdup at FRAMAC_SHARE/libc/string.c:44 (sum 4631) conflicts with the one at monstrdup.c:4 (sum 2976051); keeping the one at monstrdup.c:4.
monstrdup.c:4:[kernel] warning: found two contracts. Merging them
FRAMAC_SHARE/libc/string.h:258:[kernel] failure: [AST Integrity Check] initial AST
logic variable s (2504) is not declared
[kernel] Current source was: FRAMAC_SHARE/libc/string.h:258
The full backtrace is:
Raised at file "src/kernel/log.ml", line 524, characters 30-31
Called from file "src/kernel/log.ml", line 518, characters 9-16
Re-raised at file "src/kernel/log.ml", line 521, characters 15-16
Called from file "src/kernel/file.ml", line 393, characters 26-36
Called from file "cil/src/cil.ml", line 2014, characters 15-31
Called from file "cil/src/cil.ml", line 2311, characters 16-41
Called from file "cil/src/cil.ml", line 2029, characters 21-41
Called from file "cil/src/cil.ml", line 2302, characters 14-39
Called from file "cil/src/cil.ml", line 2029, characters 21-41
Called from file "cil/src/cil.ml", line 2168, characters 18-30
Called from file "cil/src/cil.ml", line 2029, characters 21-41
Called from file "cil/src/cil.ml", line 2145, characters 12-44
Called from file "cil/src/cil.ml", line 2029, characters 21-41
Called from file "cil/src/cil.ml", line 2141, characters 12-63
Called from file "cil/src/cil.ml", line 2053, characters 13-16
Called from file "cil/src/cil.ml", line 2535, characters 14-34
Called from file "cil/src/cil.ml", line 2029, characters 21-41
Called from file "cil/src/cil.ml", line 2523, characters 17-48
Called from file "cil/src/cil.ml", line 2029, characters 21-41
Called from file "cil/src/cil.ml", line 2517, characters 11-39
Called from file "cil/src/cil.ml", line 2029, characters 21-41
Called from file "cil/src/cil.ml", line 2053, characters 13-16
Called from file "cil/src/cil.ml", line 2696, characters 19-54
Called from file "cil/src/cil.ml", line 2029, characters 21-41
Called from file "cil/src/cil.ml", line 2053, characters 13-16
Called from file "cil/src/cil.ml", line 2719, characters 21-58
Called from file "cil/src/cil.ml", line 2029, characters 21-41
Called from file "cil/src/cil.ml", line 3502, characters 4-28
Called from file "cil/src/cil.ml", line 2053, characters 13-16
Called from file "cil/src/cil.ml", line 2098, characters 24-57
Called from file "cil/src/cil.ml", line 3469, characters 5-53
Called from file "cil/src/cil.ml", line 6090, characters 16-36
Called from file "list.ml", line 75, characters 12-15
Called from file "cil/src/cil.ml", line 5680, characters 3-30
Called from file "cil/src/cil.ml", line 6091, characters 2-420
Called from file "cil/src/cil.ml", line 2029, characters 21-41
Called from file "cil/src/cil.ml", line 6124, characters 7-84
Called from file "src/kernel/file.ml", line 1657, characters 36-147
Called from file "src/kernel/file.ml", line 2265, characters 4-27
Called from file "src/kernel/ast.ml", line 113, characters 2-28
Called from file "src/kernel/ast.ml", line 125, characters 53-71
Called from file "src/kernel/boot.ml", line 29, characters 6-20
Called from file "src/kernel/cmdline.ml", line 752, characters 2-9
Called from file "src/kernel/cmdline.ml", line 214, characters 4-8
### Additional Information :
when using -print option instead of -check i get the following contract for strdup:
/*@ requires valid_string_src: valid_string(str);
requires valid_string_src: valid_string(s);
ensures
\valid(\result+(0 .. strlen(\old(str)))) ∧
strcmp(\result, \old(str)) ≡ 0;
ensures
\valid(\result+(0 .. strlen(\old(s)))) ∧
strcmp(\result, \old(s)) ≡ 0;
assigns \nothing;
*/
char *strdup(char const *str)
{
...
}
### Steps To Reproduce :
monstrdup.c contains :
#include "string.h"
#include "stdlib.h"
char *
strdup(const char *str)
{
if (str != NULL) {
register char *copy = malloc(strlen(str) + 1);
if (copy != NULL)
return strcpy(copy, str);
}
return NULL;
}https://git.frama-c.com/pub/frama-c/-/issues/765Status of POs: the word "interruped" should be "interrupted"2021-02-22T14:02:05ZRichard BonichonStatus of POs: the word "interruped" should be "interrupted"ID0001930:
**This issue was created automatically from Mantis Issue 1930. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001930:
**This issue was created automatically from Mantis Issue 1930. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001930 | Frama-C | Plug-in > wp | public | 2014-09-26 | 2015-03-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | rbonichon | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | low | **Severity** | text | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Sodium |
### Description :
The standard output of wp displays "interruped" instead of "interrupted".
The change should occur in src/wp/register.ml
At the same time, the "mutable interruped" field should be changed to "interrupted"https://git.frama-c.com/pub/frama-c/-/issues/776WP ignores some goals when 'initialized' is used in hypotheses2021-02-22T13:11:28Zmantis-gitlab-migrationWP ignores some goals when 'initialized' is used in hypothesesID0001670:
**This issue was created automatically from Mantis Issue 1670. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001670:
**This issue was created automatically from Mantis Issue 1670. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001670 | Frama-C | Plug-in > wp | public | 2014-03-04 | 2015-03-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Anne | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Sodium |
### Description :
The message:
[wp] warning: Allocable, Freeable, Valid_read, Fresh and Initialized not yet implemented
is perfectly clear, but I would have expected that annotations using these predicates would have been ignored. Instead of that, proof obligations of other annotations simply disappear.
### Steps To Reproduce :
Example:
/*@ requires r1: \initialized(Y+(0 .. 99));
assigns X[0..99];
ensures X[0] == Y[0];
*/
void cp( int *X, int *Y );
void f (int *A, int *B) {
cp(B, A);
/*@ assert a1: A[0] == B[0]; */
}
Without the 'requires' property, the assertion is proved:
$ frama-c -wp test.c -wp-prop a1
...
[wp] 1 goal scheduled
[wp] [Qed] Goal typed_f_assert_a1 : Valid
[wp] Proved goals: 1 / 1
Qed: 1
With the 'requires' property, the assertion is not even scheduled as a goal:
$ frama-c -wp test.c -wp-prop a1
...
[wp] 0 goal scheduled
[wp] Proved goals: 0 / 0https://git.frama-c.com/pub/frama-c/-/issues/777compatibility between \null in ACSL and NULL in C in wp2021-02-22T13:11:29Zmantis-gitlab-migrationcompatibility between \null in ACSL and NULL in C in wpID0001647:
**This issue was created automatically from Mantis Issue 1647. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001647:
**This issue was created automatically from Mantis Issue 1647. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001647 | Frama-C | Plug-in > wp | public | 2014-02-17 | 2015-03-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Anne | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Sodium |
### Description :
I have tried to prove properties involving NULL pointers, and I had problem to write the ACSL part. Here is and example:
/*@
ensures e1: \result == \null;
ensures e2: \result == 0;
ensures e3: \result == (int *) \null;
ensures e4: \result == (int *) 0;
ensures e5: \result == (int *)((void *)0);
*/
int * f (void) {
return NULL;
}
None of the properties are proved with the default memory model.
I finally manage to prove them with: -wp-model Typed+cast
Since NULL is used very often in programs, even with a clean typing, maybe something could be done for this special case ? Just a suggestion... ;-)https://git.frama-c.com/pub/frama-c/-/issues/779Make identifiers in Coq proofs more similar to those from C code2021-02-22T13:11:35ZJens GerlachMake identifiers in Coq proofs more similar to those from C codeID0001630:
**This issue was created automatically from Mantis Issue 1630. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001630:
**This issue was created automatically from Mantis Issue 1630. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001630 | Frama-C | Plug-in > wp | public | 2014-01-23 | 2015-03-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130601 | **Target Version** | - | **Fixed in Version** | Frama-C Sodium |
### Description :
When I want to proof an obligation for function
foo(int* a, int n)
then the Coq representation of the obligation uses the identifiers "a_0" and "n_0".
In my opinion, the proofs would be easier to read if WP would generate the names "a"
and "n".
(I often use "remember a_0 as a" to achieve this, but it would be nicer if I did not have to do it manually.)