frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2021-03-30T08:22:30Zhttps://git.frama-c.com/pub/frama-c/-/issues/276insufficient contracts for generated constructors and assignment operator(s)2021-03-30T08:22:30ZJens Gerlachinsufficient contracts for generated constructors and assignment operator(s)ID0002356:
**This issue was created automatically from Mantis Issue 2356. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002356:
**This issue was created automatically from Mantis Issue 2356. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002356 | Frama-C | Plug-in > clang | public | 2018-02-07 | 2018-02-09 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 16-Sulfur | **Target Version** | - | **Fixed in Version** | - |
### Description :
The attached file contains a very simple class (struct).
It is used in simple copy initialization and assignment operations.
When called with with
frama-c-gui -wp -wp-rte generated_member_functions.cpp
then the two assertions are not verified by Fram-Clang/WP.
From what I see about the contracts of the generated constructors and assignment operator(s), this is not surprising because their postconditions do not refer to the member 'n'.
EVA seems to work just fine.
## Attachments
- [generated_member_functions.cpp](/uploads/c7dc2a564d7435a34294e0aa839d9178/generated_member_functions.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/855insufficient preconditions given to Alt-Ergo to prove assigns clause for muta...2021-02-22T14:02:13ZJochen Burghardtinsufficient preconditions given to Alt-Ergo to prove assigns clause for mutable variable in contract of const methodID0002000:
**This issue was created automatically from Mantis Issue 2000. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002000:
**This issue was created automatically from Mantis Issue 2000. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002000 | Frama-Clang | Plug-in > clang | public | 2014-11-27 | 2015-02-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **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 :
Running "frama-c -wp -wp-rte 171.cpp" on the attached program produces an obligation "typed__ZNK2clE3foo_assert_rte_mem_access" which is unprovable by Alt-Ergo. When the "const" is deleted in line 6, all obligations are provable.
The goal in the .mlw file is "... -> valid_rd(t, a, 1) -> valid_rw(t, shiftfield_F__Z2cl_x(a), 1)" with the "const", see attached file "_ZNK2clE3foo_assert_rte_mem_access_Alt-Ergo.mlw", and "... -> valid_rw(t, a, 1) -> valid_rw(t, shiftfield_F__Z2cl_x(a), 1)" without it, see file "_ZN2clE3foo_assert_rte_mem_access_Alt-Ergo.mlw". Since "shiftfield_F__Z2cl_x(p)" is defined as "shift(p,0)", the latter goal is trivially true.
Probably, the possibility that a "const" function well may modify a "mutable" variable has not been considered in proof goal generation.
## Attachments
- [171.cpp](/uploads/e0bcb05cd42e24bf1af6dd3309c3fc13/171.cpp)
- [_ZNK2clE3foo_assert_rte_mem_access_Alt-Ergo.mlw](/uploads/0bb4d0ab67362ba0f4c5cf4c232c3e8d/_ZNK2clE3foo_assert_rte_mem_access_Alt-Ergo.mlw)
- [_ZN2clE3foo_assert_rte_mem_access_Alt-Ergo.mlw](/uploads/c120e77b9b17d4f7e08d80aebc0cd6b6/_ZN2clE3foo_assert_rte_mem_access_Alt-Ergo.mlw)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/810insufficient preconditions given to Alt-Ergo to prove "requires" clause about...2021-02-22T14:02:09ZJochen Burghardtinsufficient preconditions given to Alt-Ergo to prove "requires" clause about class member variableID0002014:
**This issue was created automatically from Mantis Issue 2014. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002014:
**This issue was created automatically from Mantis Issue 2014. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002014 | Frama-Clang | Plug-in > clang | public | 2014-12-04 | 2015-02-18 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **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 :
In the attached program "188.cpp", the constructor "X()" initialized the class member variable "x" to 13 (contract and code in line 4 and 5, respectively; contract deliberately phrased to prevent Qed from using it). This constructor is called from the declaration in line 12.
The "assert" in line 13 can be proved without problems; however, the (literally identical) precondition of the "foo" call in line 14 cannot. The file "main_assert_Alt-Ergo.mlw" for the "assert" has the goal:
823 goal main_assert:
824 let a = shiftfield_F__Z1X_x(shift__Z1X(global(L_i_105), 0)) : addr in
825 forall t : int farray.
826 forall t_1 : (addr,int) farray.
827 linked(t) ->
828 (130 = (10 * t_1[a])) ->
829 is_sint32(t_1[a]) ->
830 (t_1[a] <= 42)
that is, t_1[a]==13 is known and t_1[a]<=42 is to be proved.
In contrast, the file "main_call__Z3foo1X_pre_Alt-Ergo.mlw" for the "requires" has the goal:
824 goal main_call__Z3foo1X_pre:
825 let a = shiftfield_F__Z1X_x(shift__Z1X(global(L_i_105), 0)) : addr in
826 let a_1 = shift__Z1X(global(L___fc_tmp_0_106), 0) : addr in
827 forall t : int farray.
828 forall t_2,t_1 : (addr,int) farray.
829 linked(t) ->
830 (t_1[a] <= 42) ->
831 (130 = (10 * t_1[a])) ->
832 IsS__Z1X(Load_S__Z1X(a_1, t_2)) ->
833 is_sint32(t_1[a]) ->
834 ((Load_S__Z1X(a_1, t_2).F__Z1X_x) <= 42)
that is, t_1[a]==13 is known and (Load_S__Z1X(a_1, t_2).F__Z1X_x)<=42 is to be proven, where no relation between t_1 and t_2 is known (both are locally quantified variables).
I guess both proof goals should be similar, or at least a relation between t_1 and t_2 should be given to Alt-Ergo in the goal stemming from "requires".
If "assigns x;" is added to the contract of "X()" in line 4, the situation doesn't improve. The goals then look as follows. In file "main_assert_Alt-Ergo.mlw":
759 goal main_assert:
760 forall i : int.
761 forall t : int farray.
762 (130 = (10 * i)) ->
763 linked(t) ->
764 is_sint32(i) ->
765 (i <= 42)
that is, i==13 is known and i<=42 is to be proved.
In file "main_call__Z3foo1X_pre_Alt-Ergo.mlw":
824 goal main_call__Z3foo1X_pre:
825 let a = shift__Z1X(global(L___fc_tmp_0_106), 0) : addr in
826 forall i : int.
827 forall t : int farray.
828 forall t_1 : (addr,int) farray.
829 (i <= 42) ->
830 (130 = (10 * i)) ->
831 linked(t) ->
832 is_sint32(i) ->
833 IsS__Z1X(Load_S__Z1X(a, t_1)) ->
834 ((Load_S__Z1X(a, t_1).F__Z1X_x) <= 42)
that is, i==13 is known and (Load_S__Z1X(a, t_1).F__Z1X_x)<=42 is to be proven, where no relation between i and t_1 is known (again, both are locally quantified variables).
## Attachments
- [188.cpp](/uploads/099b24b3b63f23a0b2d36961399b08f8/188.cpp)
- [main_assert_Alt-Ergo.mlw_without_assigns](/uploads/a178b5c1643ad780e1b69564d3ddd595/main_assert_Alt-Ergo.mlw_without_assigns)
- [main_call__Z3foo1X_pre_Alt-Ergo.mlw_without_assigns](/uploads/9353ccdc4d04963494c985a23d4a60a5/main_call__Z3foo1X_pre_Alt-Ergo.mlw_without_assigns)
- [main_assert_Alt-Ergo.mlw_with_assigns](/uploads/1763b58af26b99be4ae48ee3bbc91da3/main_assert_Alt-Ergo.mlw_with_assigns)
- [main_call__Z3foo1X_pre_Alt-Ergo.mlw_with_assigns](/uploads/926b2e468083e8df93a34ec6b80db691/main_call__Z3foo1X_pre_Alt-Ergo.mlw_with_assigns)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/2681[kernel] Conflicting types error for enum & typedef enum2024-01-17T11:25:46ZT-Gruber[kernel] Conflicting types error for enum & typedef enumI have encountered a problem that leads to an error when parsing. This occurs when an enum is defined multiple times as shown below. The expectation would be that it works as with the struct shown:
- forward declaration of struct/enum
- ...I have encountered a problem that leads to an error when parsing. This occurs when an enum is defined multiple times as shown below. The expectation would be that it works as with the struct shown:
- forward declaration of struct/enum
- introducing an alias via typedef
- both in one
```C
// test.c
// works
struct my_struct;
typedef struct my_struct my_struct;
typedef struct my_struct {
int val;
} my_struct;
// fails
enum my_enum;
typedef enum my_enum my_enum;
typedef enum my_enum {
VAL
} my_enum;
```
### Steps to reproduce the issue
Parse source file:
```
frama-c test.c
```
### Expected behaviour
Output:
```
[kernel] Parsing test.c
```
### Actual behaviour
Output:
```
[kernel] Parsing test.c
[kernel] test.c:14: User Error:
redefinition of type 'my_enum' in the same scope with conflicting type.
Previous declaration was at test.c:10
[kernel] User Error: stopping on file "test.c" that has errors.
[kernel] Frama-C aborted: invalid user input.
```
### Contextual information
- Frama-C installation mode: Opam
- Frama-C version: 27.0 (Cobalt)
- OS: Ubuntu 22.04.2 LTS (WSL)https://git.frama-c.com/pub/frama-c/-/issues/166kernel generates UnspecifiedSequence when 2 following ternary operators2021-02-22T13:34:58Zmantis-gitlab-migrationkernel generates UnspecifiedSequence when 2 following ternary operatorsID0002435:
**This issue was created automatically from Mantis Issue 2435. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002435:
**This issue was created automatically from Mantis Issue 2435. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002435 | Frama-C | Kernel | public | 2019-05-07 | 2019-05-08 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | rmalak | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | x86_64 Linux 4.19 | **OS** | OCaml 4.07.1 Opam 2.0.3 | **OS Version** | Debian Sid |
| **Product Version** | Frama-C 18-Argon | **Target Version** | - | **Fixed in Version** | - |
### Description :
Consider ternary_operator.c :
/////////////////
int main() {
return (2>1) ? 1 : (1>0) ? 1 : 0;
}
/////////////////
then frama-c generates :
/////////////////
int main(void)
{
int tmp_0;
if (2 > 1) tmp_0 = 1;
else {
int tmp;
if (1 > 0) tmp = 1; else tmp = 0;
tmp_0 = tmp;
}
return tmp_0;
}
//////////////
and considers :
if (1 > 0) tmp = 1; else tmp = 0;
tmp_0 = tmp;
as an UnspecifiedSequence statement
if (1 > 0) tmp = 1; else tmp = 0;
as a "If" statement
and
tmp_0 = tmp;
as a "Instr" statement
Is the construction of the AST with a intermediate UnspecifiedSequence the normal behaviour ?
## Attachments
- [ternary_operators.c](/uploads/90d149e439b96c230c8a26e90e2192da/ternary_operators.c)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/32Known WP limitation: Dynamic allocation is not supported2023-07-21T13:06:10ZBob RubbensKnown WP limitation: Dynamic allocation is not supportedHello everyone,
A colleague of mine tried to use variables as a length argument for an array:
```c
int const n = 4;
int main() {
int xs[n];
}
```
This yielded the following frama-c output:
```bash
[nix-shell:~]$ frama-c -wp program...Hello everyone,
A colleague of mine tried to use variables as a length argument for an array:
```c
int const n = 4;
int main() {
int xs[n];
}
```
This yielded the following frama-c output:
```bash
[nix-shell:~]$ frama-c -wp program.c
[kernel] Parsing program.c (with preprocessing)
[wp] Warning: Missing RTE guards
[wp] program.c:4: Warning:
Cast with incompatible pointers types (source: sint32*) (target: sint8*)
[wp] program.c:4: Warning:
Cast with incompatible pointers types (source: sint8*) (target: sint32*)
[wp] 1 goal scheduled
[wp] Proved goals: 1 / 1
Qed: 1
```
Frama-c version (for completeness, I'm using the version from nixpkgs unstable):
```bash
[nix-shell:~]$ frama-c --version
21.1 (Scandium)
```
The warning seems strange, as I use only ints in this program. With my limited knowledge of C, I'd say this program does no such casting. Is this a bug or is this somehow a subtle edge case in C? Or is it benign and can it be ignored?Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/2567Known WP limitations on `assigns` handling2022-09-22T08:58:28ZAllan BlanchardKnown WP limitations on `assigns` handlingThis issue lists known WP issues with the handling of `assigns` annotation. Related issues are closed (as duplicates) and listed here.
- [ ] WP assigns verification is stronger than what ACSL specifies
- mitigation: see option `-wp-...This issue lists known WP issues with the handling of `assigns` annotation. Related issues are closed (as duplicates) and listed here.
- [ ] WP assigns verification is stronger than what ACSL specifies
- mitigation: see option `-wp-unfold-assigns`
- pub/frama-c#1018
- pub/frama-c#1002
- pub/frama-c#2584
- [ ] WP does not use per behavior assigns
- pub/frama-c#2104
- pub/frama-c#3
- pub/frama-c#1019
- pub/frama-c#2629
Suggestions:
- pub/frama-c#337Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/2569Known WP limitations on statement contract2022-09-28T11:42:56ZAllan BlanchardKnown WP limitations on statement contractSince [Frama-C 23.0](https://git.frama-c.com/pub/frama-c/-/releases/23.0), statement contract are not supported anymore. Related issues are closed (as duplicates) and listed here.
- pub/frama-c#625
- pub/frama-c#1912
- pub/frama-c#511Since [Frama-C 23.0](https://git.frama-c.com/pub/frama-c/-/releases/23.0), statement contract are not supported anymore. Related issues are closed (as duplicates) and listed here.
- pub/frama-c#625
- pub/frama-c#1912
- pub/frama-c#511Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/2568Known WP limitations on the reads clause2021-08-05T09:28:31ZAllan BlanchardKnown WP limitations on the reads clauseThis issue lists known WP issues with the reads clause. Related issues are closed (as duplicates) and listed here.
- [ ] Generate `reads` footprint
- pub/frama-c#1146
- pub/frama-c#410
- [ ] Better handle missing `reads`
- p...This issue lists known WP issues with the reads clause. Related issues are closed (as duplicates) and listed here.
- [ ] Generate `reads` footprint
- pub/frama-c#1146
- pub/frama-c#410
- [ ] Better handle missing `reads`
- pub/frama-c#2172Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/272"let" in predicate body unrecognized2021-02-22T12:58:02ZJochen Burghardt"let" in predicate body unrecognizedID0002362:
**This issue was created automatically from Mantis Issue 2362. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002362:
**This issue was created automatically from Mantis Issue 2362. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002362 | Frama-C | Plug-in > clang | public | 2018-02-12 | 2018-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Sulfur-20171101 | **OS** | - | **OS Version** | Ubuntu 17.10 |
| **Product Version** | Frama-C 16-Sulfur | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp replace_copy_cpp.cpp" on the attached program issues two messages, the 2nd probably being a follow-up problem of the 1st:
replace_copy_cpp.cpp:2:47: unexpected token 'operator -> =' when starting to parse a term
replace_copy_cpp.cpp:4:21: unknown identifier 'Replace'
When the body of predicate definition of "Replace" is changed to "( \at(a[0],K) > 3 )", both message disappear.
## Attachments
- [replace_copy_cpp.cpp](/uploads/dfacff4304f7f33dc22b5bb80602202c/replace_copy_cpp.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/857Liskov substitution principle not checked for methods of same name and signat...2021-02-22T13:13:33ZJochen BurghardtLiskov substitution principle not checked for methods of same name and signature in super- and subclassID0001978:
**This issue was created automatically from Mantis Issue 1978. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001978:
**This issue was created automatically from Mantis Issue 1978. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001978 | Frama-Clang | Plug-in > clang | public | 2014-11-20 | 2015-02-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **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 :
This is not a bug report but merely a suggestion for discussion. According to the "Liskov substitution principle" (see the English wikipedia article of that name for references) a method in a subclass should have a stronger (or equivalent) contract that the corresponding method in the superclass. It could make sense to provide a corresponding check within Frama-Cxx, which could be enabled or disabled by an appropriate command-line option.
This check would be negative (i.e. unprovable) for the attached program "140.cpp"; however, it would be positive if "==" in line 3 was changed to ">=". So this program can be used as a simple test case for such a check, if and when it is implemented.
## Attachments
- [140.cpp](/uploads/1bc224ee781810c444a06c34ee30f3e8/140.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/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/881method contract in template specialization class unimplemented2021-02-22T13:14:05ZJochen Burghardtmethod contract in template specialization class unimplementedID0002037:
**This issue was created automatically from Mantis Issue 2037. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002037:
**This issue was created automatically from Mantis Issue 2037. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002037 | Frama-Clang | Plug-in > clang | public | 2014-12-18 | 2015-02-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:
unimplemented next attachment
[kernel] user error: Failed to parse C++ file. See Clang messages for more information
The error remains if "<T*>" is removed from line 4, turning the template specialization into an ordinary template definition.
The error disappears if line 5 is deleted.
## Attachments
- [418.cpp](/uploads/41c07d4334cfd74c52b3a0c1d86a481c/418.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/831missing ";" after clause causes its tacit omission2021-02-22T14:01:54ZJochen Burghardtmissing ";" after clause causes its tacit omissionID0001976:
**This issue was created automatically from Mantis Issue 1976. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001976:
**This issue was created automatically from Mantis Issue 1976. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001976 | Frama-Clang | Plug-in > clang | public | 2014-11-20 | 2015-02-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **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 goal "typed_main_assert" generated from the file "141.cpp" can't be proven; the corresponding .mlw file contains the goal formula "goal main_assert: forall i : int. is_sint32(i) -> (111 = i)"; that is, the "ensures" clause from line 2 isn't used there.
If the missing ";" at the end of line 2 is appended, the generated goal reads "goal main_assert: forall i : int. (222 = (2 * i)) -> is_sint32(i) -> (111 = i)", and is proven by Alt-Ergo.
No warning or error message about the missing ";" is issued. When the file is renamed to "141.c", frama-c prints an error message "141.c:2:[kernel] user error: expecting ';' before end of annotation".
## Attachments
- [141.cpp](/uploads/a78879845eac9a5610cf9c89525d755d/141.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/182missing E-ACSL code, control flow graph, function pointer2021-03-30T13:47:26Zmantis-gitlab-migrationmissing E-ACSL code, control flow graph, function pointerID0002416:
**This issue was created automatically from Mantis Issue 2416. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002416:
**This issue was created automatically from Mantis Issue 2416. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002416 | Frama-C | Plug-in > E-ACSL | public | 2018-12-11 | 2018-12-11 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | rmalak | **Assigned To** | signoles | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | x86_64 | **OS** | Linux 4.18 Ocaml 4.07.0 | **OS Version** | Debian Sid |
| **Product Version** | Frama-C 18-Argon | **Target Version** | - | **Fixed in Version** | - |
### Description :
Hi,
Is there a workaround for the function pointer limitation
//////////////// cfg.c
void func(void)
{
int i = 0 ;
int *ptr = &i;
/*@ assert \valid(ptr); */
*ptr = 0 ;
}
int main(int argc, char **argv)
{
void (*ptr_func)(void) = &func;
(*ptr_func)();
return 0;
}
////////////////
### Additional Information :
I would like to find a solution that do not involve :
- the use of EVA
OR
- modifying the code
### Steps To Reproduce :
$ frama-c -machdep gcc_x86_64 cfg.c -e-acsl -then-last -print -ocode cfg.e-acsl.c
[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl_gmp_api.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing)
[kernel] Parsing cfg.c (with preprocessing)
[e-acsl] beginning translation.
[e-acsl] cfg.c:12: Warning:
function pointers may introduce too limited instrumentation.
[e-acsl] translation done in project "e-acsl".
$ gcc -DE_ACSL_SEGMENT_MMODEL -Wno-attributes -I$(frama-c -print-share-path)/e-acsl/ -o cfg.e-acsl cfg.e-acsl.c $(frama-c -print-share-path)/e-acsl/e_acsl_rtl.c $(frama-c -print-share-path)/../../lib/libeacsl-dlmalloc.a $(frama-c -print-share-path)/../../lib/libeacsl-gmp.a -lm
$ ./cfg.e-acsl
Assertion failed at line 5 in function func.
The failing predicate is:
\valid(ptr).
AbortedJulien SignolesJulien Signoleshttps://git.frama-c.com/pub/frama-c/-/issues/183missing E-ACSL code when ignoring asm annotation2021-03-30T13:44:49Zmantis-gitlab-migrationmissing E-ACSL code when ignoring asm annotationID0002413:
**This issue was created automatically from Mantis Issue 2413. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002413:
**This issue was created automatically from Mantis Issue 2413. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002413 | Frama-C | Plug-in > E-ACSL | public | 2018-12-05 | 2018-12-06 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | rmalak | **Assigned To** | signoles | **Resolution** | open |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | x86_64 | **OS** | Linux 4.18 OCaml 4.07.0 | **OS Version** | Debian Sid |
| **Product Version** | Frama-C 18-Argon | **Target Version** | - | **Fixed in Version** | - |
### Description :
Hi,
//////////////// asm.c
void func()
{
int i = 0;
int *ptr=&i;
/*@ assert \valid(ptr); */
*ptr = 0;
}
int main(int argc, char **argv)
{
func();
__asm__ ("");
return 0;
}
////////////////
### Additional Information :
When one comments the __asm__ line and compare the generated code, it seems that the list of missing functions are :
__e_acsl_memory_clean
__e_acsl_store_block
__e_acsl_delete_block
__e_acsl_initialize
__e_acsl_full_init
The problem is similar on Chlorine and Argon.
i and ptr could also be global static variables, it doesn't change anything
### Steps To Reproduce :
$ frama-c -machdep gcc_x86_64 asm.c -e-acsl -then-last -print -ocode eacsl_asm.c
[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl_gmp_api.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing)
[kernel] Parsing asm.c (with preprocessing)
[e-acsl] beginning translation.
[e-acsl] asm.c:11: Warning:
E-ACSL construct `asm' is not yet supported. Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
$ gcc -DE_ACSL_SEGMENT_MMODEL -Wno-attributes -I$(frama-c -print-share-path)/e-acsl/ -o asm eacsl_asm.c $(frama-c -print-share-path)/e-acsl/e_acsl_rtl.c $(frama-c -print-share-path)/../../lib/libeacsl-dlmalloc.a $(frama-c -print-share-path)/../../lib/libeacsl-gmp.a -lm
$ ./asm
Assertion failed at line 5 in function func.
The failing predicate is:
\valid(ptr).
Aborted
## Attachments
- [asm.c](/uploads/82f7e07cbdb3e0f4c91f1bc55aa7f411/asm.c)Julien SignolesJulien Signoleshttps://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/249Model Variables in Frama C2021-02-22T13:33:10Zmantis-gitlab-migrationModel Variables in Frama CID0002397:
**This issue was created automatically from Mantis Issue 2397. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002397:
**This issue was created automatically from Mantis Issue 2397. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002397 | Frama-C | Kernel > ACSL implementation | public | 2018-08-27 | 2018-08-27 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | NewUser | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | N/A |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 17-Chlorine | **Target Version** | - | **Fixed in Version** | - |
### Description :
The model variables in FramaC are giving errors whenever I tried to use them in specification
e.g the following code in ACSL manual complaints at line 3 (unexpected token 'forbidden'):
/* public interface */
//@ model set<integer> forbidden = \empty;
/*@ assigns forbidden;
ensures ! ( \result \in \old(forbidden)) &&
\result \in forbidden && \subset(\old(forbidden),forbidden);
*/
int gen();
p.s: please share if any further examples of model variables available in FramaC?Virgile PrevostoVirgile Prevosto