frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2021-04-15T09:17:32Zhttps://git.frama-c.com/pub/frama-c/-/issues/2435Yices options while using frama-c2021-04-15T09:17:32Zmantis-gitlab-migrationYices options while using frama-cID0000308:
**This issue was created automatically from Mantis Issue 308. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000308:
**This issue was created automatically from Mantis Issue 308. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000308 | Frama-C | Plug-in > jessie | public | 2009-10-29 | 2009-12-03 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | kalyan | **Assigned To** | cmarche | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Hi,
I have installed Frama-C [Beryllium-20090902] and using Yices installed from Yices webpage. While trying to use Yices, I end up with the following message:
command line: yices -pc 0 -smt /tmp...<file.smt>
...
yices: invalid option: -pc
...
Kalyanhttps://git.frama-c.com/pub/frama-c/-/issues/2436Jessie internal error2021-04-15T09:17:38Zmantis-gitlab-migrationJessie internal errorID0000199:
**This issue was created automatically from Mantis Issue 199. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000199:
**This issue was created automatically from Mantis Issue 199. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000199 | Frama-C | Plug-in > jessie | public | 2009-07-22 | 2009-12-03 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | lukaszc | **Assigned To** | cmarche | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090601-beta1 | **Target Version** | - | **Fixed in Version** | - |
### Description :
I've obtained the following output:
[kernel] error: unexpected error File "src/jessie/interp.ml", line 1764, characters 18-24: Assertion failed
[kernel] error: please report as `crash' at http://bts.frama-c.com
### Additional Information :
It does not crash anymore but still complains about a cast from char* to int.
This is normal since "a" is a string, it should be 'a'
I agree that Frama-C front-end should complain earlier...https://git.frama-c.com/pub/frama-c/-/issues/2437(* TODO: parameters *)2021-04-15T09:17:40ZSylvie Boldo(* TODO: parameters *)ID0000112:
**This issue was created automatically from Mantis Issue 112. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000112:
**This issue was created automatically from Mantis Issue 112. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000112 | Frama-C | Plug-in > jessie | public | 2009-06-02 | 2009-12-03 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | sboldo | **Assigned To** | cmarche | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | - |
### Description :
hello,
I am in trunk, svn version 5349.
I fell into an
assert false) (* TODO: parameters *)
which is at line 718 of jc/jc_interp_misc.ml
The C file is attached. It tackles loops with floating-point matrices.
Regards,
Sylvie Boldo
## Attachments
- [int_matrix.c](/uploads/684d06b33caba66a5c5c7b153c5f0bbb/int_matrix.c)https://git.frama-c.com/pub/frama-c/-/issues/2438Jessie: the 'R' reference seems to be not present in the current release (Rea...2021-04-15T09:17:48ZVirgile PrevostoJessie: the 'R' reference seems to be not present in the current release (Real for coq ?)ID0000027:
**This issue was created automatically from Mantis Issue 27. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |...ID0000027:
**This issue was created automatically from Mantis Issue 27. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000027 | Frama-C | Plug-in > jessie | public | 2009-04-07 | 2009-12-03 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | virgile | **Assigned To** | cmarche | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Lithium-20081201 | **Target Version** | - | **Fixed in Version** | - |
### Description :
[bug 7104 of old BTS, reported by Nicolas Stouls]
when calling
cd t.jessie
make -f t.makefile coq-goals
after a "frama-c t.c -jessie-anaysis -jessie-gui"
The following error is returned :
coqc -I coq coq/t_ctx_why.v
Error while reading (...)/t.jessie/coq/t_ctx_why.v :
File "(...)/t.jessie/coq/t_ctx_why.v", line 139, characters 46-47
Error: The reference R was not found in the current environment
make: *** [coq/t_ctx_why.vo] Erreur 1
Currently, the context file generated by Jessie (t_ctx_why.v) includes some Defintions such as :
(*Why logic*) Definition add_real : R -> R -> R.
Admitted.
but R is not defined.
Regards,
Nicolas.
### Additional Information :
Depends upon coq 8.2?https://git.frama-c.com/pub/frama-c/-/issues/2439Assertion failed with exact integer model in presence of unions2021-04-15T09:17:30Zmantis-gitlab-migrationAssertion failed with exact integer model in presence of unionsID0000341:
**This issue was created automatically from Mantis Issue 341. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000341:
**This issue was created automatically from Mantis Issue 341. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000341 | Frama-C | Plug-in > jessie | public | 2009-11-23 | 2009-12-03 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | nrousset | **Assigned To** | cmarche | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090902 | **Target Version** | - | **Fixed in Version** | - |
### Description :
(Note: union1.c is taken from the Jessie Plugin Tutorial, chapter 6)
$ frama-c -jessie -jessie-int-model exact union1.c
File "jc/jc_interp.ml", line 1629, characters 13-13:
Uncaught exception: File "jc/jc_interp.ml", line 1629, characters 13-19: Assertion failed
### Additional Information :
For some reasons, functions (logic_bitvector_of_native, logic_native_of_bitvector, tr_native_type) are commented in jc_interp_misc.ml and jc_interp.ml, but uncommenting them does not magically fix the problem.
## Attachments
- [union1.c](/uploads/282ff1e0db47c4874ee64f52e024a576/union1.c)https://git.frama-c.com/pub/frama-c/-/issues/2441Jessie: infinite or not annotated loops2021-04-15T09:17:41ZDillon ParienteJessie: infinite or not annotated loopsID0000103:
**This issue was created automatically from Mantis Issue 103. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000103:
**This issue was created automatically from Mantis Issue 103. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000103 | Frama-C | Plug-in > jessie | public | 2009-05-27 | 2009-12-03 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dpariente | **Assigned To** | cmarche | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | - |
### Description :
(This issue was previously discussed through private messages but not fully resolved. It is now recorded into the BTS for traceability reasons.)
As all POs generated by Jessie/Why from the following annotated code are automatically discharged by ATPs, one might conclude that ensures clause is also validated! Which is not the case, of course!
Source code:
//@ requires \valid(p); assigns *p; ensures *p==4; void g(int*p){
int i=0;
while(1>0) { *p=3; }
}
Commande line:
frama-c -jessie-analysis -jessie-gui file.c
What could be done in Jessie to warn users about:
- the loop for which termination condition or loop variant are not provided?
- unreachable return control point due to infinite loop (=> no post-condition can be met)?https://git.frama-c.com/pub/frama-c/-/issues/2442gWhy tries to use Alt-Ergo even if not installed2021-04-15T09:17:48ZVirgile PrevostogWhy tries to use Alt-Ergo even if not installedID0000037:
**This issue was created automatically from Mantis Issue 37. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |...ID0000037:
**This issue was created automatically from Mantis Issue 37. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000037 | Frama-C | Plug-in > jessie | public | 2009-04-07 | 2009-12-03 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | virgile | **Assigned To** | cmarche | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Lithium-20081201 | **Target Version** | - | **Fixed in Version** | - |
### Description :
[bug 7532 from old bts, reported by Boris Hollas]
gWhy correctly identifies that
- Simplify is installed
- Alt-Ergo is not installed
on my system.
Although Simplify is pre-selected in the menu "Proof", gWhy tries to run Alt-Ergo when I invoke "Prove
all obligations".
Environment: Windows XP, cygwin with bashhttps://git.frama-c.com/pub/frama-c/-/issues/2443Option -jessie-cpu-limit not taken into account in GUI2021-04-15T09:17:48ZVirgile PrevostoOption -jessie-cpu-limit not taken into account in GUIID0000034:
**This issue was created automatically from Mantis Issue 34. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |...ID0000034:
**This issue was created automatically from Mantis Issue 34. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000034 | Frama-C | Plug-in > jessie | public | 2009-04-07 | 2009-12-03 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | virgile | **Assigned To** | cmarche | **Resolution** | fixed |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Lithium-20081201 | **Target Version** | - | **Fixed in Version** | - |
### Description :
[bug 7495 from old bts, reported by David Mentré]
Hello,
When calling Frama-C/Jessie with "-jessie-cpu-limit 2 -jessie-gui", the Timeout value in the GUI is not set
to 2 but to the default 10.
To reproduce the issue:
cat minimal.c
void main(void)
{
return;
}
frama-c -jessie-analysis -jessie-atp alt-ergo -jessie-cpu-limit 2 -jessie-gui minimal.c
Yours,
davidhttps://git.frama-c.com/pub/frama-c/-/issues/2444Assertion failed in jc_interp_misc.ml2021-04-15T09:17:42Zmantis-gitlab-migrationAssertion failed in jc_interp_misc.mlID0000080:
**This issue was created automatically from Mantis Issue 80. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |...ID0000080:
**This issue was created automatically from Mantis Issue 80. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000080 | Frama-C | Plug-in > jessie | public | 2009-05-11 | 2009-11-25 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | boris | **Assigned To** | cmarche | **Resolution** | duplicate |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Lithium-20081201 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Jessie crashes on code [1] with error message [2].
Environment: Windows XP, cygwin
---------------------------------------
[1]
/*@ requires \valid(p) && \valid(q);
ensures *p == \old(*q);
ensures *q == \old(*p);
assigns *p, *q;
*/
void Swap(int *p, int *q)
{
int temp;
temp = *p;
*p = *q;
*q = temp;
}
/*@ requires \valid(a+ (0..k));
*/
void foo(int a[], int k) {
Swap(&a[0], &a[k]);
}
[2]
memory (mem-field(int_M),q_21)
in memory set (mem-field(int_M),p_20),
(mem-field(int_M),q_21)
File "jc/jc_interp_misc.ml", line 707, characters 7-7:
Uncaught exception: File "jc/jc_interp_misc.ml", line 707, characters 7-13: Assertion failed
Jessie subprocess failed: jessie -why-opt -split-user-conj -v -locs tst2.cloc tst2.jc
### Additional Information :
This bug is likely related to bug 38 http://bts.frama-c.com/view.php?id=38https://git.frama-c.com/pub/frama-c/-/issues/2445Frama-C/Jessie: memory set problem2021-04-15T09:17:47ZVirgile PrevostoFrama-C/Jessie: memory set problemID0000039:
**This issue was created automatically from Mantis Issue 39. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |...ID0000039:
**This issue was created automatically from Mantis Issue 39. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000039 | Frama-C | Plug-in > jessie | public | 2009-04-07 | 2009-11-24 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | virgile | **Assigned To** | cmarche | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Lithium-20081201 | **Target Version** | - | **Fixed in Version** | - |
### Description :
[bug 7548 from old bts, reported by Dillon Pariente]
Hello,
(Issue already sent to discussion-list, and now registred into the BTS! Sorry for this "duplication".)
Launching:
frama-c.byte.exe -jessie-analysis -jessie-gen-goals foo.c
with foo.c containing:
//*****************************************
typedef struct {int i;int j;} las;
/*@ requires \valid(a) && \valid(b);
assigns *a, *b; */
void g (int *a,int *b){ *a=11; *b=15; }
/*@ requires \valid(p) ;
assigns p->i,p->j;
*/
void f (las *p)
{ g (&(p->i), &(p->j)); }
//*****************************************
returns the following error (Jessie/Why version is 2.18):
memory (mem-field(int_M),b_21)
in memory set (mem-field(int_M),a_20),
(mem-field(int_M),b_21)
File "jc/jc_interp_misc.ml", line 716, characters 7-7:
Uncaught exception: File "jc/jc_interp_misc.ml", line 716, characters 7-13: Assertion failed
Jessie subprocess failed: jessie -why-opt -split-user-conj -v -locs foo.cloc foo.jcClaude MarchéClaude Marchéhttps://git.frama-c.com/pub/frama-c/-/issues/2446Problem to give an option to Jc in command-line with -jessie-jc-opt2021-02-22T14:04:49Zmantis-gitlab-migrationProblem to give an option to Jc in command-line with -jessie-jc-optID0000340:
**This issue was created automatically from Mantis Issue 340. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000340:
**This issue was created automatically from Mantis Issue 340. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000340 | Frama-C | Kernel | public | 2009-11-23 | 2009-11-23 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | nrousset | **Assigned To** | - | **Resolution** | duplicate |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090902 | **Target Version** | - | **Fixed in Version** | - |
### Description :
All the command-lines below produces (under Cygwin) the same error message:
frama-c -jessie -jessie-jc-opt -verify credit purse.c
frama-c -jessie -jessie-jc-opt "-verify credit" purse.c
frama-c -jessie -jessie-jc-opt '-verify credit' purse.c
[kernel] user error: option '-jessie-jc-opt' requires a string as argument
## Attachments
- [purse.c](/uploads/df9e03d933dfbc66f7870423d23c296e/purse.c)https://git.frama-c.com/pub/frama-c/-/issues/2447Unbound reference raised by Why2021-04-15T09:17:31Zmantis-gitlab-migrationUnbound reference raised by WhyID0000335:
**This issue was created automatically from Mantis Issue 335. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000335:
**This issue was created automatically from Mantis Issue 335. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000335 | Frama-C | Plug-in > jessie | public | 2009-11-20 | 2009-11-20 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | nrousset | **Assigned To** | cmarche | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090902 | **Target Version** | - | **Fixed in Version** | - |
### Description :
frama-c -jessie test.c
Computation of VCs...
File "why/test.why", line 708, characters 72-103:
Unbound reference __anonstruct_str_2_f1_my_str_1
Note: frama-c -jessie -jessie-no-regions test.c is OK
## Attachments
- [test.c](/uploads/48bf958d3cffe04ae9ecb4718153bde0/test.c)Claude MarchéClaude Marchéhttps://git.frama-c.com/pub/frama-c/-/issues/2449assertion failed in Jessie with bitfields inside union2021-04-15T09:17:32Zmantis-gitlab-migrationassertion failed in Jessie with bitfields inside unionID0000328:
**This issue was created automatically from Mantis Issue 328. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000328:
**This issue was created automatically from Mantis Issue 328. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000328 | Frama-C | Plug-in > jessie | public | 2009-11-12 | 2009-11-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | nrousset | **Assigned To** | cmarche | **Resolution** | open |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090902 | **Target Version** | - | **Fixed in Version** | - |
### Description :
See the example in the attached file.
File "jc/jc_effect.ml", line 525, characters 14-14:
Uncaught exception: File "jc/jc_effect.ml", line 525, characters 14-20: Assertion failed
## Attachments
- [test_union.c](/uploads/1dbf66dfa7ca23e32eb77c216946ffcc/test_union.c)Claude MarchéClaude Marchéhttps://git.frama-c.com/pub/frama-c/-/issues/2450Problem loading Jessie plugin on Cygwin2021-02-22T13:59:12Zmantis-gitlab-migrationProblem loading Jessie plugin on CygwinID0000324:
**This issue was created automatically from Mantis Issue 324. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000324:
**This issue was created automatically from Mantis Issue 324. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000324 | Frama-C | Kernel | public | 2009-11-05 | 2009-11-05 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | nrousset | **Assigned To** | monate | **Resolution** | no change required |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090902 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Frama-C installed from the binary distribution.
Why 2.21 installed from the source distribution.
$ frama-c
[kernel] warning: cannot load file "C:\Frama-C\lib\frama-c\plugins\Jessie.cmxs" (dynlink error "error loading shared library: Cannot resolve camlPrintf__sprintf_424")https://git.frama-c.com/pub/frama-c/-/issues/2451Linking problem while compiling Frama-C-Beryllium-20090902-why-2.21 source di...2021-04-15T09:17:32Zmantis-gitlab-migrationLinking problem while compiling Frama-C-Beryllium-20090902-why-2.21 source distribution on CygwinID0000322:
**This issue was created automatically from Mantis Issue 322. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000322:
**This issue was created automatically from Mantis Issue 322. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000322 | Frama-C | Plug-in > jessie | public | 2009-11-04 | 2009-11-05 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | nrousset | **Assigned To** | monate | **Resolution** | no change required |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090902 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Packing lib/plugins/Ltl_to_acsl.cmxs
d:\Program Files\bin\..\lib\gcc\mingw32\3.4.5\..\..\..\..\mingw32\bin\ld.exe: d:\DOCUME~1\nrousset\LOCALS~1\Temp\dyndll5fd028.o: bad reloc address 0x74 in section `.data'
collect2: ld returned 1 exit status
** Fatal error: Error during linking
File "caml_startup", line 1, characters 0-1:
Error: Error during linking
make: *** [lib/plugins/Ltl_to_acsl.cmxs] Error 2
### Additional Information :
I have OCaml 3.11.0 binary distribution for Windows / MinGW
$ ld -version
GNU ld (GNU Binutils) 2.18.50.20080625
Copyright 2007 Free Software Foundation, Inc.
This program is free software; you may redistribute it under the terms of
the GNU General Public License version 3 or (at your option) a later version.
This program has absolutely no warranty.https://git.frama-c.com/pub/frama-c/-/issues/2453Recursive logic definitions are not correctly translated.2021-04-15T09:17:37ZFrançois BobotRecursive logic definitions are not correctly translated.ID0000222:
**This issue was created automatically from Mantis Issue 222. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000222:
**This issue was created automatically from Mantis Issue 222. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000222 | Frama-C | Plug-in > jessie | public | 2009-08-27 | 2009-11-03 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | bobot | **Assigned To** | cmarche | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C Beryllium-20090902 |
### Description :
The example 2.33 (p44 in acsl-implementation.pdf) is not correctly translated :
/*@ logic integer max_index { L }( int t [] , integer n ) =
@ ( n ==0) ? 0 :
@ ( t [n -1]==0) ? n : max_index (t , n -1);
@*/
# frama-c -jessie max_index.c
File "why/max_index.why", line 158, characters 13-66:
Unbound variable max_index
### Additional Information :
id : 6016https://git.frama-c.com/pub/frama-c/-/issues/2454Unbound variable raised by why in presence of an unsafe cast2021-04-15T09:17:33Zmantis-gitlab-migrationUnbound variable raised by why in presence of an unsafe castID0000291:
**This issue was created automatically from Mantis Issue 291. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000291:
**This issue was created automatically from Mantis Issue 291. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000291 | Frama-C | Plug-in > jessie | public | 2009-10-20 | 2009-10-20 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Sylvain Boulme | **Assigned To** | cmarche | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090902 | **Target Version** | - | **Fixed in Version** | - |
### Description :
In presence of an unsafe cast (that breaks the hypothesis of non-alias between pointers of distinct types), "frama-c -jessie" crashes with the error below instead of a more friendly error message:
File "why/septype0.why", line 617, characters 44-65:
Unbound variable bitvector_alloc_table
## Attachments
- [septype0.c](/uploads/f3b13146c9eb8d192dbdad1e0daca8e6/septype0.c)Claude MarchéClaude Marchéhttps://git.frama-c.com/pub/frama-c/-/issues/2455is_finite predicate: type double expected instead of real in .jc file2021-04-15T09:17:35ZDillon Parienteis_finite predicate: type double expected instead of real in .jc fileID0000260:
**This issue was created automatically from Mantis Issue 260. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000260:
**This issue was created automatically from Mantis Issue 260. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000260 | Frama-C | Plug-in > jessie | public | 2009-09-30 | 2009-10-15 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dpariente | **Assigned To** | ayad | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090902 | **Target Version** | - | **Fixed in Version** | Frama-C Beryllium-20090902 |
### Description :
Launching: frama-c -jessie foo.c
with foo.c containing:
double f(double a , double b )
{
double t ;
t = 0.0;
//@ assert \is_finite((double)(a-b));
t = a - b;
return (t);
}
yields:
File "foo.jc", line 36, characters 56-71: typing error: type double expected instead of real
[jessie] user error: Jessie subprocess failed: jessie -why-opt -split-user-conj -v -locs foo.cloc foo.jc
":> real" in foo.jc should be removed when used within "is_finite_double" predicate, not?
Regards,
Dillonhttps://git.frama-c.com/pub/frama-c/-/issues/2456Frama-C/Jessie: typing error2021-04-15T09:17:47ZVirgile PrevostoFrama-C/Jessie: typing errorID0000040:
**This issue was created automatically from Mantis Issue 40. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |...ID0000040:
**This issue was created automatically from Mantis Issue 40. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000040 | Frama-C | Plug-in > jessie | public | 2009-04-07 | 2009-10-15 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | virgile | **Assigned To** | cmarche | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Lithium-20081201 | **Target Version** | - | **Fixed in Version** | - |
### Description :
[bug 7554 from old bts, reported by Dillon Pariente]
Hello,
The two following files can be compiled separately:
//===== FILE FOO.c
typedef struct {float k;} las;
void g (float * y);
void f (las *c) { g(&(c->k)); }
//===== FILE SPECS.h
typedef struct {float k;} las;
//@ requires \valid(c); assigns c->k;
void f (las * c);
but the command line below:
//===== COMMAND LINE
frama-c.byte.exe -jessie-analysis -jessie-gui FOO.c SPECS.h
generates the following error:
//===== STDOUT
Calling Jessie tool in subdir wholeprogram.jessie File "wholeprogram.jc", line 401, characters 15-26: typing
error: type float_P[..] expected instead of real
Jessie subprocess failed: jessie -why-opt -split-user-conj -v
-why-opt -fast-wp -separation -locs wholeprogram.cloc w
holeprogram.jcClaude MarchéClaude Marchéhttps://git.frama-c.com/pub/frama-c/-/issues/2457Problem with the "-main" option2021-02-22T13:59:21Zmantis-gitlab-migrationProblem with the "-main" optionID0000279:
**This issue was created automatically from Mantis Issue 279. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000279:
**This issue was created automatically from Mantis Issue 279. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000279 | Frama-C | Kernel | public | 2009-10-09 | 2009-10-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | cbenkimoun | **Assigned To** | monate | **Resolution** | no change required |
| **Priority** | normal | **Severity** | block | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090902 | **Target Version** | - | **Fixed in Version** | Frama-C Beryllium-20090902 |
### Description :
I've just installed Frama-c on my computer.
I try to run the first.c example which is available on your web site.
I've got an error concerning the -main option.
Here is the output:
"
[kernel] preprocessing with "C:\Cygwin\bin\gcc-3.exe -CC -E -I toto.c"
# 1 "toto.c"
# 1 "<built-in>"
# 1 "<command line>"
# 1 "toto.c"
int S=0;
int T[5];
int main (void)
{
int i;
int *p = &T[0] ;
for (i=0; i<5; i++)
{ S = S+i; *p++ = S; }
return S;
}
[kernel] user error: Could not find entry point: main
"
I don't know what to do because there is a "main" function in my example.
I tried the -lib-entry option as well but without success...
Could you please help me?
Many thanks.
Cyril.
### Additional Information :
Running on Windows Vista.
Using cygwin gcc (PPC = "C:\Cygwin\bin\gcc-3.exe -CC -E -I"https://git.frama-c.com/pub/frama-c/-/issues/2460array range in requires predicate2021-04-15T09:17:36Zmantis-gitlab-migrationarray range in requires predicateID0000256:
**This issue was created automatically from Mantis Issue 256. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000256:
**This issue was created automatically from Mantis Issue 256. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000256 | Frama-C | Plug-in > jessie | public | 2009-09-25 | 2009-09-25 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jcrown | **Assigned To** | cmarche | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090902 | **Target Version** | - | **Fixed in Version** | - |
### Description :
frama-c -main foo file.c -jessie
on code
typedef struct { int a; } A;
typedef struct { A * c[10]; } B;
typedef struct { B * c[10]; } C;
C v;
/*@.......*/
void foo(void);
wth one of the 3 contracts below on foo()
/*@ requires \valid((v.c[0 .. 9])->c[0 .. 9]); */
/*@ requires \valid((v.c[0 .. 9])->c+(0 .. 9)); */
/*@ requires \valid((v.c+(0 .. 9))->c+(0 .. 9)); */
->
Uncaught exception: File "jc/jc_interp.ml", line 939, characters 25-31: Assertion failed
on the 1st and 2nd ones,
and
file.c:8:[kernel] user error: Error during annotations analysis: expected a struct with field c
on the 3rd one.Claude MarchéClaude Marchéhttps://git.frama-c.com/pub/frama-c/-/issues/2461Assertion failed at project.ml:5632021-02-22T13:59:26ZDillon ParienteAssertion failed at project.ml:563ID0000179:
**This issue was created automatically from Mantis Issue 179. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000179:
**This issue was created automatically from Mantis Issue 179. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000179 | Frama-C | Kernel | public | 2009-07-09 | 2009-09-24 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dpariente | **Assigned To** | pascal | **Resolution** | unable to reproduce |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C Beryllium-20090901 |
### Description :
Hello,
When launching: frama-c -load state.sav
(state.sav was previously generated and saved through -save command line option),
an error is displayed:
[kernel] error: unexpected error File "src/project/project.ml", line 563, characters 11-17: Assertion failed
[kernel] error: please report as `crash' at http://bts.frama-c.com
A printexc at project.ml:563 instead of "assert false" gives:
***** Stack overflow[values] computing for function MAIN
====== INITIAL STATE ======
====== INITIAL STATE COMPUTED ======
Growing heap to 289522k bytes
Regards,
Dillonhttps://git.frama-c.com/pub/frama-c/-/issues/2462For function f(int a) ; ensures a==\old(a) may be invalid2021-02-22T13:59:27ZPatrick BaudinFor function f(int a) ; ensures a==\old(a) may be invalidID0000168:
**This issue was created automatically from Mantis Issue 168. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000168:
**This issue was created automatically from Mantis Issue 168. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000168 | Frama-C | Plug-in > Eva | public | 2009-06-29 | 2009-09-24 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | patrick | **Assigned To** | pascal | **Resolution** | no change required |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C Beryllium-20090901 |
### Description :
The command "toplevel.opt -val old.c" gives the following line:
old.c:8: Warning: Function f, behavior default: postcondition got status valid
This is wrong: the postcondition is invalid.
### Additional Information :
Revision 5634
Contents of the file old.c
int *p, *q ;
/*@ ensures *q == a ;
*/
void f (int a) {
*q = a ;
*p = 3 ;
}
int main (int x, int y) {
q = &y ;
p = &x ;
f (x) ;
return x ;
}https://git.frama-c.com/pub/frama-c/-/issues/2469Static linking of the jessie plugin fails when using a non-local Jc2021-04-15T09:17:37Zmantis-gitlab-migrationStatic linking of the jessie plugin fails when using a non-local JcID0000227:
**This issue was created automatically from Mantis Issue 227. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000227:
**This issue was created automatically from Mantis Issue 227. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000227 | Frama-C | Plug-in > jessie | public | 2009-09-01 | 2009-09-23 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | mehdi | **Assigned To** | signoles | **Resolution** | won't fix |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090601-beta1 | **Target Version** | - | **Fixed in Version** | Frama-C Beryllium-20090902 |
### Description :
Hi,
When I try to link frama-c statically with the Jessie plugin (with --with-jessie-static), the compilation fails with the following message:
File "_none_", line 1, characters 0-1:
Error: No implementations provided for the following modules:
Jc referenced from lib/plugins/Jessie.cmx
make[2]: *** [bin/toplevel.opt] Erreur 2
When using a non-local Jc, you need to add jc.cm{x,o} when linking.
Please find attached a patch that fixes this issue.
Kind regards,
## Attachments
- [0004-Add-JCCM-O-X-to-BYTE-OPT-_LIBS-when-linking-statical.patch](/uploads/56c5cfaf26e17134488d24223d6e771e/0004-Add-JCCM-O-X-to-BYTE-OPT-_LIBS-when-linking-statical.patch)https://git.frama-c.com/pub/frama-c/-/issues/2470Non-exhaustive pattern matching leads to compilation error2021-02-22T14:03:27Zmantis-gitlab-migrationNon-exhaustive pattern matching leads to compilation errorID0000224:
**This issue was created automatically from Mantis Issue 224. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000224:
**This issue was created automatically from Mantis Issue 224. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000224 | Frama-C | Kernel | public | 2009-09-01 | 2009-09-23 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | mehdi | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090601-beta1 | **Target Version** | - | **Fixed in Version** | Frama-C Beryllium-20090902 |
### Description :
Hi,
When compiling frama-c in bytecode on a non-native architecture (even if OCaml 3.11.1 is available), compilation fails due to a non-exhaustive pattern matching.
The relevant lines are:
Ocamlc src/lib/dynlink_common_interface.cmi
Generating src/lib/dynlink_common_interface.ml
Ocamlc src/lib/dynlink_common_interface.cmo
File "src/lib/dynlink_common_interface.ml", line 77, characters 25-491:
Warning P: this pattern-matching is not exhaustive.
Here is an example of a value that is not matched:
Inconsistent_implementation _
File "src/lib/dynlink_common_interface.ml", line 1, characters 0-1:
Error: Error-enabled warnings (1 occurrences)
Please find attached a (trivial) patch that fixes this bug.
OCaml 3.11.1 is available on those architectures (e.g., hppa, mips, s390) with only the bytecode backend. So why do not activate the dynlink option or those too? In the configure script, you seem to rely on the presence of dynlink.cmxa. But dynlink.cma is also present when compiling in bytecode. I hope this will be fixed too.
Best regards,
--
Mehdi
## Attachments
- [0003-Fix-weak-pattern-matching-in-dynlink_lower_311_byte..patch](/uploads/198dcab076609e75bd342527b5644f0e/0003-Fix-weak-pattern-matching-in-dynlink_lower_311_byte..patch)https://git.frama-c.com/pub/frama-c/-/issues/2472The file `share/configure.ac' is missing2021-02-22T13:59:39Zmantis-gitlab-migrationThe file `share/configure.ac' is missingID0000182:
**This issue was created automatically from Mantis Issue 182. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000182:
**This issue was created automatically from Mantis Issue 182. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000182 | Frama-C | Kernel | public | 2009-07-13 | 2009-09-23 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jonathan-Christofer Demay | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090601-beta1 | **Target Version** | - | **Fixed in Version** | Frama-C Beryllium-20090901 |
### Description :
I tried to modify configure.in and then run autoreconf, but a file is missing:
aclocal-1.11: configure.in:46: file `share/configure.ac' does not exist
autoreconf-2.63: aclocal failed with exit status: 1https://git.frama-c.com/pub/frama-c/-/issues/2473type invariants2021-04-15T09:17:46ZVirgile Prevostotype invariantsID0000025:
**This issue was created automatically from Mantis Issue 25. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |...ID0000025:
**This issue was created automatically from Mantis Issue 25. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000025 | Frama-C | Plug-in > jessie | public | 2009-04-07 | 2009-09-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | virgile | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Lithium-20081201 | **Target Version** | - | **Fixed in Version** | - |
### Description :
(bts 6836)
I tried the code-example from the 1.4 ACSL document.
void out_char(char c)
{
int col = 0;
//@ global invariant I : 0 <= col <= 79;
col++;
if (col >= 80) col = 0;
}
Doing this, I get:
$ frama-c -jessie-analysis -jessie-int-model exact -jessie-gui invariant.c
Parsing
[preprocessing] running gcc -C -E -I. -include C:\Frama-C\share\frama-c\jessie\j
essie_prolog.h -D JESSIE_EXACT_INT_MODEL -dD invariant.c
invariant.c[14:0-0] : syntax error
Parsing error
Skipping file "invariant.c" that has errors.
Cleaning unused parts
Symbolic link
Your code cannot be parsed. Aborting analysis.
Starting semantical analysis
Starting Jessie translation
Nothing to process. There was probably an error before.
Cheers Christoph
### Additional Information :
There are two issues here:
- global invariant inside function body is not implemented in
current Frama-C release
- the ACSL documentation states that global invariant are meant
to be enforced on global data. Hence they are primarily global
annotation. They can be found as code annotation when dealing
with static local variables (which are in fact global variables
with specific scoping rules), but they do not apply to plain
local variables such as col in the example aboveVirgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/2474Incorrect linking order for the viewer2021-02-22T13:59:42Zmantis-gitlab-migrationIncorrect linking order for the viewerID0000225:
**This issue was created automatically from Mantis Issue 225. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000225:
**This issue was created automatically from Mantis Issue 225. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000225 | Frama-C | Graphical User Interface | public | 2009-09-01 | 2009-09-09 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | mehdi | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090601-beta1 | **Target Version** | - | **Fixed in Version** | Frama-C Beryllium-20090901 |
### Description :
Hi,
When compiling the viewer using a system-installation of ocamlgraph, the compilation fails with the following error:
ocamlc.opt -w Ael -warn-error A -annot -I src/misc -I src/ai -I src/memory_state -I src/toplevel -I src/slicing_types -I src/pdg_types -I src/kernel -I src/logic -I src/lib -I src/project -I src/buckx -I external -I cil/src -I cil/src/ext -I cil/src/frontc -I cil/src/logic -I cil/ocamlutil -I lib/plugins -I lib -I +ocamlgraph -g -I src/gui -I +lablgtk2 -I +ocamlgraph -linkall -custom -o bin/viewer.byte nums.cma unix.cma bigarray.cma str.cma dynlink.cma src/buckx/mybigarray.o src/buckx/buckx_c.o graph.cma /usr/lib/ocaml/ocamlgraph/viewGraph.cmo /usr/lib/ocaml/ocamlgraph/viewGraph_select.cmo /usr/lib/ocaml/ocamlgraph/viewGraph_utils.cmo lablgtk.cma lablgnomecanvas.cma lablgtksourceview.cma /usr/lib/ocaml/ocamlgraph/viewGraph.cmo /usr/lib/ocaml/ocamlgraph/viewGraph_select.cmo /usr/lib/ocaml/ocamlgraph/viewGraph_utils.cmo
[...]
File "_none_", line 1, characters 0-1:
Error: Error while linking /usr/lib/ocaml/ocamlgraph/viewGraph.cmo:
Reference to undefined global `GnoCanvas'
As you can see, viewGraph.cmo (and friends) are specified twice when linking and between the two groups there is lablgnomecanvas.cma which is needed by viewGraph.cmo.
Please find attached a patch that fixes this issue.
Kind regards,
## Attachments
- [0002-Do-not-add-GRAPH_GUICMO-to-BYTE_GUI_LIBS.patch](/uploads/2a2f35dda8b3eb544d3cb94fe4af1e7b/0002-Do-not-add-GRAPH_GUICMO-to-BYTE_GUI_LIBS.patch)https://git.frama-c.com/pub/frama-c/-/issues/2478crash when unbound variable2021-02-22T13:59:47Zmantis-gitlab-migrationcrash when unbound variableID0000190:
**This issue was created automatically from Mantis Issue 190. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000190:
**This issue was created automatically from Mantis Issue 190. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000190 | Frama-C | Plug-in > slicing | public | 2009-07-15 | 2009-09-02 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | lukaszc | **Assigned To** | patrick | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Beryllium-20090901 |
### Description :
"frama-c -slice-rd y -pp-annot test.c" results in a crash
------------
test.c
------------
int x(int y, int z)
{
/*@ slice pragma expr y == 1; */
//@ assert y == 1;
//@ assert y + z == 3;
return 2*y*z1();
}
int main()
{
x(1,2);
return 0;
}
int z1()
{
return 1;
}https://git.frama-c.com/pub/frama-c/-/issues/2481crash for untyped_metrics example plugin2021-02-22T13:59:50ZStephane Dupratcrash for untyped_metrics example pluginID0000163:
**This issue was created automatically from Mantis Issue 163. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000163:
**This issue was created automatically from Mantis Issue 163. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000163 | Frama-C | Kernel | public | 2009-06-25 | 2009-09-02 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | sduprat | **Assigned To** | monate | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090601-beta1 | **Target Version** | - | **Fixed in Version** | Frama-C Beryllium-20090901 |
### Description :
when running this plugin :
> frama-c -count-for tmp1.c
> [kernel] error: unexpected error Not_found
> [kernel] error: please report as `crash' at http://bts.frama-c.comhttps://git.frama-c.com/pub/frama-c/-/issues/2482'make top' fails2021-02-22T13:59:51Zmantis-gitlab-migration'make top' failsID0000183:
**This issue was created automatically from Mantis Issue 183. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000183:
**This issue was created automatically from Mantis Issue 183. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000183 | Frama-C | Kernel | public | 2009-07-13 | 2009-09-02 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jonathan-Christofer Demay | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090601-beta1 | **Target Version** | - | **Fixed in Version** | Frama-C Beryllium-20090901 |
### Description :
frama-c-Beryllium-20090601-beta1 # make top
Ocamlc src/toplevel/toplevel_topdirs.cmo
Ocamlmktop bin/toplevel.top
Error while linking src/lib/extlib.cmo:
The external function `getperfcount' is not available
make: *** [bin/toplevel.top] Error 2https://git.frama-c.com/pub/frama-c/-/issues/2487Slicing leaves unreachable code2021-02-22T13:59:57Zmantis-gitlab-migrationSlicing leaves unreachable codeID0000194:
**This issue was created automatically from Mantis Issue 194. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000194:
**This issue was created automatically from Mantis Issue 194. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000194 | Frama-C | Plug-in > slicing | public | 2009-07-15 | 2009-08-26 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | lukaszc | **Assigned To** | Anne | **Resolution** | no change required |
| **Priority** | normal | **Severity** | tweak | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090601-beta1 | **Target Version** | - | **Fixed in Version** | - |
### Description :
/*@ requires
@ (((v1 && !(v2 && v3) && v4);
@*/
extern void fun(void)
{
if (v1) {
if (v4) {
if (v2) {
if(v3) {goto return_label;}
}
}
}
}
### Additional Information :
It would be nice if slicing could remove such code.https://git.frama-c.com/pub/frama-c/-/issues/2488An extra ')' is missing in the Printexc.record_backtrace patch on the Frama-C...2021-02-22T13:59:57Zmantis-gitlab-migrationAn extra ')' is missing in the Printexc.record_backtrace patch on the Frama-C wikiID0000181:
**This issue was created automatically from Mantis Issue 181. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000181:
**This issue was created automatically from Mantis Issue 181. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000181 | Frama-C | Kernel | public | 2009-07-13 | 2009-08-26 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jonathan-Christofer Demay | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090601-beta1 | **Target Version** | - | **Fixed in Version** | - |
### Description :
http://bts.frama-c.com/view.php?id=169 is fixed by a patch posted on the Frama-C wiki (http://bts.frama-c.com/dokuwiki/lib/exe/fetch.php?media=wiki:frama-c-beryllium-20090601-beta1.patch)
However, I think near the end an extra ')' is missing:
- (Printexc.to_string e)
- (if Parameters.Debug.get () > 0 then Printexc.get_backtrace ()
- else ""));
+ (Printexc.to_string e);
It should be:
+ (Printexc.to_string e));https://git.frama-c.com/pub/frama-c/-/issues/2489Mise en hypothèse de la précondition d'une opération appelée2021-04-15T09:17:38Zmantis-gitlab-migrationMise en hypothèse de la précondition d'une opération appeléeID0000215:
**This issue was created automatically from Mantis Issue 215. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000215:
**This issue was created automatically from Mantis Issue 215. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000215 | Frama-C | Plug-in > jessie | public | 2009-08-24 | 2009-08-25 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | nstouls | **Assigned To** | cmarche | **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 :
bonjour,
Voici donc un petit exemple en pièce jointe.
Si je souhaite le prouver avec Jessie :
frama-c t2.c -jessie &
J'obtiens 5 OP.
Celles qui m'intéressent sont les 2 OP de post-condition du main. Prenons par exemple la première des deux :
main_ensures_default_po_1
H1: true = true and (0 <= integer_of_int32(i) and integer_of_int32(i) <= 1)
result: int32
H6: (integer_of_int32(i) = 1 -> integer_of_int32(result) = 1) and
(integer_of_int32(i) = 0 -> integer_of_int32(result) = 0)
tmp: int32
H7: tmp = result
H8: integer_of_int32(tmp) <> 0
result0: int32
H9: integer_of_int32(result0) = 0
__retres: int32
H10: __retres = result0
return: int32
H11: return = __retres
----------------------------------
integer_of_int32(return) = 0
H1 correspond à la pré-condition de main
H6 est issue de l'appel de fonction f(). C'est la conjonction des assumes impliquant les ensures associés
H7 et + correspond au code de la fonction main.
Dans cet exemple, il n'y a pas d'hypothèse H5 décrivant la pré-condition de f(), alors qu'elle devrait être présente.
En l'occurrence, cette pré-condition étant équivalente à H1, tout se prouve. Mais lorsqu'il est nécessaire de faire un preuve difficile pour faire ce lien, il serait intéressant d'avoir ensuite la pré de f en hypothèse.
Merci beaucoup et bonne journée,
Nicolas.
## Attachments
- [t2.c](/uploads/81e75022140928f05c14dffa872247fd/t2.c)Claude MarchéClaude Marchéhttps://git.frama-c.com/pub/frama-c/-/issues/2490-slice-print ignored when -ocode is used2021-02-22T13:59:59Zmantis-gitlab-migration-slice-print ignored when -ocode is usedID0000191:
**This issue was created automatically from Mantis Issue 191. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000191:
**This issue was created automatically from Mantis Issue 191. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000191 | Frama-C | Plug-in > slicing | public | 2009-07-15 | 2009-07-27 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | lukaszc | **Assigned To** | signoles | **Resolution** | no change required |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090601-beta1 | **Target Version** | - | **Fixed in Version** | - |
### Description :
when I use the option -slice-print together with -ocode then -slice-print is ignoredhttps://git.frama-c.com/pub/frama-c/-/issues/2491Slicing removes more code than it should2021-02-22T14:00:01Zmantis-gitlab-migrationSlicing removes more code than it shouldID0000201:
**This issue was created automatically from Mantis Issue 201. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000201:
**This issue was created automatically from Mantis Issue 201. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000201 | Frama-C | Plug-in > slicing | public | 2009-07-24 | 2009-07-24 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | lukaszc | **Assigned To** | Anne | **Resolution** | no change required |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090601-beta1 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Slicing removes more code than it should leading to erronous results.
In the example below I wanted to leave the code which influences value of temp in fun(). To this end I used the following command. However, the obtained result (no slicing errors were indicated) presented below is not equivalnet to the input.
command-----------------------------------------------
frama-c -slice-print -slice-value temp -slicing-level 3 -main fun -lib-entry -pp-annot temp.c -ocode temp2.c
input-----------------------------------------------
#define arr *(unsigned char *)
#define Alarm1_On {arr(0) |= 0;}
#define Alarm1_Off {arr(0) |= 0;}
int temp;
int temp2;
void fun()
{
temp = 2;
fun2();
}
void fun2()
{
if (temp2)
{
temp = 0;
Alarm1_Off;
}
else
{
temp = 1;
Alarm1_On;
}
}
output----------------------------------------------
/* Generated by CIL v. 1.3.6 */
/* print_CIL_Input is false */
void fun(void)
{
return;
}https://git.frama-c.com/pub/frama-c/-/issues/2492Frama-C cannot process properly arrays of structures2021-04-15T09:17:38Zmantis-gitlab-migrationFrama-C cannot process properly arrays of structuresID0000185:
**This issue was created automatically from Mantis Issue 185. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000185:
**This issue was created automatically from Mantis Issue 185. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000185 | Frama-C | Plug-in > jessie | public | 2009-07-14 | 2009-07-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | lukaszc | **Assigned To** | cmarche | **Resolution** | open |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090601-beta1 | **Target Version** | - | **Fixed in Version** | - |
### Description :
This code leads to an error
x = &str_array[i1][i2].field1;
However, this (in fact the same code), is processed properly
struct str *temp = &str_array[i1][i2];
x = &(*temp).field1;Claude MarchéClaude Marchéhttps://git.frama-c.com/pub/frama-c/-/issues/2493Indicates errors in annotations when should not2021-02-22T14:00:04Zmantis-gitlab-migrationIndicates errors in annotations when should notID0000188:
**This issue was created automatically from Mantis Issue 188. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000188:
**This issue was created automatically from Mantis Issue 188. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000188 | Frama-C | Plug-in > slicing | public | 2009-07-14 | 2009-07-15 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | lukaszc | **Assigned To** | Anne | **Resolution** | won't fix |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
- jessie accepts this code and properly infers based on it, the slicing plug-in on the other hand indicates an error in the annotations
---------------------------------------------------------------------
test.c
---------------------------------------------------------------------
#include "test.h"
/*@
@ requires y == CONS_FROM_TEST_H_DEFINED_USING_DEFINE;
@ ensures
@ \result == 2*y;
@*/
int x(int y, int z)
{
/*@ slice pragma ctrl; */
//@ assert y == 1;
//@ assert y + z == 3;
return 2*y*z1();
}
int main()
{
x(1,2);
return 0;
}
int z1()
{
return 1;
}
-------------------------------------------------------------------------
test.h
-------------------------------------------------------------------------
#define CONS_FROM_TEST_H_DEFINED_USING_DEFINE 1https://git.frama-c.com/pub/frama-c/-/issues/2494type error in generated why file2021-04-15T09:17:39ZFabrice Derepastype error in generated why fileID0000178:
**This issue was created automatically from Mantis Issue 178. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000178:
**This issue was created automatically from Mantis Issue 178. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000178 | Frama-C | Plug-in > jessie | public | 2009-07-09 | 2009-07-09 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | derepas | **Assigned To** | cmarche | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090601-beta1 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Let us consider the following program 'simple.c':
void g(int * j, int *k) {
int tmp= *j;
*j=*k;
*k=tmp;
}
void f(int * vector, int size) {
int i=0;
if (i<size)
g (&vector[i],&vector[i+1]);
}
The command line 'frama-c -main f -jessie simple.c' generates the following error:
[kernel...] preprocessing with "gcc -C -E -I. -dD simple.c"
Starting Jessie translation
Producing Jessie files in subdir simple.jessie
File simple.jessie/simple.jc written.
File simple.jessie/simple.cloc written.
Calling Jessie tool in subdir simple.jessie
Generating Why function g
Generating Why function f
Calling VCs generator.
gwhy-bin [...] why/simple.why
Computation of VCs...
File "why/simple.why", line 552, characters 9-49:
Term i is expected to have type int
make: *** [simple.stat] Erreur 1
Jessie subprocess failed: make -f simple.makefile gui
The funny thing is that when the body of function g is empty this error does not occur (though the error seems to be in function f).Claude MarchéClaude Marchéhttps://git.frama-c.com/pub/frama-c/-/issues/2495"logic set<struct something *> f(...)" throw a syntax error2021-02-22T14:00:07ZFrançois Bobot"logic set<struct something *> f(...)" throw a syntax errorID0000096:
**This issue was created automatically from Mantis Issue 96. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |...ID0000096:
**This issue was created automatically from Mantis Issue 96. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000096 | Frama-C | Kernel | public | 2009-05-25 | 2009-07-03 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | bobot | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | Frama-C Beryllium-20090601-beta1 | **Fixed in Version** | Frama-C Beryllium-20090601-beta1 |
### Description :
============
typedef struct node {
int hd;
struct list * next;
} list;
/*@
logic set<struct node *> tata(struct node * p) = \empty;
@*/
=============
throw:
File "empty.c", line 7, characters 19-23: syntax error while parsing annotation
However there is a natural work around :
=============
/*@
logic set<list *> tata(struct node * p) = \empty;
@*/
=============
is correct.
### Additional Information :
svn id : 5303https://git.frama-c.com/pub/frama-c/-/issues/2496Order of the functions in gui2021-02-22T14:00:09Zmantis-gitlab-migrationOrder of the functions in guiID0000157:
**This issue was created automatically from Mantis Issue 157. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000157:
**This issue was created automatically from Mantis Issue 157. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000157 | Frama-C | Graphical User Interface | public | 2009-06-18 | 2009-06-25 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Anne | **Assigned To** | monate | **Resolution** | won't fix |
| **Priority** | low | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
The function list in the gui sidebar is in reverse order compared to the list of the functions in the C code.https://git.frama-c.com/pub/frama-c/-/issues/2506int -> integer -> real2022-12-25T02:32:53ZSylvie Boldoint -> integer -> realID0000117:
**This issue was created automatically from Mantis Issue 117. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000117:
**This issue was created automatically from Mantis Issue 117. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000117 | Frama-C | Kernel | public | 2009-06-05 | 2009-06-23 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | sboldo | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C Beryllium-20090601-beta1 |
### Description :
From ACSL, I assume that
"C integral types char , short , int and long , signed or unsigned, are all subtypes of type integer ;
integer is itself a subtype of type real ;"
Therefore int is a subtype of real. But it does not work in practice:
int i;
/*@ loop invariant C== \pow(2., i) */
\pow takes 2 real numbers.
This annotation is refused by the message:
Error during analysis of annotation: invalid implicit conversion from int to realhttps://git.frama-c.com/pub/frama-c/-/issues/2508Compilation error if options --with-jessie-static --with-ltl_to_acsl-static a...2021-02-22T14:00:22Zmantis-gitlab-migrationCompilation error if options --with-jessie-static --with-ltl_to_acsl-static are present.ID0000111:
**This issue was created automatically from Mantis Issue 111. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000111:
**This issue was created automatically from Mantis Issue 111. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000111 | Frama-C | Kernel | public | 2009-06-02 | 2009-06-23 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | nstouls | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | block | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C Beryllium-20090601-beta1 |
### Description :
With ocamlc 3.10.2
If the configure script is launched with following options :
--with-jessie-static --with-ltl_to_acsl-static
then this error occurs during compilation:
Ocamlc src/lib/dynlink_common_interface.cmo
The implementation src/lib/dynlink_common_interface.ml
does not match the interface src/lib/dynlink_common_interface.cmi:
The field `is_native' is required but not provided
make: *** [src/lib/dynlink_common_interface.cmo] Erreur 2
Removing configure options resolves the problem.https://git.frama-c.com/pub/frama-c/-/issues/2509Jessie: static function specification2021-02-22T14:00:24ZDillon ParienteJessie: static function specificationID0000104:
**This issue was created automatically from Mantis Issue 104. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000104:
**This issue was created automatically from Mantis Issue 104. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000104 | Frama-C | Kernel | public | 2009-05-27 | 2009-06-23 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dpariente | **Assigned To** | virgile | **Resolution** | no change required |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C Beryllium-20090601-beta1 |
### Description :
(This issue was previously discussed through private messages but not fully resolved. It is now recorded into the BTS for traceability reasons.)
An annotated header file "foo.h" contains:
//***** foo.h
/*@ requires \valid(p); assigns *p; ensures *p==3; */ void f(int *p);
and this is the related "foo.c" file:
//***** foo.c
static void f(int *p) { *p = 3; }
Command line:
frama-c.byte.exe -jessie-analysis -jessie-gui foo.c foo.h
Logical specifications from foo.h file are - apparently - not taken into account in the generated POs.https://git.frama-c.com/pub/frama-c/-/issues/2512"//@ assert i >= CHAR_MIN;" not proven for char2021-04-15T09:17:41ZJens Gerlach"//@ assert i >= CHAR_MIN;" not proven for charID0000095:
**This issue was created automatically from Mantis Issue 95. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |...ID0000095:
**This issue was created automatically from Mantis Issue 95. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000095 | Frama-C | Plug-in > jessie | public | 2009-05-25 | 2009-06-23 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | mottainai | **Assigned To** | cmarche | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Lithium-20081201 | **Target Version** | - | **Fixed in Version** | Frama-C Beryllium-20090601-beta1 |
### Description :
The first assertion in the the following code fragment is not proven.
(neither alt-ergo nor yices nor cvc3).
char char_range(char i)
{
//@ assert i >= CHAR_MIN;
//@ assert i <= CHAR_MAX;
return i;
}
### Additional Information :
I am using Frama-C Lithium-20081201 on Mac OS X 10.5.7
This is probably related to bug http://bts.frama-c.com/view.php?id=94https://git.frama-c.com/pub/frama-c/-/issues/2513"assert i >= 0;" not proven for unsigned char2021-04-15T09:17:41ZJens Gerlach"assert i >= 0;" not proven for unsigned charID0000094:
**This issue was created automatically from Mantis Issue 94. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |...ID0000094:
**This issue was created automatically from Mantis Issue 94. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000094 | Frama-C | Plug-in > jessie | public | 2009-05-25 | 2009-06-23 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | mottainai | **Assigned To** | cmarche | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Lithium-20081201 | **Target Version** | - | **Fixed in Version** | Frama-C Beryllium-20090601-beta1 |
### Description :
The first assertion in the the following code fragment is not proven.
(neither alt-ergo nor yices nor cvc3).
unsigned char uchar_range(unsigned char i)
{
//@ assert i >= 0;
//@ assert i <= UCHAR_MAX;
return i;
}
### Additional Information :
I am using Frama-C Lithium-20081201 on Mac OS X 10.5.7https://git.frama-c.com/pub/frama-c/-/issues/2517A pure predicate in an axiomatic with some "unpure" axioms have some strange ...2021-04-15T09:17:42ZFrançois BobotA pure predicate in an axiomatic with some "unpure" axioms have some strange resultsID0000073:
**This issue was created automatically from Mantis Issue 73. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |...ID0000073:
**This issue was created automatically from Mantis Issue 73. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000073 | Frama-C | Plug-in > jessie | public | 2009-04-30 | 2009-06-23 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | bobot | **Assigned To** | cmarche | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C Beryllium-20090601-beta1 |
### Description :
A pure predicate in an axiomatic with some "unpure" axioms have some strange results. In this case an assertion failed :
myc.c
============================
/*@
axiomatic myaxioms{
predicate myrelation(int p,int q);
logic int mylogic{L}(int * p);
axiom myaxiom{L} :
\forall int * p, q; \at(myrelation(mylogic(p),q),L);
}
@*/
frama-c -jessie-analysis unwanted_label.c.assertion_failed.c :
=========================
Calling Jessie tool in subdir unwanted_label.c.assertion_failed.jessie
File "jc/jc_typing.ml", line 2687, characters 20-20:
Uncaught exception: File "jc/jc_typing.ml", line 2687, characters 20-26: Assertion failed
===========================
### Additional Information :
frama-c : 5186https://git.frama-c.com/pub/frama-c/-/issues/2519frama-c --help2021-02-22T14:04:56ZGuillaume Melquiondframa-c --helpID0000061:
**This issue was created automatically from Mantis Issue 61. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |...ID0000061:
**This issue was created automatically from Mantis Issue 61. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000061 | Frama-C | Kernel | public | 2009-04-24 | 2009-06-23 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | gmelquio | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C Beryllium-20090601-beta1 |
### Description :
$ frama-c --help
frama-c: option `--help' is unknown.
Use `frama-c --help' for more information.
Yeah, right... (revision 5126)https://git.frama-c.com/pub/frama-c/-/issues/2520Jessie/Gwhy: cpulimit-win.c2021-04-15T09:17:43ZDillon ParienteJessie/Gwhy: cpulimit-win.cID0000049:
**This issue was created automatically from Mantis Issue 49. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |...ID0000049:
**This issue was created automatically from Mantis Issue 49. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000049 | Frama-C | Plug-in > jessie | public | 2009-04-11 | 2009-06-23 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dpariente | **Assigned To** | cmarche | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Beryllium-20090601-beta1 |
### Description :
Hello,
The release of cpulimit-win.c currently distributed is not the good one but an old one: it does not take into account exit code from process.
A second version was forwarded by email (on 12/07/08) correcting this bug. Please find it enclosed!
Best regards,
Dillon
## Attachments
- [cpulimit-win.c](/uploads/167e27021d0ee7a802efe50778c4d08c/cpulimit-win.c)https://git.frama-c.com/pub/frama-c/-/issues/2521Jessie/GWhy/Gappa: format file and invalid POs proved valid2021-04-15T09:17:43ZDillon ParienteJessie/GWhy/Gappa: format file and invalid POs proved validID0000046:
**This issue was created automatically from Mantis Issue 46. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |...ID0000046:
**This issue was created automatically from Mantis Issue 46. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000046 | Frama-C | Plug-in > jessie | public | 2009-04-10 | 2009-06-23 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dpariente | **Assigned To** | cmarche | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Beryllium-20090601-beta1 |
### Description :
Hello,
Under Cygwin, for the following code:
/*@ requires -1.0 <= x <= 1.0;
assigns \nothing;
ensures -1.0 <= \result <= 1.0;
*/
float f(float x) { return ( -2.0*x ); }
with command-line:
frama-c -jessie-analysis -jessie-gui faux.c
all POs are proved Valid under GWhy, even they are *not*!
In GWhy's Debug mode, standard output displays:
oblig : f_ensures_default_po_1
calling Gappa on c:\TEMP\gwhyd42d1e_why.gappa
command line: gappa < c:\TEMP\gwhyd42d1e_why.gappa
Output file c:\TEMP\outba8609:
input in flex scanner failed
...
Trying to prove the 1st PO through the following command line:
gappa c:\TEMP\gwhyd42d1e_why.gappa
yields:
Error: syntax error, unexpected $undefined at line 1 column 27
1/ It seems that gappa files are expected to be in UNIX format, and not in DOS' one (i.e. with CR/LF ending lines).
2/ When gappa fails in achieving file parsing, GWhy seems to wrongly interpret it as proved Valid.
Best regards,
Dillonhttps://git.frama-c.com/pub/frama-c/-/issues/2523Inability to prove assigns clauses on simple array code2021-04-15T09:17:46ZVirgile PrevostoInability to prove assigns clauses on simple array codeID0000041:
**This issue was created automatically from Mantis Issue 41. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |...ID0000041:
**This issue was created automatically from Mantis Issue 41. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000041 | Frama-C | Plug-in > jessie | public | 2009-04-07 | 2009-06-23 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | virgile | **Assigned To** | cmarche | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Lithium-20081201 | **Target Version** | Frama-C Beryllium-20090601-beta1 | **Fixed in Version** | Frama-C Beryllium-20090601-beta1 |
### Description :
[bug 7560 from old bts, reported by David Mentré]
Hello,
With this code:
----
#include <string.h>
#define MAX 12
int a[MAX];
char *c[MAX];
/*@ assigns a[..];
*/
void assign_int(void)
{
int i;
//@ loop invariant 0 <= i && i <= MAX;
for (i = 0; i < MAX; i++) {
a[i] = 0x45;
}
}
/*@ assigns c[..];
*/
void assign_char(void)
{
int i;
//@ loop invariant 0 <= i && i <= MAX;
for (i = 0; i < MAX; i++) {
c[i] = strndup("something", MAX);
}
}
/*@ assigns a[..];
assigns c[..];
*/
void main(void)
{
assign_int();
assign_char();
}
------
On this code, I cannot prove properties "assigns a[..];" for
assign_int() and "assigns c[..];" for assign_char(). However the
assignation seems obvious to me.
I have tried "assigns a[0..11];" without success.
Is assigns broken?
Boris had a similar issue:
http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2009-April/000487.html
Yours,
d.https://git.frama-c.com/pub/frama-c/-/issues/2524GUI blocked (100% cpu used) when requested to display an assertion2021-04-15T09:17:46ZVirgile PrevostoGUI blocked (100% cpu used) when requested to display an assertionID0000036:
**This issue was created automatically from Mantis Issue 36. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |...ID0000036:
**This issue was created automatically from Mantis Issue 36. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000036 | Frama-C | Plug-in > jessie | public | 2009-04-07 | 2009-06-23 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | virgile | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Lithium-20081201 | **Target Version** | - | **Fixed in Version** | Frama-C Beryllium-20090601-beta1 |
### Description :
[bug 7497 from old bts, reported by David Mentré]
Hello,
If I do:
* Launch Jessie GUI on attached evoting.c file:
"rama-c -jessie-analysis -jessie-atp alt-ergo -jessie-std-stubs -jessie-gui evoting.c";
* Enter Ctrl+C to collapse all functions;
* Expand function "main Safety";
* Click on precondition 64.
The GUI is blocked, using 100% of CPU.
Yours,
d.
### Additional Information :
Looks a bug in gwhy itselfhttps://git.frama-c.com/pub/frama-c/-/issues/2525Lithium fool the tool2021-04-15T09:17:45ZVirgile PrevostoLithium fool the toolID0000029:
**This issue was created automatically from Mantis Issue 29. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |...ID0000029:
**This issue was created automatically from Mantis Issue 29. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000029 | Frama-C | Plug-in > jessie | public | 2009-04-07 | 2009-06-23 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | virgile | **Assigned To** | cmarche | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Lithium-20081201 | **Target Version** | - | **Fixed in Version** | Frama-C Beryllium-20090601-beta1 |
### Description :
[bug 7117 from old bts, reported by Christoph Weber]
Hello, unfortunatly I dont have time to track the bug down, so I will post the message I posted in the discussion list:
Hello again in the new year,
today I am trying to modify an implementation and still concurr with the function contract.
Therefore following code first:
/*@
requires 0 <= length;
requires \valid_range (a, 0, length-1);
requires \valid_range (b, 0, length-1);
assigns \nothing;
behavior equal:
ensures \result == 1 <==> (\forall integer i; 0 <= i < length ==> a[i] == b[i]);
behavior not_equal:
ensures \result == 0 <==> (\exists integer i; 0 <= i < length && a[i] != b[i]);
*/
int equal_array (int* a, int length, int* b )
{
int index_a = 0;
int index_b = 0;
/*@
loop invariant 0 <= index_a <= length;
loop invariant 0 <= index_b <= length;
loop invariant index_a == index_b;
loop invariant \forall integer k; 0 <= k < index_a ==> a[k] == b[k];
*/
while ( index_a != length )
{
if (a[index_a] != b[index_b])
return 0;
++index_a;
++index_b;
}
return 1;
}
Since I am using "assigns \nothing;" I expect the term \old() in comparison to be obsolete.
But as I recall, assigns \nothing allows temorary modification, as long as the content of the elements mentioned in
the parameter list of the function is restored before termination.
So I modified the algorithm, to alter the memory and restore it, allowing the algorithm to return allways
"true":
/*@
requires 0 <= length;
requires \valid_range (a, 0, length-1);
requires \valid_range (b, 0, length-1);
assigns \nothing;
behavior equal:
ensures \result == 1 <==> (\forall integer i; 0 <= i < length ==> a[i] == b[i]);
behavior not_equal:
ensures \result == 0 <==> (\exists integer i; 0 <= i < length && a[i] != b[i]);
*/
int equal_array (int* a, int length, int* b )
{
int save_array_a[length];
int save_array_b[length];
/*@
loop invariant 0 <= i <= length;
loop invariant \forall integer k; 0 <= k < i ==> a[k] == b[k] == 0;
loop invariant \forall integer k; 0 <= k < i ==> a[k] == save_array_a[k];
loop invariant \forall integer k; 0 <= k < i ==> b[k] == save_array_b[k];
*/
for(int i = 0; i < length; i++)
{
save_array_a[i] = a[i];
save_array_b[i] = b[i];
a[i] = 0;
b[i] = 0;
}
int index_a = 0;
int index_b = 0;
/*@
loop invariant 0 <= index_a <= length;
loop invariant 0 <= index_b <= length;
loop invariant index_a == index_b;
loop invariant \forall integer k; 0 <= k < index_a ==> a[k] == b[k];
*/
while ( index_a != length )
{
if (a[index_a] != b[index_b])
return 0;
++index_a;
++index_b;
}
/*@
loop invariant 0 <= i <= length;
loop invariant \forall integer k; 0 <= k < i ==> a[k] == save_array_a[k];
loop invariant \forall integer k; 0 <= k < i ==> b[k] == save_array_b[k];
*/
for(int i = 0; i < length; i++)
{
a[i] = save_array_a[i];
b[i] = save_array_b[i];
}
return 1;
}
My problem:
I cannot invoke the Jessie gui, it stops with the message:
equal_array.c:6: Warning: Variable-sized local variable save_array_a
equal_array.c:7: Warning: Variable-sized local variable save_array_b
Cleaning unused parts
Symbolic link
Starting semantical analysis
Starting Jessie translation
No code for function __builtin_alloca, default assigns generated
Producing Jessie files in subdir equal_array.jessie
File equal_array.jessie/equal_array.jc written.
File equal_array.jessie/equal_array.cloc written.
Calling Jessie tool in subdir equal_array.jessie
Generating Why function equal_array
File "jc/jc_interp.ml", line 861, characters 11-11:
Uncaught exception: File "jc/jc_interp.ml", line 861, characters 11-17: Assertion failed
Jessie subprocess failed: jessie -why-opt -split-user-conj -v -locs e
qual_array.cloc equal_array.jchttps://git.frama-c.com/pub/frama-c/-/issues/2526Jessie-gui : call of coqide and --project option2021-04-15T09:17:45ZVirgile PrevostoJessie-gui : call of coqide and --project optionID0000028:
**This issue was created automatically from Mantis Issue 28. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |...ID0000028:
**This issue was created automatically from Mantis Issue 28. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000028 | Frama-C | Plug-in > jessie | public | 2009-04-07 | 2009-06-23 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | virgile | **Assigned To** | cmarche | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Lithium-20081201 | **Target Version** | - | **Fixed in Version** | Frama-C Beryllium-20090601-beta1 |
### Description :
When calling coqide from the -jessie-gui interface, the following error occurs :
Thread 2 killed on uncaught exception Failure("For interactive provers, option --project must be set")
But i did'nt find how this option can be set. Can it be a default setting ?
Regards,
Nicolas.
### Additional Information :
seems like a bug in gwhy itself.https://git.frama-c.com/pub/frama-c/-/issues/2532Make install removes files2021-02-22T14:00:52ZSylvie BoldoMake install removes filesID0000116:
**This issue was created automatically from Mantis Issue 116. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000116:
**This issue was created automatically from Mantis Issue 116. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000116 | Frama-C | Kernel | public | 2009-06-05 | 2009-06-23 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | sboldo | **Assigned To** | signoles | **Resolution** | unable to reproduce |
| **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 :
When I want to install Frama-C after compiling the svn version , I have problems due to the fact that "make install" tries to removes files.
This is disturbing as a make install is not supposed to modify the archive, but it also makes the installation fail.
As I am under NIS, root has no right to remove my files and the installation cannot finish:
rm: cannot remove `.depend': Permission denied
/bin/sh: cannot create .depend: Permission denied
/bin/sh: cannot create .depend: Permission denied
make[1]: *** [.depend] Error 2https://git.frama-c.com/pub/frama-c/-/issues/2533Why error with logic functions returning a pointer2021-04-15T09:17:42ZVirgile PrevostoWhy error with logic functions returning a pointerID0000092:
**This issue was created automatically from Mantis Issue 92. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |...ID0000092:
**This issue was created automatically from Mantis Issue 92. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000092 | Frama-C | Plug-in > jessie | public | 2009-05-20 | 2009-06-19 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | virgile | **Assigned To** | cmarche | **Resolution** | reopened |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Lithium-20081201 | **Target Version** | - | **Fixed in Version** | - |
### Description :
The following code (a stripped down example of the bug reported by Alan Dunn on the mailing list: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2009-May/001151.html) gives an erroneous Why file when analyzed with
frama-c -jessie-analysis file.c
Either jessie should exit with an appropriate error message, or the why compilation should succeed.
char T;
/*@
axiomatic foo {
logic char* foo{L}(integer x) = &T;
}
*/
/*@ predicate strcmp{L}(char *x, char* y) =
\forall integer i; (\forall integer j; 0<=j<i ==> *(x+j) !=0) ==>
*(x+i) == *(y+i);
*/Claude MarchéClaude Marchéhttps://git.frama-c.com/pub/frama-c/-/issues/2534Default invariant should be inferred for loops2021-04-15T09:17:45ZVirgile PrevostoDefault invariant should be inferred for loopsID0000042:
**This issue was created automatically from Mantis Issue 42. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |...ID0000042:
**This issue was created automatically from Mantis Issue 42. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000042 | Frama-C | Plug-in > jessie | public | 2009-04-07 | 2009-06-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | virgile | **Assigned To** | cmarche | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Lithium-20081201 | **Target Version** | - | **Fixed in Version** | - |
### Description :
[bug 7561 from old bts, reported by Boris Hollas]
For loops that loop on a variable i that is not decreased inside the loop a default loop invariant should be inferred.
For example, in
for(i=0; i<n; i++) {
a[i] = 0;
}
the loop invariant
//@ loop invariant 0 <= i;
should be inferred by default.
A similar loop invariant should be inferred for decreasing loops.Claude MarchéClaude Marchéhttps://git.frama-c.com/pub/frama-c/-/issues/2535Why- error :-jessie-no-regions and assigns does not work2021-04-15T09:17:44ZVirgile PrevostoWhy- error :-jessie-no-regions and assigns does not workID0000031:
**This issue was created automatically from Mantis Issue 31. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |...ID0000031:
**This issue was created automatically from Mantis Issue 31. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000031 | Frama-C | Plug-in > jessie | public | 2009-04-07 | 2009-06-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | virgile | **Assigned To** | cmarche | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Lithium-20081201 | **Target Version** | - | **Fixed in Version** | - |
### Description :
[bug 7242 of old bts reported by Christoph Weber]
Hello,
for the following function I get the error:
in memory set (mem-field(int_M),a_20),
(mem-field(int_M),b_21)
File "jc/jc_interp_misc.ml", line 707, characters 7-7:
Uncaught exception: File "jc/jc_interp_misc.ml", line 707, characters 7-13: Asse
rtion failed
Jessie subprocess failed: jessie -why-opt -split-user-conj -v -locs i
nt_alignment.cloc int_alignment.jc
======
/*@
requires 0 <= length;
requires \valid_range (a, 0, length-1);
requires \valid_range (b, 0, length-1);
ensures \forall integer i; 0 <= i < length ==> b[i] == a[i];
*/
void copy (int* a, int length, int* b)
{
int i=0;
/*@
loop invariant 0 <= i <= length;
loop invariant \forall integer k; 0 <= k < i ==> a[k] == b[k];
loop assigns b[0 .. i-1];
*/
for(;i<length;i++ )
b[i]=a[i];
}
int main()
{
int array_int[10]={1,2,3,4,5,6,7,8,9,0};
int* first_int = &array_int[0];
char array_char_to_int[50];
copy(first_int, 10, array_char_to_int);
//create pointers to the same array,
//shift the second by one byte
int* first_char_to_int = &array_char_to_int[0];
int* first_char_to_int_shift = &array_char_to_int[1];
//call copy to the same array
//why error
copy(first_char_to_int, 10, first_char_to_int_shift);
return 0;
}
By the way, assigns b[0..length-1]; is never provable.
Cheers
ChristophClaude MarchéClaude Marchéhttps://git.frama-c.com/pub/frama-c/-/issues/2537Unable to verify pointer dereferencing2021-04-15T09:17:39Zmantis-gitlab-migrationUnable to verify pointer dereferencingID0000156:
**This issue was created automatically from Mantis Issue 156. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000156:
**This issue was created automatically from Mantis Issue 156. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000156 | Frama-C | Plug-in > jessie | public | 2009-06-09 | 2009-06-10 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | boris | **Assigned To** | - | **Resolution** | no change required |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Lithium-20081201 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Jessie is unable to verify pointer dereferencing in the following code:
/*@ requires \valid(a+ (left..right));
*/
void foo(int a[], int left, int right) {
int k;
k = a[right]; // Jessie fails here
}https://git.frama-c.com/pub/frama-c/-/issues/2539Jessie: float_P[..] expected instead of real2021-04-15T09:17:40ZDillon ParienteJessie: float_P[..] expected instead of realID0000105:
**This issue was created automatically from Mantis Issue 105. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000105:
**This issue was created automatically from Mantis Issue 105. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000105 | Frama-C | Plug-in > jessie | public | 2009-05-27 | 2009-05-28 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dpariente | **Assigned To** | - | **Resolution** | duplicate |
| **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 :
(This issue was previously discussed through private messages but not fully resolved. It is now recorded into the BTS for traceability reasons.)
Please, find below the contents of files foo.c and foo.h:
//===== file foo.c
typedef struct {float k;} las;
void g (float * y);
void f (las *c) { g(&(c->k)); }
//===== file foo.h
typedef struct {float k;} las;
//@ requires \valid(c); assigns c->k;
void f (las * c);
command line:
frama-c.exe -jessie-analysis -jessie-gui foo.c foo.h
Error message:
Calling Jessie tool in subdir wholeprogram.jessie File "wholeprogram.jc", line 401, characters 15-26: typing error: type float_P[..] expected instead of real
Jessie subprocess failed: jessie -why-opt -split-user-conj -v
-why-opt -fast-wp -separation -locs wholeprogram.cloc w
holeprogram.jchttps://git.frama-c.com/pub/frama-c/-/issues/2540Jessie: memory in memeory set2021-04-15T09:17:40ZDillon ParienteJessie: memory in memeory setID0000106:
**This issue was created automatically from Mantis Issue 106. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000106:
**This issue was created automatically from Mantis Issue 106. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000106 | Frama-C | Plug-in > jessie | public | 2009-05-27 | 2009-05-28 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dpariente | **Assigned To** | - | **Resolution** | duplicate |
| **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 :
(This issue was previously discussed through private messages but not fully resolved. It is now recorded into the BTS for traceability reasons.)
An uncaugth exception is generated on the followin code:
typedef struct {int i;int j;} las;
/*@ requires \valid(a) && \valid(b);
assigns *a, *b; */
void g (int *a,int *b){ *a=11; *b=15; }
/*@ requires \valid(p) ;
assigns p->i,p->j;
*/
void f (las *p)
{ g (&(p->i), &(p->j)); }
Command line:
frama-c.exe -jessie-analysis -jessie-gui foo.c
Error message:
memory (mem-field(int_M),b_2)
in memory set (mem-field(int_M),a_1),
(mem-field(int_M),b_2)
File "jc/jc_interp_misc.ml", line 714, characters 7-7:
Uncaught exception: File "jc/jc_interp_misc.ml", line 714, characters 7-13: Assertion failedhttps://git.frama-c.com/pub/frama-c/-/issues/2542Internal error with assign specification on bi-dimensional arrays2021-04-15T09:17:44ZVirgile PrevostoInternal error with assign specification on bi-dimensional arraysID0000032:
**This issue was created automatically from Mantis Issue 32. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |...ID0000032:
**This issue was created automatically from Mantis Issue 32. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000032 | Frama-C | Plug-in > jessie | public | 2009-04-07 | 2009-04-10 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | virgile | **Assigned To** | cmarche | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Lithium-20081201 | **Target Version** | - | **Fixed in Version** | - |
### Description :
[bug 7435 from old bts, reported by David Mentré]
Hello,
Using this code:
=== bidim_array.c
int a[12][45] = {0, };
//@ assigns a[..][..];
void f(void)
{
a[1][3] = 42;
}
void main(void)
{
f();
}
===
The assigns clause triggers an internal error in Jessie.
$ frama-c -jessie-analysis -jessie-gen-only bidim_array.c
Parsing
[preprocessing] running gcc -C -E -I. -include
/usr/local/stow/frama-c-lithium-2008-12-01/share/frama-c/jessie/jessie_prolog.h -dD bidim_array.c
Cleaning unused parts
Symbolic link
Starting semantical analysis
Starting Jessie translation
Fatal error: exception Assert_failure("src/jessie/interp.ml", 807, 33)
Yours,
d.
### Additional Information :
Normalization of multi-dimensional array accesses in jessie plugin is not compatible with use of range.Claude MarchéClaude Marchéhttps://git.frama-c.com/pub/frama-c/-/issues/2543Jessie crashes on simple program without annotations2021-04-15T09:17:44ZVirgile PrevostoJessie crashes on simple program without annotationsID0000038:
**This issue was created automatically from Mantis Issue 38. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |...ID0000038:
**This issue was created automatically from Mantis Issue 38. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000038 | Frama-C | Plug-in > jessie | public | 2009-04-07 | 2009-04-10 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | virgile | **Assigned To** | cmarche | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Lithium-20081201 | **Target Version** | - | **Fixed in Version** | - |
### Description :
[bug 7541 from old bts, reported by Boris Hollas]
Jessie crashes on the following code:
void Copy(int *p, int *q)
{
*q = *p;
}
int foo(int a[]) {
int i=1;
Copy(&a[0], &a[i]);
return i;
}
int main() {
int a[2] = {1,2};
printf("%d\n", foo(a));
}
Output:
~/progs/fc/tst> frama-c -jessie-analysis tst4.c
Parsing
[preprocessing] running gcc -C -E -I. -include C:\Frama-C\share\frama-c\jessie\jessie_prolog.h -dD tst4.c
tst4.c:17: Warning: Body of function main falls-through. Adding a return statement
Cleaning unused parts
Symbolic link
Starting semantical analysis
Starting Jessie translation
No code for function printf, default assigns generated
tst4.c:15: Warning: skipping all arguments of implicit prototype printf
Producing Jessie files in subdir tst4.jessie
File tst4.jessie/tst4.jc written.
File tst4.jessie/tst4.cloc written.
Calling Jessie tool in subdir tst4.jessie
Generating Why function Copy
Generating Why function foo
Generating Why function main
Calling VCs generator.
why -simplify [...] why/tst4.why
File "why/tst4.why", line 1418, characters 8-49:
Term i_27 is expected to have type int
make: *** [simplify/tst4_why.sx] Error 1
Jessie subprocess failed: make -f tst4.makefile simplify
### Additional Information :
Claude Marché: Issues lies in the lack of a conversion from int32 into int in pset generation (in jessie plugin)Claude MarchéClaude Marchéhttps://git.frama-c.com/pub/frama-c/-/issues/2547"Unknown Error" with Alt-Ergo2021-06-01T11:23:20ZQix"Unknown Error" with Alt-ErgoBefore submitting the issue, please confirm (by adding a X in the [ ]):
- [x] the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- [X] the issue has not yet been reported on our old
[BTS](http...Before submitting the issue, please confirm (by adding a X in the [ ]):
- [x] the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- [X] the issue has not yet been reported on our old
[BTS](https://bts.frama-c.com) (*note: the old BTS is deprecated*);
- [X] you installed Frama-C as prescribed in the [instructions](INSTALL.md).
# Contextual information
- Frama-C installation mode: *Opam*
- Frama-C version: *21.1 (Scandium)*
- Plug-in used: *wp*
- OS name: *Windows (via WSL 1)*
- OS version: *Windows 10 Pro build 19041.685*
I have also done `rm -f ~/.why3.conf; why3 config --detect --full-config` quite a few times now.
# Steps to reproduce the issue
Just creating a simple C file called `swap.c`:
```c
/*@
requires \valid(a) && \valid(b);
assigns *a, *b;
ensures *a == \old(*b);
ensures *b == \old(*a);
*/
void swap(int *a, int *b) {
int tmp = *a;
*a = *b;
*b = tmp;
}
int main() {
int a = 42;
int b = 37;
swap(&a, &b);
//@ assert a == 37 && b == 42;
return 0;
}
```
And running it with
```shell
frama-c -wp swap.c
```
# Expected behaviour
All goals proven.
# Actual behaviour
Alt-Ergo gives an `Unknown error`.
```
[kernel] Parsing swap.c (with preprocessing)
[wp] Warning: Missing RTE guards
[wp] 6 goals scheduled
[wp] [Alt-Ergo 2.2.0] Goal typed_swap_ensures : Failed
Unknown error
[wp] Proved goals: 5 / 6
Qed: 5
Alt-Ergo 2.2.0: 0 (failed: 1)
```
I'm seeing this happen with a much larger project for just about every single goal there, too. I cannot verify a single C program with ACSL annotations, it seems.
# Fix ideas
No idea. I can't seem to find any information about this aside from a single unanswered StackOverflow question.Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/2548Error: Unbound value Why3.Whyconf.load_default_config_if_needed2021-04-13T17:49:41ZQixError: Unbound value Why3.Whyconf.load_default_config_if_needed
Before submitting the issue, please confirm (by adding a X in the [ ]):
- [x] the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- [ ] the issue has not yet been reported on our old
[BTS](htt...
Before submitting the issue, please confirm (by adding a X in the [ ]):
- [x] the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- [ ] the issue has not yet been reported on our old
[BTS](https://bts.frama-c.com) (*note: the old BTS is deprecated*); **(Can't tell; getting a database connection error)**
- [ ] you installed Frama-C as prescribed in the [instructions](INSTALL.md). **(Not exactly; I'm building from source within a Dockerfile)**
# Contextual information
- Frama-C installation mode: from source
- Frama-C version: c4d10fb975d443e3c40289843fae89c424b54e63
- Plug-in used: WP
- OS name: Debian Buster
- OS version: 20210326 (10.8)
# Steps to reproduce the issue
Dockerfile:
```Dockerfile
FROM debian:buster-20210326 AS base
RUN apt update -y
RUN apt install -y gnupg2 wget apt-transport-https ca-certificates
RUN wget -O - https://apt.llvm.org/llvm-snapshot.gpg.key | apt-key add -
RUN bash -c "cat >> /etc/apt/sources.list <<< \"deb http://apt.llvm.org/buster/ llvm-toolchain-buster main\""
RUN bash -c "cat >> /etc/apt/sources.list <<< \"deb-src http://apt.llvm.org/buster/ llvm-toolchain-buster main\""
RUN bash -c "cat >> /etc/apt/sources.list <<< \"deb http://apt.llvm.org/buster/ llvm-toolchain-buster-12 main\""
RUN bash -c "cat >> /etc/apt/sources.list <<< \"deb-src http://apt.llvm.org/buster/ llvm-toolchain-buster-12 main\""
RUN cat /etc/apt/sources.list
RUN apt update -y
RUN apt install -y clang-12 lld-12 grub-common ninja-build git libssl-dev libgmp-dev pkg-config make m4 unzip tar bzip2 gcc g++ autoconf zlib1g-dev time
RUN cc --version
RUN c++ --version
WORKDIR /opam
RUN wget https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh
RUN echo "/opam" | sh install.sh --no-backup
ENV PATH="/opam:/opam/bin:${PATH}"
RUN opam --version
RUN time opam init -y --disable-sandboxing --jobs=1
RUN time opam install -y depext ocamlfind ocamlgraph zarith yojson why3.1.4.0 alt-ergo.2.4.0
ENV PATH="/root/.opam/default/bin:${PATH}"
RUN why3 --version
RUN why3 config detect
ARG FRAMAC_REF=c4d10fb975d443e3c40289843fae89c424b54e63
WORKDIR /framac
RUN git init .
RUN git remote add origin https://git.frama-c.com/pub/frama-c.git
RUN git fetch origin ${FRAMAC_REF}
RUN git checkout ${FRAMAC_REF}
RUN autoconf
RUN ./configure
RUN make -j4
RUN make install
RUN frama-c --version; echo
```
# Expected behaviour
Should build to completion.
# Actual behaviour
```
File "src/plugins/wp/Why3Provers.ml", line 31, characters 19-61:
31 | let config = Why3.Whyconf.load_default_config_if_needed config in
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: Unbound value Why3.Whyconf.load_default_config_if_needed
make: *** [share/Makefile.generic:78: src/plugins/wp/Why3Provers.cmo] Error 2
make: *** Waiting for unfinished jobs....
The command '/bin/sh -c make -j4' returned a non-zero code: 2
```
---
Some context: Trying to verify a new toy OS and having a bunch of issues since I can't use the standard C library that ships with Frama-C (as there is no C library available in this environment) so I've ended up copying the axiomatic clauses from the `__fc_xxx.h` headers directly.
I saw on StackOverflow that a few bugs that seemed to be affecting me were recently patched on master but not yet released, so I spun up a Dockerfile in order to try to see if any of the verification could be fixed by trying it with the latest head.
However, it doesn't seem to be working - much less getting even simple programs to verify correctly :/ Hence why I'm trying to update everything to latest to see if I can't get _any_ verification to work.
Anyway this is the latest issue I've hit trying to get everything up to date.
Note that there is a lot of stuff in there that isn't directly related to this bug - this is a stripped down Dockerfile, and there is a bunch of extra stuff that comes after this step that I removed to keep things small.https://git.frama-c.com/pub/frama-c/-/issues/2549Undefined behavior in pointer arithmetic2024-01-24T09:06:24ZRicardo M. CorreiaUndefined behavior in pointer arithmeticBefore submitting the issue, please confirm (by adding a X in the [ ]):
- [X] the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- [x] the issue has not yet been reported on our old
[BTS](http...Before submitting the issue, please confirm (by adding a X in the [ ]):
- [X] the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- [x] the issue has not yet been reported on our old
[BTS](https://bts.frama-c.com) (*note: the old BTS is deprecated*);
- [X] you installed Frama-C as prescribed in the [instructions](INSTALL.md).
# Contextual information
- Frama-C installation mode: *package from NixOS/nixpkgs*
- Frama-C version: *21.1 and master commit 2fc0990864 (from 2021-03-31)* (as reported by `frama-c -version`)
- Plug-in used: *WP*
- OS name: *NixOS*
- OS version: *20.09+patches*
*Please add specific information deemed relevant with regard to this issue.*
# Steps to reproduce the issue
Given the following C file called pointer.c:
```C
#include <stddef.h>
/*@
requires \valid(&p[0..len-1]);
*/
int *one_minus(int *p) /*@ ghost (size_t len) */
{
return p - 1;
}
/*@
requires \valid(&p[0..len-1]);
*/
int *plus_two(int *p, size_t len)
{
return p + len + 1;
}
```
... I then run the following frama-c command:
```bash
$ frama-c -wp -wp-prover Z3 -wp-rte -wp-smoke-tests -wp-par 8 -wp-cache rebuild -warn-signed-downcast -warn-unsigned-downcast -warn-unsigned-overflow -warn-right-shift-negative "$@" -then -report-no-proven -report pointer.c
```
# Expected behaviour
I would've expected Frama-C to point out that both functions can have undefined behavior, i.e. they should have unproven properties/goals.
Perhaps I'm misunderstand Frama-C's limitations or the C standard, but as far as I understand, C considers references to 1 index below or 2 indexes above the valid addresses of an allocated array to be undefined behaviors, i.e. you can't even reference those addresses. Thus, dereference is not even necessary for undefined behavior, except for the special case of 1 index past the valid addresses of an allocated array, which is valid to reference but not valid to dereference.
# Actual behaviour
With Frama-C 21.1, I get the following result:
```
[kernel] Parsing pointer.c (with preprocessing)
[rte] annotating function one_minus
[rte] annotating function plus_two
[wp] 2 goals scheduled
[wp] [Cache] updated:2
[wp] Proved goals: 2 / 2
Qed: 0 (0.89ms-1ms)
Z3 4.8.8 (counterexamples): 2
[report] Computing properties status...
--------------------------------------------------------------------------------
--- No status to report
--------------------------------------------------------------------------------
```
No warnings or errors.
I skipped Frama-C 22.0 because I encountered more serious, but unrelated, correctness issues in that version.
With Frama-C master branch, commit 2fc0990864 (from 2021-03-31):
```
[kernel] Parsing pointer.c (with preprocessing)
[rte] annotating function one_minus
[rte] annotating function plus_two
[wp] 2 goals scheduled
[wp] [Cache] updated:2
[wp] Proved goals: 2 / 2
Qed: 0 (0.94ms-2ms)
Z3 4.8.8 (counterexamples): 2
[wp:pedantic-assigns] pointer.c:6: Warning:
No 'assigns' specification for function 'one_minus'.
Callers assumptions might be imprecise.
[wp:pedantic-assigns] pointer.c:14: Warning:
No 'assigns' specification for function 'plus_two'.
Callers assumptions might be imprecise.
[report] Computing properties status...
--------------------------------------------------------------------------------
--- No status to report
--------------------------------------------------------------------------------
```
Just a couple of warnings about callers assumptions being imprecise. This doesn't indicate that there's a problem with the function implementations.
# Fix ideas
I don't know of any workarounds. I'm guessing new goals should be added to make sure pointers can only point to either valid memory addresses or addresses one past the end of an array.https://git.frama-c.com/pub/frama-c/-/issues/2550Frama-c crash with z.Overflow error2021-10-13T09:04:40ZKarine EMFrama-c crash with z.Overflow error<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the iss...<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- you installed Frama-C as prescribed in the [instructions](INSTALL.md).
If the issue applies to a specific Frama-C plug-in, please prefix the title
by the plug-in name: [Eva], [WP], [E-ACSL]…
-->
### Steps to reproduce the issue
No external headers required, just run: (the program is at the end of this report)
```
frama-c -eva da8af4f574fcb46b5bdc926cec29f39db03d1fb4.c
```
<!--
Please indicate here steps to follow to get a [minimal, complete, and verifiable example](https://stackoverflow.com/help/mcve) which reproduces the issue.
-->
### Expected behaviour
<!--
Please explain here what is the expected behaviour.
-->
Not to crash. The code is passing compilation with gcc and clang with few warnings.
### Actual behaviour
<!--
Please explain here what is the actual (faulty) behaviour.
-->
Frama-c crashed:
```
[kernel] Parsing da8af4f574fcb46b5bdc926cec29f39db03d1fb4.c (with preprocessing)
[kernel] Current source was: da8af4f574fcb46b5bdc926cec29f39db03d1fb4.c:4
The full backtrace is:
Raised by primitive operation at file "src/libraries/stdlib/integer.ml" (inlined), line 100, characters 13-21
Called from file "src/kernel_internals/typing/cabs2cil.ml", line 10006, characters 47-64
Called from file "src/kernel_internals/typing/cabs2cil.ml", line 9976, characters 13-36
Called from file "src/kernel_internals/typing/cabs2cil.ml", line 9697, characters 25-48
Called from file "list.ml", line 121, characters 24-34
Called from file "src/kernel_internals/typing/cabs2cil.ml", line 9687, characters 9-1023
Called from file "src/kernel_internals/typing/cabs2cil.ml", line 9328, characters 10-294
Called from file "src/kernel_internals/typing/cabs2cil.ml", line 10326, characters 12-35
Called from file "list.ml", line 110, characters 12-15
Called from file "src/kernel_internals/typing/cabs2cil.ml", line 10330, characters 2-25
Called from file "src/kernel_internals/typing/frontc.ml", line 83, characters 14-36
Called from file "src/kernel_services/ast_queries/file.ml", line 602, characters 25-44
Called from file "src/kernel_services/ast_queries/file.ml", line 622, characters 14-38
Called from file "src/kernel_services/ast_queries/file.ml", line 685, characters 46-72
Called from file "list.ml", line 121, characters 24-34
Called from file "src/kernel_services/ast_queries/file.ml", line 685, characters 17-89
Called from file "src/kernel_services/ast_queries/file.ml", line 1625, characters 24-60
Called from file "src/kernel_services/ast_queries/file.ml", line 1702, characters 4-27
Called from file "src/kernel_services/ast_data/ast.ml", line 110, characters 2-28
Called from file "src/kernel_services/ast_data/ast.ml", line 118, characters 53-71
Called from file "src/kernel_internals/runtime/boot.ml", line 29, characters 6-20
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 842, characters 2-9
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 872, characters 18-64
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 231, characters 4-8
Unexpected error (Z.Overflow).
Please report as 'crash' at https://git.frama-c.com/pub/frama-c/issues
Your Frama-C version is 22.0 (Titanium).
Note that a version and a backtrace alone often do not contain enough
information to understand the bug. Guidelines for reporting bugs are at:
https://git.frama-c.com/pub/frama-c/-/wikis/Guidelines-for-reporting-bugs
```
### Contextual information
- Frama-C installation mode: Opam
- Frama-C version: Frama-C version is 21.0 (Scandium) and Frama-C version is 22.0 (Titanium)
- Plug-in used: eva
- OS name: Ubuntu
- OS version: 18
### Additional information (optional)
<!--
You may add here any information deemed relevant with regard to this issue,
and tell us if you already tried some workarounds or have some ideas to solve this issue.
-->
I reduced the program that crashed Frama-c into this: (via Creduce)
```
long a;
void b() {
switch (a)
case 0 ... 9999999999999999999:;
}
void main() {}
```Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/2551Frama-c crash with Cil.SizeOfError sizeof(void)2021-04-30T07:59:31ZKarine EMFrama-c crash with Cil.SizeOfError sizeof(void)<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the iss...<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- you installed Frama-C as prescribed in the [instructions](INSTALL.md).
If the issue applies to a specific Frama-C plug-in, please prefix the title
by the plug-in name: [Eva], [WP], [E-ACSL]…
-->
This issue looks like a similar one to https://git.frama-c.com/pub/frama-c/-/issues/263, which was closed because it is related to jessie plug-in. The example here gives an error message that is almost the same as the one reported in bug 263 but with eva plug-in.
Since I am getting this error quite a lot, I was thinking it is important to report.
### Steps to reproduce the issue
```
frama-c -eva test.c
```
<!--
Please indicate here steps to follow to get a [minimal, complete, and verifiable example](https://stackoverflow.com/help/mcve) which reproduces the issue.
-->
### Expected behaviour
Not to crash frama-c.
<!--
Please explain here what is the expected behaviour.
-->
### Actual behaviour
Frama-c crashed with this error trace:
<!--
Please explain here what is the actual (faulty) behaviour.
-->
```
[kernel] Parsing test.c (with preprocessing)
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
[kernel] Current source was: test.c:5
The full backtrace is:
Raised at file "src/kernel_services/ast_queries/cil.ml", line 4038, characters 22-72
Called from file "src/kernel_services/ast_queries/cil.ml", line 4533, characters 42-58
Called from file "src/kernel_services/ast_queries/cil.ml", line 4793, characters 8-29
Called from file "src/plugins/value/engine/evaluation.ml", line 917, characters 12-35
Called from file "src/plugins/value/engine/evaluation.ml", line 864, characters 6-40
Called from file "src/plugins/value/engine/evaluation.ml", line 801, characters 27-57
Called from file "src/plugins/value/engine/evaluation.ml", line 907, characters 6-33
Called from file "src/plugins/value/engine/evaluation.ml", line 834, characters 35-69
Called from file "src/plugins/value/engine/evaluation.ml", line 801, characters 27-57
Called from file "src/plugins/value/engine/evaluation.ml", line 1103, characters 6-36
Called from file "src/plugins/value/engine/evaluation.ml" (inlined), line 1148, characters 4-67
Called from file "src/plugins/value/engine/evaluation.ml", line 1509, characters 23-77
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 157, characters 14-59
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 177, characters 4-54
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 526, characters 6-65
Called from file "src/plugins/value/eval.ml", line 48, characters 29-32
Called from file "list.ml", line 126, characters 16-37
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 564, characters 4-68
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 752, characters 29-72
Called from file "list.ml", line 121, characters 24-34
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 769, characters 24-59
Called from file "src/kernel_services/abstract_interp/bottom.ml" (inlined), line 31, characters 18-21
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 742, characters 6-1023
Called from file "src/plugins/value/engine/iterator.ml", line 274, characters 6-47
Called from file "src/plugins/value/partitioning/partition.ml", line 494, characters 29-34
Called from file "list.ml", line 121, characters 24-34
Called from file "src/plugins/value/engine/iterator.ml", line 430, characters 15-71
Called from file "src/plugins/value/engine/iterator.ml", line 494, characters 18-35
Called from file "list.ml", line 92, characters 20-23
Called from file "src/plugins/value/engine/iterator.ml", line 496, characters 18-60
Called from file "src/plugins/value/engine/iterator.ml", line 543, characters 13-31
Called from file "list.ml", line 110, characters 12-15
Called from file "src/plugins/value/engine/iterator.ml" (inlined), line 540, characters 4-31
Called from file "src/plugins/value/engine/iterator.ml", line 602, characters 6-22
Called from file "src/plugins/value/engine/iterator.ml", line 769, characters 20-39
Called from file "src/plugins/value/engine/compute_functions.ml", line 201, characters 8-45
Called from file "src/plugins/value/engine/compute_functions.ml", line 333, characters 25-75
Called from file "src/libraries/project/state_builder.ml", line 994, characters 9-13
Re-raised at file "src/libraries/project/state_builder.ml", line 1002, characters 9-18
Called from file "src/plugins/value/register.ml", line 39, characters 46-66
Called from file "queue.ml", line 121, characters 6-15
Called from file "src/kernel_internals/runtime/boot.ml", line 36, characters 4-20
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 842, characters 2-9
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 872, characters 18-64
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 231, characters 4-8
Unexpected error (Cil.SizeOfError("Undefined sizeof(void).", _)).
Please report as 'crash' at https://git.frama-c.com/pub/frama-c/issues
Your Frama-C version is 22.0 (Titanium).
Note that a version and a backtrace alone often do not contain enough
information to understand the bug. Guidelines for reporting bugs are at:
https://git.frama-c.com/pub/frama-c/-/wikis/Guidelines-for-reporting-bugs
```
### Contextual information
- Frama-C installation mode: Opam
- Frama-C version: Frama-C version is 21.0 (Scandium) and Frama-C version is 22.0 (Titanium)
- Plug-in used: eva
- OS name: Ubuntu
- OS version: 18
### Additional information (optional)
<!--
You may add here any information deemed relevant with regard to this issue,
and tell us if you already tried some workarounds or have some ideas to solve this issue.
-->
I reduced the program that crashed Frama-c into this: (via Creduce)
```
void a(char *b, int align) {}
#define c(d) #d
#define f() c()
#define a(e) a(f(), __alignof__(e))
int main() { a(void); return 0; }
```David BühlerDavid Bühlerhttps://git.frama-c.com/pub/frama-c/-/issues/2553Install and run Frama-C by OPAM with OCaml for Windows2022-09-28T13:59:32ZweijianInstall and run Frama-C by OPAM with OCaml for WindowsI have tried to install and run Frama-C by OPAM with OCaml for Windows.
Win10+cygwin64,but it didn't work.
```
$ frama-c
[kernel] User Error: cannot load plug-in 'num.core': cannot load module
Details: error loading shared library: D...I have tried to install and run Frama-C by OPAM with OCaml for Windows.
Win10+cygwin64,but it didn't work.
```
$ frama-c
[kernel] User Error: cannot load plug-in 'num.core': cannot load module
Details: error loading shared library: Dynlink.Error (Dynlink.Cannot_open_dll "Failure(\"flexdll error: cannot relocate RELOC_REL32, target is too far: ffffffff6a110d73 000000006a110d73\")")
[kernel] User Error: cannot load plug-in 'zip': cannot load module
Details: error loading shared library: Dynlink.Error (Dynlink.Cannot_open_dll "Failure(\"flexdll error: cannot relocate RELOC_REL32, target is too far: fffffffe488b648d 00000000488b648d\")")
[kernel] User Error: cannot load plug-in 'why3': cannot load module
Details: error loading shared library: Dynlink.Error (Dynlink.Cannot_open_dll "Failure(\"Cannot resolve camlGzip\")")
[kernel] User Error: cannot load plug-in 'frama-c-wp': cannot load module
Details: error loading shared library: Dynlink.Error (Dynlink.Cannot_open_dll "Failure(\"Cannot resolve camlWhy3__Ident\")")
[kernel] User Error: Deferred error message was emitted during execution. See above messages for more information.
[kernel] Frama-C aborted: invalid user input.`
```
Can someone explain the installation process is a clear and simple way, and I will grateful?Andre MaronezeAndre Maronezehttps://git.frama-c.com/pub/frama-c/-/issues/2554Error when using docker file with Singularity2021-09-03T20:05:38Zthuynt_57Error when using docker file with Singularity<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the iss...<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- you installed Frama-C as prescribed in the [instructions](INSTALL.md).
If the issue applies to a specific Frama-C plug-in, please prefix the title
by the plug-in name: [Eva], [WP], [E-ACSL]…
-->
I used **Singularity** to pull the image of frama-c from docker hub.
However, when I run `frama-c -help`, I got the following error.
Could you please help me check it?
I don't have any problem when I use docker desktop.
[Updated] The image I tried is the one with tag 22.0
> [kernel] Current source was: :0
> The full backtrace is:
> Raised at file "stdlib.ml", line 29, characters 17-33
> Called from file "findlib.ml", line 166, characters 10-151
> Called from file "src/kernel_services/plugin_entry_points/dynamic.ml", line 299, characters 2-45
> Called from file "src/kernel_services/plugin_entry_points/kernel.ml", line 848, characters 4-49
> Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 886, characters 2-22
> Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 231, characters 4-8
>
> Unexpected error (Failure("Config file not found - neither /root/.opam/ocaml-base-compiler.4.08.1/lib/findlib.conf nor the directory /root/.opam/ocaml-base-compiler.4.08.1/lib/findlib.conf.d")).
> Please report as 'crash' at https://git.frama-c.com/pub/frama-c/issues
> Your Frama-C version is 22.0 (Titanium).
> Note that a version and a backtrace alone often do not contain enough
> information to understand the bug. Guidelines for reporting bugs are at:
> https://git.frama-c.com/pub/frama-c/-/wikis/Guidelines-for-reporting-bugsAndre MaronezeAndre Maronezehttps://git.frama-c.com/pub/frama-c/-/issues/2555Crash in abstract_interp with an unexpected error when the input program has ...2021-05-21T09:25:42ZKarine EMCrash in abstract_interp with an unexpected error when the input program has a syntax error.<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the iss...<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- you installed Frama-C as prescribed in the [instructions](INSTALL.md).
If the issue applies to a specific Frama-C plug-in, please prefix the title
by the plug-in name: [Eva], [WP], [E-ACSL]…
-->
### Steps to reproduce the issue
<!--
Please indicate here steps to follow to get a [minimal, complete, and verifiable example](https://stackoverflow.com/help/mcve) which reproduces the issue.
-->
### Expected behaviour
<!--
Please explain here what is the expected behaviour.
-->
The following program has a syntax error that crashed frama-c instead of returning an alarm.
E.g., gcc returns the following compile-time error:
```
user42@srg08:~/directed-compiler-fuzzing-code/scripts/9-reduce-bugs/Frama-C-zone$ gcc -w 0bd2a2aa5631e87ab09386dc82e092f5aab23f0e.c
0bd2a2aa5631e87ab09386dc82e092f5aab23f0e.c:10:11: error: negative width in bit-field ‘b’
10 | int32_t b:(-19);
|
```
### Actual behaviour
<!--
Please explain here what is the actual (faulty) behaviour.
-->
The following code crashed frama-c:
```
user42@srg08:~/directed-compiler-fuzzing-code/scripts/9-reduce-bugs/Frama-C-zone$ more 0bd2a2aa5631e87ab09386dc82e092f5aab23f0e.c
#if __SIZEOF_INT__ < 4
__extension__ typedef __INT32_TYPE__ int32_t;
#else
typedef int int32_t;
#endif
#pragma pack(1)
struct S
{
int32_t b:(-19);
} i;
int main ()
{
return (-1);
}
```
with the following error:
```
user42@srg08:~/directed-compiler-fuzzing-code/scripts/9-reduce-bugs/Frama-C-zone$ frama-c -eva 0bd2a2aa5631e87ab09386dc82e092f5aab23f0e.c
[kernel] Parsing 0bd2a2aa5631e87ab09386dc82e092f5aab23f0e.c (with preprocessing)
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[kernel] Current source was: 0bd2a2aa5631e87ab09386dc82e092f5aab23f0e.c:11
The full backtrace is:
Raised at file "src/kernel_services/abstract_interp/base.ml", line 217, characters 2-27
Called from file "src/kernel_services/abstract_interp/base.ml", line 480, characters 17-43
Called from file "src/libraries/project/state_builder.ml", line 565, characters 17-22
Called from file "src/plugins/value/domains/cvalue/cvalue_domain.ml", line 394, characters 15-38
Called from file "list.ml", line 121, characters 24-34
Called from file "src/plugins/value/domains/cvalue/cvalue_domain.ml", line 405, characters 4-34
Called from file "src/plugins/value/engine/initialization.ml", line 309, characters 16-68
Called from file "list.ml", line 121, characters 24-34
Called from file "src/kernel_services/ast_data/globals.ml" (inlined), line 128, characters 33-72
Called from file "src/plugins/value/engine/initialization.ml", line 324, characters 15-65
Called from file "src/libraries/project/state_builder.ml", line 403, characters 17-21
Called from file "src/plugins/value/engine/initialization.ml", line 396, characters 20-43
Called from file "src/plugins/value/engine/compute_functions.ml", line 357, characters 10-55
Called from file "src/libraries/project/state_builder.ml", line 994, characters 9-13
Re-raised at file "src/libraries/project/state_builder.ml", line 1002, characters 9-18
Called from file "src/plugins/value/register.ml", line 39, characters 46-66
Called from file "queue.ml", line 121, characters 6-15
Called from file "src/kernel_internals/runtime/boot.ml", line 36, characters 4-20
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 842, characters 2-9
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 872, characters 18-64
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 231, characters 4-8
Unexpected error (File "src/kernel_services/abstract_interp/base.ml", line 217, characters 2-8: Assertion failed).
Please report as 'crash' at https://git.frama-c.com/pub/frama-c/issues
Your Frama-C version is 22.0 (Titanium).
Note that a version and a backtrace alone often do not contain enough
information to understand the bug. Guidelines for reporting bugs are at:
https://git.frama-c.com/pub/frama-c/-/wikis/Guidelines-for-reporting-bugs
```
### Contextual information
- Frama-C installation mode: Opam
- Frama-C version: *Frama-C version* (as reported by `frama-c -version`) 22.0 (Titanium)
- Plug-in used: -eva
- OS name: Ubuntu
- OS version: 18
### Additional information (optional)
<!--
You may add here any information deemed relevant with regard to this issue,
and tell us if you already tried some workarounds or have some ideas to solve this issue.
-->
I reduced the program manually, I can also share the original code or other examples.Andre MaronezeAndre Maronezehttps://git.frama-c.com/pub/frama-c/-/issues/2556Unexpected error "Z.shift_left" with invalid_argument with -eva option when t...2022-01-11T10:02:05Zarindam-8Unexpected error "Z.shift_left" with invalid_argument with -eva option when the code had syntax errors<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the iss...<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- you installed Frama-C as prescribed in the [instructions](INSTALL.md).
If the issue applies to a specific Frama-C plug-in, please prefix the title
by the plug-in name: [Eva], [WP], [E-ACSL]…
-->
### Steps to reproduce the issue
frama-c -eva 1cb6e7577d2fe06f3a0e71a0f8bf2af3d964c6f9_copy1.c
### Expected behaviour
When an error-containing program is fed into Frama-C, the expected behaviour should be of it giving an appropriate message instead of a crash (an alarm).
### Actual behaviour
The following code:
```
typedef enum bfd_boolean {false, true} boolean;
typedef unsigned long long bfd_size_type;
typedef unsigned int flagword;
typedef unsigned long long CORE_ADDR;
typedef unsigned long long bfd_vma;
struct bfd_struct {
int x;
};
struct asection_struct {
unsigned int user_set_vma : (-2);
bfd_vma vma;
bfd_vma lma;
unsigned int alignment_power;
unsigned int entsize;
};
typedef struct bfd_struct bfd;
typedef struct asection_struct asection;
static bfd *
bfd_openw_with_cleanup (char *filename, const char *target, char *mode)
{
static bfd foo_bfd = { (-1) };
return &foo_bfd;
}
static asection *
bfd_make_section_anyway (bfd *abfd, const char *name)
{
static asection foo_section = { false, (0), (0), (-1) };
return &foo_section;
}
static boolean
bfd_set_section_size (bfd *abfd, asection *sec, bfd_size_type val)
{
return true;
}
static char hello[] = "hello";
int main(void)
{
}
```
gives the following trace:
```
The full backtrace is:
Raised by primitive operation at file "src/libraries/stdlib/integer.ml", line 30, characters 2-22
Called from file "src/kernel_services/abstract_interp/int_val.ml", line 552, characters 14-39
Called from file "src/kernel_services/abstract_interp/int_val.ml", line 566, characters 10-59
Called from file "src/kernel_services/abstract_interp/ival.ml", line 521, characters 24-65
Called from file "src/plugins/value_types/cvalue.ml", line 427, characters 23-57
Called from file "src/plugins/value/engine/evaluation.ml", line 700, characters 18-50
Called from file "src/plugins/value/engine/evaluation.ml", line 747, characters 10-57
Called from file "src/plugins/value/engine/evaluation.ml", line 908, characters 14-39
Called from file "src/plugins/value/eval.ml", line 48, characters 29-32
Called from file "src/plugins/value/engine/evaluation.ml", line 834, characters 35-69
Called from file "src/plugins/value/engine/evaluation.ml", line 801, characters 27-57
Called from file "src/plugins/value/engine/evaluation.ml", line 1103, characters 6-36
Called from file "src/plugins/value/engine/evaluation.ml" (inlined), line 1148, characters 4-67
Called from file "src/plugins/value/engine/evaluation.ml", line 1509, characters 23-77
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 157, characters 14-59
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 177, characters 4-54
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 251, characters 10-55
Called from file "src/plugins/value/engine/initialization.ml", line 130, characters 10-48
Called from file "list.ml", line 121, characters 24-34
Called from file "list.ml", line 121, characters 24-34
Called from file "src/kernel_services/ast_data/globals.ml" (inlined), line 128, characters 33-72
Called from file "src/plugins/value/engine/initialization.ml", line 324, characters 15-65
Called from file "src/libraries/project/state_builder.ml", line 403, characters 17-21
Called from file "src/plugins/value/engine/initialization.ml", line 396, characters 20-43
Called from file "src/plugins/value/engine/compute_functions.ml", line 357, characters 10-55
Called from file "src/libraries/project/state_builder.ml", line 994, characters 9-13
Re-raised at file "src/libraries/project/state_builder.ml", line 1002, characters 9-18
Called from file "src/plugins/value/register.ml", line 39, characters 46-66
Called from file "queue.ml", line 121, characters 6-15
Called from file "src/kernel_internals/runtime/boot.ml", line 36, characters 4-20
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 842, characters 2-9
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 872, characters 18-64
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 231, characters 4-8
Unexpected error (Invalid_argument("Z.shift_left: count argument must be positive")).
Please report as 'crash' at https://git.frama-c.com/pub/frama-c/issues
Your Frama-C version is 22.0 (Titanium).
Note that a version and a backtrace alone often do not contain enough
information to understand the bug. Guidelines for reporting bugs are at:
https://git.frama-c.com/pub/frama-c/-/wikis/Guidelines-for-reporting-bugs
```
### Contextual information
- Frama-C installation mode: Opam
- Frama-C version: *Frama-C version* (as reported by `frama-c -version`) 22.0 (Titanium)
- Plug-in used: -eva
- OS name: Ubuntu
- OS version: 18
### Additional information (optional)
I see that there is a similar bug reported 5 years ago (https://git.frama-c.com/pub/frama-c/-/issues/499) which has been marked as fixed but with -wp option instead of -eva. But evidently, we still receive this crash with the given message. I reduced this program manually so that the program is small enough for this bug report. I can provide the original code if required.Andre MaronezeAndre Maronezehttps://git.frama-c.com/pub/frama-c/-/issues/2557Installation on Windows 10 WSL2 Debian?2022-09-28T13:54:37ZNightlyHerbInstallation on Windows 10 WSL2 Debian?Thank you for your development on this project.
I managed to install `frama-c-gui` on WSL2 Ubuntu 20.04 as per the documentation.
I did have to `eval $(opam env)` after **every** `opam` related installation process,
including the last ...Thank you for your development on this project.
I managed to install `frama-c-gui` on WSL2 Ubuntu 20.04 as per the documentation.
I did have to `eval $(opam env)` after **every** `opam` related installation process,
including the last `frama-c` install which would help users if documented more clearly.
When I didn't do this Ubuntu couldn't find `frama-c` from `$PATH`.
I was wondering if the process can be modified to run on Debian?
I couldn't install yaru gtk themes, and as a result could only run frama-c (not the GUI.)
What kind of packages are needed to run the GUI? I may test it.Andre MaronezeAndre Maronezehttps://git.frama-c.com/pub/frama-c/-/issues/2558[frama-clang] Cannot parse built-in function __underlying_type()2021-07-14T17:00:34ZStefan Gränitz[frama-clang] Cannot parse built-in function __underlying_type()<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the iss...<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- you installed Frama-C as prescribed in the [instructions](INSTALL.md).
If the issue applies to a specific Frama-C plug-in, please prefix the title
by the plug-in name: [Eva], [WP], [E-ACSL]…
-->
### Steps to reproduce the issue
Please find attached two example sources that demonstrate the issue:
[fails.cpp](/uploads/61673f65c32ca8006fd5da43333d0b96/fails.cpp)
[works.cpp](/uploads/1ed13606089f45a7eac4f3a3ce77b275/works.cpp)
```
> cat fails.cpp
enum class SelectedNumbers : int { One = 1 };
int main() {
return static_cast<__underlying_type(SelectedNumbers)>(SelectedNumbers::One);
}
> clang++-11 -E -o fails.ii fails.cpp
> frama-c -deps fails.ii
```
### Expected output
```
[kernel] Parsing fails.ii (external front-end)
Now output intermediate result
<...>
[from] Computing for function main
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
These dependencies hold at termination for the executions that terminate:
[from] Function main:
\result FROM \nothing
[from] ====== END OF DEPENDENCIES ======
```
### Actual output
```
[kernel] Parsing fails.ii (external front-end)
fails.cpp:4:10: Unsupported Type (unknown kind (48)):__underlying_type(enum SelectedNumbers)
Aborting
[kernel] User Error: Failed to parse C++ file. See Clang messages for more information
[kernel] User Error: stopping on file "fails1.ii" that has errors.
[kernel] Frama-C aborted: invalid user input.
```
### Minimal working diff
It works if we avoid the `__underlying_type()` built-in function and instead specify it manually:
```
diff -u fails.cpp works.cpp
--- fails.cpp 2021-05-26 10:25:30.839759691 +0000
+++ works.cpp 2021-05-26 10:40:31.251352326 +0000
@@ -1,5 +1,5 @@
enum class SelectedNumbers : int { One = 1 };
int main() {
- return static_cast<__underlying_type(SelectedNumbers)>(SelectedNumbers::One);
+ return static_cast<int>(SelectedNumbers::One);
}
```
### Contextual information
- Frama-C: framac/frama-c:22.0 Docker Image ID e45780e160f1
- Plug-in used: frama-clang-0.0.10 built from official source drop
- Compiler: Debian clang version 11.1.0
- Target: x86_64-pc-linux-gnuVirgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/2559No support for complex numbers via the keyword _Complex2022-04-27T15:22:34ZKarine EMNo support for complex numbers via the keyword _Complex<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the iss...<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- you installed Frama-C as prescribed in the [instructions](INSTALL.md).
If the issue applies to a specific Frama-C plug-in, please prefix the title
by the plug-in name: [Eva], [WP], [E-ACSL]…
-->
### Steps to reproduce the issue
<!--
Please indicate here steps to follow to get a [minimal, complete, and verifiable example](https://stackoverflow.com/help/mcve) which reproduces the issue.
-->
### Expected behaviour
<!--
Please explain here what is the expected behaviour.
-->
Frama-c does not support complex numbers via the keyword _Complex for C code.
See here: https://gcc.gnu.org/onlinedocs/gcc-4.1.2/gcc/Complex.html
### Actual behaviour
<!--
Please explain here what is the actual (faulty) behaviour.
-->
When running this code:
```
float _Complex f;
int main () { }
```
Frama-c returns an error:
```
[kernel] Parsing test12.c (with preprocessing) [kernel] test12.c:1:
syntax error:
Location: line 1, between columns 6 and 15, before or at token: f
1 float _Complex f;
^^^^^^^^^^^^^^^^^
2 int main () { }
[kernel] Frama-C aborted: invalid user input.
```
### Contextual information
- Frama-C installation mode: Opam
- Frama-C version: *Frama-C version* (as reported by `frama-c -version`) 22\.0 (Titanium)
- Plug-in used: -eva
- OS name: Ubuntu
- OS version: 18
### Additional information (optional)
<!--
You may add here any information deemed relevant with regard to this issue,
and tell us if you already tried some workarounds or have some ideas to solve this issue.
-->
We use Frama-c to automatically analyse code from llvm and gcc test-suites; some of the programs triggered this error message.
I reduced the code but I can add the link to the original one.Andre MaronezeAndre Maronezehttps://git.frama-c.com/pub/frama-c/-/issues/2561[frama-clang] Cannot parse C++14 generic lambda2022-04-14T17:19:42ZStefan Gränitz[frama-clang] Cannot parse C++14 generic lambda<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the iss...<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- you installed Frama-C as prescribed in the [instructions](INSTALL.md).
If the issue applies to a specific Frama-C plug-in, please prefix the title
by the plug-in name: [Eva], [WP], [E-ACSL]…
-->
### Steps to reproduce the issue
Please find attached two example sources that demonstrate the issue:
[fails.cpp](/uploads/2a5f09fd150e99bb9978ee9eb06d252f/fails.cpp)
[works.cpp](/uploads/e4f05a0dd3348d8d0367afde1d2f1ec0/works.cpp)
```
> cat fails.cpp
int main(int argc, char *argv[]) {
auto lambda = [](auto argc) { return argc; };
return lambda(argc);
}
> clang++-11 -E -o fails.ii fails.cpp
> frama-c -deps -cpp-extra-args="-std=c++14" fails.ii
```
### Expected output
```
[kernel] Parsing fails.ii (external front-end)
Now output intermediate result
<...>
[from] Computing for function main
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
These dependencies hold at termination for the executions that terminate:
[from] Function UliEUcE__cons:
__fc_lam FROM __fc_closure; __fc_func
[from] Function __fc_lambda_def:
\result FROM argc
[from] Function main:
\result FROM argc
[from] ====== END OF DEPENDENCIES ======
```
### Actual output
```
[kernel] Parsing fails.ii (external front-end)
framaCIRGen: /usr/lib/llvm-11/include/clang/AST/Type.h:671: const clang::ExtQualsTypeCommonBase *clang::QualType::getCommonPtr() const: Assertion `!isNull() && "Cannot retrieve a NULL type pointer"' failed.
Aborted
[kernel] User Error: Failed to parse C++ file. See Clang messages for more information
[kernel] User Error: stopping on file "fails.ii" that has errors.
[kernel] Frama-C aborted: invalid user input.
```
### Minimal working diff
It works if we write `int` instead of `auto` for the type of the lambda parameter:
```
> diff -u fails.cpp works.cpp
--- fails.cpp 2021-06-08 22:42:13 +0200
+++ works.cpp 2021-06-08 22:43:48 +0200
@@ -1,4 +1,4 @@
int main(int argc, char *argv[]) {
- auto lambda = [](auto argc) { return argc; };
+ auto lambda = [](int argc) { return argc; };
return lambda(argc);
}
```
### Contextual information
- Frama-C: framac/frama-c:22.0 Docker Image ID e45780e160f1
- Plug-in used: frama-clang-0.0.10 built from official source drop
- Compiler: Debian clang version 11.1.0
- Target: x86_64-pc-linux-gnu
### Additional information
Generic lambdas are a C++14 language feature:
https://isocpp.org/wiki/faq/cpp14-language#generic-lambdasVirgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/2563Frama-C crashed with an unexpected error Abstract_interp.Error_Bottom2021-06-10T09:45:22ZKarine EMFrama-C crashed with an unexpected error Abstract_interp.Error_Bottom<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the iss...<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- you installed Frama-C as prescribed in the [instructions](INSTALL.md).
If the issue applies to a specific Frama-C plug-in, please prefix the title
by the plug-in name: [Eva], [WP], [E-ACSL]…
-->
### Steps to reproduce the issue
<!--
Please indicate here steps to follow to get a [minimal, complete, and verifiable example](https://stackoverflow.com/help/mcve) which reproduces the issue.
-->
I ran frama-c with these parameters:
```
frama-c -eva -slevel 100 -plevel 255 -eva-precision 5 -val-warn-undefined-pointer-comparison pointer -no-val-alloc-returns-null -warn-signed-overflow -val -no-val-show-progress -machdep x86_64 4ee67af5850fa1e85ef52301e74c7093eba28573.c
```
and 4ee67af5850fa1e85ef52301e74c7093eba28573.c is the following program:
```
__attribute__((noinline)) int
f (int a, int b, int d)
{
int r = 8;
b += d + 42 -((short)((((int)(b)) %((int)(d)))))-((short)((((int)(b)) >>((int)(b))))) + 42 -((short)((((int)(b)) %((int)(d + 42 -((short)((((int)(b)) %((int)(d)))))-((short)((((int)(b)) >>((int)(b))))))))))-((short)((((int)(b)) >>((int)(b)))));
r = b - d + 42 +((long)((((double)(r)) -((double)(r)))))-((int)((((double)(b - d)) -((double)(d)))))-((long)((((int)(b - d)) ^((int)(d)))))+((int)((((double)(b - d)) *((double)(b)))))-((int)((((int)(d)) >>((int)(b - d)))))-((short)((((int)(b)) >>((int)(r)))))-((int)((((int)(b - d)) >>((int)(b)))))+((long)((((int)(d)) &((int)(b - d))))) + 42 +((long)((((double)(r)) -((double)(r)))))-((int)((((int)(b - d + 42 +((long)((((double)(r)) -((double)(r)))))-((int)((((double)(b - d)) -((double)(d)))))-((long)((((int)(b - d)) ^((int)(d)))))+((int)((((double)(b - d)) *((double)(b)))))-((int)((((int)(d)) >>((int)(b - d)))))-((short)((((int)(b)) >>((int)(r)))))-((int)((((int)(b - d)) >>((int)(b)))))+((long)((((int)(d)) &((int)(b - d))))))) %((int)(b - d + 42 +((long)((((double)(r)) -((double)(r)))))-((int)((((double)(b - d)) -((double)(d)))))-((long)((((int)(b - d)) ^((int)(d)))))+((int)((((double)(b - d)) *((double)(b)))))-((int)((((int)(d)) >>((int)(b - d)))))-((short)((((int)(b)) >>((int)(r)))))-((int)((((int)(b - d)) >>((int)(b)))))+((long)((((int)(d)) &((int)(b - d))))))))))-((long)((((int)(b - d + 42 +((long)((((double)(r)) -((double)(r)))))-((int)((((double)(b - d)) -((double)(d)))))-((long)((((int)(b - d)) ^((int)(d)))))+((int)((((double)(b - d)) *((double)(b)))))-((int)((((int)(d)) >>((int)(b - d)))))-((short)((((int)(b)) >>((int)(r)))))-((int)((((int)(b - d)) >>((int)(b)))))+((long)((((int)(d)) &((int)(b - d))))))) ^((int)(b - d + 42 +((long)((((double)(r)) -((double)(r)))))-((int)((((double)(b - d)) -((double)(d)))))-((long)((((int)(b - d)) ^((int)(d)))))+((int)((((double)(b - d)) *((double)(b)))))-((int)((((int)(d)) >>((int)(b - d)))))-((short)((((int)(b)) >>((int)(r)))))-((int)((((int)(b - d)) >>((int)(b)))))+((long)((((int)(d)) &((int)(b - d))))))))))+((int)((((int)(b - d + 42 +((long)((((double)(r)) -((double)(r)))))-((int)((((double)(b - d)) -((double)(d)))))-((long)((((int)(b - d)) ^((int)(d)))))+((int)((((double)(b - d)) *((double)(b)))))-((int)((((int)(d)) >>((int)(b - d)))))-((short)((((int)(b)) >>((int)(r)))))-((int)((((int)(b - d)) >>((int)(b)))))+((long)((((int)(d)) &((int)(b - d))))))) &((int)(r)))))-((int)((((int)(b - d + 42 +((long)((((double)(r)) -((double)(r)))))-((int)((((double)(b - d)) -((double)(d)))))-((long)((((int)(b - d)) ^((int)(d)))))+((int)((((double)(b - d)) *((double)(b)))))-((int)((((int)(d)) >>((int)(b - d)))))-((short)((((int)(b)) >>((int)(r)))))-((int)((((int)(b - d)) >>((int)(b)))))+((long)((((int)(d)) &((int)(b - d))))))) >>((int)(b - d + 42 +((long)((((double)(r)) -((double)(r)))))-((int)((((double)(b - d)) -((double)(d)))))-((long)((((int)(b - d)) ^((int)(d)))))+((int)((((double)(b - d)) *((double)(b)))))-((int)((((int)(d)) >>((int)(b - d)))))-((short)((((int)(b)) >>((int)(r)))))-((int)((((int)(b - d)) >>((int)(b)))))+((long)((((int)(d)) &((int)(b - d))))))))))-((short)((((int)(r)) >>((int)(r)))))-((int)((((int)(b - d + 42 +((long)((((double)(r)) -((double)(r)))))-((int)((((double)(b - d)) -((double)(d)))))-((long)((((int)(b - d)) ^((int)(d)))))+((int)((((double)(b - d)) *((double)(b)))))-((int)((((int)(d)) >>((int)(b - d)))))-((short)((((int)(b)) >>((int)(r)))))-((int)((((int)(b - d)) >>((int)(b)))))+((long)((((int)(d)) &((int)(b - d))))))) >>((int)(r)))))+((long)((((int)(b - d + 42 +((long)((((double)(r)) -((double)(r)))))-((int)((((double)(b - d)) -((double)(d)))))-((long)((((int)(b - d)) ^((int)(d)))))+((int)((((double)(b - d)) *((double)(b)))))-((int)((((int)(d)) >>((int)(b - d)))))-((short)((((int)(b)) >>((int)(r)))))-((int)((((int)(b - d)) >>((int)(b)))))+((long)((((int)(d)) &((int)(b - d))))))) &((int)(b - d + 42 +((long)((((double)(r)) -((double)(r)))))-((int)((((double)(b - d)) -((double)(d)))))-((long)((((int)(b - d)) ^((int)(d)))))+((int)((((double)(b - d)) *((double)(b)))))-((int)((((int)(d)) >>((int)(b - d)))))-((short)((((int)(b)) >>((int)(r)))))-((int)((((int)(b - d)) >>((int)(b)))))+((long)((((int)(d)) &((int)(b - d))))))))));
return r;
}
int
main (void)
{
int l = 8;
asm ("" : "=r" (l) : "0" ((-(-2))));
if (((int)((int)f (l + (-(-2)), l + (-(-3)), l + (-(-6))) != -(-(-3)) + 42 -((short)((((double)(-(-(-3)))) -((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))-((int)((((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) -((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))+((long)((((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) *((double)(-(-(-3)))))))-((short)((((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) <<((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))*((short)((((int)(-(-(-3)))) &((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))-((short)((((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) |((int)(-(-(-3)))))))+((short)((((double)(-(-(-3)))) *((double)(-(-(-3)))))))*((int)((((int)(-(-(-3)))) <<((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))-((long)((((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) %((int)(-(-(-3)))))))+((long)((((int)(-(-(-3)))) |((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))) + 42 -((short)((((int)(-(-(-3)) + 42 -((short)((((double)(-(-(-3)))) -((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))-((int)((((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) -((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))+((long)((((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) *((double)(-(-(-3)))))))-((short)((((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) <<((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))*((short)((((int)(-(-(-3)))) &((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))-((short)((((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) |((int)(-(-(-3)))))))+((short)((((double)(-(-(-3)))) *((double)(-(-(-3)))))))*((int)((((int)(-(-(-3)))) <<((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))-((long)((((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) %((int)(-(-(-3)))))))+((long)((((int)(-(-(-3)))) |((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6)))))))))) %((int)((int)f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))-((int)((((int)((int)f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) %((int)(-(-(-3)) + 42 -((short)((((double)(-(-(-3)))) -((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))-((int)((((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) -((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))+((long)((((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) *((double)(-(-(-3)))))))-((short)((((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) <<((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))*((short)((((int)(-(-(-3)))) &((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))-((short)((((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) |((int)(-(-(-3)))))))+((short)((((double)(-(-(-3)))) *((double)(-(-(-3)))))))*((int)((((int)(-(-(-3)))) <<((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6)))))))))))))+((long)((((int)(-(-(-3)) + 42 -((short)((((double)(-(-(-3)))) -((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))-((int)((((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) -((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))+((long)((((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) *((double)(-(-(-3))))))))) &((int)(((short)((((double)(-(-(-3)))) *((double)(-(-(-3)))))))*((int)((((int)(-(-(-3)))) <<((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6)))))))))))))-((short)((((int)((int)f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) <<((int)((int)f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))*((short)((((int)(((short)((((double)(-(-(-3)))) *((double)(-(-(-3)))))))*((int)((((int)(-(-(-3)))) <<((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6)))))))))) &((int)(-(-(-3)) + 42 -((short)((((double)(-(-(-3)))) -((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))-((int)((((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) -((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))+((long)((((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) *((double)(-(-(-3)))))))-((short)((((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) <<((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))*((short)((((int)(-(-(-3)))) &((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))-((short)((((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) |((int)(-(-(-3)))))))+((short)((((double)(-(-(-3)))) *((double)(-(-(-3)))))))*((int)((((int)(-(-(-3)))) <<((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6)))))))))))))-((short)((((int)(-(-(-3)) + 42 -((short)((((double)(-(-(-3)))) -((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))-((int)((((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) -((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))+((long)((((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) *((double)(-(-(-3)))))))-((short)((((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) <<((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))*((short)((((int)(-(-(-3)))) &((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))-((short)((((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) |((int)(-(-(-3))))))))) |((int)(((long)((((int)(-(-(-3)))) |((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6)))))))))))))+((short)((((int)(((long)((((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) *((double)(-(-(-3))))))))) &((int)(((long)((((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) *((double)(-(-(-3))))))))))))*((int)((((int)(((short)((((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) <<((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))*((short)((((int)(-(-(-3)))) &((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6)))))))))) <<((int)(-(-(-3)) + 42 -((short)((((double)(-(-(-3)))) -((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))-((int)((((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) -((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))+((long)((((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) *((double)(-(-(-3))))))))))))-((long)((((int)(-(-(-3)) + 42 -((short)((((double)(-(-(-3)))) -((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))-((int)((((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) -((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))+((long)((((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) *((double)(-(-(-3)))))))-((short)((((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) <<((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))*((short)((((int)(-(-(-3)))) &((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))-((short)((((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) |((int)(-(-(-3))))))))) %((int)(((long)((((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) %((int)(-(-(-3))))))))))))+((long)((((int)(-(-(-3)) + 42 -((short)((((double)(-(-(-3)))) -((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))-((int)((((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) -((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))+((long)((((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) *((double)(-(-(-3)))))))-((short)((((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) <<((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))*((short)((((int)(-(-(-3)))) &((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))-((short)((((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) |((int)(-(-(-3)))))))+((short)((((double)(-(-(-3)))) *((double)(-(-(-3)))))))*((int)((((int)(-(-(-3)))) <<((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))-((long)((((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) %((int)(-(-(-3)))))))+((long)((((int)(-(-(-3)))) |((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6)))))))))) |((int)(-(-(-3)) + 42 -((short)((((double)(-(-(-3)))) -((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))-((int)((((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) -((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))+((long)((((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) *((double)(-(-(-3)))))))-((short)((((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) <<((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))*((short)((((int)(-(-(-3)))) &((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))-((short)((((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) |((int)(-(-(-3)))))))+((short)((((double)(-(-(-3)))) *((double)(-(-(-3)))))))*((int)((((int)(-(-(-3)))) <<((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6)))))))))))))))
return 0;
}
```
### Expected behaviour
<!--
Please explain here what is the expected behaviour.
-->
Not to crash.
### Actual behaviour
<!--
Please explain here what is the actual (faulty) behaviour.
-->
The program crashed with this trace:
```
[kernel] Warning: -slevel is a deprecated alias for option -eva-slevel.
Please use -eva-slevel instead.
[kernel] Warning: -plevel is a deprecated alias for option -eva-plevel.
Please use -eva-plevel instead.
[kernel] Warning: -val-warn-undefined-pointer-comparison is a deprecated alias
for option -eva-warn-undefined-pointer-comparison.
Please use -eva-warn-undefined-pointer-comparison instead.
[kernel] Warning: -no-val-alloc-returns-null is a deprecated alias
for option -eva-no-alloc-returns-null.
Please use -eva-no-alloc-returns-null instead.
[kernel] Warning: -val is a deprecated alias for option -eva. Please use -eva instead.
[kernel] Warning: -no-val-show-progress is a deprecated alias for option -eva-no-show-progress.
Please use -eva-no-show-progress instead.
[kernel] Parsing 4ee67af5850fa1e85ef52301e74c7093eba28573.c (with preprocessing)
[eva] Option -eva-precision 5 detected, automatic configuration of the analysis:
option -eva-min-loop-unroll set to 0 (default value).
option -eva-auto-loop-unroll set to 128.
option -eva-widening-delay set to 3 (default value).
option -eva-partition-history set to 0 (default value).
option -eva-slevel already set to 100.
option -eva-ilevel set to 48.
option -eva-plevel already set to 255 (not modified).
option -eva-subdivide-non-linear set to 100.
option -eva-remove-redundant-alarms set to true (default value).
option -eva-domains set to 'cvalue,equality,gauges,octagon,symbolic-locations'.
option -eva-split-return set to 'auto'.
option -eva-equality-through-calls set to 'formals' (default value).
option -eva-octagon-through-calls set to false (default value).
[eva] Splitting return states on:
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
[eva:alarm] 4ee67af5850fa1e85ef52301e74c7093eba28573.c:17: Warning:
signed overflow. assert l + (int)(-((int)(-6))) ≤ 2147483647;
[eva:alarm] 4ee67af5850fa1e85ef52301e74c7093eba28573.c:6: Warning:
division by zero. assert d ≢ 0;
[eva:alarm] 4ee67af5850fa1e85ef52301e74c7093eba28573.c:6: Warning:
invalid RHS operand for shift. assert 0 ≤ b < 32;
[eva:alarm] 4ee67af5850fa1e85ef52301e74c7093eba28573.c:6: Warning:
signed overflow. assert d + 42 ≤ 2147483647;
[eva:alarm] 4ee67af5850fa1e85ef52301e74c7093eba28573.c:6: Warning:
signed overflow.
assert -2147483648 ≤ (int)(d + 42) - (int)((short)((int)(b % d)));
[eva:alarm] 4ee67af5850fa1e85ef52301e74c7093eba28573.c:6: Warning:
signed overflow.
assert (int)(d + 42) - (int)((short)((int)(b % d))) ≤ 2147483647;
[eva:alarm] 4ee67af5850fa1e85ef52301e74c7093eba28573.c:6: Warning:
division by zero.
assert
(int)((int)((int)(d + 42) - (int)((short)((int)(b % d)))) -
(int)((short)((int)(b >> b))))
≢ 0;
[eva:alarm] 4ee67af5850fa1e85ef52301e74c7093eba28573.c:6: Warning:
signed overflow.
assert
(int)((int)((int)(d + 42) - (int)((short)((int)(b % d)))) -
(int)((short)((int)(b >> b))))
+ 42 ≤ 2147483647;
[eva:alarm] 4ee67af5850fa1e85ef52301e74c7093eba28573.c:6: Warning:
signed overflow.
assert
b +
(int)((int)((int)((int)((int)((int)(d + 42) - (int)((short)((int)(b % d)))) -
(int)((short)((int)(b >> b))))
+ 42)
-
(int)((short)((int)(b %
(int)((int)((int)(d + 42) -
(int)((short)((int)(b % d))))
- (int)((short)((int)(b >> b))))))))
- (int)((short)((int)(b >> b))))
≤ 2147483647;
[kernel] Current source was: 4ee67af5850fa1e85ef52301e74c7093eba28573.c:8
The full backtrace is:
Raised at file "src/kernel_services/abstract_interp/ival.ml", line 267, characters 14-32
Called from file "src/kernel_services/abstract_interp/ival.ml", line 281, characters 16-30
Called from file "src/plugins/value/domains/octagons.ml", line 352, characters 11-43
Called from file "src/plugins/value/domains/octagons.ml", line 360, characters 8-74
Called from file "src/plugins/value/domains/octagons.ml", line 395, characters 19-48
Called from file "src/plugins/value/domains/octagons.ml", line 1054, characters 6-77
Called from file "src/plugins/value/domains/domain_product.ml", line 94, characters 6-42
Called from file "src/plugins/value/domains/domain_product.ml", line 95, characters 6-44
Called from file "src/plugins/value/domains/domain_product.ml", line 95, characters 6-44
Called from file "src/plugins/value/domains/domain_product.ml", line 95, characters 6-44
Called from file "src/plugins/value/engine/evaluation.ml", line 837, characters 36-73
Called from file "src/plugins/value/engine/evaluation.ml", line 801, characters 27-57
Called from file "src/plugins/value/engine/evaluation.ml", line 899, characters 6-34
Called from file "src/plugins/value/engine/evaluation.ml", line 834, characters 35-69
Called from file "src/plugins/value/engine/evaluation.ml", line 801, characters 27-57
Called from file "src/plugins/value/engine/evaluation.ml", line 907, characters 6-33
Called from file "src/plugins/value/engine/evaluation.ml", line 834, characters 35-69
Called from file "src/plugins/value/engine/evaluation.ml", line 801, characters 27-57
Called from file "src/plugins/value/engine/evaluation.ml", line 899, characters 6-34
Called from file "src/plugins/value/engine/evaluation.ml", line 834, characters 35-69
Called from file "src/plugins/value/engine/evaluation.ml", line 801, characters 27-57
Called from file "src/plugins/value/engine/evaluation.ml", line 899, characters 6-34
Called from file "src/plugins/value/engine/evaluation.ml", line 834, characters 35-69
Called from file "src/plugins/value/engine/evaluation.ml", line 801, characters 27-57
Called from file "src/plugins/value/engine/evaluation.ml", line 899, characters 6-34
Called from file "src/plugins/value/engine/evaluation.ml", line 834, characters 35-69
Called from file "src/plugins/value/engine/evaluation.ml", line 801, characters 27-57
Called from file "src/plugins/value/engine/evaluation.ml", line 899, characters 6-34
Called from file "src/plugins/value/engine/evaluation.ml", line 834, characters 35-69
Called from file "src/plugins/value/engine/evaluation.ml", line 801, characters 27-57
Called from file "src/plugins/value/engine/evaluation.ml", line 899, characters 6-34
Called from file "src/plugins/value/engine/evaluation.ml", line 834, characters 35-69
Called from file "src/plugins/value/engine/evaluation.ml", line 801, characters 27-57
Called from file "src/plugins/value/engine/evaluation.ml", line 899, characters 6-34
Called from file "src/plugins/value/engine/evaluation.ml", line 834, characters 35-69
Called from file "src/plugins/value/engine/evaluation.ml", line 801, characters 27-57
Called from file "src/plugins/value/engine/evaluation.ml", line 899, characters 6-34
Called from file "src/plugins/value/engine/evaluation.ml", line 834, characters 35-69
Called from file "src/plugins/value/engine/evaluation.ml", line 801, characters 27-57
Called from file "src/plugins/value/engine/evaluation.ml", line 899, characters 6-34
Called from file "src/plugins/value/engine/evaluation.ml", line 834, characters 35-69
Called from file "src/plugins/value/engine/evaluation.ml", line 801, characters 27-57
Called from file "src/plugins/value/engine/evaluation.ml", line 899, characters 6-34
Called from file "src/plugins/value/engine/evaluation.ml", line 834, characters 35-69
Called from file "src/plugins/value/engine/evaluation.ml", line 801, characters 27-57
Called from file "src/plugins/value/engine/evaluation.ml", line 899, characters 6-34
Called from file "src/plugins/value/engine/evaluation.ml", line 834, characters 35-69
Called from file "src/plugins/value/engine/evaluation.ml", line 801, characters 27-57
Called from file "src/plugins/value/engine/evaluation.ml", line 899, characters 6-34
Called from file "src/plugins/value/engine/evaluation.ml", line 834, characters 35-69
Called from file "src/plugins/value/engine/evaluation.ml", line 801, characters 27-57
Called from file "src/plugins/value/engine/evaluation.ml", line 899, characters 6-34
Called from file "src/plugins/value/engine/evaluation.ml", line 834, characters 35-69
Called from file "src/plugins/value/engine/evaluation.ml", line 801, characters 27-57
Called from file "src/plugins/value/engine/evaluation.ml", line 899, characters 6-34
Called from file "src/plugins/value/engine/evaluation.ml", line 834, characters 35-69
Called from file "src/plugins/value/engine/evaluation.ml", line 801, characters 27-57
Called from file "src/plugins/value/engine/evaluation.ml", line 899, characters 6-34
Called from file "src/plugins/value/engine/evaluation.ml", line 834, characters 35-69
Called from file "src/plugins/value/engine/evaluation.ml", line 801, characters 27-57
Called from file "src/plugins/value/engine/evaluation.ml", line 899, characters 6-34
Called from file "src/plugins/value/engine/evaluation.ml", line 834, characters 35-69
Called from file "src/plugins/value/engine/evaluation.ml", line 801, characters 27-57
Called from file "src/plugins/value/engine/evaluation.ml", line 899, characters 6-34
Called from file "src/plugins/value/engine/evaluation.ml", line 834, characters 35-69
Called from file "src/plugins/value/engine/evaluation.ml", line 801, characters 27-57
Called from file "src/plugins/value/engine/evaluation.ml", line 899, characters 6-34
Called from file "src/plugins/value/engine/evaluation.ml", line 834, characters 35-69
Called from file "src/plugins/value/engine/evaluation.ml", line 801, characters 27-57
Called from file "src/plugins/value/engine/evaluation.ml", line 907, characters 6-33
Called from file "src/plugins/value/engine/evaluation.ml", line 834, characters 35-69
Called from file "src/plugins/value/engine/evaluation.ml", line 801, characters 27-57
Called from file "src/plugins/value/engine/evaluation.ml", line 1103, characters 6-36
Called from file "src/plugins/value/engine/subdivided_evaluation.ml", line 664, characters 25-60
Called from file "src/plugins/value/engine/subdivided_evaluation.ml", line 602, characters 21-38
Called from file "list.ml", line 121, characters 24-34
Called from file "src/plugins/value/engine/subdivided_evaluation.ml", line 618, characters 23-76
Called from file "src/plugins/value/engine/subdivided_evaluation.ml", line 685, characters 17-73
Called from file "src/plugins/value/engine/evaluation.ml" (inlined), line 1148, characters 4-67
Called from file "src/plugins/value/engine/evaluation.ml", line 1509, characters 23-77
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 157, characters 14-59
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 177, characters 4-54
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 251, characters 10-55
Called from file "src/plugins/value/engine/iterator.ml" (inlined), line 233, characters 28-33
Called from file "src/plugins/value/engine/iterator.ml", line 261, characters 4-60
Called from file "src/plugins/value/partitioning/partition.ml", line 494, characters 29-34
Called from file "list.ml", line 121, characters 24-34
Called from file "src/plugins/value/engine/iterator.ml", line 430, characters 15-71
Called from file "src/plugins/value/engine/iterator.ml", line 494, characters 18-35
Called from file "list.ml", line 92, characters 20-23
Called from file "src/plugins/value/engine/iterator.ml", line 496, characters 18-60
Called from file "src/plugins/value/engine/iterator.ml", line 543, characters 13-31
Called from file "list.ml", line 110, characters 12-15
Called from file "src/plugins/value/engine/iterator.ml" (inlined), line 540, characters 4-31
Called from file "src/plugins/value/engine/iterator.ml", line 602, characters 6-22
Called from file "src/plugins/value/engine/iterator.ml", line 769, characters 20-39
Called from file "src/plugins/value/engine/compute_functions.ml", line 201, characters 8-45
Called from file "src/plugins/value/engine/compute_functions.ml", line 221, characters 26-36
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 318, characters 10-43
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 456, characters 22-60
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 758, characters 26-75
Called from file "src/kernel_services/abstract_interp/bottom.ml" (inlined), line 31, characters 18-21
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 754, characters 10-447
Called from file "list.ml", line 121, characters 24-34
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 769, characters 24-59
Called from file "src/kernel_services/abstract_interp/bottom.ml" (inlined), line 31, characters 18-21
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 742, characters 6-1023
Called from file "src/plugins/value/engine/iterator.ml", line 274, characters 6-47
Called from file "src/plugins/value/partitioning/partition.ml", line 494, characters 29-34
Called from file "list.ml", line 121, characters 24-34
Called from file "src/plugins/value/engine/iterator.ml", line 430, characters 15-71
Called from file "src/plugins/value/engine/iterator.ml", line 494, characters 18-35
Called from file "list.ml", line 92, characters 20-23
Called from file "src/plugins/value/engine/iterator.ml", line 496, characters 18-60
Called from file "src/plugins/value/engine/iterator.ml", line 543, characters 13-31
Called from file "list.ml", line 110, characters 12-15
Called from file "src/plugins/value/engine/iterator.ml" (inlined), line 540, characters 4-31
Called from file "src/plugins/value/engine/iterator.ml", line 602, characters 6-22
Called from file "src/plugins/value/engine/iterator.ml", line 769, characters 20-39
Called from file "src/plugins/value/engine/compute_functions.ml", line 201, characters 8-45
Called from file "src/plugins/value/engine/compute_functions.ml", line 333, characters 25-75
Called from file "src/libraries/project/state_builder.ml", line 994, characters 9-13
Re-raised at file "src/libraries/project/state_builder.ml", line 1002, characters 9-18
Called from file "src/plugins/value/register.ml", line 39, characters 46-66
Called from file "queue.ml", line 121, characters 6-15
Called from file "src/kernel_internals/runtime/boot.ml", line 36, characters 4-20
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 842, characters 2-9
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 872, characters 18-64
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 231, characters 4-8
Unexpected error (Abstract_interp.Error_Bottom).
Please report as 'crash' at https://git.frama-c.com/pub/frama-c/issues
Your Frama-C version is 22.0 (Titanium).
Note that a version and a backtrace alone often do not contain enough
information to understand the bug. Guidelines for reporting bugs are at:
https://git.frama-c.com/pub/frama-c/-/wikis/Guidelines-for-reporting-bugs
```
### Contextual information
- Frama-C installation mode: Opam
- Frama-C version: *Frama-C version* (as reported by `frama-c -version`) 22.0 (Titanium)
- Plug-in used: eva
- OS name: Ubuntu
- OS version: 18
### Additional information (optional)
<!--
You may add here any information deemed relevant with regard to this issue,
and tell us if you already tried some workarounds or have some ideas to solve this issue.
-->Andre MaronezeAndre Maronezehttps://git.frama-c.com/pub/frama-c/-/issues/2564[frama-clang] std::forward with non-primitive type causes NON TERMINATING2022-04-22T13:54:07ZStefan Gränitz[frama-clang] std::forward with non-primitive type causes NON TERMINATING<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the iss...<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- you installed Frama-C as prescribed in the [instructions](INSTALL.md).
If the issue applies to a specific Frama-C plug-in, please prefix the title
by the plug-in name: [Eva], [WP], [E-ACSL]…
-->
### Steps to reproduce the issue
~~Please find attached two example sources that demonstrate the issue: [fails.cpp](/uploads/69d2c79afe05be14b237e337c90f0d9b/fails.cpp) [works.cpp](/uploads/a28e5308e6b0f638172b084eb5572861/works.cpp)~~
Please find attached the narrowed example sources that demonstrate the issue with `std::forward` alone:
[fails.cpp](/uploads/8f135c54a38dc95e8cb162033dc7e29b/fails.cpp)[works.cpp](/uploads/1c2846a51c27d8cd745afff3baf6d950/works.cpp)
**Further investigation details can be found in the comments.** What follows here is the original issue description:
```
> cat fails.cpp
#include <memory>
struct Foo {
int val;
Foo(int val) : val(val) {}
int bar() { return val; }
};
int main(int argc, char **argv) {
std::unique_ptr<Foo> foo1(new Foo(argc));
std::unique_ptr<Foo> foo2 = std::move(foo1);
return foo2->bar();
}
> frama-c -deps fails.cpp
```
### Expected behaviour
```
[kernel] Parsing fails.cpp (external front-end)
Now output intermediate result
...
[from] Function main:
__malloc_main_l10 FROM argc
\result FROM argc
[from] ====== END OF DEPENDENCIES ======
```
### Actual behaviour
```
[kernel] Parsing fails.cpp (external front-end)
Now output intermediate result
...
[from] Function main:
NON TERMINATING - NO EFFECTS
[from] ====== END OF DEPENDENCIES ======
```
### Minimal working diff
It works if we avoid the move assignment:
```
> diff -u fails.cpp works.cpp
--- fails.cpp 2021-06-21 10:40:26.613967584 +0000
+++ works.cpp 2021-06-21 10:38:12.276859713 +0000
@@ -8,6 +8,5 @@
int main(int argc, char **argv) {
std::unique_ptr<Foo> foo1(new Foo(argc));
- std::unique_ptr<Foo> foo2 = std::move(foo1);
- return foo2->bar();
+ return foo1->bar();
}
```
### Contextual information
* Frama-C: framac/frama-c:22.0 Docker Image ID e45780e160f1
* Plug-in used: frama-clang-0.0.10 built from official source drop
* Compiler: Debian clang version 11.1.0
* Target: x86_64-pc-linux-gnu
### Additional information
One more observation is that the plugin is unable to parse a preprocessed source file:
```
> clang++-11 -E -o works.ii works.cpp
> frama-c -deps works.ii
[kernel] Parsing works.ii (external front-end)
works.ii:316:32: error: __int128 is not supported on this target
template<> struct __is_integer<__int128> { enum { __value = 1 }; typedef __true_type __type; }; template<> struct __is_integer<unsigned __int128> { enum { __value = 1 }; typedef __true_type __type; };
^
...
code generation aborted due to compilation errors
[kernel] User Error: Failed to parse C++ file. See Clang messages for more information
[kernel] User Error: stopping on file "works.ii" that has errors.
[kernel] Frama-C aborted: invalid user input.
```Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/2565Arch Linux package uninstallable due to dependency that no longer exists2021-10-06T07:53:07ZOlivier NicoleArch Linux package uninstallable due to dependency that no longer exists- [X] the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- [X] the issue has not yet been reported on our old
[BTS](https://bts.frama-c.com) (*note: the old BTS is deprecated*);
- [ ] you insta...- [X] the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- [X] the issue has not yet been reported on our old
[BTS](https://bts.frama-c.com) (*note: the old BTS is deprecated*);
- [ ] you installed Frama-C as prescribed in the [instructions](INSTALL.md).
# Contextual information
- Frama-C installation mode: Arch Linux User Repository package
- Frama-C version: 21.1-1
- Plug-in used: N/A
- OS name: Arch Linux
- OS version: N/A
The Arch Linux User Repository package `frama-c` depends on gtksourceview2 which seems to no longer exist in the repositories, preventing the installation.
# Fix ideas
I'm not sure which would be simpler between upgrading to a newer version of gtksourceview or making that dependency available again.https://git.frama-c.com/pub/frama-c/-/issues/2566[WP] Frama-C Vanadium crashes when calling RTE through WP on complicated or a...2021-07-20T11:07:43ZYani ZIANI[WP] Frama-C Vanadium crashes when calling RTE through WP on complicated or abstract structures<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the iss...<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- you installed Frama-C as prescribed in the [instructions](INSTALL.md).
If the issue applies to a specific Frama-C plug-in, please prefix the title
by the plug-in name: [Eva], [WP], [E-ACSL]…
-->
I've run into some trouble trying to parse and verify C code with complicated data structures.
Please note that I've also been able to reproduce the same error with more complex structures, but the following example only features an abstract data structure so as to keep it as minimal as (probably) possible.
### Steps to reproduce the issue
<!--
Please indicate here steps to follow to get a [minimal, complete, and verifiable example](https://stackoverflow.com/help/mcve) which reproduces the issue.
-->
Running Frama-C on the following code using the ``-wp-rte`` option:
```C
#include <stdint.h>
#include <string.h>
typedef struct _TEST_STRUCT BLOB;
int test_fun(int alg, uint8_t * key, size_t keySize, const char *label)
{
size_t lsize = strlen(label) + 1; //crashes frama-c if uncommented
BLOB *context;
int r = update(context);
return 0;
}
/*frama-c code.c -wp -wp-rte*/
```
### Expected behaviour
<!--
Please explain here what is the expected behaviour.
-->
Frama-C Vanadium parsing the code without any issue, and having WP call the RTE plugin, much like Frama-C Titanium.
### Actual behaviour
<!--
Please explain here what is the actual (faulty) behaviour.
-->
Vanadium crashes when the "strlen" line is uncommented, returning the following error:
```
Uncaught exception:
Current source was: frama_tests/crypto_crash/crypto_crash.c:7
The full backtrace is:
Raised at file "src/kernel_services/plugin_entry_points/log.ml" (inlined), line 546, characters 24-31
Called from file "src/kernel_services/plugin_entry_points/log.ml", line 1115, characters 17-55
Called from file "src/kernel_services/plugin_entry_points/log.ml", line 539, characters 9-23
Re-raised at file "src/kernel_services/plugin_entry_points/log.ml", line 542, characters 9-16
Called from file "src/kernel_services/ast_queries/cil_datatype.ml", line 2207, characters 34-294
Called from file "hashtbl.ml", line 512, characters 17-31
Called from file "src/libraries/project/state_builder.ml" (inlined), line 550, characters 17-34
Called from file "src/libraries/project/state_builder.ml", line 561, characters 16-24
Called from file "list.ml", line 164, characters 12-15
Called from file "src/plugins/wp/GuiSource.ml", line 111, characters 17-38
Called from file "src/plugins/gui/design.ml", line 728, characters 6-11
Frama-C aborted: internal error.
Reverting to previous state.
Check the Console tab for additional information.
Please report as 'crash' at https://git.frama-c.com/pub/frama-c/issues
Your Frama-C version is 23.0 (Vanadium).
Note that a version and a backtrace alone often do not contain enough
information to understand the bug. Guidelines for reporting bugs are at:
https://git.frama-c.com/pub/frama-c/-/wikis/Guidelines-for-reporting-bugs
```
### Contextual information
- Frama-C installation mode: *Opam*
- Frama-C version: 23.0 (Vanadium)
- Plug-in used: WP and RTE, tested both ``-wp-rte`` and ``-rte`` options
- OS name: Ubuntu
- OS version: 20.04.2 LTS
### Additional information (optional)
<!--
You may add here any information deemed relevant with regard to this issue,
and tell us if you already tried some workarounds or have some ideas to solve this issue.
-->
In the more extensive code I'm actually working on, I've also noticed that:
- Frama-C *Titanium* run with the``-wp -rte`` options seems to behave similarly as with the ``-wp -wp-rte`` options, and does not crash in either of those cases.
- Frama-C *Vanadium* run with the ``-wp -rte`` options does not crash, and seems to behave in a similar way to Frama-C *Titanium* using the previous options.
I'm actually not sure what the fundamental differences between calling the RTE plugin through the ``-rte`` option and calling it through WP, but would it be possible to use ``-rte`` as a temporary workaround ?
FYI @nkosmatovAllan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/2571struct fields not assignable if any are const2021-08-31T16:52:57ZAaron Carrollstruct fields not assignable if any are const### Steps to reproduce the issue
Consider the following C snippet:
```
struct A {
const int x;
int y;
};
static struct A a;
/*@
assigns a.y;
*/
void f(void)
{
a.y = 1;
}
```
produces:
```
$ frama-c test_global_assi...### Steps to reproduce the issue
Consider the following C snippet:
```
struct A {
const int x;
int y;
};
static struct A a;
/*@
assigns a.y;
*/
void f(void)
{
a.y = 1;
}
```
produces:
```
$ frama-c test_global_assign.c
[kernel] Parsing test_global_assign.c (with preprocessing)
[kernel:annot-error] test_global_assign.c:9: Warning:
not an assignable left value: a.y. Ignoring logic specification of function f
[kernel] User Error: warning annot-error treated as fatal error.
[kernel] User Error: stopping on file "test_global_assign.c" that has errors. Add
'-kernel-msg-key pp' for preprocessing command.
[kernel] Frama-C aborted: invalid user input.
```
### Expected behavior
Frama-C should accept the snippet since the `y` field of `a` is mutable.
### Actual behaviour
Code is rejected for `a.y` being non-assignable lvalue. Frama-C seems to treat the entire struct `a` as const, even though only one field is declared const. Removing the `const` specifier from `x` causes Frama-C to accept the code.
### Contextual information
23.1 (Vanadium) via opam on macOS. Does not reproduce on Frama-C 22.Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/2572[WP] Lange Projekt course Stack Overflow in WP Plugin since 23.02021-10-27T06:27:08ZAndreas Werner[WP] Lange Projekt course Stack Overflow in WP Plugin since 23.0Hi for some time I Analyse a big Embedded Software Projekt for my Dissertation Project, the project has over 3000 LOCs.
Until Version 23.0 we have a Stack Overflow Error in the WP Plugin.
The Proof is currently Work-in-Progress.
### S...Hi for some time I Analyse a big Embedded Software Projekt for my Dissertation Project, the project has over 3000 LOCs.
Until Version 23.0 we have a Stack Overflow Error in the WP Plugin.
The Proof is currently Work-in-Progress.
### Steps to reproduce the issue
I am unable to reproduce the bug in a small Projekt, to verify the Projekt you can use the Offizial docker container.
To reproduce the bug you can clone the whole Projekt:
Small Script to clone the whole Projekt:
```
git clone https://gitlab.cs.hs-rm.de/CaroloCup/carolocupFirmware.git --recurse-submodules
cd carolocupFirmware
git remote add diss https://gitlab.cs.hs-rm.de/projekte_werner/carolocupFirmware.git
git fetch
git pull diss master
git submodule update
make carFramaC_defconfig # Init Config
make silentoldconfig # Fix Error in Config
FRAMAC=1 make # Run Frama-C
```
Our CI Server run an Verifikation automatically, we use the Offizial docker container.
We test the bug under differierend Version of Frama-C here the result:
- Frama-C Version 22.0: https://gitlab.cs.hs-rm.de/projekte_werner/carolocupFirmware/-/jobs/20042
- Frama-C Version 23.1: https://gitlab.cs.hs-rm.de/projekte_werner/carolocupFirmware/-/jobs/20043
- Frama-C Version Dev: https://gitlab.cs.hs-rm.de/projekte_werner/carolocupFirmware/-/jobs/20044
On the Version 22.0 Frama-C run to completion, on the latest Release and on the latest dev build a Stack Overflow occurred on the same code.
### Expected behaviour
Run without Stack Overflow link in Frama-C Version 22.0
### Actual behaviour
Stack Overflow in Version 23, 23.1 and dev.
### Contextual information
- Frama-C installation mode: Offizial Docker Container
- Frama-C version: 22.0, 23.0, 23.1, 23.1-dev
- Plug-in used: WP, EVA, RTE
- OS name: Docker
- OS version: Docker
### Additional information (optional)
I tried to increase the stack size with `ulimit` (Until 8GB) same result.Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/2573Frama-c fails parsing gcc/llvm single source test case (exit with "invalid us...2022-07-11T16:12:43ZKarine EMFrama-c fails parsing gcc/llvm single source test case (exit with "invalid user input")<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the iss...<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- you installed Frama-C as prescribed in the [instructions](INSTALL.md).
If the issue applies to a specific Frama-C plug-in, please prefix the title
by the plug-in name: [Eva], [WP], [E-ACSL]…
-->
### Steps to reproduce the issue
```
frama-c pr85169.c
```
see the code below or get from here: https://github.com/llvm/llvm-test-suite/blob/main/SingleSource/Regression/C/gcc-c-torture/execute/pr85169.c
<!--
Please indicate here steps to follow to get a [minimal, complete, and verifiable example](https://stackoverflow.com/help/mcve) which reproduces the issue.
-->
### Expected behaviour
<!--
Please explain here what is the expected behaviour.
-->
I tried to run frama-c on one of the GCC/LLVM single source test case which passes compilation with both compilers.
I expected Frama-c to also pass the parsing stage.
```
gcc /home/user42/directed-compiler-fuzzing-code/scripts/1-general-utils/testme_07092021-processed.ubfree.ubfree/A_pr85169_copy.c
./a.out
clang /home/user42/directed-compiler-fuzzing-code/scripts/1-general-utils/testme_07092021-processed.ubfree.ubfree/A_pr85169_copy.c
/home/user42/directed-compiler-fuzzing-code/scripts/1-general-utils/testme_07092021-processed.ubfree.ubfree/A_pr85169_copy.c:7:29: warning: unknown attribute 'noipa' ignored [-Wunknown-attributes]
static void __attribute__ ((noipa))
^~~~~
1 warning generated.
./a.out
```
### Actual behaviour
<!--
Please explain here what is the actual (faulty) behaviour.
-->
Frama-c cannot parse the program; /tmp/A_pr85169_copy.c04c2b1.i exists and passes compilation with gcc. Exit with this error:
```
user42@srg08:~/directed-compiler-fuzzing-code/scripts/7-diff-testing/Frama-C-zone$ frama-c ../../1-general-utils/testme_07092021-processed.ubfree.ubfree/A_pr85169_copy.c -kernel-msg-key pp
[kernel:pp]
preprocessing with "gcc -E -C -I. -I/home/user42/.opam/4.10.0/share/frama-c/libc -D__FRAMAC__ -D__FC_MACHDEP_X86_32 -dD -nostdinc -m32 '/home/user42/directed-compiler-fuzzing-code/scripts/1-general-utils/testme_07092021-processed.ubfree.ubfree/A_pr85169_copy.c' -o '/tmp/A_pr85169_copy.c04c2b1.i'"
[kernel] Parsing /home/user42/directed-compiler-fuzzing-code/scripts/1-general-utils/testme_07092021-processed.ubfree.ubfree/A_pr85169_copy.c (with preprocessing)
[kernel] /home/user42/directed-compiler-fuzzing-code/scripts/1-general-utils/testme_07092021-processed.ubfree.ubfree/A_pr85169_copy.c:11: Failure:
Expecting exactly one pointer type in array access v[63] (V and int)
[kernel] User Error: stopping on
file "/home/user42/directed-compiler-fuzzing-code/scripts/1-general-utils/testme_07092021-processed.ubfree.ubfree/A_pr85169_copy.c"
that has errors.
[kernel] Frama-C aborted: invalid user input.
```
### Contextual information
- Frama-C installation mode: Opam 4.10.0
- Frama-C version: *Frama-C version* 22.0 (Titanium)
- Plug-in used:
- OS name: Ubuntu
- OS version: 18
### Additional information (optional)
<!--
You may add here any information deemed relevant with regard to this issue,
and tell us if you already tried some workarounds or have some ideas to solve this issue.
-->
The program is taken from here: https://github.com/llvm/llvm-test-suite/blob/main/SingleSource/Regression/C/gcc-c-torture/execute/pr85169.c, and it is this one:
```
user42@srg08:~/directed-compiler-fuzzing-code/scripts/7-diff-testing/Frama-C-zone$ more /home/user42/directed-compiler-fuzzing-code/scripts/1-general-utils/testme_07092021-processed.ubfree.ubfree/A_pr85169_copy.c
/* PR target/85169 */
typedef char V __attribute__((vector_size (64)));
static void __attribute__ ((noipa))
foo (V *p)
{
V v = *p;
v[63] = 1;
*p = v;
}
int main()
{
V v = (V) { };
foo (&v);
for (unsigned i = 0; i < 64; i++) {
if (v[i] != (i == 63))
{ __builtin_abort (); }
}
return 0;
}
```Andre MaronezeAndre Maronezehttps://git.frama-c.com/pub/frama-c/-/issues/2574Frama-c fails parsing gcc/llvm single source test case with typedef depended ...2022-10-24T14:54:46ZKarine EMFrama-c fails parsing gcc/llvm single source test case with typedef depended on function's parameter<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the iss...<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- you installed Frama-C as prescribed in the [instructions](INSTALL.md).
If the issue applies to a specific Frama-C plug-in, please prefix the title
by the plug-in name: [Eva], [WP], [E-ACSL]…
-->
### Steps to reproduce the issue
<!--
Please indicate here steps to follow to get a [minimal, complete, and verifiable example](https://stackoverflow.com/help/mcve) which reproduces the issue.
-->
```
frama-c 20040411-1.c
```
### Expected behaviour
<!--
Please explain here what is the expected behaviour.
-->
Frama-c cannot parse the following C single source test case from GCC/LLVM test suite.
https://github.com/llvm/llvm-test-suite/blob/main/SingleSource/Regression/C/gcc-c-torture/execute/20040411-1.c
and gcc and llvm seem to be able to compile the program:
```
gcc A_20040411-1.c
A_20040411-1.c: In function ‘sub1’:
A_20040411-1.c:10:7: warning: implicit declaration of function ‘memcpy’ [-Wimplicit-function-declaration]
10 | memcpy (x, y, 10 * sizeof (int));
| ^~~~~~
A_20040411-1.c:10:7: warning: incompatible implicit declaration of built-in function ‘memcpy’
A_20040411-1.c:1:1: note: include ‘<string.h>’ or provide a declaration of ‘memcpy’
+++ |+#include <string.h>
1 | /* corpus/20040411-1.c */
A_20040411-1.c: In function ‘main’:
A_20040411-1.c:20:7: warning: implicit declaration of function ‘abort’ [-Wimplicit-function-declaration]
20 | { abort (); }
| ^~~~~
A_20040411-1.c:20:7: warning: incompatible implicit declaration of built-in function ‘abort’
A_20040411-1.c:1:1: note: include ‘<stdlib.h>’ or provide a declaration of ‘abort’
+++ |+#include <stdlib.h>
1 | /* corpus/20040411-1.c */
./a.out
clang-12 A_20040411-1.c
A_20040411-1.c:10:7: warning: implicitly declaring library function 'memcpy' with type 'void *(void *, const void *, unsigned long)' [-Wimplicit-function-declaration]
memcpy (x, y, 10 * sizeof (int));
^
A_20040411-1.c:10:7: note: include the header <string.h> or explicitly provide a declaration for 'memcpy'
A_20040411-1.c:20:7: warning: implicitly declaring library function 'abort' with type 'void (void) __attribute__((noreturn))' [-Wimplicit-function-declaration]
{ abort (); }
^
A_20040411-1.c:20:7: note: include the header <stdlib.h> or explicitly provide a declaration for 'abort'
2 warnings generated.
./a.out
```
### Actual behaviour
<!--
Please explain here what is the actual (faulty) behaviour.
-->
Frama-c exit with the following error:
```
[kernel] Parsing /home/user42/directed-compiler-fuzzing-code/scripts/7-diff-testing/results_output/A_20040411-1.c (with preprocessing)
[kernel] /home/user42/directed-compiler-fuzzing-code/scripts/7-diff-testing/results_output/A_20040411-1.c:5: User Error:
Array length i + 2 is not a compile-time constant.
[kernel:typing:implicit-function-declaration] /home/user42/directed-compiler-fuzzing-code/scripts/7-diff-testing/results_output/A_20040411-1.c:10: Warning:
Calling undeclared function memcpy. Old style K&R code?
[kernel:typing:implicit-function-declaration] /home/user42/directed-compiler-fuzzing-code/scripts/7-diff-testing/results_output/A_20040411-1.c:20: Warning:
Calling undeclared function abort. Old style K&R code?
[kernel] User Error: stopping on
file "/home/user42/directed-compiler-fuzzing-code/scripts/7-diff-testing/results_output/A_20040411-1.c"
that has errors. Add '-kernel-msg-key pp' for preprocessing command.
[kernel] Frama-C aborted: invalid user input.
```
### Contextual information
- Frama-C installation mode: Opam 4.10.0
- Frama-C version: 22.0 (Titanium)
- Plug-in used: *Plug-in used*
- OS name: Ubuntu
- OS version: 18
### Additional information (optional)
<!--
You may add here any information deemed relevant with regard to this issue,
and tell us if you already tried some workarounds or have some ideas to solve this issue.
-->Andre MaronezeAndre Maronezehttps://git.frama-c.com/pub/frama-c/-/issues/2575[WP] Soundness issue when handling a pointer on a structure containing an array.2021-10-06T07:07:23ZAlexCid[WP] Soundness issue when handling a pointer on a structure containing an array.<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the iss...<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- you installed Frama-C as prescribed in the [instructions](INSTALL.md).
If the issue applies to a specific Frama-C plug-in, please prefix the title
by the plug-in name: [Eva], [WP], [E-ACSL]…
-->
### Steps to reproduce the issue
Save the following code into a file called "error.c":
```C
#include <__fc_builtin.h>
struct slice {
int len;
char *buf;
};
int main() {
char b[4] = {0};
struct slice s = {.len = Frama_C_int_interval(2, 100000), .buf=b};
struct slice *p = &s;
//@ assert \valid_read(p->buf + (0..(p->len-1)));
return (int)p->buf[p->len-1];
}
```
Then analyse this code using the WP plugin with the command
`frama-c error.c -eva -wp -wp-rte -wp-prover alt-ergo`
<!--
Please indicate here steps to follow to get a [minimal, complete, and verifiable example](https://stackoverflow.com/help/mcve) which reproduces the issue.
-->
### Expected behaviour
The assertion `//@ assert \valid_read(p->buf + (0..(p->len-1)));` does obviously not hold and should be rejected by WP.
<!--
Please explain here what is the expected behaviour.
-->
### Actual behaviour
The manually added assertion, as well as the RTE assertion generated by wp-rte, are proved by alt-ergo. Using a different prover (z3, cvc4) yields the same result.
<!--
Please explain here what is the actual (faulty) behaviour.
-->
### Contextual information
- Frama-C installation mode: docker
- Frama-C version: 23.1
- Plug-in used: Eva, WP
- OS name: Ubuntu
- OS version: 20.04
### Additional information (optional)
Handling a pointer on a structure containing the array is required to trigger the bug - a simple structure containing the array won't trigger it.
This bug can also be triggered in a slightly more complex setting, where the array access is done in a second function and the `assert` clause is replaced by an equivalent `requires` clause in the preconditions of that second function.
<!--
You may add here any information deemed relevant with regard to this issue,
and tell us if you already tried some workarounds or have some ideas to solve this issue.
-->Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/2576Eva plugin crashed with program calling memset2021-12-03T14:07:13ZKarine EMEva plugin crashed with program calling memset<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the iss...<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- you installed Frama-C as prescribed in the [instructions](INSTALL.md).
If the issue applies to a specific Frama-C plug-in, please prefix the title
by the plug-in name: [Eva], [WP], [E-ACSL]…
-->
### Steps to reproduce the issue
frama-c -eva with the following program:
```
#include <string.h>
int main (void)
{
void *x;
memset (x, 0, 2 * 4);
return 0;
}
```
<!--
Please indicate here steps to follow to get a [minimal, complete, and verifiable example](https://stackoverflow.com/help/mcve) which reproduces the issue.
-->
### Expected behaviour
<!--
Please explain here what is the expected behaviour.
-->
Not to crash.
### Actual behaviour
<!--
Please explain here what is the actual (faulty) behaviour.
-->
Crash with this error:
```
frama-c -eva ../../9-reduce-bugs/crash-frama-c/9-error-Not_found/6185ea1b8f1da01180c959fe26694bb58e3d3241_reduced.c
[kernel] Parsing /home/user42/directed-compiler-fuzzing-code/scripts/9-reduce-bugs/crash-frama-c/9-error-Not_found/6185ea1b8f1da01180c959fe26694bb58e3d3241_reduced.c (with preprocessing)
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
[eva:alarm] /home/user42/directed-compiler-fuzzing-code/scripts/9-reduce-bugs/crash-frama-c/9-error-Not_found/6185ea1b8f1da01180c959fe26694bb58e3d3241_reduced.c:5: Warning:
function memset: precondition 'valid_s' got status unknown.
[eva] FRAMAC_SHARE/libc/string.h:118:
cannot evaluate ACSL term, unsupported ACSL construct: logic function memset
[kernel] Current source was: /home/user42/directed-compiler-fuzzing-code/scripts/9-reduce-bugs/crash-frama-c/9-error-Not_found/6185ea1b8f1da01180c959fe26694bb58e3d3241_reduced.c:5
The full backtrace is:
Raised at file "src/kernel_services/abstract_interp/map_lattice.ml", line 220, characters 14-29
Called from file "src/kernel_services/abstract_interp/map_lattice.ml", line 230, characters 25-42
Called from file "src/kernel_services/abstract_interp/map_lattice.ml", line 237, characters 25-42
Called from file "src/plugins/value/domains/cvalue/builtins_memory.ml", line 580, characters 35-73
Called from file "src/plugins/value/domains/cvalue/builtins_memory.ml", line 634, characters 10-61
Called from file "src/plugins/value/domains/cvalue/builtins.ml", line 253, characters 6-27
Called from file "src/plugins/value/domains/cvalue/builtins.ml", line 268, characters 12-54
Called from file "src/plugins/value/engine/compute_functions.ml", line 304, characters 10-65
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 318, characters 10-43
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 456, characters 22-60
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 758, characters 26-75
Called from file "src/kernel_services/abstract_interp/bottom.ml" (inlined), line 31, characters 18-21
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 754, characters 10-447
Called from file "list.ml", line 121, characters 24-34
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 769, characters 24-59
Called from file "src/kernel_services/abstract_interp/bottom.ml" (inlined), line 31, characters 18-21
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 742, characters 6-1023
Called from file "src/plugins/value/engine/iterator.ml", line 274, characters 6-47
Called from file "src/plugins/value/partitioning/partition.ml", line 494, characters 29-34
Called from file "list.ml", line 121, characters 24-34
Called from file "src/plugins/value/engine/iterator.ml", line 430, characters 15-71
Called from file "src/plugins/value/engine/iterator.ml", line 494, characters 18-35
Called from file "list.ml", line 92, characters 20-23
Called from file "src/plugins/value/engine/iterator.ml", line 496, characters 18-60
Called from file "src/plugins/value/engine/iterator.ml", line 543, characters 13-31
Called from file "list.ml", line 110, characters 12-15
Called from file "src/plugins/value/engine/iterator.ml" (inlined), line 540, characters 4-31
Called from file "src/plugins/value/engine/iterator.ml", line 602, characters 6-22
Called from file "src/plugins/value/engine/iterator.ml", line 769, characters 20-39
Called from file "src/plugins/value/engine/compute_functions.ml", line 201, characters 8-45
Called from file "src/plugins/value/engine/compute_functions.ml", line 333, characters 25-75
Called from file "src/libraries/project/state_builder.ml", line 994, characters 9-13
Re-raised at file "src/libraries/project/state_builder.ml", line 1002, characters 9-18
Called from file "src/plugins/value/register.ml", line 39, characters 46-66
Called from file "queue.ml", line 121, characters 6-15
Called from file "src/kernel_internals/runtime/boot.ml", line 36, characters 4-20
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 842, characters 2-9
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 872, characters 18-64
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 231, characters 4-8
Unexpected error (Not_found).
Please report as 'crash' at https://git.frama-c.com/pub/frama-c/issues
Your Frama-C version is 22.0 (Titanium).
Note that a version and a backtrace alone often do not contain enough
information to understand the bug. Guidelines for reporting bugs are at:
https://git.frama-c.com/pub/frama-c/-/wikis/Guidelines-for-reporting-bugs
```
### Contextual information
- Frama-C installation mode: Opam
- Frama-C version: 22.0 (Titanium)
- Plug-in used: eva
- OS name: Ubuntu
- OS version: 18
### Additional information (optional)
This is program compiles but got runtime errors, I would expect frama-c to give a warning. It seems like it crashed when analysing the memset line.
<!--
You may add here any information deemed relevant with regard to this issue,
and tell us if you already tried some workarounds or have some ideas to solve this issue.
-->David BühlerDavid Bühlerhttps://git.frama-c.com/pub/frama-c/-/issues/2577[EVA] Question about \tainted2022-02-15T09:15:50ZAlix Trieu[EVA] Question about \taintedHi,
I know the taint analysis is still in experimental phase, but I was wondering why Frama-C cannot prove the following assertion in this program.
```C
#include "__fc_builtin.h"
int tainted;
int main(void){
tainted = Frama_C_nonde...Hi,
I know the taint analysis is still in experimental phase, but I was wondering why Frama-C cannot prove the following assertion in this program.
```C
#include "__fc_builtin.h"
int tainted;
int main(void){
tainted = Frama_C_nondet(0, 1);
//@ taint tainted;
//@ assert \tainted(tainted);
return 0;
}
```
Frama-C commit `437130a79253e90571fc44a90732290da5957f07` using the command `frama-c -eva -eva-domains taint -eva-msg-key=d-taint,-d-c-value test.c` says
```Assertions 0 valid 1 unknown 0 invalid 1 total```
Even though `Frama_C_domain_show_each` shows that the variable is indeed tainted.
```
Frama_C_domain_show_each:
tainted : # cvalue: {0; 1}
# taint: true
```
Is `\tainted` just a placeholder to be implemented for now ?David BühlerDavid Bühlerhttps://git.frama-c.com/pub/frama-c/-/issues/2578Path Crawler Installation2022-09-28T12:18:03ZHarshit SinghalPath Crawler InstallationHi, I am installing Path-Crawler plugin in frama-c, I am referring the following user manual https://frama-c.com/download/frama-c-pathcrawler.pdf I this document there is no information about the tar file which i have to download. I have...Hi, I am installing Path-Crawler plugin in frama-c, I am referring the following user manual https://frama-c.com/download/frama-c-pathcrawler.pdf I this document there is no information about the tar file which i have to download. I have attached the document screenshot. Please let me know about where can I find the compressed file for path-crawler.
![Screenshot_from_2021-10-18_19-12-34](/uploads/a630ffd1386e730239046addc6fcacb6/Screenshot_from_2021-10-18_19-12-34.png)https://git.frama-c.com/pub/frama-c/-/issues/2579Parsing a file with including some bits of the STL2021-10-20T06:02:24ZHarshit SinghalParsing a file with including some bits of the STLThe following file does not parse when running `frama-c testing.cpp`, with Frama-Clang 0.0.11 installed, with a Frama-C 23.1+dev, OCaml 4.13, in Ubuntu 20.04:
```
#include<bits/stdc++.h>
using namespace std;
int main(){
cout<<"Hello Wor...The following file does not parse when running `frama-c testing.cpp`, with Frama-Clang 0.0.11 installed, with a Frama-C 23.1+dev, OCaml 4.13, in Ubuntu 20.04:
```
#include<bits/stdc++.h>
using namespace std;
int main(){
cout<<"Hello World"<<endl;
return 0;
}
```
It results in:
```
[kernel] Parsing testing.cpp (external front-end)
In file included from /home/harshit/Desktop/testing.cpp:1:
In file included from /usr/lib/gcc/x86_64-linux-gnu/9/../../../../include/x86_64-linux-gnu/c++/9/bits/stdc++.h:35:
In file included from /usr/lib/gcc/x86_64-linux-gnu/9/../../../../include/c++/9/cctype:41:
In file included from /usr/lib/gcc/x86_64-linux-gnu/9/../../../../include/x86_64-linux-gnu/c++/9/bits/c++config.h:524:
/usr/lib/gcc/x86_64-linux-gnu/9/../../../../include/x86_64-linux-gnu/c++/9/bits/os_defines.h:44:5: error: function-like macro '__GLIBC_PREREQ' is not defined
#if __GLIBC_PREREQ(2,15) && defined(_GNU_SOURCE)
^
In file included from /home/harshit/Desktop/testing.cpp:1:
In file included from /usr/lib/gcc/x86_64-linux-gnu/9/../../../../include/x86_64-linux-gnu/c++/9/bits/stdc++.h:41:
/usr/lib/gcc/x86_64-linux-gnu/9/../../../../include/c++/9/cmath:45:15: fatal error: 'math.h' file not found
#include_next <math.h>
^~~~~~~~
code generation aborted due to compilation errors
[kernel] User Error: Failed to parse C++ file. See Clang messages for more information
[kernel] User Error: stopping on file "testing.cpp" that has errors.
[kernel] Frama-C aborted: invalid user input.
```
Is there a way to parse it? Does it require some specific command-line option?
(*issue migrated from a comment in the old, now archived, Frama-Clang Github repository: https://github.com/Frama-C/Frama-C-snapshot/issues/45*)https://git.frama-c.com/pub/frama-c/-/issues/2580Non ghost lvalue when assigning array (frama-c 22)2022-10-05T06:41:34ZRaul MontiNon ghost lvalue when assigning array (frama-c 22)The following code aborts when using the e-acsl plug-in of frama-c 22.0, while it passes when using frama-c 20.0. I paste the failing case output bellow. The warning mentions lines `//@ ghost int acopy[len];` and `//@ ghost acopy[i] = a[...The following code aborts when using the e-acsl plug-in of frama-c 22.0, while it passes when using frama-c 20.0. I paste the failing case output bellow. The warning mentions lines `//@ ghost int acopy[len];` and `//@ ghost acopy[i] = a[i];`. I am wondering if this is actually not allowed or if it is just a bug?
Regards,
Raúl Monti.
```
#include <stdio.h>
/*@ requires len >= 0;
@ requires \valid(a+(0..len-1));
@*/
void add1(int* a, int len) {
//@ ghost int acopy[len];
int i;
for(i = 0; i < len; i++) {
//@ ghost acopy[i] = a[i];
}
for(i = 0; i < len; i++) {
a[i] = a[i] + 1;
}
//@ assert \forall integer i; 0 <= i < len ==> a[i] == acopy[i] + 1;
}
int main() {
int a[3];
a[0] = 0;
a[1] = 1;
a[2] = 2;
add1(a, 3);
return 0;
}
```
The output I get when running e-acsl-gcc.sh add.c -c -O add in frama-c-22:
```
e-acsl-gcc.sh add.c -c -O add
+ frama-c -remove-unused-specified-functions -machdep gcc_x86_64 -cpp-extra-args= -std=c99 -D_DEFAULT_SOURCE -D__NO_CTYPE -D__FC_MACHDEP_X86_64 -no-frama-c-stdlib add.c -e-acsl -e-acsl-share=.../.opam/default/bin/../share/frama-c/e-acsl/ -then-last -print -ocode a.out.frama.c
[kernel] Parsing add.c (with preprocessing)
[kernel:ghost:bad-use] add.c:7: Warning:
Call to non-ghost function from ghost code is not allowed
[kernel:ghost:bad-use] add.c:10: Warning:
'*(acopy + i)' is a non-ghost lvalue, it cannot be assigned in ghost code
[e-acsl] beginning translation.
[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing)
[e-acsl] translation done in project "e-acsl".
[kernel] Warning: warning ghost:bad-use treated as deferred error. See above messages for more information.
[kernel] Frama-C aborted: invalid user input.
```Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/2581Problem in _CoqProject generation2022-01-25T08:41:34ZKailiang JiProblem in _CoqProject generationWhile I am trying to prove the goal with proof-general, I got `bad bounding indices: 0, 1` error in my emacs editor. After several times of checking on the generated `_CoqProject` file, I found that when I replace the `''` with `""` in t...While I am trying to prove the goal with proof-general, I got `bad bounding indices: 0, 1` error in my emacs editor. After several times of checking on the generated `_CoqProject` file, I found that when I replace the `''` with `""` in the lines with `-R` ahead and remove option `-arg` in `_CoqObject`, it works.
It seems that you need to rewrite line 411 of `/frama-c/src/plugins/wp/ProverCoq.ml` with
```ocaml
Format.fprintf fmt "-R %s \"\"@\n" dir
```
and delete line 415.Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/2583Stack overflow with WP in MemTyped.Layout.compare_slot2021-11-03T11:19:09ZGuerricChupinStack overflow with WP in MemTyped.Layout.compare_slotRunning `frama-c -wp file.c` causes a stack overflow when `file.c` contains:
```C
int a;
fn() { struct b *c = &a; }
```
The stack trace is:
```
[kernel] Parsing file.c (with preprocessing)
[kernel:CERT:MSC:37] file.c:2: Warning:
B...Running `frama-c -wp file.c` causes a stack overflow when `file.c` contains:
```C
int a;
fn() { struct b *c = &a; }
```
The stack trace is:
```
[kernel] Parsing file.c (with preprocessing)
[kernel:CERT:MSC:37] file.c:2: Warning:
Body of function fn falls-through. Adding a return statement
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[kernel] Current source was: file.c:2
The full backtrace is:
Raised by primitive operation at MemTyped.Layout.clayout in file "src/plugins/wp/MemTyped.ml", line 773, characters 19-29
Called from MemTyped.Layout.compare_slot in file "src/plugins/wp/MemTyped.ml", line 796, characters 33-45
<repeated around 1000 times>
Called from MemTyped.Layout.compare in file "src/plugins/wp/MemTyped.ml", line 812, characters 20-36
Unexpected error (Stack overflow).
Please report as 'crash' at https://git.frama-c.com/pub/frama-c/issues
Your Frama-C version is 23.1 (Vanadium).
Note that a version and a backtrace alone often do not contain enough
information to understand the bug. Guidelines for reporting bugs are at:
https://git.frama-c.com/pub/frama-c/-/wikis/Guidelines-for-reporting-bugs
```
This C program looks a bit strange so I don't know how interesting this is but since I discovered it while searching for a simpler example of #2582, I thought I might as well report it.
# Contextual information
- Frama-C installation method: opam
- Frama-C version: 23.1
- Plug-in used: WP + RTE
- OS Name: Fedora
- OS Version: 34Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/2584[WP] Correction of loop-based copy function not prooved if using 32-bit integ...2021-11-23T08:12:16ZAlexCid[WP] Correction of loop-based copy function not prooved if using 32-bit integer sizes
### Steps to reproduce the issue
Save the following code into a file called "copy.c"
```C
#include <stdint.h>
typedef uint32_t size_t;
typedef enum {
OK, NOK
} error_t;
typedef struct {
size_t size;
unsigned int *values;
} bu...
### Steps to reproduce the issue
Save the following code into a file called "copy.c"
```C
#include <stdint.h>
typedef uint32_t size_t;
typedef enum {
OK, NOK
} error_t;
typedef struct {
size_t size;
unsigned int *values;
} buffer_t ;
/*@
requires
\valid(destination) && \valid(source) &&
\valid(destination->values+(0..destination->size-1)) &&
\valid(source->values+(0..source->size-1)) &&
\separated(source->values+(0..source->size-1), destination->values+(0..destination->size-1));
assigns
*(destination->values+(0..source->size-1));
ensures
(destination->size >= source->size) ==> ((\forall integer i; 0 <= i < source->size
==> (destination->values[i] == source->values[i])) && \result == OK);
ensures
(destination->size < source->size) ==> (\forall integer i; 0 <= i < destination->size
==> (destination->values[i] == \old(destination->values[i])) && \result == NOK);
*/
error_t copy(buffer_t* source, buffer_t* destination) {
error_t ret = NOK;
if (destination->size >= source->size) {
/*@
loop invariant 0 <= i <= source->size <= destination->size;
loop invariant \forall integer j ; 0 <= j < i ==> destination->values[j] == source->values[j];
loop assigns i, destination->values[0..source->size-1];
loop variant source->size-i;
*/
for(size_t i=0; i<source->size; i++) {
destination->values[i] = source->values[i];
}
ret = OK;
}
return ret;
}
```
Then analyse this code using the WP plugin with the command
`frama-c copy.c -wp -wp-rte -wp-prover alt-ergo,z3,cvc4 -wp-cache none`
<!--
Please indicate here steps to follow to get a [minimal, complete, and verifiable example](https://stackoverflow.com/help/mcve) which reproduces the issue.
-->
### Expected behaviour
The annotations should be proved. Indeed, if the type of our local "size_t" type is changed to uint8_t, uint16_t or uint64_t, then all assertions are proved.
<!--
Please explain here what is the expected behaviour.
-->
### Actual behaviour
Only 12 out of the 20 assertions are proved. Notably, none of the loop annotations can be proved.
### Contextual information
- Frama-C installation mode: docker
- Frama-C version: 23.1
- Plug-in used: Eva, WP
- OS name: Ubuntu
- OS version: 20.04https://git.frama-c.com/pub/frama-c/-/issues/2585Unexpected error (Stack overflow) with large array sizes and expressions2022-09-15T15:56:24Zarindam-8Unexpected error (Stack overflow) with large array sizes and expressions
### Steps to reproduce the issue
[fc-bug.c](/uploads/a314f79930f93d2f2a1cea3080b7b043/fc-bug.c)Run the following command:
```
frama-c -eva -eva-slevel 100 -eva-plevel 256 -eva-precision 5 -eva-warn-undefined-pointer-comparison pointe...
### Steps to reproduce the issue
[fc-bug.c](/uploads/a314f79930f93d2f2a1cea3080b7b043/fc-bug.c)Run the following command:
```
frama-c -eva -eva-slevel 100 -eva-plevel 256 -eva-precision 5 -eva-warn-undefined-pointer-comparison pointer -eva-no-alloc-returns-null -warn-signed-overflow -eva-no-show-progress -machdep x86_64 fuzzer-file-102106.c
```
### Expected behaviour
Frama-C when run on the test program with the given command should exit gracefully instead of resulting in an "Unexpected
stackoverflow error"
### Actual behaviour
When Frama-C is run on the program with the given command parameters it results in a Frama-C crash. with the following trace (abbreviated)
```
[kernel] Parsing _rmv_fuzzer-file-102106.c (with preprocessing)
[eva] Option -eva-precision 5 detected, automatic configuration of the analysis:
option -eva-min-loop-unroll set to 0 (default value).
option -eva-auto-loop-unroll set to 128.
option -eva-widening-delay set to 3 (default value).
option -eva-partition-history set to 0 (default value).
option -eva-slevel already set to 100.
option -eva-ilevel set to 48.
option -eva-plevel already set to 256 (not modified).
option -eva-subdivide-non-linear set to 100.
option -eva-remove-redundant-alarms set to true (default value).
option -eva-domains set to 'cvalue,equality,gauges,octagon,symbolic-locations'.
option -eva-split-return set to 'auto'.
option -eva-equality-through-calls set to 'formals' (default value).
option -eva-octagon-through-calls set to false (default value).
[eva] Splitting return states on:
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
b.f2 ∈ {0}
.f3 ∈ {65006}
.[bits 65047 to 65055] ∈ {0}
.f5 ∈ {65005}
.[bits 130059 to 130063] ∈ {0}
.f6 ∈ {-536}
g.f2 ∈ {65008}
.f3 ∈ {65000}
.[bits 65047 to 65055] ∈ {0}
.f5 ∈ {65005}
.[bits 130059 to 130063] ∈ {0}
.f6 ∈ {-536}
d ∈ {0}
l ∈ {0}
a ∈ {0}
c ∈ {0}
h ∈ {65008}
e[0] ∈ {-20}
[1..65236] ∈ {0}
f ∈ {{ &d }}
i[0] ∈ {-533}
[1..65004] ∈ {0}
j ∈ {0}
k ∈ {{ &c }}
[kernel] Current source was: _rmv_fuzzer-file-102106.c:20
The full backtrace is:
Raised by primitive operation at file "src/blocks.ml", line 691, characters 11-59
Called from file "src/blocks.ml", line 703, characters 17-53
Called from file "src/libraries/utils/wto.ml", line 168, characters 18-36
Called from file "src/libraries/utils/wto.ml", line 170, characters 34-66
...
Unexpected error (Stack overflow).
Please report as 'crash' at https://git.frama-c.com/pub/frama-c/issues
Your Frama-C version is 22.0 (Titanium).
Note that a version and a backtrace alone often do not contain enough
information to understand the bug. Guidelines for reporting bugs are at:
https://git.frama-c.com/pub/frama-c/-/wikis/Guidelines-for-reporting-bugs
```
### Contextual information
- Frama-C installation mode: Opam
- Frama-C version: 22.0 (Titanium)
- Plug-in used: eva
- OS name: Ubuntu
- OS version: Bionic 18.04
### Additional information (optional)
The crash seems inconsistent and appears sporadically. It seg-faults on some occasions while on others it crashes like mentioned above. With such expression length issues the crash seems legitimate.David BühlerDavid Bühlerhttps://git.frama-c.com/pub/frama-c/-/issues/2586** (frama-c-gui:11256): CRITICAL **2021-12-14T13:30:19Zankit247** (frama-c-gui:11256): CRITICAL **<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the iss...<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- you installed Frama-C as prescribed in the [instructions](INSTALL.md).
If the issue applies to a specific Frama-C plug-in, please prefix the title
by the plug-in name: [Eva], [WP], [E-ACSL]…
-->
### Steps to reproduce the issue
$ frama-c-gui foo.c Gdk-Message: 00:28:20.600: Unable to load arrow from the cursor theme ** (frama-c-gui:11388): CRITICAL **: 00:28:32.491: GSourceFunc: callback raised an exception
<!--
Please indicate here steps to follow to get a [minimal, complete, and verifiable example](https://stackoverflow.com/help/mcve) which reproduces the issue.
-->
### Expected behaviour
Getting error opening GUI for Frama-c
<!--
-->
### Actual behaviour
Should open the GUI
<!--
-->
### Contextual information
- Frama-C installation mode: **Opam**
- Frama-C version: **24.0**
- Plug-in used: **eva**
- OS name: Windows 11 (UBUNTU as WSLg)
- OS version: ubuntu 20.04 LTS
### Additional information (optional)
Usig command **frama-c -eva -main SumHadCoefficients foo.c**, not getting any error, also analysis result is getting dumped on terminal. But using gui gives error
![framac_gui_error_eva](/uploads/79eef02f4cce41c37a7ea764844fbe78/framac_gui_error_eva.png)
While running command frama-c-gui foo.c gives followin error
![framac_gui_error](/uploads/18d90850585b150c1ce9c3992a069e8c/framac_gui_error.png)
<!--
-->Andre MaronezeAndre Maronezehttps://git.frama-c.com/pub/frama-c/-/issues/2587Crash on Startup of frama-c-gui on WSL2022-01-18T09:06:14ZmoemodeCrash on Startup of frama-c-gui on WSL### Steps to reproduce the issue
Install frama-c on Windows 11 WSL according to install instructions. Then launch frama-c-gui
### Expected behaviour
frama-c-gui opens the gui
### Actual behaviour
![frama_err](/uploads/88a88cea9d4899...### Steps to reproduce the issue
Install frama-c on Windows 11 WSL according to install instructions. Then launch frama-c-gui
### Expected behaviour
frama-c-gui opens the gui
### Actual behaviour
![frama_err](/uploads/88a88cea9d4899909f2ee7ef74c73099/frama_err.png)
[frama_c_journal.ml](/uploads/a75256b6f842241a1e7ffb7ab0919b00/frama_c_journal.ml)
### Contextual information
- Frama-C installation mode: Opam as described on [Website](https://frama-c.com/html/get-frama-c.html)
- Frama-C version: 24.0 (Chromium)
- OS name: Windows
- OS version: 11Andre MaronezeAndre Maronezehttps://git.frama-c.com/pub/frama-c/-/issues/2588Frama-c crashes with "src/kernel_services/abstract_interp/ival.ml", line 444,...2022-01-24T09:36:26ZKarine EMFrama-c crashes with "src/kernel_services/abstract_interp/ival.ml", line 444, characters 31-37: Assertion failed<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the iss...<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- you installed Frama-C as prescribed in the [instructions](INSTALL.md).
If the issue applies to a specific Frama-C plug-in, please prefix the title
by the plug-in name: [Eva], [WP], [E-ACSL]…
-->
### Steps to reproduce the issue
```
frama-c -eva fuzzer-file-49652.c
```
<!--
Please indicate here steps to follow to get a [minimal, complete, and verifiable example](https://stackoverflow.com/help/mcve) which reproduces the issue.
-->
### Expected behaviour
Not to crash
<!--
Please explain here what is the expected behaviour.
-->
### Actual behaviour
Frama-c 24.0 crashed with "src/kernel_services/abstract_interp/ival.ml", line 444, characters 31-37: Assertion failed
I reduced the original program to this:
```
#include <stdarg.h>
long a;
void b(va_list ap) {
a = va_arg(ap, double);
a += va_arg(ap, long);
}
void c(int d, ...) {
va_list ap;
va_start(ap, d);
b(ap);
}
void main() { c(0, 8.1, 7.1); }
```
<!--
Please explain here what is the actual (faulty) behaviour.
-->
The crash's trace is:
```
[kernel] Parsing fuzzer-file-49652.c (with preprocessing)
[kernel:parser:decimal-float] fuzzer-file-49652.c:12: Warning:
Floating-point constant 7.1 is not represented exactly. Will use 0x1.c666666666666p2.
(warn-once: no further messages from category 'parser:decimal-float' will be emitted)
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
a ∈ {0}
[eva:alarm] fuzzer-file-49652.c:5: Warning:
signed overflow. assert a + tmp ≤ 9223372036854775807;
(tmp from vararg)
[kernel] Current source was: fuzzer-file-49652.c:5
The full backtrace is:
Raised at file "src/kernel_services/abstract_interp/ival.ml", line 444, characters 31-43
Called from file "src/libraries/utils/hptmap.ml", line 934, characters 18-24
Called from file "src/kernel_services/abstract_interp/map_lattice.ml", line 428, characters 24-39
Called from file "src/plugins/value_types/cvalue.ml", line 557, characters 10-64
Called from file "src/plugins/value/legacy/eval_terms.ml", line 1357, characters 17-46
Called from file "src/plugins/value/legacy/eval_terms.ml" (inlined), line 2680, characters 25-57
Called from file "src/plugins/value/legacy/eval_terms.ml", line 2690, characters 22-36
Called from file "src/plugins/value/legacy/eval_terms.ml", line 2736, characters 11-29
Called from file "src/plugins/inout/operational_inputs.ml", line 383, characters 19-67
Called from file "list.ml", line 110, characters 12-15
Called from file "src/plugins/inout/operational_inputs.ml", line 485, characters 6-28
Called from file "src/kernel_services/analysis/dataflows.ml", line 514, characters 12-42
Called from file "src/kernel_services/analysis/dataflows.ml", line 522, characters 19-30
Called from file "src/kernel_services/analysis/dataflows.ml", line 523, characters 5-14
Called from file "src/kernel_services/analysis/dataflows.ml" (inlined), line 582, characters 10-48
Called from file "src/kernel_services/analysis/dataflows.ml" (inlined), line 582, characters 10-57
Called from file "src/kernel_services/analysis/dataflows.ml", line 582, characters 10-60
Called from file "src/plugins/inout/operational_inputs.ml" (inlined), line 702, characters 6-37
Called from file "src/plugins/inout/operational_inputs.ml", line 702, characters 6-48
Called from file "src/plugins/inout/operational_inputs.ml", line 716, characters 14-78
Called from file "queue.ml", line 121, characters 6-15
Called from file "src/plugins/value/engine/iterator.ml", line 731, characters 8-214
Called from file "src/plugins/value/engine/iterator.ml", line 780, characters 6-31
Called from file "src/plugins/value/utils/value_util.ml", line 114, characters 6-10
Called from file "src/plugins/value/engine/compute_functions.ml", line 206, characters 8-45
Called from file "src/plugins/value/engine/compute_functions.ml", line 228, characters 26-36
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 326, characters 10-53
Called from file "src/plugins/value/utils/value_util.ml", line 114, characters 6-10
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 463, characters 22-70
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 767, characters 14-73
Called from file "src/kernel_services/abstract_interp/bottom.ml", line 36, characters 25-30
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 762, characters 12-489
Called from file "list.ml", line 121, characters 24-34
Called from file "src/kernel_services/abstract_interp/bottom.ml", line 36, characters 25-30
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 749, characters 6-1023
Called from file "src/plugins/value/engine/iterator.ml", line 278, characters 6-47
Called from file "src/plugins/value/partitioning/partition.ml", line 649, characters 29-42
Called from file "list.ml", line 121, characters 24-34
Called from file "src/plugins/value/engine/iterator.ml", line 436, characters 15-74
Called from file "src/plugins/value/engine/iterator.ml", line 501, characters 18-35
Called from file "list.ml", line 92, characters 20-23
Called from file "src/plugins/value/engine/iterator.ml", line 503, characters 18-60
Called from file "src/plugins/value/engine/iterator.ml", line 550, characters 13-31
Called from file "list.ml", line 110, characters 12-15
Called from file "src/plugins/value/engine/iterator.ml" (inlined), line 547, characters 4-31
Called from file "src/plugins/value/engine/iterator.ml", line 609, characters 6-22
Called from file "src/plugins/value/engine/iterator.ml", line 776, characters 20-39
Called from file "src/plugins/value/utils/value_util.ml", line 114, characters 6-10
Called from file "src/plugins/value/engine/compute_functions.ml", line 206, characters 8-45
Called from file "src/plugins/value/engine/compute_functions.ml", line 228, characters 26-36
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 326, characters 10-53
Called from file "src/plugins/value/utils/value_util.ml", line 114, characters 6-10
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 463, characters 22-70
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 767, characters 14-73
Called from file "src/kernel_services/abstract_interp/bottom.ml", line 36, characters 25-30
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 762, characters 12-489
Called from file "list.ml", line 121, characters 24-34
Called from file "src/kernel_services/abstract_interp/bottom.ml", line 36, characters 25-30
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 749, characters 6-1023
Called from file "src/plugins/value/engine/iterator.ml", line 278, characters 6-47
Called from file "src/plugins/value/partitioning/partition.ml", line 649, characters 29-42
Called from file "list.ml", line 121, characters 24-34
Called from file "src/plugins/value/engine/iterator.ml", line 436, characters 15-74
Called from file "src/plugins/value/engine/iterator.ml", line 501, characters 18-35
Called from file "list.ml", line 92, characters 20-23
Called from file "src/plugins/value/engine/iterator.ml", line 503, characters 18-60
Called from file "src/plugins/value/engine/iterator.ml", line 550, characters 13-31
Called from file "list.ml", line 110, characters 12-15
Called from file "src/plugins/value/engine/iterator.ml" (inlined), line 547, characters 4-31
Called from file "src/plugins/value/engine/iterator.ml", line 609, characters 6-22
Called from file "src/plugins/value/engine/iterator.ml", line 776, characters 20-39
Called from file "src/plugins/value/utils/value_util.ml", line 114, characters 6-10
Called from file "src/plugins/value/engine/compute_functions.ml", line 206, characters 8-45
Called from file "src/plugins/value/engine/compute_functions.ml", line 344, characters 8-63
Called from file "src/plugins/value/utils/value_util.ml", line 114, characters 6-10
Called from file "src/plugins/value/engine/analysis.ml", line 181, characters 2-49
Called from file "src/libraries/project/state_builder.ml", line 998, characters 9-13
Re-raised at file "src/libraries/project/state_builder.ml", line 1006, characters 9-18
Called from file "src/plugins/value/register.ml", line 39, characters 46-66
Called from file "queue.ml", line 121, characters 6-15
Called from file "src/kernel_internals/runtime/boot.ml", line 36, characters 4-20
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 846, characters 2-9
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 876, characters 18-64
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 235, characters 4-8
Unexpected error (File "src/kernel_services/abstract_interp/ival.ml", line 444, characters 31-37: Assertion failed).
Please report as 'crash' at https://git.frama-c.com/pub/frama-c/issues
Your Frama-C version is 24.0 (Chromium).
Note that a version and a backtrace alone often do not contain enough
information to understand the bug. Guidelines for reporting bugs are at:
https://git.frama-c.com/pub/frama-c/-/wikis/Guidelines-for-reporting-bugs
```
### Contextual information
- Frama-C installation mode: Opam
- Frama-C version: 24.0 (Chromium)
- Plug-in used: eva
- OS name: Ubuntu
- OS version: 18.04
### Additional information (optional)
<!--
You may add here any information deemed relevant with regard to this issue,
and tell us if you already tried some workarounds or have some ideas to solve this issue.
-->David BühlerDavid Bühlerhttps://git.frama-c.com/pub/frama-c/-/issues/2589[WP] Failure to verify range information after bitwise and on signed integers2022-01-11T07:16:49ZGuerricChupin[WP] Failure to verify range information after bitwise and on signed integersIn the function below, WP fails to verify the assertion (which I believe is true after exhaustively testing it):
```c
/*@ assigns \nothing;
@*/
int8_t foo(int8_t n) {
int8_t m = n & 0xF;
/*@ assert 0 <= m < 16; */
return ...In the function below, WP fails to verify the assertion (which I believe is true after exhaustively testing it):
```c
/*@ assigns \nothing;
@*/
int8_t foo(int8_t n) {
int8_t m = n & 0xF;
/*@ assert 0 <= m < 16; */
return m;
}
```
It does so with all signed integer types, but doesn't with unsigned integer types. Performing the `&` on an unsigned integer type and casting the result to a signed integer doesn't work either. For instance, in the function below, the first assertion is verified but not the second:
```c
int8_t bar(int8_t n) {
uint8_t m = n & 0xF;
/*@ assert 0 <= m < 16; */
int8_t p = m;
/*@ assert 0 <= p < 16; */
return p;
}
```
Test file: [test.c](/uploads/2751b8e74f9f0f37840a32cbff4965ce/test.c)
I used this command to run Frama-C:
```bash
frama-c -wp -wp-rte test.c -wp-prover why3:alt-ergo -wp-prover why3:cvc4 -wp-prover why3:Z3
```
### Contextual information
- Frama-C installation mode: Opam
- Frama-C version: 24.0
- Plug-in used: WP, RTE
- OS name: Fedora
- OS version: 35
- Solvers: Alt-Ergo 2.4.1, CVC4 1.8, Z3 4.8.11
### Additional information (optional)
<!--
You may add here any information deemed relevant with regard to this issue,
and tell us if you already tried some workarounds or have some ideas to solve this issue.
-->https://git.frama-c.com/pub/frama-c/-/issues/2590Frama-c crash with Unexpected error (Invalid_argument("Array.make"))2022-02-09T07:14:30ZKarine EMFrama-c crash with Unexpected error (Invalid_argument("Array.make"))<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the iss...<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- you installed Frama-C as prescribed in the [instructions](INSTALL.md).
If the issue applies to a specific Frama-C plug-in, please prefix the title
by the plug-in name: [Eva], [WP], [E-ACSL]…
-->
### Steps to reproduce the issue
`frama-c 8ff8d2fc802d04c6a8b50094288d03e291d2c9bf.c`
<!--
Please indicate here steps to follow to get a [minimal, complete, and verifiable example](https://stackoverflow.com/help/mcve) which reproduces the issue.
-->
### Expected behaviour
<!--
Please explain here what is the expected behaviour.
-->
Not to crash
### Actual behaviour
<!--
Please explain here what is the actual (faulty) behaviour.
-->
Crash with Unexpected error (Invalid_argument("Array.make")), for this (reduced) program:
```
int a[] = {[72057594037927936] 0};
void main() {}
```
### Contextual information
- Frama-C installation mode: Opam
- Frama-C version: *Frama-C version* 24.0 (Chromium)
- Plug-in used: none
- OS name: Ubuntu
- OS version: 18
### Additional information (optional)
<!--
You may add here any information deemed relevant with regard to this issue,
and tell us if you already tried some workarounds or have some ideas to solve this issue.
-->
The trace of the error:
```
frama-c 8ff8d2fc802d04c6a8b50094288d03e291d2c9bf.c
[kernel] Parsing 8ff8d2fc802d04c6a8b50094288d03e291d2c9bf.c (with preprocessing)
[kernel] Current source was: 8ff8d2fc802d04c6a8b50094288d03e291d2c9bf.c:1
The full backtrace is:
Raised by primitive operation at file "src/kernel_internals/typing/cabs2cil.ml", line 3393, characters 21-62
Called from file "src/kernel_internals/typing/cabs2cil.ml", line 8353, characters 19-72
Called from file "src/kernel_internals/typing/cabs2cil.ml", line 8379, characters 8-85
Called from file "src/kernel_internals/typing/cabs2cil.ml", line 8076, characters 4-112
Called from file "src/kernel_internals/typing/cabs2cil.ml", line 8639, characters 27-73
Called from file "src/kernel_internals/typing/cabs2cil.ml", line 9137, characters 18-76
Called from file "list.ml", line 121, characters 24-34
Called from file "src/kernel_internals/typing/cabs2cil.ml", line 9154, characters 14-53
Called from file "src/kernel_internals/typing/cabs2cil.ml", line 10455, characters 12-35
Called from file "list.ml", line 110, characters 12-15
Called from file "src/kernel_internals/typing/cabs2cil.ml", line 10459, characters 2-25
Called from file "src/kernel_internals/typing/frontc.ml", line 82, characters 14-36
Called from file "src/kernel_services/ast_queries/file.ml", line 617, characters 25-44
Called from file "src/kernel_services/ast_queries/file.ml", line 637, characters 14-38
Called from file "src/kernel_services/ast_queries/file.ml", line 700, characters 46-72
Called from file "list.ml", line 121, characters 24-34
Called from file "src/kernel_services/ast_queries/file.ml", line 700, characters 17-89
Called from file "src/kernel_services/ast_queries/file.ml", line 1792, characters 24-60
Called from file "src/kernel_services/ast_queries/file.ml", line 1869, characters 4-27
Called from file "src/kernel_services/ast_data/ast.ml", line 110, characters 2-28
Called from file "src/kernel_services/ast_data/ast.ml", line 118, characters 53-71
Called from file "src/kernel_internals/runtime/boot.ml", line 29, characters 6-20
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 846, characters 2-9
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 876, characters 18-64
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 235, characters 4-8
Unexpected error (Invalid_argument("Array.make")).
Please report as 'crash' at https://git.frama-c.com/pub/frama-c/issues
Your Frama-C version is 24.0 (Chromium).
Note that a version and a backtrace alone often do not contain enough
information to understand the bug. Guidelines for reporting bugs are at:
https://git.frama-c.com/pub/frama-c/-/wikis/Guidelines-for-reporting-bugs
```Andre MaronezeAndre Maronezehttps://git.frama-c.com/pub/frama-c/-/issues/2591Error when install frama-c with opam2022-09-28T12:52:59ZryancaicseError when install frama-c with opamWhen I use `opam install frama-c` I got the below errors. What should I do? Thanks!
```
rando@ubuntu:~$ opam install frama-c
The following actions will be performed:
∗ install conf-gtk2 1 [required by lablgtk]
∗ insta...When I use `opam install frama-c` I got the below errors. What should I do? Thanks!
```
rando@ubuntu:~$ opam install frama-c
The following actions will be performed:
∗ install conf-gtk2 1 [required by lablgtk]
∗ install conf-gtksourceview 2 [required by frama-c]
∗ install conf-gnomecanvas 2 [required by frama-c]
∗ install lablgtk 2.18.11 [required by frama-c]
∗ install ocamlgraph_gtk 2.0.0 [required by frama-c]
∗ install frama-c 24.0
The Frama-C/Wp now uses Why-3 for all provers (Cf.
deprecated -wp-prover native:alt-ergo)
===== ∗ 6 =====
Do you want to continue? [Y/n] y
<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><>
⬇ retrieved frama-c.24.0 (cached)
⬇ retrieved lablgtk.2.18.11 (cached)
⬇ retrieved ocamlgraph_gtk.2.0.0 (cached)
[ERROR] The compilation of conf-gnomecanvas.2 failed at "pkg-config
libgnomecanvas-2.0".
[ERROR] The compilation of conf-gtk2.1 failed at "pkg-config --exists
gtk+-2.0".
[ERROR] The compilation of conf-gtksourceview.2 failed at "pkg-config
--short-errors --print-errors gtksourceview-2.0".
#=== ERROR while compiling conf-gtksourceview.2 =====================#
# context 2.1.2 | linux/x86_64 | ocaml-option-flambda.1 ocaml-variants.4.12.0+options | https://opam.ocaml.org/#3aeec9a7
# path ~/.opam/4.12.0+flambda/.opam-switch/build/conf-gtksourceview.2
# command ~/.opam/opam-init/hooks/sandbox.sh build pkg-config --short-errors --print-errors gtksourceview-2.0
# exit-code 1
# env-file ~/.opam/log/conf-gtksourceview-53359-4fbae4.env
# output-file ~/.opam/log/conf-gtksourceview-53359-4fbae4.out
### output ###
# No package 'gtksourceview-2.0' found
#=== ERROR while compiling conf-gtk2.1 ==============================#
# context 2.1.2 | linux/x86_64 | ocaml-option-flambda.1 ocaml-variants.4.12.0+options | https://opam.ocaml.org/#3aeec9a7
# path ~/.opam/4.12.0+flambda/.opam-switch/build/conf-gtk2.1
# command ~/.opam/opam-init/hooks/sandbox.sh build pkg-config --exists gtk+-2.0
# exit-code 1
# env-file ~/.opam/log/conf-gtk2-53359-73ec4e.env
# output-file ~/.opam/log/conf-gtk2-53359-73ec4e.out
#=== ERROR while compiling conf-gnomecanvas.2 =======================#
# context 2.1.2 | linux/x86_64 | ocaml-option-flambda.1 ocaml-variants.4.12.0+options | https://opam.ocaml.org/#3aeec9a7
# path ~/.opam/4.12.0+flambda/.opam-switch/build/conf-gnomecanvas.2
# command ~/.opam/opam-init/hooks/sandbox.sh build pkg-config libgnomecanvas-2.0
# exit-code 1
# env-file ~/.opam/log/conf-gnomecanvas-53359-4e35be.env
# output-file ~/.opam/log/conf-gnomecanvas-53359-4e35be.out
<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><>
┌─ The following actions failed
│ λ build conf-gnomecanvas 2
│ λ build conf-gtk2 1
│ λ build conf-gtksourceview 2
└─
╶─ No changes have been performed
```Andre MaronezeAndre Maroneze