frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2021-02-22T12:59:09Zhttps://git.frama-c.com/pub/frama-c/-/issues/315Parser does not handle mixed concatenations of wide and non-wide strings2021-02-22T12:59:09ZPascal CuoqParser does not handle mixed concatenations of wide and non-wide stringsID0001467:
**This issue was created automatically from Mantis Issue 1467. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001467:
**This issue was created automatically from Mantis Issue 1467. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001467 | Frama-C | Kernel | public | 2013-08-07 | 2017-12-06 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | valentin.perrelle | **Resolution** | fixed |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130601 | **Target Version** | - | **Fixed in Version** | Frama-C 16-Sulfur |
### Description :
~/ppc $ cat tests/misc/wstring_phase6.i
/* run.config
OPT: -journal-disable -print
*/
// See http://stackoverflow.com/questions/18102502/mixing-wide-and-narrow-string-literals-in-c
main(){
printf( "%s\n", "123" "456" );
printf( "%ls\n", L"123" L"456" );
printf( "%ls\n", "123" L"456" );
printf( "%ls\n", L"123" "456" );
printf( "%ls\n", L"123" L"456" );
}
~/ppc $ bin/toplevel.opt -print tests/misc/wstring_phase6.i
tests/misc/wstring_phase6.i:9:[kernel] user error: syntax error
[kernel] user error: skipping file "tests/misc/wstring_phase6.i" that has errors.
[kernel] Frama-C aborted: invalid user input.
~/ppc $
### Additional Information :
As commented in the test, the behavior is defined and is explained in http://stackoverflow.com/questions/18102502/mixing-wide-and-narrow-string-literals-in-chttps://git.frama-c.com/pub/frama-c/-/issues/314File frama-c/libc/features.h should include definition of the macro __GNUC_PR...2021-04-01T21:06:09ZJochen BurghardtFile frama-c/libc/features.h should include definition of the macro __GNUC_PREREQ from file /usr/include/features.hID0002253:
**This issue was created automatically from Mantis Issue 2253. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002253:
**This issue was created automatically from Mantis Issue 2253. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002253 | Frama-C | Kernel > libc | public | 2016-10-17 | 2017-12-06 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | maroneze | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | xubuntu | **OS Version** | - |
| **Product Version** | Frama-C Aluminium | **Target Version** | - | **Fixed in Version** | Frama-C 16-Sulfur |
### Description :
The macro __GNUC_PREREQ is used in many system include files. It is defined in referring to "/usr/include/features.h"l.
However, a "#include <features.h>" directive is redirected by Frama-C to (e.g.) "~/.opam/system/share/frama-c/libc/features.h" which doesn't define the macro.
Adding the definition there wouldn't cause any harm (? - at least, I can't think of any) and would help to make more system include files work with Frama-C.https://git.frama-c.com/pub/frama-c/-/issues/313compilation fails on i386 with gcc-72021-02-22T13:40:00ZRalf Treinencompilation fails on i386 with gcc-7ID0002328:
**This issue was created automatically from Mantis Issue 2328. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002328:
**This issue was created automatically from Mantis Issue 2328. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002328 | Frama-C | Plug-in > E-ACSL | public | 2017-09-08 | 2017-12-06 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | treinen | **Assigned To** | kvorobyov | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | have not tried |
| **Platform** | i386 | **OS** | linux | **OS Version** | debian sid |
| **Product Version** | Frama-C 15-Phosphorus | **Target Version** | Frama-C 16-Sulfur | **Fixed in Version** | Frama-C 16-Sulfur |
### Description :
we have a compilation failure of frama-c on i386. A complete log of an attempt to compile can be found here:
https://buildd.debian.org/status/fetch.php?pkg=frama-c&arch=i386&ver=20170501%2Bphosphorus%2Bdfsg-1&stamp=1502480362&raw=0
Please note that the default compiler on debian sid is gcc-7.https://git.frama-c.com/pub/frama-c/-/issues/312Command "Show callgraph" fails.2021-02-22T13:38:43Zmantis-gitlab-migrationCommand "Show callgraph" fails.ID0002270:
**This issue was created automatically from Mantis Issue 2270. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002270:
**This issue was created automatically from Mantis Issue 2270. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002270 | Frama-C | Graphical User Interface | public | 2017-01-12 | 2017-12-06 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Max P. | **Assigned To** | maroneze | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | Cygwin | **OS** | Windows 7 | **OS Version** | x64 SP1 |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | Frama-C 15-Phosphorus | **Fixed in Version** | Frama-C 16-Sulfur |
### Description :
Callgraph is not displayed with "Show callgraph".
In cygwin terminal prints as follows:
"dot" ▒▒ ▒▒▒▒ ▒▒▒▒७▒▒▒ ▒▒▒ ▒▒▒譥▒
▒▒▒▒▒▒▒▒, ▒ᯮ▒▒塞▒▒ ▒ணࠬ▒▒▒ ▒▒▒ ▒▒▒▒▒▒ 䠩▒▒▒.
In callback for signal activate, uncaught exception: DGraphModel.DotError("Error during dot execution")
Raised at file "format.ml", line 185, characters 41-52
Called from file "format.ml", line 427, characters 6-24
### Additional Information :
Callgraph plug-in was run with default settings. File dgraph######.dot was created in cygwin64/tmp directory successfully.
### Steps To Reproduce :
In GUI select Analises -> Show callgraphhttps://git.frama-c.com/pub/frama-c/-/issues/311opam installation of frama-c-base fails2021-02-22T12:59:01Zmantis-gitlab-migrationopam installation of frama-c-base failsID0002331:
**This issue was created automatically from Mantis Issue 2331. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002331:
**This issue was created automatically from Mantis Issue 2331. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002331 | Frama-C | Kernel > Makefile | public | 2017-11-07 | 2017-12-06 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | seberoon | **Assigned To** | bobot | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | mac | **OS** | mac os | **OS Version** | 10.11.6 |
| **Product Version** | Frama-C 15-Phosphorus | **Target Version** | - | **Fixed in Version** | Frama-C 16-Sulfur |
### Description :
Following opam installation instructions at https://frama-c.com/install-phosphorus-20170501.html#installing-frama-c-on-mac-os-x.
All ok up until opam install frama-c-base, which fails:
# File "src/plugins/wp/qed/src/numbers.mll", line 131, characters 18-19:
# Error: This expression has type string but an expression was expected of type
# bytes
This is using a fresh installation of homebrew and opam.
### Additional Information :
Mac OS 10.11.6
Xcode 8.2.1
## Attachments
- [frama-c_install_fail.txt](/uploads/21e1e50e3f88505149e7ba982b3583b9/frama-c_install_fail.txt)https://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/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/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/284BTS does not allow do select "Frama-C 16 Sulfur" as "Product Version"2021-02-22T12:58:14ZJens GerlachBTS does not allow do select "Frama-C 16 Sulfur" as "Product Version"ID0002343:
**This issue was created automatically from Mantis Issue 2343. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002343:
**This issue was created automatically from Mantis Issue 2343. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002343 | Frama-C | Documentation | public | 2018-01-18 | 2018-01-31 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 16-Sulfur | **Target Version** | - | **Fixed in Version** | Frama-C 16-Sulfur |
### Description :
BTS does not allow do select "Frama-C 16 Sulfur" as "Product Version" ...https://git.frama-c.com/pub/frama-c/-/issues/282no diagnostics on wrong keyword2021-03-30T07:48:10ZJens Gerlachno diagnostics on wrong keywordID0002351:
**This issue was created automatically from Mantis Issue 2351. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002351:
**This issue was created automatically from Mantis Issue 2351. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002351 | Frama-C | Plug-in > clang | public | 2018-01-31 | 2018-01-31 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 16-Sulfur | **Target Version** | - | **Fixed in Version** | - |
### Description :
The attached ACSL/C code contains a typo in the assigns clause:
"assign" instead of "assigns".
Frama-Clang provides no diagnostic message on this
frama-c -wp -wp-rte wrong_keyword.cpp
[kernel] Parsing wrong_keyword.cpp (external front-end)
Now output intermediate result
[rte] annotating function foo
[wp] 0 goal scheduled
[wp] Proved goals: 0 / 0
When processed as a normal C file by Frama-C/WP a more appropriated message is shown
frama-c -wp -wp-rte wrong_keyword.c
[kernel] Parsing wrong_keyword.c (with preprocessing)
wrong_keyword.c:5:[kernel] user error: unexpected token 'a'
[kernel] user error: stopping on file "wrong_keyword.c" that has errors. Add '-kernel-msg-key pp'
for preprocessing command.
[kernel] Frama-C aborted: invalid user input.
## Attachments
- [wrong_keyword.cpp](/uploads/577364237c433e7a05c5ae2104548eda/wrong_keyword.cpp)Virgile PrevostoVirgile Prevosto