frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2021-02-22T13:34:00Zhttps://git.frama-c.com/pub/frama-c/-/issues/310syntax error before loop contract reported after loop contract2021-02-22T13:34:00ZJochen Burghardtsyntax error before loop contract reported after loop contractID0002297:
**This issue was created automatically from Mantis Issue 2297. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002297:
**This issue was created automatically from Mantis Issue 2297. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002297 | Frama-C | Kernel | public | 2017-05-08 | 2017-12-06 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | maroneze | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Phosphorus-20170501-beta1 | **OS** | xubuntu 16.04.1 | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C 16-Sulfur |
### Description :
Running "frama-c -wp synt.c" gives the output:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing synt.c (with preprocessing)
[kernel] syntax error at synt.c:7:
5 loop assigns i,s;
6 loop variant 9-i;
7 */
^^^
8 for (int i=0; i<9; ++i)
9 s += 2;
[kernel] Frama-C aborted: invalid user input.
This suggests that there is some syntax error within the loop contract (and it often takes a long time to check the contract byte by byte for correctness). However, the error is the missing semi-colon in line 3, immediately before the contract.
## Attachments
- [synt.c](/uploads/394b26965a65ecc018ff2e8c94d2008b/synt.c)https://git.frama-c.com/pub/frama-c/-/issues/309E-ACSL generates functions definitions without argument-names2021-02-22T12:58:57Zmantis-gitlab-migrationE-ACSL generates functions definitions without argument-namesID0002303:
**This issue was created automatically from Mantis Issue 2303. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002303:
**This issue was created automatically from Mantis Issue 2303. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002303 | Frama-C | Plug-in > E-ACSL | public | 2017-05-29 | 2017-12-06 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | evdenis | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | - | **Fixed in Version** | Frama-C 16-Sulfur |
### Description :
Test:
extern int test(int *);
static inline int test2(int *a)
{
return test(a);
}
Output:
...
/*@
predicate diffSize{L1, L2}(ℤ i) =
\at(__e_acsl_heap_allocation_size,L1) -
\at(__e_acsl_heap_allocation_size,L2) ≡ i;
*/
/*@ assigns \result;
assigns \result \from \nothing; */
int __gen_e_acsl_test(int *);
/*@ assigns \result;
assigns \result \from \nothing; */
extern int test(int *);
...
/*@ assigns \result;
assigns \result \from \nothing; */
int __gen_e_acsl_test(int *) // <== ERROR
{
int __retres;
__retres = test();
return __retres;
}
### Additional Information :
Possible fix:
diff --git a/dup_functions.ml b/dup_functions.ml
index e87ce02..d447353 100644
--- a/dup_functions.ml
+++ b/dup_functions.ml
@@ -157,10 +157,22 @@ let dup_funspec tbl bhv spec =
end in
Cil.visitCilFunspec o spec
+
+let gen_name name idnum =
+ if name = ""
+ then
+ let id = idnum + 1 in
+ ("__e_acsl_tmp_var_" ^ string_of_int (id), id)
+ else
+ (name, idnum)
+
let dup_fundec loc spec bhv kf vi new_vi =
new_vi.vdefined <- true;
let formals = Kernel_function.get_formals kf in
- let new_formals = List.map (fun vi -> Cil.copyVarinfo vi vi.vname) formals in
+ let idnum : int ref = ref 0 in
+ let new_formals = List.map (fun vi -> let (name, id) = gen_name vi.vname !idnum in
+ (idnum := id);
+ Cil.copyVarinfo vi name) formals in
let res =
let ty = Kernel_function.get_return_type kf in
if Cil.isVoidType ty then None
### Steps To Reproduce :
frama-c -main test2 -e-acsl-prepare -rte -rte-precond ./argument_names.c -then -e-acsl -then-last -print
## Attachments
- [argument_names.c](/uploads/f6a48e4adf8624e308ef43220f1b2a94/argument_names.c)
- [argument_names.patch](/uploads/2f81a843d78ef5f5e7d9a9a21c2d9c14/argument_names.patch)https://git.frama-c.com/pub/frama-c/-/issues/308E-ACSL: compilation fail: generated functions doesn't have static inline attr...2021-02-22T12:58:55Zmantis-gitlab-migrationE-ACSL: compilation fail: generated functions doesn't have static inline attributesID0002304:
**This issue was created automatically from Mantis Issue 2304. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002304:
**This issue was created automatically from Mantis Issue 2304. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002304 | Frama-C | Plug-in > E-ACSL | public | 2017-05-29 | 2017-12-06 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | evdenis | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | - | **Fixed in Version** | Frama-C 16-Sulfur |
### Description :
The absence of static inline attributes forces optional dependencies to be strict. This leads to undefined reference errors during compilation.
Test (inline.c):
extern int do_mmap(int *a);
static inline int test_extern(int *a) // Static inline
{
return do_mmap(a);
}
int main(void)
{
return 0;
}
GCC Run:
$ gcc ./inline.c # There is no error about do_mmap
$ echo $?
0
Generated Code (inline_generated.c):
...
/*@ assigns \result, *a;
assigns \result \from *a;
assigns *a \from *a; */
int __gen_e_acsl_do_mmap(int *a);
...
__inline static int test_extern(int *a)
{
int tmp;
/*@ behavior pre_do_mmap:
assigns tmp, *a;
assigns tmp \from *a;
assigns *a \from *a;
*/
tmp = __gen_e_acsl_do_mmap(a);
return tmp;
}
...
/*@ assigns \result, *a;
assigns \result \from *a;
assigns *a \from *a; */
int __gen_e_acsl_do_mmap(int *a) // <== ERROR
{
int __retres;
__retres = do_mmap(a);
return __retres;
}
GCC Run:
$ gcc ./inline_generated.c
/tmp/cczBUd0r.o: In function `__gen_e_acsl_do_mmap':
inline_generated.c:(.text+0x24): undefined reference to `do_mmap'
collect2: error: ld returned 1 exit status
### Additional Information :
Quickfix:
diff --git a/dup_functions.ml b/dup_functions.ml
index 5774115..3b25fde 100644
--- a/dup_functions.ml
+++ b/dup_functions.ml
@@ -197,6 +197,8 @@ let dup_global loc old_prj spec bhv kf vi new_vi =
let name = vi.vname in
Options.feedback ~dkey ~level:2 "entering in function %s" name;
let fundec = dup_fundec loc spec bhv kf vi new_vi in
+ fundec.svar.vinline <- true;
+ fundec.svar.vstorage <- Static;
let fct = Definition(fundec, loc) in
let new_spec = fundec.sspec in
let new_kf = { fundec = fct; spec = new_spec } in
### Steps To Reproduce :
frama-c -e-acsl-prepare -rte -rte-precond ./inline.c -then -e-acsl -then-last -print > inline_generated.c
gcc inline_generated.c
## Attachments
- [inline.c](/uploads/c2d9a86ad5918510e45daae55935ae17/inline.c)
- [inline.patch](/uploads/df7aafd5ea9cdab056e99d6bec1a5365/inline.patch)https://git.frama-c.com/pub/frama-c/-/issues/307predicate overloading causes crash when multiple files are given to wp2021-02-22T14:01:23ZJochen Burghardtpredicate overloading causes crash when multiple files are given to wpID0002151:
**This issue was created automatically from Mantis Issue 2151. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002151:
**This issue was created automatically from Mantis Issue 2151. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002151 | Frama-C | Kernel > ACSL implementation | public | 2015-07-30 | 2017-12-06 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | duplicate |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | Sodium-20150201 | **OS** | xubuntu14.04 | **OS Version** | - |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | Frama-C GIT, precise the release id |
### Description :
Running "frama-c -wp 481a.c 481b.c" on the attached files causes a crash with following output:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing 481a.c (with preprocessing)
[kernel] Parsing 481b.c (with preprocessing)
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[wp] warning: Missing RTE guards
[kernel] Current source was: 481b.c:9
The full backtrace is:
Raised at file "map.ml", line 117, characters 16-25
Called from file "list.ml", line 55, characters 20-23
Called from file "src/wp/LogicCompiler.ml", line 776, characters 17-61
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 "src/wp/Warning.ml", line 155, characters 14-18
Called from file "src/wp/cfgWP.ml", line 462, characters 23-140
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 "list.ml", line 84, characters 24-34
Called from file "src/wp/calculus.ml", line 331, characters 22-64
Called from file "src/wp/calculus.ml", line 341, characters 23-45
Called from file "src/wp/calculus.ml", line 613, characters 20-43
Called from file "src/wp/calculus.ml", line 536, characters 19-40
Called from file "src/wp/calculus.ml", line 586, characters 20-43
Called from file "src/wp/calculus.ml", line 536, characters 19-40
Called from file "src/wp/calculus.ml", line 589, characters 20-43
Called from file "src/wp/calculus.ml", line 536, characters 19-40
Called from file "src/wp/calculus.ml", line 589, characters 20-43
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/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 (Not_found).
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Sodium-20150201.
## Attachments
- [481a.c](/uploads/bbfbbd240806e1f43941db309a86ecd8/481a.c)
- [481b.c](/uploads/6eb9eab3b5ff4466235f341d5f87e5c4/481b.c)https://git.frama-c.com/pub/frama-c/-/issues/306repeated predicate definitions in separate file cause crash2021-02-22T14:01:23ZJochen Burghardtrepeated predicate definitions in separate file cause crashID0002322:
**This issue was created automatically from Mantis Issue 2322. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002322:
**This issue was created automatically from Mantis Issue 2322. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002322 | Frama-C | Kernel | public | 2017-07-31 | 2017-12-06 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | Phosphorus-20170501-beta1 | **OS** | xubuntu | **OS Version** | - |
| **Product Version** | Frama-C 15-Phosphorus | **Target Version** | - | **Fixed in Version** | Frama-C 16-Sulfur |
### Description :
Running 'frama-c -wp part.c whole.c' on the attached files causes the follwoing crash:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing part.c (with preprocessing)
[kernel] Parsing whole.c (with preprocessing)
[wp] warning: Missing RTE guards
[kernel] Current source was: whole.c:12
The full backtrace is:
Raised at file "map.ml", line 117, characters 16-25
Called from file "list.ml", line 55, characters 20-23
Called from file "src/plugins/wp/LogicCompiler.ml", line 772, characters 17-61
Called from file "src/plugins/wp/Warning.ml", line 139, characters 6-10
Called from file "src/plugins/wp/LogicSemantics.ml", line 853, characters 12-42
Called from file "src/plugins/wp/Context.ml", line 31, characters 12-17
Re-raised at file "src/plugins/wp/Context.ml", line 34, characters 41-46
Called from file "src/plugins/wp/Warning.ml", line 155, characters 14-18
Called from file "src/plugins/wp/cfgWP.ml", line 461, characters 23-135
Called from file "src/plugins/wp/Context.ml", line 68, characters 14-17
Re-raised at file "src/plugins/wp/Context.ml", line 69, characters 43-48
Called from file "src/plugins/wp/Context.ml", line 68, characters 14-17
Re-raised at file "src/plugins/wp/Context.ml", line 69, characters 43-48
Called from file "src/plugins/wp/Context.ml", line 68, characters 14-17
Re-raised at file "src/plugins/wp/Context.ml", line 69, characters 43-48
Called from file "src/plugins/wp/Context.ml", line 68, characters 14-17
Re-raised at file "src/plugins/wp/Context.ml", line 69, characters 43-48
Called from file "list.ml", line 84, characters 24-34
Called from file "src/plugins/wp/calculus.ml", line 339, characters 22-62
Called from file "src/plugins/wp/calculus.ml", line 343, characters 23-45
Called from file "src/plugins/wp/calculus.ml", line 647, characters 20-43
Called from file "src/plugins/wp/calculus.ml", line 606, characters 19-40
Called from file "src/plugins/wp/calculus.ml", line 757, characters 40-59
Called from file "set.ml", line 305, 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 "src/plugins/wp/calculus.ml", line 757, characters 4-64
Called from file "src/plugins/wp/calculus.ml", line 793, characters 19-51
Called from file "src/plugins/wp/cfgWP.ml", line 1468, characters 43-66
Called from file "src/plugins/wp/Context.ml", line 68, characters 14-17
Re-raised at file "src/plugins/wp/Context.ml", line 69, characters 43-48
Called from file "src/plugins/wp/cfgWP.ml", line 1456, characters 14-957
Called from file "src/plugins/wp/Model.ml", line 120, characters 17-20
Re-raised at file "src/plugins/wp/Model.ml", line 125, characters 25-28
Called from file "src/plugins/wp/Model.ml", line 126, characters 19-36
Called from file "src/plugins/wp/register.ml", line 654, characters 15-40
Called from file "src/libraries/stdlib/extlib.ml", line 299, characters 14-17
Re-raised at file "src/libraries/stdlib/extlib.ml", line 299, characters 47-48
Called from file "src/libraries/stdlib/extlib.ml", line 300, characters 2-12
Called from file "src/libraries/stdlib/extlib.ml", line 300, characters 2-12
Called from file "queue.ml", line 134, characters 6-20
Called from file "src/kernel_internals/runtime/boot.ml", line 37, characters 4-20
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 789, characters 2-9
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 819, characters 18-64
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 228, characters 4-8
Unexpected error (Not_found).
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Phosphorus-20170501-beta1.
The problem disappears if:
* the source file order is exchanged on the command line,
* the overloaded predicate 'Bnd(integer n)' in while.c:5 is renamed e.g. to 'Bnd2',
* the trivial 'ensures' clause is removed in whole.c:10, or
* the 'requires' clause in whole.c:9 is changed to 'Bnd(1,(int)0)', i.e. 'Bnd' is inlined.
## Attachments
- [part.c](/uploads/d19b970ae0a4ede44f1a974e55fcd0b9/part.c)
- [whole.c](/uploads/2cc05d6d85775174d51049260a279891/whole.c)https://git.frama-c.com/pub/frama-c/-/issues/305the return statement of a called function was wrongly removed2021-02-22T13:36:13Zmantis-gitlab-migrationthe return statement of a called function was wrongly removedID0002302:
**This issue was created automatically from Mantis Issue 2302. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002302:
**This issue was created automatically from Mantis Issue 2302. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002302 | Frama-C | Plug-in > slicing | public | 2017-05-23 | 2017-12-06 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Yangyibiao | **Assigned To** | Nikolai_Kosmatov | **Resolution** | fixed |
| **Priority** | high | **Severity** | major | **Reproducibility** | always |
| **Platform** | x86_64 | **OS** | Ubuntu | **OS Version** | Ubuntu 16.04.4 |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | - | **Fixed in Version** | Frama-C 16-Sulfur |
### Description :
While slicing the last statement in the attached test.c file, the "return g_79;" statement in function func_2 (line 312 in the test.c file) was wrongly removed from the slice.
gcc version: gcc(Ubuntu-5.4.0-6ubuntu1~16.04.4) 5.4.0 20160609
frama-c version: Silicon-20161101
### Tags :
csmith
### Steps To Reproduce :
frama-c -cpp-command "gcc -C -E " test.c -slice-pragma main -then-on 'Slicing export' -print -ocode slice.c
gcc test.c -o test && ./test
gcc slice.c -o slice && ./slice
## Attachments
- [test.c](/uploads/adbee40e23d6254e092332570c6b656f/test.c)https://git.frama-c.com/pub/frama-c/-/issues/303Support for struct containing flexible array members2021-03-23T17:20:25Zmantis-gitlab-migrationSupport for struct containing flexible array membersID0002306:
**This issue was created automatically from Mantis Issue 2306. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002306:
**This issue was created automatically from Mantis Issue 2306. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002306 | Frama-C | Kernel | public | 2017-05-29 | 2017-12-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | evdenis | **Assigned To** | maroneze | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | - | **Fixed in Version** | - |
### Description :
Flexible array member is a feature introduced in the C99 standard of the C programming language (in particular, in section §6.7.2.1, item 16, page 103).
Test:
struct cgroup {
int a;
int b[];
};
struct {
struct cgroup cgrp;
};
Frama-c run:
$ frama-c rte_cgrp.c
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing rte_cgrp.c (with preprocessing)
rte_cgrp.c:5:[kernel] user error: field cgrp is declared with incomplete type struct cgroup
[kernel] user error: stopping on file "rte_cgrp.c" that has errors. Add '-kernel-msg-key pp'
for preprocessing command.
[kernel] Frama-C aborted: invalid user input.
### Steps To Reproduce :
frama-c rte_cgrp.c
## Attachments
- [rte_cgrp.c](/uploads/0ad8c8b6e4cd151d69fcefe6ec3fbf0d/rte_cgrp.c)Andre MaronezeAndre Maronezehttps://git.frama-c.com/pub/frama-c/-/issues/301Substraction results in unknown values2021-03-26T16:58:43Zmantis-gitlab-migrationSubstraction results in unknown valuesID0002166:
**This issue was created automatically from Mantis Issue 2166. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002166:
**This issue was created automatically from Mantis Issue 2166. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002166 | Frama-C | Plug-in > Eva | public | 2015-09-17 | 2017-12-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | kroeckx | **Assigned To** | buhler | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | - |
### Description :
This line of code has:
if (len + n >= 64) len -= n;
For callstack [SHA256_Update :: frama-test.c:19 <- main]
Before this statement / after this statement:
n ∈ [1..63]
and:
For callstack [SHA256_Update :: frama-test.c:19 <- main]
Before this statement:
len ∈ [1..1024]
After this statement:
len ∈ [--..--]
I was expecting len after this to be:
len ∈ [0..1023]
It might be non-obvious to get that completely correct from the first time, and could understand that it would be turned in:
len ∈ [-62..1023]
KurtDavid BühlerDavid Bühlerhttps://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/297suggest to provide and document a unique warning string to grep for in value-...2021-02-22T13:36:36ZJochen Burghardtsuggest to provide and document a unique warning string to grep for in value-analysis output filesID0002259:
**This issue was created automatically from Mantis Issue 2259. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002259:
**This issue was created automatically from Mantis Issue 2259. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002259 | Frama-C | Plug-in > Eva | public | 2016-11-28 | 2017-12-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | text | **Reproducibility** | N/A |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Aluminium | **Target Version** | Frama-C 15-Phosphorus | **Fixed in Version** | - |
### Description :
When running Frama-C value analysis with parameters that cause a huge output file, it is not possible to read thourgh it line by line. (My current output file, "results.txt.gz", has the size 700 MB in gzipped format) In this case, it is only possible to use tools like "zgrep -10 -n -i 'warning:' results.txt.gz >resultsExcerpt.txt" to find relevant messages.
The value analysis manual suggests (on p.41) to grep for "assert" to get all messages that relate to a proof obligation. However, warnings about non-terminating functions are not found this way, so at least another grep for "terminat" seems necessary. More important, I can't be not sure that "assert" and "terminat" will cover all relevant messages.
Therefore I suggest to provide a single search string that will appear at every relevant message. It shouldn't fit into C's variable name syntax (so 'warning:' is ok, but 'warning' is not). It should be mentioned in the manual at a prominent place when discussing the batch (i.e. non-gui) version of value analysis; it is an essential part of the methodology then.
If there are several such strings (e.g. for different degrees of severity, like 'error:' or 'hint:'), they should all be documented in that same place. A user who has read this documentation part should be confident about how to catch all relevant messages.https://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/295Should warn for overlapping lv=lv; assignments2021-03-29T08:03:16ZPascal CuoqShould warn for overlapping lv=lv; assignmentsID0000945:
**This issue was created automatically from Mantis Issue 945. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000945:
**This issue was created automatically from Mantis Issue 945. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000945 | Frama-C | Plug-in > Eva | public | 2011-09-01 | 2017-12-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | maroneze | **Resolution** | open |
| **Priority** | low | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20110201 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Frama-C should warn for this program:
struct S { int x; int y; };
struct T { int z; struct S s; };
union U { struct S f ; struct T g; } u;
main(){
u.f = u.g.s;
return 0;
}
6.5.16.1 3:
If the value being stored in an object is read from another object that overlaps in any way the storage of the first object, then the overlap shall be exact and the two objects shall have qualified or unqualified versions of a compatible type; otherwise, the behavior is undefined.Andre MaronezeAndre Maronezehttps://git.frama-c.com/pub/frama-c/-/issues/294opam upgrade/update failed to update frama-c2021-02-22T12:58:31Zmantis-gitlab-migrationopam upgrade/update failed to update frama-cID0002335:
**This issue was created automatically from Mantis Issue 2335. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002335:
**This issue was created automatically from Mantis Issue 2335. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002335 | Frama-C | Kernel | public | 2017-12-07 | 2017-12-29 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | cdelord | **Assigned To** | maroneze | **Resolution** | unable to reproduce |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | Linux x86_64 | **OS** | Fedora | **OS Version** | 26 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
opam refuses to upgrade from Frama-C Phosphorus to Sulfur because of dependency issues with the legacy frama-c-base package.
### Additional Information :
Workaround: opam remove frama-c-base
### Steps To Reproduce :
(previous version of frama-c installed with opam)
opam update
opam upgradehttps://git.frama-c.com/pub/frama-c/-/issues/293Incorrect overflow and cast assertions for bitfields2021-02-22T13:36:38ZKostyantyn VorobyovIncorrect overflow and cast assertions for bitfieldsID0002314:
**This issue was created automatically from Mantis Issue 2314. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002314:
**This issue was created automatically from Mantis Issue 2314. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002314 | Frama-C | Plug-in > RTE | public | 2017-06-26 | 2017-12-29 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | kvorobyov | **Assigned To** | signoles | **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** | - |
### Description :
The following snippet:
struct STR { int num : 7; };
void foo(int a, long b) {
struct STR s = { .num = 0 };
s.num = b;
s.num += a;
}
generates the following assertions
/*@ assert rte: signed_downcast: b ≤ 2147483647; */
/*@ assert rte: signed_downcast: -2147483648 ≤ b; */
s.num = (int)b;
/*@ assert rte: signed_overflow: -2147483648 ≤ (int)s.num + a; */
/*@ assert rte: signed_overflow: (int)s.num + a ≤ 2147483647; */
s.num = (int)((int)s.num + a);
The limits for s.num are incorrect, since s.num is a bitfield of 7 bits its limits should be [-64, 63]
### Steps To Reproduce :
frama-c -machdep x86_64 file.c -rte -warn-signed-overflow -warn-signed-downcast -print
## Attachments
- [b.c](/uploads/40289826f17e8973d35c95cb375e1d60/b.c)
- [patch-downcast-rte](/uploads/f5123ced359a007c0de00ba52c7fc3cd/patch-downcast-rte)https://git.frama-c.com/pub/frama-c/-/issues/291Incorrect dependency assignment using arraay inside for loop2021-02-22T13:12:37Zmantis-gitlab-migrationIncorrect dependency assignment using arraay inside for loopID0002341:
**This issue was created automatically from Mantis Issue 2341. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002341:
**This issue was created automatically from Mantis Issue 2341. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002341 | Frama-C | Plug-in > from | public | 2018-01-11 | 2018-01-11 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jaimeabe | **Assigned To** | yakobowski | **Resolution** | no change required |
| **Priority** | urgent | **Severity** | major | **Reproducibility** | always |
| **Platform** | Linux | **OS** | Ubuntu | **OS Version** | 16.04.3 LTS (GN |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | - | **Fixed in Version** | - |
### Description :
In the attached file, the dependencies Analysis result should be GlobalVector[3] FROM Schalter dependent. However, the reality is that it assigns the dependenciy of Schalter to the whole vector (GlobalVector[0..4]).
### Steps To Reproduce :
Call the -deps Option in frama-c from command line using the attached file.
## Attachments
- [arrayInLoop.c](/uploads/54a6bd7ff7988631cf94538bcc12e52e/arrayInLoop.c)https://git.frama-c.com/pub/frama-c/-/issues/290How to use the "Callers ..." context menu item2021-02-22T12:58:22Zmantis-gitlab-migrationHow to use the "Callers ..." context menu itemID0001431:
**This issue was created automatically from Mantis Issue 1431. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001431:
**This issue was created automatically from Mantis Issue 1431. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001431 | Frama-C | Graphical User Interface | public | 2013-05-27 | 2018-01-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dhekir | **Assigned To** | maroneze | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130401 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Pardon the ignorance, but I couldn't find this on the manual...
I have a program where, after parsing, some warnings of this form are emitted:
"Calling undeclared function __builtin_swap32. Old style K&R code?"
I know there is a missing source file somewhere in my project, but I'd like to know who is calling these functions (since they are never directly called in my code). So I right-click on the function prototype on the GUI, and the last button in the context menu is "Callers ...". If I click on it, the "Launching analysis" window is displayed, with no indication of which analysis to choose.
I suppose the analysis I'd like is "Syntactic callgraph". So I choose it, without customizing any options, click Execute, but nothing changes. The "Callers ..." button is always visible when right-clicking the function declaration.
I noticed that if I choose the "Users" analysis, when right-clicking afterwards there is no more "Callers ..." button on the context menu, but I fail to see how any of the new options (e.g. Dependencies) could help me identify the function callers.
Is there a simpler way, other than by manually parsing the DOT file (the produced graph is too large for me to visually inspect it), to obtain information about function callers?Andre MaronezeAndre Maronezehttps://git.frama-c.com/pub/frama-c/-/issues/289std::bad_alloc not supported2021-02-22T12:58:19ZJens Gerlachstd::bad_alloc not supportedID0002342:
**This issue was created automatically from Mantis Issue 2342. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002342:
**This issue was created automatically from Mantis Issue 2342. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002342 | Frama-C | Plug-in > clang | public | 2018-01-18 | 2018-01-18 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | linux | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Attached is a simple C++ (03) program that checks whether 'new' has thrown an exception.
I am not yet sure whether this is due to general lack of exceptions or just a library issue.
I report just for completeness.
### Steps To Reproduce :
Call 'frama-c -val new_bad_alloc.cpp'
## Attachments
- [new_bad_alloc.cpp](/uploads/d2abd5208e0f45238cee308e702b69b7/new_bad_alloc.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/288range based for loop from C++11 not supported2021-02-22T12:58:19ZJens Gerlachrange based for loop from C++11 not supportedID0002345:
**This issue was created automatically from Mantis Issue 2345. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002345:
**This issue was created automatically from Mantis Issue 2345. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002345 | Frama-C | Plug-in > clang | public | 2018-01-19 | 2018-01-19 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | virgile | **Resolution** | open |
| **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 :
The attached example compiles without waring in C++11 mode
g++ --std=c++11 -Wall -c -o range_based_for_loop.o range_based_for_loop.cpp
but it fails with
frama-c -val range_based_for_loop.cpp
Error message says:
[kernel] user error: Failed to parse C++ file. See Clang messages for more information
[kernel] user error: stopping on file "range_based_for_loop.cpp" that has errors.
[kernel] Frama-C aborted: invalid user input.
## Attachments
- [range_based_for_loop.cpp](/uploads/06215bb4a9f91910a1a0bacff4ffa79f/range_based_for_loop.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/287C++11 delegating constructor not supported2021-02-22T12:58:18ZJens GerlachC++11 delegating constructor not supportedID0002346:
**This issue was created automatically from Mantis Issue 2346. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002346:
**This issue was created automatically from Mantis Issue 2346. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002346 | Frama-C | Plug-in > clang | public | 2018-01-19 | 2018-01-19 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | virgile | **Resolution** | open |
| **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 :
The attached two examples for with g++ in C++11 mode.
The first example is pure C++03. Fram-Clang can handle it.
The second version uses a delegation constructor.
Frama-Clang fails on this one with the error message:
frama-c -val object_construction2.cpp
[kernel] Parsing object_construction2.cpp (external front-end)
Unsupported constructor initializer:SomeType
Aborting
[kernel] user error: Failed to parse C++ file. See Clang messages for more information
[kernel] user error: stopping on file "object_construction2.cpp" that has errors.
[kernel] Frama-C aborted: invalid user input.
### Additional Information :
frama-clang 0.0.4
## Attachments
- [object_construction1.cpp](/uploads/9470c7f8b2af8d771a6a8e48784a42c4/object_construction1.cpp)
- [object_construction2.cpp](/uploads/7f0b7bc342fb3b3b749aafd7bce30c70/object_construction2.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/286direct initialisation of bool by nullptr2021-02-22T13:36:06ZJens Gerlachdirect initialisation of bool by nullptrID0002347:
**This issue was created automatically from Mantis Issue 2347. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002347:
**This issue was created automatically from Mantis Issue 2347. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002347 | Frama-C | Plug-in > clang | public | 2018-01-22 | 2018-01-23 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | - |
### Description :
The attached program "nullptr_crash.cpp" compiles without warnings with g++-7.2 in C++11 mode.
Clang-5.0 issues a warning (and if I understood the standard correctly, it shouldn't, because the example uses "direct initialisation").
Frama-Clang crashes on the example.
The second example "nullptr_bool.cpp" which uses "copy initialisation" only warns about implicit conversion...
## Attachments
- [nullptr_crash.cpp](/uploads/7975ccda4df20b073580f91557d4e559/nullptr_crash.cpp)
- [nullptr_bool.cpp](/uploads/cecfd360ef834b1bcbf7a7a9606df04f/nullptr_bool.cpp)
- [nullptr_no_crash.cpp](/uploads/7bfd118ea401a367676355d8352849c2/nullptr_no_crash.cpp)Virgile PrevostoVirgile Prevosto