frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2021-02-22T13:39:25Zhttps://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/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/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/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/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/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/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/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/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/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/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/174Failure to record global variable with initialiser2022-09-28T12:12:55ZKostyantyn VorobyovFailure to record global variable with initialiserID0002194:
**This issue was created automatically from Mantis Issue 2194. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002194:
**This issue was created automatically from Mantis Issue 2194. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002194 | Frama-C | Plug-in > E-ACSL | public | 2015-12-04 | 2019-01-25 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | kvorobyov | **Assigned To** | signoles | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
/* The following example wrongly fails the assertion */
#include <inttypes.h>
char *B = "foo";
unsigned long ref() {
return (intptr_t)B;
}
int main(int argc, char **argv) {
char *ptr = (char*)ref();
//@ assert \valid_read(ptr);
return 0;
}
### Additional Information :
This seems to be the case where memory analysis incorrectly determines that global variable 'B' should not be modelled and therefore it is omitted from the instrumentation.Julien SignolesJulien Signoleshttps://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/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/296Option "-lib-entry" results misses possible values of function pointers2021-02-22T12:58:33ZJochen BurghardtOption "-lib-entry" results misses possible values of function pointersID0002254:
**This issue was created automatically from Mantis Issue 2254. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002254:
**This issue was created automatically from Mantis Issue 2254. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002254 | Frama-C | Plug-in > Eva | public | 2016-11-07 | 2017-12-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | maroneze | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | xubuntu | **OS Version** | - |
| **Product Version** | Frama-C Aluminium | **Target Version** | - | **Fixed in Version** | - |
### Description :
(I posed this question also on frama-c-discuss on 3 Nov 2016, 16:20, and received a reply from David Mentré on 5 Nov 2016, 15:52. The advice to use an invariant and increase the slevel originates from Julien Signoles.)
Running "frama-c -val -main foo -lib-entry -slevel 10 fctptr.c" on the attached program results in an output of:
a ∈ [--..--]
fct ∈ {0}
While option "-lib-entry" behaves on the int variable "a" as described in the value analysis manual (sect.5.2.3, p.58), it seems to have no effect on the function pointer variable "fct". Moreover, the latter is analyzed to contain a null pointer, while it actually never does, due to its initialization at the declaration. Instead, since "fct" is declared "static", I'd expect the analysis to report:
a ∈ [--..--]
fct ∈ {{ &f1, &f2 }}
When "-lib-entry" is omitted, Frama-C's analysis coincides with mine:
a ∈ {1}
fct ∈ {{ &f1 }}
Both with and without option "-lib-entry", Frama-C's results don't change when the invariant is removed. To sum up, it seems that the use of option "-lib-entry" inhibits information from call analysis, but also from explicit invariants.
## Attachments
- [fctptr.c](/uploads/35907f38d48ab7e62a81d969080d542a/fctptr.c)Andre MaronezeAndre Maronezehttps://git.frama-c.com/pub/frama-c/-/issues/298"pointer comparison" warning emitted for "p==NULL"2021-02-22T12:58:36ZJochen Burghardt"pointer comparison" warning emitted for "p==NULL"ID0002256:
**This issue was created automatically from Mantis Issue 2256. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002256:
**This issue was created automatically from Mantis Issue 2256. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002256 | Frama-C | Plug-in > Eva | public | 2016-11-11 | 2017-12-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | maroneze | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | xubuntu | **OS Version** | - |
| **Product Version** | Frama-C Aluminium | **Target Version** | Frama-C 15-Phosphorus | **Fixed in Version** | - |
### Description :
Running "frama-c -val -val-warn-undefined-pointer-comparison=pointer ptrcmp3.c" on the attached file results in a warning:
ptrcmp3.c:10:[kernel] warning: pointer comparison. assert \pointer_comparable((void *)p, (void *)0);
The warning disappears if
1. the type of parameter "name" is changed from "char*" to "char" both in "foo" and in "main", or
2. the "assigns" clause for "foo" is deleted.
The warning seems strange by itself, as every pointer should be comparable to NULL. The changes that make the warning disappear (in particular 1.) support the hypothesis that this is a bug.
## Attachments
- [ptrcmp3.c](/uploads/3c9e9c4fc07c25680f1e5c42b0b24b71/ptrcmp3.c)Andre MaronezeAndre Maronezehttps://git.frama-c.com/pub/frama-c/-/issues/389wp: the example from Getting Started guide doesn't work (all goals are Unknown)2021-04-15T09:14:52Zmantis-gitlab-migrationwp: the example from Getting Started guide doesn't work (all goals are Unknown)ID0002261:
**This issue was created automatically from Mantis Issue 2261. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002261:
**This issue was created automatically from Mantis Issue 2261. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002261 | Frama-C | Plug-in > wp | public | 2016-12-14 | 2016-12-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | vlad | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Windows | **OS** | Windows 7 | **OS Version** | - |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | - | **Fixed in Version** | - |
### Description :
I'm trying to reproduce ASCL example from frama-c manual. For some reason all goals sent to alt-ergo end up with unknown result.
Code:
$ cat frama-c-test.c
/*@ requires \valid(a) && \valid(b);
@ ensures A: *a == \old(*b);
@ ensures B: *b == \old(*a);
@ assigns *a,*b;
@*/
void swap(int * a, int * b);
void swap(int *a,int *b)
{
int tmp = *a ;
*a = *b ;
*b = tmp ;
return ;
}
Frama-C result:
$ frama-c -wp -wp-rte frama-c-test.c
[kernel] Parsing .opam/4.02.3+mingw32c/share/frama-c/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing frama-c-test.c (with preprocessing)
[wp] Running WP plugin...
[rte] annotating function swap
[wp] 4 goals scheduled
[wp] [Alt-Ergo] Goal typed_swap_assert_rte_mem_access_4 : Unknown (65ms)
[wp] [Alt-Ergo] Goal typed_swap_assert_rte_mem_access_3 : Unknown (64ms)
[wp] [Alt-Ergo] Goal typed_swap_assert_rte_mem_access_2 : Unknown (61ms)
[wp] [Alt-Ergo] Goal typed_swap_assert_rte_mem_access : Unknown (60ms)
[wp] Proved goals: 0 / 4
Alt-Ergo: 0 (unknown: 4)
The exact same code works with Frama-C Aluminum on Linux. I'm running Frama-C on Windows 7 (with cygwin).
### Additional Information :
$ alt-ergo -version
1.30
$ frama-c --version
Silicon-20161101Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/383structure in logic not supported?2021-02-22T13:58:05ZJens Gerlachstructure in logic not supported?ID0002264:
**This issue was created automatically from Mantis Issue 2264. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002264:
**This issue was created automatically from Mantis Issue 2264. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002264 | Frama-C | Kernel > ACSL implementation | public | 2016-12-20 | 2017-01-04 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | - | **Fixed in Version** | - |
### Description :
When running 'frama-c type.c" on the attached file, I receive the following error message:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing type.c (with preprocessing)
type.c:2:[kernel] user error: unexpected token '{'
[kernel] user error: stopping on file "type.c" that has errors. Add '-kernel-msg-key pp'
for preprocessing command.
[kernel] Frama-C aborted: invalid user input.
I took the example straight from acsl-implementation manual (first line on page 27).
## Attachments
- [type.c](/uploads/48e85835fc8bbcc9b8a1e97921ee7581/type.c)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/381WP appears to assume left-to-right evaluation order for int addition2021-02-22T13:00:44ZJochen BurghardtWP appears to assume left-to-right evaluation order for int additionID0002272:
**This issue was created automatically from Mantis Issue 2272. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002272:
**This issue was created automatically from Mantis Issue 2272. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002272 | Frama-C | Kernel | public | 2017-01-16 | 2017-01-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | low | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Silicon-20161101 | **OS** | xubuntu | **OS Version** | - |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | - | **Fixed in Version** | - |
### Description :
The following issue originated from our student Robert. Running "frama-c -wp -wp-rte robert.c" on the attached program reports 3 proof goals, all of which are proven by Qed. However, according to ISO/IEC 9899:2011 §6.5 (2), the behavior of this function is undefined, since "x" is modified more than once between two sequence points.
Replacing the "4" in the ensures clause in line 2 by "2" or "3", or replacing the whole formula in line 2 by "\false", all results in one unproven goal (and two proven goals). Therefore, it seems that Frama-C's justification for proving "\result==4" is not that the function won't return anyway, due to the undefined behavior, considered as throwing an exception.
## Attachments
- [robert.c](/uploads/22bdf3d8de3739a26c3887d856f6b98c/robert.c)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/370problem with Qed's simplification power2021-02-22T13:00:23ZJochen Burghardtproblem with Qed's simplification powerID0002278:
**This issue was created automatically from Mantis Issue 2278. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002278:
**This issue was created automatically from Mantis Issue 2278. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002278 | Frama-C | Plug-in > wp | public | 2017-02-06 | 2017-02-06 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Silicon-20161101 | **OS** | Ubuntu 16.04.1 LTS | **OS Version** | - |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp -wp-out wp-out shift.c" on the attached file and inspecting the file "wp-out/typed/foo_post_Alt-Ergo.mlw" shows that lemma "ShiftAssociative" is simplified to "true" (see line 360) by Qed. (The postcondition of foo doesn't matter here, except that it is intentionally unprovable in order to demonstrate the lemma's simplification.)
This situation doesn't change even when all options to disable Qed functionality (i.e. "-wp-no-bits -wp-no-clean -wp-no-core -wp-no-filter -wp-no-init-summarize-array -wp-no-let -wp-no-pruning -wp-no-simpl -wp-no-simplify-forall -wp-no-simplify-is-cint -wp-no-simplify-type") are given. (In contrast, in the somewhat related issue #1751, providing option "-wp-no-bits" is sufficient to circumvent the problem.)
While Qed's simplification capabilities are appreciated in general, the disappearance of the lemma can be a problem:
* In many Coq proofs related to C address computation, a similar lemma has to be stated and proven again and again. There seems to be no easy way to make Coq see what is considered trivial by Qed.
* Considering the discussion at https://github.com/OCamlPro/alt-ergo/issues/19, if I understood the Alt-Ergo people right, Alt-Ergo isn't complete on linear arithmetic with arrays (except for quantifier-free formulas). Therefore it sometimes needs trivial lemmas. In the particular example, to make Alt-Ergo prove the goal "reverse", a kind of associtivity property (axiom "arith") is needed that Qed would simplify also to "true", and even Alt-Ergo would.
Generally speaking, Qed should be (configurable such that it is) no stronger than any of the external provers, such as Coq and Alt-Ergo. This would enable the user to provide appropriate prover hints that are not simplified away by Qed. Maybe a command line option to completely switch off Qed is sufficient. As an alternative, a command-line switch could reduce the capabilities of Qed when applied to lemmas, assuming that the user is responsible to give them in an optimal form.
## Attachments
- [shift.c](/uploads/572d124b06bee30721a80150255027ac/shift.c)
- [foo_post_Alt-Ergo.mlw](/uploads/746bbaa9bc36a947691d7be190773542/foo_post_Alt-Ergo.mlw)Loïc CorrensonLoïc Correnson