frama-c issues
https://git.frama-c.com/pub/frama-c/-/issues
2021-02-22T13:59:50Z
https://git.frama-c.com/pub/frama-c/-/issues/2481
crash for untyped_metrics example plugin
2021-02-22T13:59:50Z
Stephane Duprat
crash for untyped_metrics example plugin
ID0000163:
**This issue was created automatically from Mantis Issue 163. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000163:
**This issue was created automatically from Mantis Issue 163. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000163 | Frama-C | Kernel | public | 2009-06-25 | 2009-09-02 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | sduprat | **Assigned To** | monate | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090601-beta1 | **Target Version** | - | **Fixed in Version** | Frama-C Beryllium-20090901 |
### Description :
when running this plugin :
> frama-c -count-for tmp1.c
> [kernel] error: unexpected error Not_found
> [kernel] error: please report as `crash' at http://bts.frama-c.com
https://git.frama-c.com/pub/frama-c/-/issues/2478
crash when unbound variable
2021-02-22T13:59:47Z
mantis-gitlab-migration
crash when unbound variable
ID0000190:
**This issue was created automatically from Mantis Issue 190. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000190:
**This issue was created automatically from Mantis Issue 190. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000190 | Frama-C | Plug-in > slicing | public | 2009-07-15 | 2009-09-02 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | lukaszc | **Assigned To** | patrick | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Beryllium-20090901 |
### Description :
"frama-c -slice-rd y -pp-annot test.c" results in a crash
------------
test.c
------------
int x(int y, int z)
{
/*@ slice pragma expr y == 1; */
//@ assert y == 1;
//@ assert y + z == 3;
return 2*y*z1();
}
int main()
{
x(1,2);
return 0;
}
int z1()
{
return 1;
}
https://git.frama-c.com/pub/frama-c/-/issues/2474
Incorrect linking order for the viewer
2021-02-22T13:59:42Z
mantis-gitlab-migration
Incorrect linking order for the viewer
ID0000225:
**This issue was created automatically from Mantis Issue 225. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000225:
**This issue was created automatically from Mantis Issue 225. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000225 | Frama-C | Graphical User Interface | public | 2009-09-01 | 2009-09-09 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | mehdi | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090601-beta1 | **Target Version** | - | **Fixed in Version** | Frama-C Beryllium-20090901 |
### Description :
Hi,
When compiling the viewer using a system-installation of ocamlgraph, the compilation fails with the following error:
ocamlc.opt -w Ael -warn-error A -annot -I src/misc -I src/ai -I src/memory_state -I src/toplevel -I src/slicing_types -I src/pdg_types -I src/kernel -I src/logic -I src/lib -I src/project -I src/buckx -I external -I cil/src -I cil/src/ext -I cil/src/frontc -I cil/src/logic -I cil/ocamlutil -I lib/plugins -I lib -I +ocamlgraph -g -I src/gui -I +lablgtk2 -I +ocamlgraph -linkall -custom -o bin/viewer.byte nums.cma unix.cma bigarray.cma str.cma dynlink.cma src/buckx/mybigarray.o src/buckx/buckx_c.o graph.cma /usr/lib/ocaml/ocamlgraph/viewGraph.cmo /usr/lib/ocaml/ocamlgraph/viewGraph_select.cmo /usr/lib/ocaml/ocamlgraph/viewGraph_utils.cmo lablgtk.cma lablgnomecanvas.cma lablgtksourceview.cma /usr/lib/ocaml/ocamlgraph/viewGraph.cmo /usr/lib/ocaml/ocamlgraph/viewGraph_select.cmo /usr/lib/ocaml/ocamlgraph/viewGraph_utils.cmo
[...]
File "_none_", line 1, characters 0-1:
Error: Error while linking /usr/lib/ocaml/ocamlgraph/viewGraph.cmo:
Reference to undefined global `GnoCanvas'
As you can see, viewGraph.cmo (and friends) are specified twice when linking and between the two groups there is lablgnomecanvas.cma which is needed by viewGraph.cmo.
Please find attached a patch that fixes this issue.
Kind regards,
## Attachments
- [0002-Do-not-add-GRAPH_GUICMO-to-BYTE_GUI_LIBS.patch](/uploads/2a2f35dda8b3eb544d3cb94fe4af1e7b/0002-Do-not-add-GRAPH_GUICMO-to-BYTE_GUI_LIBS.patch)
https://git.frama-c.com/pub/frama-c/-/issues/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/2472
The file `share/configure.ac' is missing
2021-02-22T13:59:39Z
mantis-gitlab-migration
The file `share/configure.ac' is missing
ID0000182:
**This issue was created automatically from Mantis Issue 182. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000182:
**This issue was created automatically from Mantis Issue 182. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000182 | Frama-C | Kernel | public | 2009-07-13 | 2009-09-23 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jonathan-Christofer Demay | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090601-beta1 | **Target Version** | - | **Fixed in Version** | Frama-C Beryllium-20090901 |
### Description :
I tried to modify configure.in and then run autoreconf, but a file is missing:
aclocal-1.11: configure.in:46: file `share/configure.ac' does not exist
autoreconf-2.63: aclocal failed with exit status: 1
https://git.frama-c.com/pub/frama-c/-/issues/2470
Non-exhaustive pattern matching leads to compilation error
2021-02-22T14:03:27Z
mantis-gitlab-migration
Non-exhaustive pattern matching leads to compilation error
ID0000224:
**This issue was created automatically from Mantis Issue 224. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000224:
**This issue was created automatically from Mantis Issue 224. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000224 | Frama-C | Kernel | public | 2009-09-01 | 2009-09-23 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | mehdi | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090601-beta1 | **Target Version** | - | **Fixed in Version** | Frama-C Beryllium-20090902 |
### Description :
Hi,
When compiling frama-c in bytecode on a non-native architecture (even if OCaml 3.11.1 is available), compilation fails due to a non-exhaustive pattern matching.
The relevant lines are:
Ocamlc src/lib/dynlink_common_interface.cmi
Generating src/lib/dynlink_common_interface.ml
Ocamlc src/lib/dynlink_common_interface.cmo
File "src/lib/dynlink_common_interface.ml", line 77, characters 25-491:
Warning P: this pattern-matching is not exhaustive.
Here is an example of a value that is not matched:
Inconsistent_implementation _
File "src/lib/dynlink_common_interface.ml", line 1, characters 0-1:
Error: Error-enabled warnings (1 occurrences)
Please find attached a (trivial) patch that fixes this bug.
OCaml 3.11.1 is available on those architectures (e.g., hppa, mips, s390) with only the bytecode backend. So why do not activate the dynlink option or those too? In the configure script, you seem to rely on the presence of dynlink.cmxa. But dynlink.cma is also present when compiling in bytecode. I hope this will be fixed too.
Best regards,
--
Mehdi
## Attachments
- [0003-Fix-weak-pattern-matching-in-dynlink_lower_311_byte..patch](/uploads/198dcab076609e75bd342527b5644f0e/0003-Fix-weak-pattern-matching-in-dynlink_lower_311_byte..patch)
https://git.frama-c.com/pub/frama-c/-/issues/2469
Static linking of the jessie plugin fails when using a non-local Jc
2021-04-15T09:17:37Z
mantis-gitlab-migration
Static linking of the jessie plugin fails when using a non-local Jc
ID0000227:
**This issue was created automatically from Mantis Issue 227. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000227:
**This issue was created automatically from Mantis Issue 227. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000227 | Frama-C | Plug-in > jessie | public | 2009-09-01 | 2009-09-23 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | mehdi | **Assigned To** | signoles | **Resolution** | won't fix |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090601-beta1 | **Target Version** | - | **Fixed in Version** | Frama-C Beryllium-20090902 |
### Description :
Hi,
When I try to link frama-c statically with the Jessie plugin (with --with-jessie-static), the compilation fails with the following message:
File "_none_", line 1, characters 0-1:
Error: No implementations provided for the following modules:
Jc referenced from lib/plugins/Jessie.cmx
make[2]: *** [bin/toplevel.opt] Erreur 2
When using a non-local Jc, you need to add jc.cm{x,o} when linking.
Please find attached a patch that fixes this issue.
Kind regards,
## Attachments
- [0004-Add-JCCM-O-X-to-BYTE-OPT-_LIBS-when-linking-statical.patch](/uploads/56c5cfaf26e17134488d24223d6e771e/0004-Add-JCCM-O-X-to-BYTE-OPT-_LIBS-when-linking-statical.patch)
https://git.frama-c.com/pub/frama-c/-/issues/2462
For function f(int a) ; ensures a==\old(a) may be invalid
2021-02-22T13:59:27Z
Patrick Baudin
For function f(int a) ; ensures a==\old(a) may be invalid
ID0000168:
**This issue was created automatically from Mantis Issue 168. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000168:
**This issue was created automatically from Mantis Issue 168. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000168 | Frama-C | Plug-in > Eva | public | 2009-06-29 | 2009-09-24 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | patrick | **Assigned To** | pascal | **Resolution** | no change required |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C Beryllium-20090901 |
### Description :
The command "toplevel.opt -val old.c" gives the following line:
old.c:8: Warning: Function f, behavior default: postcondition got status valid
This is wrong: the postcondition is invalid.
### Additional Information :
Revision 5634
Contents of the file old.c
int *p, *q ;
/*@ ensures *q == a ;
*/
void f (int a) {
*q = a ;
*p = 3 ;
}
int main (int x, int y) {
q = &y ;
p = &x ;
f (x) ;
return x ;
}
https://git.frama-c.com/pub/frama-c/-/issues/2461
Assertion failed at project.ml:563
2021-02-22T13:59:26Z
Dillon Pariente
Assertion failed at project.ml:563
ID0000179:
**This issue was created automatically from Mantis Issue 179. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000179:
**This issue was created automatically from Mantis Issue 179. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000179 | Frama-C | Kernel | public | 2009-07-09 | 2009-09-24 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dpariente | **Assigned To** | pascal | **Resolution** | unable to reproduce |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C Beryllium-20090901 |
### Description :
Hello,
When launching: frama-c -load state.sav
(state.sav was previously generated and saved through -save command line option),
an error is displayed:
[kernel] error: unexpected error File "src/project/project.ml", line 563, characters 11-17: Assertion failed
[kernel] error: please report as `crash' at http://bts.frama-c.com
A printexc at project.ml:563 instead of "assert false" gives:
***** Stack overflow[values] computing for function MAIN
====== INITIAL STATE ======
====== INITIAL STATE COMPUTED ======
Growing heap to 289522k bytes
Regards,
Dillon
https://git.frama-c.com/pub/frama-c/-/issues/2460
array range in requires predicate
2021-04-15T09:17:36Z
mantis-gitlab-migration
array range in requires predicate
ID0000256:
**This issue was created automatically from Mantis Issue 256. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000256:
**This issue was created automatically from Mantis Issue 256. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000256 | Frama-C | Plug-in > jessie | public | 2009-09-25 | 2009-09-25 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jcrown | **Assigned To** | cmarche | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090902 | **Target Version** | - | **Fixed in Version** | - |
### Description :
frama-c -main foo file.c -jessie
on code
typedef struct { int a; } A;
typedef struct { A * c[10]; } B;
typedef struct { B * c[10]; } C;
C v;
/*@.......*/
void foo(void);
wth one of the 3 contracts below on foo()
/*@ requires \valid((v.c[0 .. 9])->c[0 .. 9]); */
/*@ requires \valid((v.c[0 .. 9])->c+(0 .. 9)); */
/*@ requires \valid((v.c+(0 .. 9))->c+(0 .. 9)); */
->
Uncaught exception: File "jc/jc_interp.ml", line 939, characters 25-31: Assertion failed
on the 1st and 2nd ones,
and
file.c:8:[kernel] user error: Error during annotations analysis: expected a struct with field c
on the 3rd one.
Claude Marché
Claude Marché
https://git.frama-c.com/pub/frama-c/-/issues/2459
Frama-C fails to parse a file
2022-12-28T10:05:19Z
mantis-gitlab-migration
Frama-C fails to parse a file
ID0000261:
**This issue was created automatically from Mantis Issue 261. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000261:
**This issue was created automatically from Mantis Issue 261. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000261 | Frama-C | Kernel | public | 2009-10-01 | 2009-10-01 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jonathan-Christofer Demay | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090901 | **Target Version** | - | **Fixed in Version** | - |
### Description :
It compiles fine with "gcc -I. -I./libtomcrypt/src/headers/ -DDROPBEAR_SERVER -DDROPBEAR_CLIENT dbutil.c -c -o dbutil.o"
But when given to Frama-C (CPP is set accordinly), I get the following error:
libtommath/tommath.h:77:[kernel] user error: GCC width mode TI applied to unexpected type, or unexpected mode
In tommath.h line 77 we have a mysterious GCC incantation (>_<):
typedef unsigned long mp_word __attribute__ ((mode(TI)));
### Additional Information :
Uploaded a preprocessed file: "gcc -I. -I./libtomcrypt/src/headers/ -DDROPBEAR_SERVER -DDROPBEAR_CLIENT dbutil.c -C -E -o dbutil.i"
## Attachments
- [dbutil.i](/uploads/ca1ba34059bd1dd4efa823437f09a2c6/dbutil.i)
Virgile Prevosto
Virgile Prevosto
https://git.frama-c.com/pub/frama-c/-/issues/2457
Problem with the "-main" option
2021-02-22T13:59:21Z
mantis-gitlab-migration
Problem with the "-main" option
ID0000279:
**This issue was created automatically from Mantis Issue 279. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000279:
**This issue was created automatically from Mantis Issue 279. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000279 | Frama-C | Kernel | public | 2009-10-09 | 2009-10-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | cbenkimoun | **Assigned To** | monate | **Resolution** | no change required |
| **Priority** | normal | **Severity** | block | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090902 | **Target Version** | - | **Fixed in Version** | Frama-C Beryllium-20090902 |
### Description :
I've just installed Frama-c on my computer.
I try to run the first.c example which is available on your web site.
I've got an error concerning the -main option.
Here is the output:
"
[kernel] preprocessing with "C:\Cygwin\bin\gcc-3.exe -CC -E -I toto.c"
# 1 "toto.c"
# 1 "<built-in>"
# 1 "<command line>"
# 1 "toto.c"
int S=0;
int T[5];
int main (void)
{
int i;
int *p = &T[0] ;
for (i=0; i<5; i++)
{ S = S+i; *p++ = S; }
return S;
}
[kernel] user error: Could not find entry point: main
"
I don't know what to do because there is a "main" function in my example.
I tried the -lib-entry option as well but without success...
Could you please help me?
Many thanks.
Cyril.
### Additional Information :
Running on Windows Vista.
Using cygwin gcc (PPC = "C:\Cygwin\bin\gcc-3.exe -CC -E -I"
https://git.frama-c.com/pub/frama-c/-/issues/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/2455
is_finite predicate: type double expected instead of real in .jc file
2021-04-15T09:17:35Z
Dillon Pariente
is_finite predicate: type double expected instead of real in .jc file
ID0000260:
**This issue was created automatically from Mantis Issue 260. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000260:
**This issue was created automatically from Mantis Issue 260. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000260 | Frama-C | Plug-in > jessie | public | 2009-09-30 | 2009-10-15 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dpariente | **Assigned To** | ayad | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090902 | **Target Version** | - | **Fixed in Version** | Frama-C Beryllium-20090902 |
### Description :
Launching: frama-c -jessie foo.c
with foo.c containing:
double f(double a , double b )
{
double t ;
t = 0.0;
//@ assert \is_finite((double)(a-b));
t = a - b;
return (t);
}
yields:
File "foo.jc", line 36, characters 56-71: typing error: type double expected instead of real
[jessie] user error: Jessie subprocess failed: jessie -why-opt -split-user-conj -v -locs foo.cloc foo.jc
":> real" in foo.jc should be removed when used within "is_finite_double" predicate, not?
Regards,
Dillon
https://git.frama-c.com/pub/frama-c/-/issues/2454
Unbound variable raised by why in presence of an unsafe cast
2021-04-15T09:17:33Z
mantis-gitlab-migration
Unbound variable raised by why in presence of an unsafe cast
ID0000291:
**This issue was created automatically from Mantis Issue 291. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000291:
**This issue was created automatically from Mantis Issue 291. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000291 | Frama-C | Plug-in > jessie | public | 2009-10-20 | 2009-10-20 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Sylvain Boulme | **Assigned To** | cmarche | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090902 | **Target Version** | - | **Fixed in Version** | - |
### Description :
In presence of an unsafe cast (that breaks the hypothesis of non-alias between pointers of distinct types), "frama-c -jessie" crashes with the error below instead of a more friendly error message:
File "why/septype0.why", line 617, characters 44-65:
Unbound variable bitvector_alloc_table
## Attachments
- [septype0.c](/uploads/f3b13146c9eb8d192dbdad1e0daca8e6/septype0.c)
Claude Marché
Claude Marché
https://git.frama-c.com/pub/frama-c/-/issues/2453
Recursive logic definitions are not correctly translated.
2021-04-15T09:17:37Z
François Bobot
Recursive logic definitions are not correctly translated.
ID0000222:
**This issue was created automatically from Mantis Issue 222. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000222:
**This issue was created automatically from Mantis Issue 222. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000222 | Frama-C | Plug-in > jessie | public | 2009-08-27 | 2009-11-03 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | bobot | **Assigned To** | cmarche | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C Beryllium-20090902 |
### Description :
The example 2.33 (p44 in acsl-implementation.pdf) is not correctly translated :
/*@ logic integer max_index { L }( int t [] , integer n ) =
@ ( n ==0) ? 0 :
@ ( t [n -1]==0) ? n : max_index (t , n -1);
@*/
# frama-c -jessie max_index.c
File "why/max_index.why", line 158, characters 13-66:
Unbound variable max_index
### Additional Information :
id : 6016
https://git.frama-c.com/pub/frama-c/-/issues/2451
Linking problem while compiling Frama-C-Beryllium-20090902-why-2.21 source di...
2021-04-15T09:17:32Z
mantis-gitlab-migration
Linking problem while compiling Frama-C-Beryllium-20090902-why-2.21 source distribution on Cygwin
ID0000322:
**This issue was created automatically from Mantis Issue 322. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000322:
**This issue was created automatically from Mantis Issue 322. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000322 | Frama-C | Plug-in > jessie | public | 2009-11-04 | 2009-11-05 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | nrousset | **Assigned To** | monate | **Resolution** | no change required |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090902 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Packing lib/plugins/Ltl_to_acsl.cmxs
d:\Program Files\bin\..\lib\gcc\mingw32\3.4.5\..\..\..\..\mingw32\bin\ld.exe: d:\DOCUME~1\nrousset\LOCALS~1\Temp\dyndll5fd028.o: bad reloc address 0x74 in section `.data'
collect2: ld returned 1 exit status
** Fatal error: Error during linking
File "caml_startup", line 1, characters 0-1:
Error: Error during linking
make: *** [lib/plugins/Ltl_to_acsl.cmxs] Error 2
### Additional Information :
I have OCaml 3.11.0 binary distribution for Windows / MinGW
$ ld -version
GNU ld (GNU Binutils) 2.18.50.20080625
Copyright 2007 Free Software Foundation, Inc.
This program is free software; you may redistribute it under the terms of
the GNU General Public License version 3 or (at your option) a later version.
This program has absolutely no warranty.
https://git.frama-c.com/pub/frama-c/-/issues/2450
Problem loading Jessie plugin on Cygwin
2021-02-22T13:59:12Z
mantis-gitlab-migration
Problem loading Jessie plugin on Cygwin
ID0000324:
**This issue was created automatically from Mantis Issue 324. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000324:
**This issue was created automatically from Mantis Issue 324. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000324 | Frama-C | Kernel | public | 2009-11-05 | 2009-11-05 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | nrousset | **Assigned To** | monate | **Resolution** | no change required |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090902 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Frama-C installed from the binary distribution.
Why 2.21 installed from the source distribution.
$ frama-c
[kernel] warning: cannot load file "C:\Frama-C\lib\frama-c\plugins\Jessie.cmxs" (dynlink error "error loading shared library: Cannot resolve camlPrintf__sprintf_424")
https://git.frama-c.com/pub/frama-c/-/issues/2449
assertion failed in Jessie with bitfields inside union
2021-04-15T09:17:32Z
mantis-gitlab-migration
assertion failed in Jessie with bitfields inside union
ID0000328:
**This issue was created automatically from Mantis Issue 328. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000328:
**This issue was created automatically from Mantis Issue 328. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000328 | Frama-C | Plug-in > jessie | public | 2009-11-12 | 2009-11-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | nrousset | **Assigned To** | cmarche | **Resolution** | open |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090902 | **Target Version** | - | **Fixed in Version** | - |
### Description :
See the example in the attached file.
File "jc/jc_effect.ml", line 525, characters 14-14:
Uncaught exception: File "jc/jc_effect.ml", line 525, characters 14-20: Assertion failed
## Attachments
- [test_union.c](/uploads/1dbf66dfa7ca23e32eb77c216946ffcc/test_union.c)
Claude Marché
Claude Marché
https://git.frama-c.com/pub/frama-c/-/issues/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é