frama-c issues
https://git.frama-c.com/pub/frama-c/-/issues
2021-02-22T13:36:11Z
https://git.frama-c.com/pub/frama-c/-/issues/1621
Problem with is_finite predicate generated by -val
2021-02-22T13:36:11Z
Dillon Pariente
Problem with is_finite predicate generated by -val
ID0000259:
**This issue was created automatically from Mantis Issue 259. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000259:
**This issue was created automatically from Mantis Issue 259. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000259 | Frama-C | Plug-in > Eva | public | 2009-09-30 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dpariente | **Assigned To** | pascal | **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 Carbon-20101201-beta1 |
### Description :
Launching: frama-c foo.c
with foo.c (generated by "frama-c -val" on the original code) containing:
/* Generated by Frama-C */
double f(double a , double b )
{
double t ;
t = 0.0;
/*@
assert \is_finite("+", a, b);
// synthesized
assert \is_finite("*", a+b, a-b);
// synthesized
assert \is_finite("-", a, b);
// synthesized
*/
t = (a + b) * (a - b);
return (t);
}
yields:
foo.c:13:[kernel] user error: syntax error while parsing annotation
which seems to be due to multiple asserts in the same @-comment.
Please note also that once the 3 asserts are 'exploded' into their own
@-comment, then "frama-c foo.c" displays:
foo.c:13:[kernel] user error: Error during annotations analysis: no such
predicate or logic function \is_finite(char *, double , double )
(but this very last point was already discussed in other threads).
Kernel seems to wait for a double typed expression parameter in \is_finite predicate, doesn't it? Like this single assert: //@ assert \is_finite((double)((a + b) * (a - b)));
Regards,
Dillon
https://git.frama-c.com/pub/frama-c/-/issues/1610
block-local variables not handled correctly in conjunction with -ulevel
2021-02-22T13:35:52Z
Pascal Cuoq
block-local variables not handled correctly in conjunction with -ulevel
ID0000244:
**This issue was created automatically from Mantis Issue 244. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000244:
**This issue was created automatically from Mantis Issue 244. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000244 | Frama-C | Plug-in > Eva | public | 2009-09-14 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | pascal | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090901 | **Target Version** | - | **Fixed in Version** | Frama-C Carbon-20101201-beta1 |
### Description :
int R,*p;
void main(void)
{
int a,i;
a=2;
for(i=0; i<2; i++)
{
int u=a;
p = &u;
}
R = *p;
}
Commandline:
bin/toplevel.opt -val u.c -ulevel 5
Result:
R ? {2; }
Should be:
NON TERMINATING FUNCTION
https://git.frama-c.com/pub/frama-c/-/issues/1597
Plug-in inout fails to parse clause /*@ assigns s[..]; */
2021-02-22T14:03:27Z
David Delmas
Plug-in inout fails to parse clause /*@ assigns s[..]; */
ID0000068:
**This issue was created automatically from Mantis Issue 68. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |...
ID0000068:
**This issue was created automatically from Mantis Issue 68. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000068 | Frama-C | Plug-in > Eva | public | 2009-04-28 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | ddelmas | **Assigned To** | pascal | **Resolution** | fixed |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Lithium-20081201 | **Target Version** | Frama-C Boron-20100401 | **Fixed in Version** | Frama-C Beryllium-20090902 |
### Description :
Consider the following example:
//@ assigns s[..];
void F1(char *s);
char T[100];
void F2(int c)
{
if (c) F1(T);
}
Running "frama-c file.c -main F2 -lib-entry -out" yields a parse error.
https://git.frama-c.com/pub/frama-c/-/issues/1584
wrongly synthesized assert
2021-02-22T13:35:11Z
Fabrice Derepas
wrongly synthesized assert
ID0000195:
**This issue was created automatically from Mantis Issue 195. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000195:
**This issue was created automatically from Mantis Issue 195. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000195 | Frama-C | Plug-in > Eva | public | 2009-07-16 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | derepas | **Assigned To** | pascal | **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 :
Let's consider the following program:
1. #include <stdlib.h>
2.
3. struct my_struct {
4. void * my_field;
5. };
6.
7. void main(struct my_struct * l) {
8. if (l!=NULL) {
9. if (l->my_field!=NULL) {
10. l->my_field=NULL;
11. }
12. }
13. }
Then I launch frama-c-gui and value analysis on entry point 'main'.
The following assert is synthesized between line 8 and 9:
//@ assert \valid(&l->my_field);
Even though l->my_field could be NULL and the program be ok.
https://git.frama-c.com/pub/frama-c/-/issues/1554
int a; main(){ return 100 / (int)(&a + 2); } fails to report a division by zero
2021-02-22T13:34:33Z
Pascal Cuoq
int a; main(){ return 100 / (int)(&a + 2); } fails to report a division by zero
ID0000076:
**This issue was created automatically from Mantis Issue 76. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |...
ID0000076:
**This issue was created automatically from Mantis Issue 76. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000076 | Frama-C | Plug-in > Eva | public | 2009-05-04 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | pascal | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Lithium-20081201 | **Target Version** | - | **Fixed in Version** | Frama-C Beryllium-20090601-beta1 |
### Description :
See summary
https://git.frama-c.com/pub/frama-c/-/issues/1553
if((int)(&a+2)) fails to warn about being unspecified
2021-02-22T13:34:32Z
Pascal Cuoq
if((int)(&a+2)) fails to warn about being unspecified
ID0000077:
**This issue was created automatically from Mantis Issue 77. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |...
ID0000077:
**This issue was created automatically from Mantis Issue 77. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000077 | Frama-C | Plug-in > Eva | public | 2009-05-05 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | pascal | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C Beryllium-20090601-beta1 |
### Description :
see summary.
This is related to bug 76, which is fixed and partially fixes
this problem too: at least the condition is correctly
analyzed as being 0 or 1. But the policy is to emit an alarm
(that is complicated to express, but that's another issue)
and to consider the condition to be 1 modulo the verification
of the alarm.
https://git.frama-c.com/pub/frama-c/-/issues/1542
propagation of \result clauses
2021-02-22T14:03:19Z
Jean-François Lalande
propagation of \result clauses
ID0000381:
**This issue was created automatically from Mantis Issue 381. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000381:
**This issue was created automatically from Mantis Issue 381. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000381 | Frama-C | Plug-in > Eva | public | 2010-01-21 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | lalande | **Assigned To** | pascal | **Resolution** | fixed |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090901 | **Target Version** | - | **Fixed in Version** | Frama-C Boron-20100401 |
### Description :
Hello,
when discovering Frama-C, I tried to specify some clauses on some functions to specify constraints on the return statement. But it seems that the "ensures" clauses that are "unknown" are not propagated after the analysis of the function.
For example:
/*@ensures \result >= 0;
@ensures \result <= 10;
int fonc()
{
int y = rand();
return y;
}
int main()
{
u = fonc();
}
gives
y in [--;--]
u in [--;--]
The @assert seems to be propagated, whereas the constraints on \result not.
I got a response of one of the developer that says that this is in the TODO list... Is it right ?
Best regards,
JF Lalande.
### Additional Information :
Frama-C Beryllium 2009-09-01
https://git.frama-c.com/pub/frama-c/-/issues/1536
Incorrect 'assert false' in value analysis
2021-02-22T13:34:10Z
Boris Yakobowski
Incorrect 'assert false' in value analysis
ID0000388:
**This issue was created automatically from Mantis Issue 388. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000388:
**This issue was created automatically from Mantis Issue 388. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000388 | Frama-C | Plug-in > Eva | public | 2010-02-01 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | yakobowski | **Assigned To** | monate | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C Boron-20100401 |
### Description :
This might be related to variadic calls, but I'm not really sure.
The crash is triggered by the following code:
typedef void *va_list;
#define va_start(AP, LASTARG) \
(AP = ((va_list) __builtin_next_arg (LASTARG)))
void main(const char *pszMessage,...) {
va_list vlParameters;
va_start(vlParameters,pszMessage);
}
### Additional Information :
SVN 7571
https://git.frama-c.com/pub/frama-c/-/issues/1526
malloc.h can't be preprocessed: __func__ is not a macro
2021-02-22T13:33:55Z
mantis-gitlab-migration
malloc.h can't be preprocessed: __func__ is not a macro
ID0000314:
**This issue was created automatically from Mantis Issue 314. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000314:
**This issue was created automatically from Mantis Issue 314. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000314 | Frama-C | Plug-in > Eva | public | 2009-11-03 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | akvadrako | **Assigned To** | pascal | **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 Boron-20100401 |
### Description :
Hi. The included sample malloc.h does not compile because __func__ is not a macro, but a static string variable. I am using clang/LLVM to preprocess my code. Also, please add "int" to the counter declaration, to avoid warnings. Thanks
C99, 6.4.2.2 #1 says:
The identifier __func__ shall be implicitly declared by the translator
as if, immediately following the opening brace of each function
definition, the declaration
static const char __func__[] = "function-name";
### Additional Information :
Please apply this patch. It's not ideal, because it uses snprintf. But at least the code is valid C:
--- tmp/frama-c-Beryllium-20090902-why-2.21/share/malloc.c 2009-09-23 15:21:30.000000000 +0000
+++ /usr/local/share/frama-c/malloc.c 2009-11-03 15:46:47.000000000 +0000
@@ -55,13 +55,15 @@
*/
#define FRAMA_C_STRINGIFY(x) #x
#define FRAMA_C_XSTRINGIFY(x) FRAMA_C_STRINGIFY(x)
-#define malloc(x) (Frama_C_malloc_at_pos(x,__FILE__ "_function_" __func__ "_line_" FRAMA_C_XSTRINGIFY(__LINE__)))
+#define malloc(x) (Frama_C_malloc_at_pos(x,__func__,__LINE__,__FILE__))
#define FRAMA_C_LOCALIZE_WARNING(x) (x " file " __FILE__ " line " FRAMA_C_XSTRINGIFY(__LINE__))
#define FRAMA_C_VALID 1
#define FRAMA_C_FREED 2
- static void *Frama_C_malloc_at_pos(size_t size,const char* file) {
- static counter = 0;
+ static void *Frama_C_malloc_at_pos(size_t size,const char *func,int line,const char* file) {
+ char pos[100];
+ snprintf(pos, 100, "%s_function_%s_line_%i", file, func, line);
+ static int counter = 0;
counter++;
char *base = Frama_C_alloc_infinite(file);
char *tag = Frama_C_alloc_infinite(base);
https://git.frama-c.com/pub/frama-c/-/issues/1481
non-constant size of 2-dim array leads to crash (some similarities to issue #...
2021-02-22T14:03:13Z
mantis-gitlab-migration
non-constant size of 2-dim array leads to crash (some similarities to issue #852)
ID0000856:
**This issue was created automatically from Mantis Issue 856. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000856:
**This issue was created automatically from Mantis Issue 856. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000856 | Frama-C | Plug-in > Eva | public | 2011-06-07 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | kerstin | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20110201 | **Target Version** | - | **Fixed in Version** | Frama-C Fluorine-20130401 |
### Description :
Hello,
frama-c -val -main ftest ftest.c leads to a crash.
The program is kind of similar to #852, but without recursive call to ftest and variable size (b[10][a]) instead of variable size (b[1][a]).
But, here you do not obtain the error with frama-c -ftest.c .
Regards,
Kerstin
## Attachments
- [ftest.c](/uploads/4caafd5020f8db63a51896b534f4f4de/ftest.c)
https://git.frama-c.com/pub/frama-c/-/issues/1444
Double version of program considerably slower to analyze than float version (...
2021-02-22T14:03:09Z
mantis-gitlab-migration
Double version of program considerably slower to analyze than float version (svn 19535)
ID0001260:
**This issue was created automatically from Mantis Issue 1260. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001260:
**This issue was created automatically from Mantis Issue 1260. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001260 | Frama-C | Plug-in > Eva | public | 2012-08-03 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | sven | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | - |
### Description :
When analyzing the attached program, Value is much slower when analyzing a double version than when analyzing with floats.
### Additional Information :
Steps to reproduce:
time -v -- frama-c -val -slevel 1100 interp.c
change typedef
time -v -- frama-c -val -slevel 1100 interp.c
## Attachments
- [interp.c](/uploads/8bfbc504d93081e0a2a204f1fc22326e/interp.c)
- [prof-double](/uploads/2f2093a32183da4e374ef69e73da48fa/prof-double)
https://git.frama-c.com/pub/frama-c/-/issues/1418
FRAMA_C_MALLOC_INFINITE not used in stdlib.c
2021-02-22T13:30:40Z
mantis-gitlab-migration
FRAMA_C_MALLOC_INFINITE not used in stdlib.c
ID0001214:
**This issue was created automatically from Mantis Issue 1214. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001214:
**This issue was created automatically from Mantis Issue 1214. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001214 | Frama-C | Plug-in > Eva | public | 2012-06-18 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Anne | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Oxygen-20120901 |
### Description :
#define FRAMA_C_MALLOC_INFINITE
#include "stdlib.c"
doesn't do what is expected since stdlib.c begins with :
#ifndef FRAMA_C_MALLOC_HEAP
#ifndef FRAMA_C_MALLOC_CHUNKS
#ifndef FRAMA_C_MALLOC_INDIVIDUAL
#ifndef FRAMA_C_MALLOC_POSITION
#define FRAMA_C_MALLOC_HEAP
so it ends up with FRAMA_C_MALLOC_HEAP instead. Is this on purpose ?
PS. I select [Kernel] category because I don't know where else to put it...
https://git.frama-c.com/pub/frama-c/-/issues/1402
wrong origin displayed in the GUI
2021-02-22T13:30:08Z
Pascal Cuoq
wrong origin displayed in the GUI
ID0000251:
**This issue was created automatically from Mantis Issue 251. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000251:
**This issue was created automatically from Mantis Issue 251. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000251 | Frama-C | Plug-in > Eva | public | 2009-09-20 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | immediate | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090901 | **Target Version** | - | **Fixed in Version** | Frama-C Oxygen-20120901 |
### Description :
~/ppc/bin/viewer.opt -val imprecise.c
Inspect value of F at the last statement before return.
It shows Origin: Misaligned ..:19
This is correct (we are at line 19).
Inspect the value of "*p"
It shows Origin: Misaligned ..:20
This is incorrect. Line 20 has not even been analyzed yet.
Note: this is probably only a problem in display (since F is correct).
Unfortunately this happens in a demo I was planning to do soon for
someone that matters a lot. Quick fix very much appreciated if at all
possible (meanwhile I will try to hide the problem by adjusting
the demo).
## Attachments
- [imprecise.c](/uploads/d0430283fcaa57d47ff326e878716536/imprecise.c)
https://git.frama-c.com/pub/frama-c/-/issues/1394
relation chains exploited incompletely
2021-02-22T13:29:43Z
Jochen Burghardt
relation chains exploited incompletely
ID0001071:
**This issue was created automatically from Mantis Issue 1071. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001071:
**This issue was created automatically from Mantis Issue 1071. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001071 | Frama-C | Plug-in > Eva | public | 2012-01-26 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | pascal | **Resolution** | fixed |
| **Priority** | normal | **Severity** | tweak | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Nitrogen-20111001 | **Target Version** | - | **Fixed in Version** | Frama-C Oxygen-20120901 |
### Description :
Running "frama-c -val ftest.c" on the attached program yields
"Called Frama_C_show_each_m([0..2147483647])
Called Frama_C_show_each_n([0..9])".
When the precondition in line 1 is replaced by the equivalent version in line 2, we obtain
"Called Frama_C_show_each_m([0..9])
Called Frama_C_show_each_n([0..9])".
Seemingly, from the relation chain "0 <= m <= n <= 9", the information "m <= 9" is not used.
## Attachments
- [ftest.c](/uploads/6bd935ca5fd432edc92877b733d621ff/ftest.c)
https://git.frama-c.com/pub/frama-c/-/issues/1389
suggest to use "NULL" rather than "&NULL" for null pointer
2021-02-22T13:44:22Z
Jochen Burghardt
suggest to use "NULL" rather than "&NULL" for null pointer
ID0001066:
**This issue was created automatically from Mantis Issue 1066. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001066:
**This issue was created automatically from Mantis Issue 1066. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001066 | Frama-C | Plug-in > Eva | public | 2012-01-19 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | pascal | **Resolution** | fixed |
| **Priority** | normal | **Severity** | trivial | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Nitrogen-20111001 | **Target Version** | - | **Fixed in Version** | Frama-C Oxygen-20120901 |
### Description :
Running "frama-c -val exm4.c -no-unicode" on the attached program produces an output "p IN {{ &NULL ; &n }}", which is unusual and confusing for a C-programmer. I'd prefer to get "p IN {{ NULL ; &n }}" instead, which also resembles the C code in line 4 of the program.
From p.26 of file "value-analysis-Nitrogen-20111001.pdf", I understand that (void*)0, which I consider an absolute address, handled in the 2nd item under "A set of addresses", should be denoted as "NULL+0". The notation "&NULL", on the other hand, could be subsumed only under the 1st item on p.26, which seems to indicate that "NULL" denotes some variable. So I consider the output on exm4.c to be inconsistent with the explanations on p.26. The same applies to the use of "&NULL" on p.51 and later in the manual.
## Attachments
- [exm4.c](/uploads/b1ce66eefcc2c74cab2007322c4be3f0/exm4.c)
https://git.frama-c.com/pub/frama-c/-/issues/1379
Emitted assertion wrongly reduces to bottom (apparently) (csmith)
2021-02-22T13:29:18Z
Pascal Cuoq
Emitted assertion wrongly reduces to bottom (apparently) (csmith)
ID0001024:
**This issue was created automatically from Mantis Issue 1024. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001024:
**This issue was created automatically from Mantis Issue 1024. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001024 | Frama-C | Plug-in > Eva | public | 2011-11-19 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Nitrogen-20111001 | **Target Version** | Frama-C Oxygen-20120901 | **Fixed in Version** | Frama-C Oxygen-20120901 |
### Description :
Soundness bug, probably caused by wrong reduction on emitted assertions.
~/ppc/bin/toplevel.opt -slevel 5 -slevel-function main:0 -no-results -val-signed-overflow-alarms -cpp-command "gcc -C -E -Iruntime -m32 " a.c -precise-unions -val
...
a.c:236:[value] Assertion got status invalid (stopping propagation).
[value] Recording results for func_1
[value] Done for function func_1
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
L'analyse avec -slevel 5 dit que la fin du programme et le Frama_C_dump... n'est pas atteint. Pourtant, il l'est comme le montre l'analyse avec -slevel 5000000:
~/ppc/bin/toplevel.opt -slevel 5000000 -slevel-function main:0 -no-results -val-signed-overflow-alarms -cpp-command "gcc -C -E -Iruntime -m32 " a.c -precise-unions -val
...
&& *(unsigned short*)&g_1113 == 65535)
End of Frama_C_dump_assert_each output
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
## Attachments
- [emassert.tgz](/uploads/a75264748678243f7dd1e887608fb9bf/emassert.tgz)
https://git.frama-c.com/pub/frama-c/-/issues/1374
Bad AST generation ?
2021-02-22T13:29:05Z
mantis-gitlab-migration
Bad AST generation ?
ID0001142:
**This issue was created automatically from Mantis Issue 1142. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001142:
**This issue was created automatically from Mantis Issue 1142. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001142 | Frama-C | Plug-in > Eva | public | 2012-04-04 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pherrmann | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Oxygen-20120901 |
### Description :
See program attached: it is accepted as correct (-check passes) but rejected later on (cf. value analysis crashes on it).
## Attachments
- [e.c](/uploads/3efaa42532fa642b0a57d167949b412f/e.c)
https://git.frama-c.com/pub/frama-c/-/issues/1320
File "src/memory_state/lmap.ml", line 931, characters 22-28: Assertion failed
2021-02-22T13:42:52Z
Benjamin Monate
File "src/memory_state/lmap.ml", line 931, characters 22-28: Assertion failed
ID0000889:
**This issue was created automatically from Mantis Issue 889. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000889:
**This issue was created automatically from Mantis Issue 889. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000889 | Frama-C | Plug-in > Eva | public | 2011-07-25 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | monate | **Assigned To** | pascal | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
frama-c /usr/local/share/frama-c/libc/fc_runtime.c main.i protocol.i util.i -val -quiet
crashes the value analysis.
## Attachments
- [main.i](/uploads/f310746c6649373aefea3edc9602f483/main.i)
- [util.i](/uploads/15ac5f03bcc13cfed5c759fbc47a64fc/util.i)
- [protocol.i](/uploads/9753b8a9322f329b2774dc0429fc793b/protocol.i)
https://git.frama-c.com/pub/frama-c/-/issues/1316
Results differ between value analysis and GCC on bitfields
2024-03-15T09:13:18Z
Benjamin Monate
Results differ between value analysis and GCC on bitfields
ID0000890:
**This issue was created automatically from Mantis Issue 890. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000890:
**This issue was created automatically from Mantis Issue 890. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000890 | Frama-C | Plug-in > Eva | public | 2011-07-25 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | monate | **Assigned To** | pascal | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
On the program
==bug.i==============
union U0 {
unsigned short f0 ;
int f1 ;
int f2 : 5 ;
unsigned char const f3 ;
};
unsigned short G0 ;
int G1 ;
int G2;
unsigned char G3 ;
union U0 G={(unsigned short)65532U};
int main() {
G0=G.f0;
G1=G.f1;
G2=G.f2;
G3=G.f3;
printf("%d %d %d %d : %d\n",G0,G1,G2,G3,G2==-4);
return (G2==-4);
}
=========================
frama-c -val bug.i
returns:
===
[value] Values for function main:
G0 ? {65532}
G1[bits 0 to 15] ? {65532}
[bits 16 to 31] ? {0}
G2 ? {28}
G3# ? {65532} misaligned 0%16
__retres ? {0}
===
but gcc bug.i && ./a.out ; echo $?
displays :
===
65532 65532 -4 252 : 1
1
===
They do not agree on the result nor on the value of G2.
https://git.frama-c.com/pub/frama-c/-/issues/1313
Crash du builtin memcpy, par une exception non rattrapable
2023-11-27T14:01:56Z
Boris Yakobowski
Crash du builtin memcpy, par une exception non rattrapable
ID0000883:
**This issue was created automatically from Mantis Issue 883. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000883:
**This issue was created automatically from Mantis Issue 883. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000883 | Frama-C | Plug-in > Eva | public | 2011-07-07 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | yakobowski | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
À analyser avec -val
extern unsigned int i;
char src[20];
char dst[10];
void main () {
if (i <= 10)
Frama_C_memcpy(dst+1, src, i);
}
### Additional Information :
svn 14142