frama-c issues
https://git.frama-c.com/pub/frama-c/-/issues
2021-04-20T17:20:20Z
https://git.frama-c.com/pub/frama-c/-/issues/263
frama-c/jessie crashes with Unexpected error (Cil.SizeOfError("Undefined size...
2021-04-20T17:20:20Z
mantis-gitlab-migration
frama-c/jessie crashes with Unexpected error (Cil.SizeOfError("Undefined sizeof on a function.", _)).
ID0002376:
**This issue was created automatically from Mantis Issue 2376. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002376:
**This issue was created automatically from Mantis Issue 2376. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002376 | Frama-C | Plug-in > jessie | public | 2018-05-29 | 2018-05-29 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | foo | **Assigned To** | cmarche | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 16-Sulfur | **Target Version** | - | **Fixed in Version** | - |
### Description :
Hi all,
I'm very new to the frama-c and why ecosystem. I hope it's really a bug with frama-c and not jessie.
The C input is:
#include<stdlib.h>
int main(void) {
char *p =malloc(5);
p[0] = 4;
return 3;
}
I'd like to verify that the write to p[0] goes toa valid address.
$ Frama-c -val -jessie t.c
[kernel] Parsing t.c (with preprocessing)
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
[value:initial-state] Values of globals at initialization
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__fc_mblen_state ∈ [--..--]
__fc_mbtowc_state ∈ [--..--]
__fc_wctomb_state ∈ [--..--]
t.c:4:[value] allocating variable __malloc_main_l4
t.c:5:[value] warning: out of bounds write. assert \valid(p + 0);
[value] done for function main
[value] ====== VALUES COMPUTED ======
[value:final-states] Values at end of function main:
__fc_heap_status ∈ [--..--]
p ∈ {{ &__malloc_main_l4[0] }}
__retres ∈ {3}
__malloc_main_l4[0] ∈ {4}
[1..4] ∈ UNINITIALIZED
[jessie] Starting Jessie translation
[jessie] warning: \separated is not supported by Jessie. This predicate will be ignored
[kernel] Current source was: FRAMAC_SHARE/libc/stdlib.h:389
The full backtrace is:
Raised at file "src/kernel_services/ast_queries/cil.ml", line 5238, characters 9-67
Called from file "common.ml", line 329, characters 27-46
Called from file "norm.ml", line 1551, characters 11-55
Called from file "norm.ml", line 1571, characters 37-71
Called from file "norm.ml", line 1614, characters 22-47
Called from file "norm.ml", line 1685, characters 19-43
Called from file "src/kernel_services/ast_queries/cil.ml", line 2239, characters 15-31
Called from file "src/kernel_services/ast_queries/cil.ml" (inlined), line 3543, characters 17-35
Called from file "src/kernel_services/ast_queries/cil.ml", line 3572, characters 12-19
Called from file "src/kernel_services/ast_queries/cil.ml", line 2278, characters 13-16
Called from file "src/kernel_services/ast_queries/cil.ml", line 3576, characters 23-50
Called from file "src/kernel_services/ast_queries/cil.ml", line 2254, characters 21-41
Called from file "src/kernel_services/ast_queries/cil.ml", line 3613, characters 14-38
Called from file "src/kernel_services/ast_queries/cil.ml", line 2254, characters 21-41
Called from file "src/kernel_services/ast_queries/cil.ml", line 3602, characters 5-80
Called from file "src/kernel_services/ast_queries/cil.ml", line 3840, characters 16-37
Called from file "src/kernel_services/ast_queries/cil.ml", line 2278, characters 13-16
Called from file "src/kernel_services/ast_queries/cil.ml", line 2323, characters 24-57
Called from file "src/kernel_services/ast_queries/cil.ml", line 3808, characters 5-53
Called from file "src/kernel_services/ast_queries/cil.ml" (inlined), line 6463, characters 17-37
Called from file "src/kernel_services/ast_queries/cil.ml", line 6468, characters 24-33
Called from file "src/kernel_services/ast_queries/cil.ml", line 6470, characters 3-20
Called from file "src/kernel_services/ast_queries/cil.ml", line 2254, characters 21-41
Called from file "src/kernel_services/ast_queries/cil.ml", line 6487, characters 15-39
Called from file "common.ml", line 580, characters 2-13
Called from file "norm.ml", line 1959, characters 2-26
Called from file "register.ml", line 158, characters 4-23
Called from file "register.ml", line 278, characters 6-12
Called from file "src/kernel_services/plugin_entry_points/journal.ml", line 442, characters 19-22
Re-raised at file "src/kernel_services/plugin_entry_points/journal.ml", line 457, characters 10-17
Called from file "queue.ml", line 105, characters 6-15
Called from file "src/kernel_internals/runtime/boot.ml", line 37, characters 4-20
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 789, characters 2-9
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 819, characters 18-64
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 228, characters 4-8
Unexpected error (Cil.SizeOfError("Undefined sizeof on a function.", _)).
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Sulfur-20171101.
Note that a version and a backtrace alone often do not contain enough
information to understand the bug. Guidelines for reporting bugs are at:
http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelines
[kernel] writing journal in file `./.frama-c/frama_c_journal.ml'.
### Additional Information :
I'm using
frama-c Sulfur-20171101
why 2.40
Why3 0.88.3
ocaml 4.06.1
## Attachments
- [frama_c_journal.ml](/uploads/d55e08324ce8dc26fa7317cab9a5d1be/frama_c_journal.ml)
Claude Marché
Claude Marché
https://git.frama-c.com/pub/frama-c/-/issues/1496
Lithum- Z3 shell aborts with error message
2021-04-15T09:17:49Z
Virgile Prevosto
Lithum- Z3 shell aborts with error message
ID0000030:
**This issue was created automatically from Mantis Issue 30. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |...
ID0000030:
**This issue was created automatically from Mantis Issue 30. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000030 | Frama-C | Plug-in > jessie | public | 2009-04-07 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | virgile | **Assigned To** | cmarche | **Resolution** | unable to reproduce |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Lithium-20081201 | **Target Version** | - | **Fixed in Version** | Frama-C Beryllium-20090902 |
### Description :
[bug #7241 from old bts, reported by Christoph Weber]
Hello,
while I was trying to proof a function I got an error message.
Unfortunatly, I dont have time to figure out a smaller example
But the error occured when I altered the clause:
======
ensures
(
(\exists integer k1; (0 <= k1 < length_a && 0 <= k1 < length_b) &&
a[k1] < b[k1]) ||
(\forall integer k2; (0 <= k2 < length_a) ==>
length_a < length_b && a[k2] == b[k2])
) ==> \result == 1 ;
--------
into:
ensures
(
(\exists integer k1; (0 <= k1 < length_a && 0 <= k1 < length_b) &&
a[k1] < b[k1]) ||
(\forall integer k2; (0 <= k2 < length_a) ==>
length_a < length_b && a[k2] == b[k2])
) ^^ \result == 0 ;
==========
Here the source-code:
/*@
requires 0 <= length_a;
requires 0 <= length_b;
requires \valid_range (a, 0, length_a-1);
requires \valid_range (b, 0, length_b-1);
assigns \nothing;
ensures \result == 1 || \result == 0;
ensures
(
(\exists integer k1; (0 <= k1 < length_a && 0 <= k1 < length_b) &&
a[k1] < b[k1]) ||
(\forall integer k2; (0 <= k2 < length_a) ==>
length_a < length_b && a[k2] == b[k2])
) ^^ \result ==0 ;
*/
int lexicographical_compare_array (int* a, int length_a, int* b, int length_b)
{
int i = 0;
/*@
loop invariant 0 <= i <= length_a;
loop invariant 0 <= i <= length_b;
loop invariant \forall integer k; 0 <= k < i ==> a[k] == b[k];
*/
for ( ; i != length_a && i != length_b; ++i)
{
if (a[i] < b[i])
{
/*@
assert \exists integer k1; 0 <= k1 <= i && a[k1] < b[k1];
*/
return 1;
}
if (b[i] < a[i])
{
return 0;
}
}
//return i == length_a && i != length_b ? 1 : 0;
if (i == length_a && i != length_b)
{
/*@
assert
(
(\exists integer k1; (0 <= k1 < length_a && 0 <= k1 < length_b) &&
a[k1] < b[k1]) ||
(\forall integer k2; (0 <= k2 < length_a) ==>
length_a < length_b && a[k2] == b[k2])
);
*/
return 1;
}
else
{
return 0;
}
}
Sorry for the complex function,
Cheers
Christoph
https://git.frama-c.com/pub/frama-c/-/issues/1629
Lithium: behavior, complete disjoint does not work
2021-04-15T09:17:49Z
Virgile Prevosto
Lithium: behavior, complete disjoint does not work
ID0000026:
**This issue was created automatically from Mantis Issue 26. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |...
ID0000026:
**This issue was created automatically from Mantis Issue 26. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000026 | Frama-C | Plug-in > jessie | public | 2009-04-07 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **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** | - |
### Description :
[bug 7080 in old bts]
Hello, I am using the latest Lithium,
if I am using the short notation for complete, disjoint beaviors, i get:
File "find_array.h", line 46, characters 24-25: syntax error while parsing annot
ation
If i list the behaviors manually,
i get:
Warning: [Jessie plugin] complete behaviors specification ignored
Warning: [Jessie plugin] disjoint behaviors specification ignored
Cheers
Christoph
https://git.frama-c.com/pub/frama-c/-/issues/2101
Ordering of lemma in coq output of jessie
2021-04-15T09:17:48Z
Virgile Prevosto
Ordering of lemma in coq output of jessie
ID0000024:
**This issue was created automatically from Mantis Issue 24. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |...
ID0000024:
**This issue was created automatically from Mantis Issue 24. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000024 | Frama-C | Plug-in > jessie | public | 2009-04-07 | 2011-10-28 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **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 Nitrogen-20111001 |
### Description :
(bug 5878 from old bts)
The file in attachment declares a predicate together with two axioms on it, and has a lemma which can be inferred from
the axioms. However, in the coq output, axioms and lemmas are sorted alphabetically, so that the lemma comes before
the axioms, making the proof impossible to complete. The relative ordering of axioms and lemmas in the C file should
be preserved.
## Attachments
- [logic.c](/uploads/fd6b15724dcfe623df3e05f0aa7d6c60/logic.c)
https://git.frama-c.com/pub/frama-c/-/issues/2220
Highlighted text in code part of the GUI does not take into account size of #...
2021-04-15T09:17:48Z
Virgile Prevosto
Highlighted text in code part of the GUI does not take into account size of #defined symbols
ID0000035:
**This issue was created automatically from Mantis Issue 35. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |...
ID0000035:
**This issue was created automatically from Mantis Issue 35. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000035 | Frama-C | Plug-in > jessie | public | 2009-04-07 | 2011-04-01 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | virgile | **Assigned To** | virgile | **Resolution** | not fixable |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Lithium-20081201 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Hello,
With following code:
===
#define MAX 5
int c[5] = {0, };
int global = 0;
void main(void)
{
//@ assert global == 0;
//@ assert \forall integer i; 0 <= i < MAX ==> c[i] == 0;
return;
}
===
After launching Jessie GUI on it, if one selects assertion 2., the highlighted text in the lower right corner of the
GUI does not cover the " 0" characters.
The previous assertion (1.) is correclty highlighted.
I assume this is because the GUI rely on the size of the expression after preprocessor (CPP) pass while it highlights
source code as seen before preprocessor pass.
[bug 7496 from old bts, reported by David Mentré]
In above example, the expand #define "MAX" is "5", only 1 character wide compared to 3
of "MAX", corresponding to the 3-1=2 characters not highlighted.
I have observed similar behaviour on bigger code, when the highlight is not covering the correct expression at all.
Yours,
d.
https://git.frama-c.com/pub/frama-c/-/issues/2264
Launching several instances of the prover in parallel from the GUI?
2021-04-15T09:17:48Z
Virgile Prevosto
Launching several instances of the prover in parallel from the GUI?
ID0000033:
**This issue was created automatically from Mantis Issue 33. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |...
ID0000033:
**This issue was created automatically from Mantis Issue 33. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000033 | Frama-C | Plug-in > jessie | public | 2009-04-07 | 2010-12-22 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **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** | Frama-C Carbon-20101202-beta2 |
### Description :
Hello,
[bug 7439 from old bts, reported by David Mentré]
I'm using frama-c on multi-core and multi-processor machines. Would it be possible, when proving all obligations or
obligations from a selected function using the GUI (gWhy), to launch several instances of the prover at the same time?
It could speed-up the proving time.
Yours,
d.
### Additional Information :
This feature will be available in Why3 IDE, released in dec 2010
(This won't be avalable in Why2)
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/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/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/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/2456
Frama-C/Jessie: typing error
2021-04-15T09:17:47Z
Virgile Prevosto
Frama-C/Jessie: typing error
ID0000040:
**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.jc
Claude Marché
Claude Marché
https://git.frama-c.com/pub/frama-c/-/issues/2473
type invariants
2021-04-15T09:17:46Z
Virgile Prevosto
type invariants
ID0000025:
**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 above
Virgile Prevosto
Virgile Prevosto
https://git.frama-c.com/pub/frama-c/-/issues/2523
Inability to prove assigns clauses on simple array code
2021-04-15T09:17:46Z
Virgile Prevosto
Inability to prove assigns clauses on simple array code
ID0000041:
**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/2524
GUI blocked (100% cpu used) when requested to display an assertion
2021-04-15T09:17:46Z
Virgile Prevosto
GUI blocked (100% cpu used) when requested to display an assertion
ID0000036:
**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 itself
https://git.frama-c.com/pub/frama-c/-/issues/2525
Lithium fool the tool
2021-04-15T09:17:45Z
Virgile Prevosto
Lithium fool the tool
ID0000029:
**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.jc
https://git.frama-c.com/pub/frama-c/-/issues/2526
Jessie-gui : call of coqide and --project option
2021-04-15T09:17:45Z
Virgile Prevosto
Jessie-gui : call of coqide and --project option
ID0000028:
**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/2534
Default invariant should be inferred for loops
2021-04-15T09:17:45Z
Virgile Prevosto
Default invariant should be inferred for loops
ID0000042:
**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/2535
Why- error :-jessie-no-regions and assigns does not work
2021-04-15T09:17:44Z
Virgile Prevosto
Why- error :-jessie-no-regions and assigns does not work
ID0000031:
**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
Christoph
Claude Marché
Claude Marché
https://git.frama-c.com/pub/frama-c/-/issues/2542
Internal error with assign specification on bi-dimensional arrays
2021-04-15T09:17:44Z
Virgile Prevosto
Internal error with assign specification on bi-dimensional arrays
ID0000032:
**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/2543
Jessie crashes on simple program without annotations
2021-04-15T09:17:44Z
Virgile Prevosto
Jessie crashes on simple program without annotations
ID0000038:
**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é