frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2021-04-15T09:17:41Zhttps://git.frama-c.com/pub/frama-c/-/issues/2357Jessie: struct field's validity2021-04-15T09:17:41ZDillon ParienteJessie: struct field's validityID0000102:
**This issue was created automatically from Mantis Issue 102. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000102:
**This issue was created automatically from Mantis Issue 102. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000102 | Frama-C | Plug-in > jessie | public | 2009-05-27 | 2010-07-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dpariente | **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 :
(This issue was previously discussed through private messages but not fully resolved. It is now recorded into the BTS for traceability reasons.)
The following annotated code can not be proved by ATPs.
Function f() needs an invariant on global var v :
//@ global invariant aa: \valid(&v.c);
that should normally be generated automatically.
Function f2() needs a type invariant :
//@ type invariant Tt(las* l) = \valid(&(l->c)); but this type invariant is visibly not taken into account in the Why generated file (predicate Tt does exist but is not axiomatized).
Source code:
typedef struct { int c; } las;
las v;
//@ requires \valid(p);
void g(int * p);
void f(){ g(&v.c); }
//@ requires \valid(x);
void f2(las * x){ g(&(x->c)); }
Commande line:
frama-c -jessie-analysis -jessie-gui file.cClaude MarchéClaude Marchéhttps://git.frama-c.com/pub/frama-c/-/issues/2356Enhancement on assigns annotation and the name of proof obligation2021-04-15T09:17:15Zmantis-gitlab-migrationEnhancement on assigns annotation and the name of proof obligationID0000544:
**This issue was created automatically from Mantis Issue 544. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000544:
**This issue was created automatically from Mantis Issue 544. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000544 | Frama-C | Plug-in > jessie | public | 2010-07-17 | 2010-07-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | logan | **Assigned To** | cmarche | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Boron-20100401 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Consider the following functions. Both function violates
ACSL specification, and all of the theorem prover gives
UNKNOWN as result (which is correct and expected).
However, the name of proof obligation of test2() is
"loop invariants initially holds" which is a little
confusing. Since the problem is actually on the assign
statement instead of the while-loop. I think it will be
better to have an independent check for @assigns annotation
just like the "postcondition" proof obligation of test1().
--------------------------------------------------------
int global;
/*@ assigns \nothing;
*/
int test1() {
global = 1;
}
/*@ assigns \nothing;
*/
int test2() {
global = 2;
/*@ loop variant 0; */
while (0) {
}
}
--------------------------------------------------------Claude MarchéClaude Marchéhttps://git.frama-c.com/pub/frama-c/-/issues/2355unbound logic variable INT_MAX ,why?2021-02-22T13:57:10Zmantis-gitlab-migrationunbound logic variable INT_MAX ,why?ID0000545:
**This issue was created automatically from Mantis Issue 545. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000545:
**This issue was created automatically from Mantis Issue 545. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000545 | Frama-C | Kernel > ACSL implementation | public | 2010-07-19 | 2010-07-19 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | luoting | **Assigned To** | virgile | **Resolution** | no change required |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
When I run ' frama-c -jessie a.c', it goes as follows:
[kernel] preprocessing with "gcc -C -E -I. -dD a.c"
a.c:22:[kernel] user error: Error during annotations analysis: unbound logic variable INT_MAX
My frama-c version is Beryllium-20090902 and why is 2.23.
### Additional Information :
#include <limits.h>
However ,when I try another example b.c
'
int sqsum(int* p, int n) {
int S=0, tmp;
for(int i = 0; i < n; i++) {
//@ assert p[i] * p[i] <= INT_MAX;
tmp = p[i] * p[i];
//@ assert tmp >= 0;
//@ assert S + tmp <= INT_MAX;
S += tmp;
}
return S;
}
'
Gwhy can generate VC .
[kernel] preprocessing with "gcc -C -E -I. -dD b.c"
[jessie] Starting Jessie translation
[jessie] Producing Jessie files in subdir b.jessie
[jessie] File b.jessie/b.jc written.
[jessie] File b.jessie/b.cloc written.
[jessie] Calling Jessie tool in subdir b.jessie
Generating Why function sqsum
[jessie] Calling VCs generator.
gwhy-bin [...] why/b.why
Computation of VCs...
Computation of VCs done.
Reading GWhy configuration...
Loading .gwhyrc config file
GWhy configuration loaded...
Creating GWhy Tree view...
GWhy Tree view created...
Creating GWhy views...
Saving .gwhyrc config file
GWhy views created.
## Attachments
- [a.c](/uploads/e19866c69ef19bb978e5b46c64ab1704/a.c)https://git.frama-c.com/pub/frama-c/-/issues/2354how works the plug-in metrics?2021-02-22T13:57:09Zmantis-gitlab-migrationhow works the plug-in metrics?ID0000583:
**This issue was created automatically from Mantis Issue 583. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000583:
**This issue was created automatically from Mantis Issue 583. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000583 | Frama-C | Plug-in > metrics | public | 2010-09-13 | 2010-09-15 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | fsd | **Assigned To** | monate | **Resolution** | no change required |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | N/A |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Boron-20100401 | **Target Version** | - | **Fixed in Version** | - |
### Description :
I'm interested in the structure of the file metrics.ml
how does it work?
it isn't possible to watch the source code of metrics.ml which is used in Frama-C.
But for my analysation, i need to know why the framework Frama-C change the C-code in another C-code and then verify the changed code?
I must verify the current C-code with all "switch, if, while, for, do while, ..." and let it print on the screen.
Thanks,
Jean-Pierrehttps://git.frama-c.com/pub/frama-c/-/issues/2353problem to make install the "hello_world"-plugin2021-02-22T13:57:08Zmantis-gitlab-migrationproblem to make install the "hello_world"-pluginID0000582:
**This issue was created automatically from Mantis Issue 582. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000582:
**This issue was created automatically from Mantis Issue 582. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000582 | Frama-C | Kernel > Makefile | public | 2010-09-13 | 2010-09-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | fsd | **Assigned To** | signoles | **Resolution** | no change required |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | N/A |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Boron-20100401 | **Target Version** | - | **Fixed in Version** | - |
### Description :
I've installed frama-c on ubuntu lucid lynx 10.04
I wanted to make a simple plugin "hello_world" like in the description of the documentation "plugin-developer-Boron-20100401.pdf" with the two files Makefile and hello_world.ml
After copying the sources of the documentation and saving both in the folder /home/jean-pierre/Bureau/ocamldoc/ i started the terminal, went to the folder and wrote "make". the terminal said:
jean-pierre@jean-pierre-laptop:~/Bureau/ocamldoc$ make
/usr/share/frama-c/Makefile.dynamic:180: .depend: Aucun fichier ou dossier de ce type
ocamlc.opt -c -I . -w Ael -warn-error A -annot -g -I /usr/lib/frama-c hello_world.ml
File "hello_world.ml", line 12, characters 14-18:
Warning Z: unused variable name.
File "hello_world.ml", line 3, characters 3-119:
Error: Signature mismatch:
Modules do not match:
sig val name : string val shortname : string val deser : string end
is not included in
sig val name : string val shortname : string val descr : string end
The field `descr' is required but not provided
make: *** [hello_world.cmo] Erreur 2
### Additional Information :
i tried for windows XP with frama-c and cygwin but there are also problems.
any ideas?https://git.frama-c.com/pub/frama-c/-/issues/2352Jessie plugin does not support logic label Post in ensures clause2021-04-15T09:17:14Zmantis-gitlab-migrationJessie plugin does not support logic label Post in ensures clauseID0000590:
**This issue was created automatically from Mantis Issue 590. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000590:
**This issue was created automatically from Mantis Issue 590. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000590 | Frama-C | Plug-in > jessie | public | 2010-09-22 | 2010-09-22 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | khoroshilov | **Assigned To** | cmarche | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Boron-20100401 | **Target Version** | - | **Fixed in Version** | - |
### Description :
If Post is replaced with Here, the tool works fine.
$ frama-c -jessie -jessie-atp goals post-bug.c
[kernel] preprocessing with "gcc -C -E -I. -dD post-bug.c"
[jessie] Starting Jessie translation
[jessie] Producing Jessie files in subdir post-bug.jessie
[jessie] File post-bug.jessie/post-bug.jc written.
[jessie] File post-bug.jessie/post-bug.cloc written.
[jessie] Calling Jessie tool in subdir post-bug.jessie
File "post-bug.jc", line 90, characters 28-63: typing error: label `Post' not found
[jessie] user error: Jessie subprocess failed: jessie -why-opt -split-user-conj -v -locs post-bug.cloc post-bug.jc
## Attachments
- [post-bug.c](/uploads/a1174c48f32167fbc4167c2936748132/post-bug.c)Claude MarchéClaude Marchéhttps://git.frama-c.com/pub/frama-c/-/issues/2351Addition that may overflow passes verification2021-04-15T09:17:15Zmantis-gitlab-migrationAddition that may overflow passes verificationID0000539:
**This issue was created automatically from Mantis Issue 539. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000539:
**This issue was created automatically from Mantis Issue 539. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000539 | Frama-C | Plug-in > jessie | public | 2010-07-09 | 2010-09-29 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | boris | **Assigned To** | cmarche | **Resolution** | no change required |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Boron-20100401 | **Target Version** | - | **Fixed in Version** | - |
### Description :
This line passes in the binary search example:
mid = (low + high) / 2;
## Attachments
- [binary-search.c](/uploads/f10a66f299a024f0a9651a3d77f4d794/binary-search.c)https://git.frama-c.com/pub/frama-c/-/issues/2350Loop variant which does not always decrease passed the verification2021-04-15T09:17:15Zmantis-gitlab-migrationLoop variant which does not always decrease passed the verificationID0000533:
**This issue was created automatically from Mantis Issue 533. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000533:
**This issue was created automatically from Mantis Issue 533. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000533 | Frama-C | Plug-in > jessie | public | 2010-07-08 | 2010-09-29 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | logan | **Assigned To** | cmarche | **Resolution** | no change required |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Boron-20100401 | **Target Version** | - | **Fixed in Version** | - |
### Description :
I have written an implementation of Binary Search and tried to verify it with Frama-C Jessie plug-in. My code passed the verification process but in some cases the loop won't stop. (These cases can be checked by both gcc and hand-calculation.)
There's the loop and its variant:
(reference the attachment for the complete source code)
-------------------------------------------------------------
/*@ loop invariant \valid_range(array, left, right);
loop invariant left <= right;
loop invariant diff == right - left;
loop invariant \forall integer i; 0 <= i <= left ==> array[i] != key ;
loop invariant \forall integer i; right <= i < n ==> array[i] != key ;
loop variant diff; // NOTICE HERE
*/
while (diff > 0) { // FIXME: This line is INCORRECT actually.
// Change to while (diff > 1) for correct version.
unsigned int mid = left + (right - left) / 2;
// FIXME: Since (right - left) / 2 will be rounded-off,
// it is possible that the value of left and right will
// NEVER be updated.
if (array[mid] == key) { return mid; }
else if (array[mid] < key) { left = mid; }
else { right = mid; }
diff = right - left;
}
-------------------------------------------------------------
REPRODUCE PROCEDURE:
1. Download bisearch.c
2. Start Frama-C/Jessie with:
$ frama-c -jessie bisearch.c
3. Click on "Alt-Ergo 0.91"
4. All proof obligations are GREEN.
EXPECTED RESULT:
The proof obligations for "Function bsearch Safety > variant decreases" should result in either FALSE or Time Limit Exceed.
GOT RESULT:
Alt-Ergo 0.91 returns TRUE for such proof obligations.
### Additional Information :
I am using the precompiled Frama-C executables from Debian/sid (i386) repository.
VERSION:
Frama-C: Boron-20100401 (deb-version: 20100401+boron+dfsg-3)
Why: 2.26 (deb-version: 2.26+dfsg-1+b1)
Alt-Ergo: 0.91 (deb-version: 0.91-2)
## Attachments
- [bisearch.c](/uploads/9f46df865150e7d0ecb83336304aa324/bisearch.c)https://git.frama-c.com/pub/frama-c/-/issues/2349Correctness bug: division by 0 not detected2021-04-15T09:17:17ZPascal CuoqCorrectness bug: division by 0 not detectedID0000514:
**This issue was created automatically from Mantis Issue 514. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000514:
**This issue was created automatically from Mantis Issue 514. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000514 | Frama-C | Plug-in > jessie | public | 2010-06-18 | 2010-09-29 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | cmarche | **Resolution** | no change required |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Boron-20100401 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Verifying the code in the attached file, I was boasting I had found an overflow, and someone pointed out to me a division by zero. This was very embarrassing.
Frama-C 20100401, Why 2.26, Alt-Ergo 0.91
frama-c -jessie interp_search.c
The safety of the function interpolationSearch is not proved yet with the invariants I wrote so far, but what worries me is that the VC for the division (number 37 in the list) is proved when this function clearly has division-by-zero problems, for instance when run on the input vector provided in the main() function in the file. Compiling and executing does not make the error manifest itself, but the value analysis guarantees that there is one (frama-c-gui -val interp_search.c).
I am not sure whether it is a good idea to report a bug when there are still unproved VCs, but the establishment/preservation of the invariants I wrote are proved, so hopefully they are not false. Also I had the hope that there no longer was any overflow with the casts to "long long" I have introduced, so that the division-by-zero bug would be first in the control flow (so that the proof of its absence may not be caused by assuming another, false, VC above it).
Aside: the original function appear to have all the mentioned problems and to be in Java. Maybe it is a good example to run Krakatoa on?
## Attachments
- [interp_search.c](/uploads/4dd458f3c61f0d2f79a57c6841d66915/interp_search.c)https://git.frama-c.com/pub/frama-c/-/issues/2348Jessie + alt-ergo unsound in presence of division2021-04-15T09:17:14ZPascal CuoqJessie + alt-ergo unsound in presence of divisionID0000571:
**This issue was created automatically from Mantis Issue 571. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000571:
**This issue was created automatically from Mantis Issue 571. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000571 | Frama-C | Plug-in > jessie | public | 2010-08-24 | 2010-09-29 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | pascal | **Resolution** | no change required |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Boron-20100401 | **Target Version** | - | **Fixed in Version** | - |
### Description :
A shorter example than the previous ones of functions named "search", where Jessie + Alt-ergo emit an unsound result:
/*@
requires 0 < x <= 1000000000 ;
ensures \result / 2 > x;
*/
int function1(int x) {
return (2*x + 1);
}
frama-c -jessie t.c
With Frama-C 20100401, Why 2.26, Alt-ergo 0.91, the post-condition is proved, when it is in fact false for all arguments that satisfy the pre-condition.https://git.frama-c.com/pub/frama-c/-/issues/2347Parse error when using a wide string literal to initialize uint16 array2021-02-22T13:56:58Zmantis-gitlab-migrationParse error when using a wide string literal to initialize uint16 arrayID0000593:
**This issue was created automatically from Mantis Issue 593. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000593:
**This issue was created automatically from Mantis Issue 593. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000593 | Frama-C | Kernel | public | 2010-09-30 | 2010-10-01 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Maria | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
I'm trying to analyze Brew with Frama-C. OS - windows XP.
I've created simple Brew project(see attach), preprocessed it with Visual Studio and after it try to analyze with Frama-C:
C:\Frama-C\bin>frama-c.exe "\Program Files\BREW 3.1.5\sdk\examples\helloworld"\*.i
Also, I've tried to add files to project, using user interface, but nothing happened.
## Attachments
- [helloworld.zip](/uploads/e1faf5861730eaa7d75da589b90c18c6/helloworld.zip)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/2346Suggest to close a section if each obligation is proven by *some* prover2021-02-22T13:56:58ZJochen BurghardtSuggest to close a section if each obligation is proven by *some* proverID0000602:
**This issue was created automatically from Mantis Issue 602. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000602:
**This issue was created automatically from Mantis Issue 602. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000602 | Frama-C | Graphical User Interface | public | 2010-10-12 | 2010-10-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | monate | **Resolution** | not fixable |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Boron-20100401 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Currently, a section (like e.g. "fctxxx default behaviour" is automatically closed when *one* prover was able to prove all its contained obligations. However, often no single prover can prove them all, but each of them can be proved by some prover (i.e. in each line a green bullet appears, although not in the same column).
As a result, the user has to check all lines by himself, which is tedious (and even error-prone) when sections are large and the process of finding an adequate and verifiable specification involves many edit->vcg->prove cycles.
Therefor, I suggest to close a section once the statistics count has reached 100% of proven obligations (i.e. n/n). A "summary column" could be introduced showing a green bullet for single a obligation if it was proven by some prover, and a green check-mark for a section if its statistics count is 100%. For "very large" programs, it might even be desirable to have an icon summarizing all sections, i.e. the whole program, in a corresponding way.https://git.frama-c.com/pub/frama-c/-/issues/2345Failure with division by zero2021-04-15T09:17:20ZJulien SignolesFailure with division by zeroID0000473:
**This issue was created automatically from Mantis Issue 473. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000473:
**This issue was created automatically from Mantis Issue 473. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000473 | Frama-C | Plug-in > jessie | public | 2010-05-10 | 2010-10-14 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | signoles | **Assigned To** | cmarche | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Boron-20100401 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Jessie fails to generate the Why file corresponding to this trivial erroneous program:
=====
void main(void) {
int x = 1 / 0;
}
=====
$ frama-c -jessie a.c
[kernel] preprocessing with "gcc -C -E -I. -dD a.c"
[jessie] Starting Jessie translation
[jessie] Producing Jessie files in subdir a.jessie
[jessie] File a.jessie/a.jc written.
[jessie] File a.jessie/a.cloc written.
[jessie] Calling Jessie tool in subdir a.jessie
Generating Why function main
Uncaught exception: Failure("create_ratio infinite or undefined rational number")
[jessie] user error: Jessie subprocess failed: jessie -why-opt -split-user-conj -v -locs a.cloc a.jchttps://git.frama-c.com/pub/frama-c/-/issues/2344"\valid(&aaa)" unprovable for global variable aaa - missing antecedens in pro...2021-04-15T09:17:13ZJochen Burghardt"\valid(&aaa)" unprovable for global variable aaa - missing antecedens in proof obligation?ID0000614:
**This issue was created automatically from Mantis Issue 614. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000614:
**This issue was created automatically from Mantis Issue 614. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000614 | Frama-C | Plug-in > jessie | public | 2010-10-22 | 2010-10-22 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | cmarche | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Boron-20100401 | **Target Version** | - | **Fixed in Version** | - |
### Description :
See attached program. Jessie generates the proof obligation "(FORALL (int_P_alloc_table) (IMPLIES TRUE (<= (offset_min int_P_alloc_table aaa) 0)))" for the assert in line 8, and a similar one for offset_max.
Neither of them can be proved by any automatic prover.
I guess, the reason is that the name "aaa" appears unbound in the conclusions of both obligations, but does not appear anywhere else in the file ftest1_why.sx, so nothing is known (by the provers) about it.
If I make "aaa" a local rather than a global variable, the generated proof obligations look completely different; I feel unable to summarize the differences.
## Attachments
- [ftest1.c](/uploads/7ebd12c6cba8cb429b96a819b1369872/ftest1.c)Claude MarchéClaude Marchéhttps://git.frama-c.com/pub/frama-c/-/issues/2343separately verified files show code-bug when linked together2021-04-15T09:17:14ZJochen Burghardtseparately verified files show code-bug when linked togetherID0000615:
**This issue was created automatically from Mantis Issue 615. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000615:
**This issue was created automatically from Mantis Issue 615. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000615 | Frama-C | Plug-in > jessie | public | 2010-10-22 | 2010-10-22 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | cmarche | **Resolution** | open |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Boron-20100401 | **Target Version** | - | **Fixed in Version** | - |
### Description :
The attached file contains the files "ftest3a.c" and "ftestMain.c. Each of them can be verified (by alt-ergo), except for "\valid(&b)" in ftestMain, cf. issue #614. Although the "assert res == 1" in ftestMain is verified, it does not hold, as can be seen by removing both "////"-comments, compiling, and running: "gcc ftest3a.c ftestMain.c && ./a.out" yields "main: res=0\n" on stdout. Note that the contracts of "f()" and "g()" are identical across both files, and that they don't omit neccessary or provide invalid preconditions (e.g. no "assigns \nothing"). Also, the "no-regions"-model is used in both files.
The parameter "x" in "g()" is an alias to the global "b", and "f()" modifies "b". Both facts can be detected only by looking into ftestMain. Hence, by looking into ftest3a only, it cannot be detected that "g"s ensures clause is wrong; there is no other hint than nonexistent "assigns"-clauses.
## Attachments
- [ftest_2files](/uploads/a7b465d31dd2bbdfdee78aa5b6c48cfa/ftest_2files)Claude MarchéClaude Marchéhttps://git.frama-c.com/pub/frama-c/-/issues/2342star_star dump2021-02-22T14:02:46Zmantis-gitlab-migrationstar_star dumpID0000623:
**This issue was created automatically from Mantis Issue 623. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000623:
**This issue was created automatically from Mantis Issue 623. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000623 | Frama-C | Plug-in > Eva | public | 2010-11-10 | 2010-11-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | teamod | **Assigned To** | pascal | **Resolution** | no change required |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Boron-20100401 | **Target Version** | - | **Fixed in Version** | - |
### Description :
I preprocessed the Apache project (httpd-2.2.15) by Gcc-4.2.4 on linux2.6.28, and applied "frama-c -val apr_pools.i -main apr_pool_create_ex". Then the frama-c kernel dumped a lot of star_star_blablabla, and seems to be trapped into a deadlock.
Like below:
"
It contains a garbled mix of {star_star_star_allocator_0nth__owner_0nth__parent;
star_star_star_allocator_0nth__owner_0nth__parent_0nth__parent_WELL;
star_star_star_allocator_0nth__owner_0nth__parent_0nth__child_WELL;
star_star_star_allocator_0nth__owner_0nth__parent_0nth__sibling_WELL;
star_star_star_allocator_0nth__owner_0nth__parent_0nth__ref_WELL;
star_star_star_allocator_0nth__owner_0nth__parent_0nth__cleanups_WELL;
star_star_star_allocator_0nth__owner_0nth__parent_0nth__free_cleanups_WELL;
star_star_star_allocator_0nth__owner_0nth__parent_0nth__allocator_WELL;
star_star_star_allocator_0nth__owner_0nth__parent_0nth__subprocesses_WELL;
star_star_star_allocator_0nth__owner_0nth__parent_0nth__abort_fn_WELL;
star_star_star_allocator_0nth__owner_0nth__parent_0nth__user_data_WELL;
star_star_star_allocator_0nth__owner_0nth__parent_0nth__tag_WELL;
star_star_star_allocator_0nth__owner_0nth__parent_0nth__active_WELL;
star_star_star_allocator_0nth__owner_0nth__parent_0nth__self_WELL;
star_star_star_allocator_0nth__owner_0nth__parent_0nth__self_first_avail_WELL;
star_star_star_allocator_0nth__owner_0nth__parent_0nth__pre_cleanups_WELL;
star_star_star_allocator_0nth__owner_0nth__parent_1nth__parent_WELL;
star_star_star_allocator_0nth__owner_0nth__parent_1nth__child_WELL;
star_star_star_allocator_0nth__owner_0nth__parent_1nth__sibling_WELL;
star_star_star_allocator_0nth__owner_0nth__parent_1nth__ref_WELL;
star_star_star_allocator_0nth__owner_0nth__parent_1nth__cleanups_WELL;
star_star_star_allocator_0nth__owner_0nth__parent_1nth__free_cleanups_WELL;
star_star_star_allocator_0nth__owner_0nth__parent_1nth__allocator_WELL;
"
## Attachments
- [apr_pools.i](/uploads/c3bbcca5ed518b25062a920c7f29435c/apr_pools.i)https://git.frama-c.com/pub/frama-c/-/issues/2341Error parsing annotation2021-04-15T09:17:13Zmantis-gitlab-migrationError parsing annotationID0000627:
**This issue was created automatically from Mantis Issue 627. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000627:
**This issue was created automatically from Mantis Issue 627. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000627 | Frama-C | Plug-in > jessie | public | 2010-11-12 | 2010-11-15 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | ElenaNaum | **Assigned To** | cmarche | **Resolution** | no change required |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Boron-20100401 | **Target Version** | - | **Fixed in Version** | - |
### Description :
I am a new user and I tried to install Frama-c with the Jessie plug-in. I went through all the steps that are listed in the INSTALL files.
The problem occurs when I try to execute the following:
frama-c -jessie frama-c-Boron-20100401-why-2.24/why/examples-c/sorting/quicksort.c
[or any other example in the why/examples-c/ folder].
/frama-c-Boron-20100401-why-2.24/why/examples-c/sorting/quicksort.c:5:[kernel] user error: syntax error while parsing annotation
[kernel] user error: skipping file "frama-c-Boron-20100401-why-2.24/why/examples-c/sorting/quicksort.c" that has errors.
[kernel] Frama-C aborted because of an invalid user input.
### Additional Information :
I did not modify in any way the code for the examples.https://git.frama-c.com/pub/frama-c/-/issues/2340Incorrect processing of "type var[]" constructions2021-04-15T09:17:12Zmantis-gitlab-migrationIncorrect processing of "type var[]" constructionsID0000629:
**This issue was created automatically from Mantis Issue 629. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000629:
**This issue was created automatically from Mantis Issue 629. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000629 | Frama-C | Plug-in > jessie | public | 2010-11-16 | 2010-11-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Astra | **Assigned To** | cmarche | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Boron-20100401 | **Target Version** | - | **Fixed in Version** | - |
### Description :
During the processing of axiomatic Permut (taken from the ACSL specification file, page 51) Frama gives the next message:
tester@ubuntu-fm:~/workspace/prac1$ frama-c -jessie -jessie-atp gui qsorti.c
[kernel] preprocessing with "gcc -C -E -I. -dD qsorti.c"
[jessie] Starting Jessie translation
qsorti.c:27:[jessie] failure: Unexpected failure.
Please submit bug report (Ref. "norm.ml:1533:10").
[kernel] The full backtrace is:
Raised at file "src/kernel/log.ml", line 506, characters 30-31
Called from file "src/kernel/log.ml", line 500, characters 2-9
Re-raised at file "src/kernel/log.ml", line 503, characters 8-9
Called from file "src/lib/type.ml", line 746, characters 40-45
Called from file "queue.ml", line 134, characters 6-20
Called from file "src/kernel/boot.ml", line 50, characters 4-20
Called from file "src/kernel/cmdline.ml", line 170, characters 4-8
Plug-in jessie aborted because of an internal error.
Please report as 'crash' at http://bts.frama-c.com
Specified line number corresponds to the next axiom:
@ axiom permut_exchange{L1,L2} :
@ \forall double t1[], double t2[], integer i, integer j, integer n;
@ \at(t1[i],L1) == \at(t2[j],L2) &&
@ \at(t1[j],L1) == \at(t2[i],L2) &&
@ (\forall integer k; 0 <= k < n && k != i && k != j ==>
@ \at(t1[k],L1) == \at(t2[k],L2))
@ ==> permut{L1,L2}(t1,t2,n);
The same message is displayed while attempting to process the predicate Swap:
@ predicate Swap{L1,L2}(int a[], integer i, integer j) =
@ \at(a[i],L1) == \at(a[j],L2) &&
@ \at(a[j],L1) == \at(a[i],L2) &&
@ \forall integer k; k != i && k != j
@ ==> \at(a[k],L1) == \at(a[k],L2);
The reason is the incorrect processing of constructions like "type var[]".
The equal construction "type* var" causes no error.Claude MarchéClaude Marchéhttps://git.frama-c.com/pub/frama-c/-/issues/2339assigns nothing ?2021-04-15T09:17:13Zmantis-gitlab-migrationassigns nothing ?ID0000617:
**This issue was created automatically from Mantis Issue 617. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000617:
**This issue was created automatically from Mantis Issue 617. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000617 | Frama-C | Plug-in > jessie | public | 2010-10-26 | 2010-11-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jnarboux | **Assigned To** | cmarche | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Boron-20100401 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Hi,
Using the following example:
/*@
ensures \result == 1;
assigns \nothing;
*/
int foo()
{
int v[9];
v[0] =1;
return 1;
}
I get:
[kernel] preprocessing with "gcc -C -E -I. -dD bug.c"
[jessie] Starting Jessie translation
[jessie] Producing Jessie files in subdir bug.jessie
[jessie] File bug.jessie/bug.jc written.
[jessie] File bug.jessie/bug.cloc written.
[jessie] Calling Jessie tool in subdir bug.jessie
Generating Why function foo
[jessie] Calling VCs generator.
gwhy-bin [...] why/bug.why
Computation of VCs...
File "why/bug.why", line 392, characters 20-42:
Unbound variable int_P_v_1_alloc_table
make: *** [bug.stat] Erreur 1
is it normal ? if I remove the assign nothing it works.
Julien NarbouxClaude MarchéClaude Marchéhttps://git.frama-c.com/pub/frama-c/-/issues/2338Suggest to rename user identifiers to avoid name clashes in ..._why.sx files2021-04-15T09:17:12ZJochen BurghardtSuggest to rename user identifiers to avoid name clashes in ..._why.sx filesID0000632:
**This issue was created automatically from Mantis Issue 632. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000632:
**This issue was created automatically from Mantis Issue 632. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000632 | Frama-C | Plug-in > jessie | public | 2010-11-29 | 2010-11-29 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | cmarche | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Boron-20100401 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Simplify yields a "!" ("failure") on the attached program, seemingly because f's parameter name "EQ" clashes with the name of the equality predicate used in the preamble of ftest_why.sx. Simplfy has similar problems with a couple of other names, e.g. "AND". (Alt-ergo doesn't have these problems).
I'd like to suggest to catch those "reserved identifiers" by Jessie and to rename them, like this seems to be done already for "result".
It seems pretty dangerous that the "0.0" in g's body is currently translated into an occurrence of the quantified variable representing g's parameter. While the incorrect g is not verifiable right now, it might become so in future - as soon as a property like "double_value(real_constant_0_0e) == real_constant_0_0e" becomes derivable.
## Attachments
- [ftest.c](/uploads/cb37bc6d94f7428d03c340ad9836e58a/ftest.c)Claude MarchéClaude Marché