frama-c issues
https://git.frama-c.com/pub/frama-c/-/issues
2021-04-15T09:17:31Z
https://git.frama-c.com/pub/frama-c/-/issues/2447
Unbound reference raised by Why
2021-04-15T09:17:31Z
mantis-gitlab-migration
Unbound reference raised by Why
ID0000335:
**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/2446
Problem to give an option to Jc in command-line with -jessie-jc-opt
2021-02-22T14:04:49Z
mantis-gitlab-migration
Problem to give an option to Jc in command-line with -jessie-jc-opt
ID0000340:
**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/2445
Frama-C/Jessie: memory set problem
2021-04-15T09:17:47Z
Virgile Prevosto
Frama-C/Jessie: memory set problem
ID0000039:
**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.jc
Claude Marché
Claude Marché
https://git.frama-c.com/pub/frama-c/-/issues/2444
Assertion failed in jc_interp_misc.ml
2021-04-15T09:17:42Z
mantis-gitlab-migration
Assertion failed in jc_interp_misc.ml
ID0000080:
**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=38
https://git.frama-c.com/pub/frama-c/-/issues/2443
Option -jessie-cpu-limit not taken into account in GUI
2021-04-15T09:17:48Z
Virgile Prevosto
Option -jessie-cpu-limit not taken into account in GUI
ID0000034:
**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,
david
https://git.frama-c.com/pub/frama-c/-/issues/2442
gWhy tries to use Alt-Ergo even if not installed
2021-04-15T09:17:48Z
Virgile Prevosto
gWhy tries to use Alt-Ergo even if not installed
ID0000037:
**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 bash
https://git.frama-c.com/pub/frama-c/-/issues/2441
Jessie: infinite or not annotated loops
2021-04-15T09:17:41Z
Dillon Pariente
Jessie: infinite or not annotated loops
ID0000103:
**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/2439
Assertion failed with exact integer model in presence of unions
2021-04-15T09:17:30Z
mantis-gitlab-migration
Assertion failed with exact integer model in presence of unions
ID0000341:
**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/2438
Jessie: the 'R' reference seems to be not present in the current release (Rea...
2021-04-15T09:17:48Z
Virgile Prevosto
Jessie: 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/2437
(* TODO: parameters *)
2021-04-15T09:17:40Z
Sylvie 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/2436
Jessie internal error
2021-04-15T09:17:38Z
mantis-gitlab-migration
Jessie internal error
ID0000199:
**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/2435
Yices options while using frama-c
2021-04-15T09:17:32Z
mantis-gitlab-migration
Yices options while using frama-c
ID0000308:
**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
...
Kalyan
https://git.frama-c.com/pub/frama-c/-/issues/2434
Arithmetic safety of bitwise operators cannot be verified
2021-04-15T09:17:29Z
mantis-gitlab-migration
Arithmetic safety of bitwise operators cannot be verified
ID0000348:
**This issue was created automatically from Mantis Issue 348. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000348:
**This issue was created automatically from Mantis Issue 348. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000348 | Frama-C | Plug-in > jessie | public | 2009-12-03 | 2009-12-03 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | boris | **Assigned To** | cmarche | **Resolution** | open |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090901 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Jessie cannot verify arithmetic safety in the following code:
typedef unsigned int uint32;
uint32 b1(uint32 x, uint32 y)
{
return x^y;
}
uint32 b2(uint32 x, uint32 y)
{
return x&y;
}
uint32 b3(uint32 x, uint32 y)
{
return x|y;
}
uint32 b4(uint32 x)
{
return ~x;
}
Claude Marché
Claude Marché
https://git.frama-c.com/pub/frama-c/-/issues/2433
Using Z3 dumps plenty logs of texts in the console
2021-04-15T09:17:29Z
Julien Signoles
Using Z3 dumps plenty logs of texts in the console
ID0000347:
**This issue was created automatically from Mantis Issue 347. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000347:
**This issue was created automatically from Mantis Issue 347. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000347 | Frama-C | Plug-in > jessie | public | 2009-12-02 | 2009-12-05 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | signoles | **Assigned To** | cmarche | **Resolution** | fixed |
| **Priority** | normal | **Severity** | text | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090902 | **Target Version** | - | **Fixed in Version** | Frama-C Beryllium-20090902 |
### Description :
All in the title. That's too much verbose of course.
Appear with why 2.22.
### Steps To Reproduce :
Simply try to prove any VC in gwhy with Z3.
https://git.frama-c.com/pub/frama-c/-/issues/2431
Global invariants are not verified
2021-04-15T09:17:27Z
Guillaume Melquiond
Global invariants are not verified
ID0000373:
**This issue was created automatically from Mantis Issue 373. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000373:
**This issue was created automatically from Mantis Issue 373. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000373 | Frama-C | Plug-in > jessie | public | 2010-01-14 | 2010-01-14 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | gmelquio | **Assigned To** | cmarche | **Resolution** | open |
| **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 :
No proof obligations are generated for global invariants, which makes it easy to validate incorrect specifications.
/*@ global invariant toto: 0 == 1; */
/*@ ensures \result == 0; */
int main() { return 1; }
$ frama-c -jessie -jessie-atp=ergo b.c
...
[jessie] Calling VCs generator.
Running Alt-Ergo on proof obligations
total : 1
valid : 1 (100%)
Claude Marché
Claude Marché
https://git.frama-c.com/pub/frama-c/-/issues/2429
cast between homogenous struct and array
2021-04-15T09:17:31Z
Dillon Pariente
cast between homogenous struct and array
ID0000336:
**This issue was created automatically from Mantis Issue 336. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000336:
**This issue was created automatically from Mantis Issue 336. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000336 | Frama-C | Plug-in > jessie | public | 2009-11-20 | 2010-01-22 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dpariente | **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 :
Ensures PO generated by "frama-c -jessie"
on this example code can not be discharged:
float v;
typedef struct {float f0;float f1;float f2;} ts;
typedef ts las;
/*@
requires \valid_range(d,0,2);
assigns v;
ensures v == d[1];
*/
void f(float d[])
{ v = d[1]; }
//@ ensures v==9.0;
void main()
{ las x;
x.f1 = 9.0;
f(&x);
}
ANSI C allows this "transparent" casting between homogenously typed structure and array.
Simulating the cast by means of an additional C function and predicate (with its axiomatization) - a solution previously proposed Frama-C team - works well but entails modifying the source code!
Claude Marché
Claude Marché
https://git.frama-c.com/pub/frama-c/-/issues/2426
The specifications of statements are not translated
2021-04-15T09:17:42Z
François Bobot
The specifications of statements are not translated
ID0000072:
**This issue was created automatically from Mantis Issue 72. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |...
ID0000072:
**This issue was created automatically from Mantis Issue 72. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000072 | Frama-C | Plug-in > jessie | public | 2009-04-30 | 2010-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | bobot | **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 :
No vc are produced with this function.
spec_statement.c :
==============================
void myfun(int p){
p = 1;
/*@ requires p==1;
@ ensures \old(p)==p-1;
@*/
p = 2;
}
=============================
spec_statement.jc:
========================
unit myfun(integer p)
behavior default:
assumes true;
ensures (C_3 : true);
{
{ (C_1 : (p = 1));
(C_2 : (p = 2));
(return ())
}
}
========================
### Additional Information :
frama-c : 5186
Claude Marché
Claude Marché
https://git.frama-c.com/pub/frama-c/-/issues/2425
share/Makefile.kernel: No such file or directory
2021-02-22T14:04:47Z
mantis-gitlab-migration
share/Makefile.kernel: No such file or directory
ID0000408:
**This issue was created automatically from Mantis Issue 408. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000408:
**This issue was created automatically from Mantis Issue 408. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000408 | Frama-C | Kernel > Makefile | public | 2010-02-16 | 2010-02-18 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | javert42 | **Assigned To** | signoles | **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** | - |
### Description :
running 'make' gives the following errors:
share/Makefile.dynamic:55: share/Makefile.kernel: No such file or directory
Makefile:1853: .depend: No such file or directory
Copying to lib/dgraph.cmi
cp: cannot stat `ocamlgraph/dgraph/dgraph.cmi': No such file or directory
make: *** [lib/dgraph.cmi] Error 1
https://git.frama-c.com/pub/frama-c/-/issues/2424
cp: cannot stat `ocamlgraph/dgraph/dgraph.cmi': No such file or directory
2021-02-22T14:04:47Z
mantis-gitlab-migration
cp: cannot stat `ocamlgraph/dgraph/dgraph.cmi': No such file or directory
ID0000409:
**This issue was created automatically from Mantis Issue 409. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000409:
**This issue was created automatically from Mantis Issue 409. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000409 | Frama-C | Kernel > Makefile | public | 2010-02-16 | 2010-02-18 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | javert42 | **Assigned To** | signoles | **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** | - |
### Description :
frama-c-Beryllium-20090902-why-2.21
Running make gives the following error:
share/Makefile.dynamic:55: share/Makefile.kernel: No such file or directory
Makefile:1853: .depend: No such file or directory
Copying to lib/dgraph.cmi
cp: cannot stat `ocamlgraph/dgraph/dgraph.cmi': No such file or directory
make: *** [lib/dgraph.cmi] Error 1
### Additional Information :
dgraph.cmi does not exist in ocamlgraph/dgraph
dgraph.cmi does not exist anywhere in ocamlgraph.tar.gz
https://git.frama-c.com/pub/frama-c/-/issues/2423
local array decl with non-constant size causes Why error
2021-04-15T09:17:24Z
Jochen Burghardt
local array decl with non-constant size causes Why error
ID0000416:
**This issue was created automatically from Mantis Issue 416. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000416:
**This issue was created automatically from Mantis Issue 416. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000416 | Frama-C | Plug-in > jessie | public | 2010-02-22 | 2010-02-22 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **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 :
After declaring in a procedure a local array of a size depending on some parameter, when I assert the range-validity, I get (a Kernel warning "No code for function __builtin_alloca" and) a Why error message "Unbound variable bitvector_alloc_table". This doesnt happen for a constant size (see attached file).
## Attachments
- [localFlexArray01.c](/uploads/a05a9a037a93d34b2c583224ef734c52/localFlexArray01.c)
Claude Marché
Claude Marché