frama-c issues
https://git.frama-c.com/pub/frama-c/-/issues
2021-02-22T13:26:14Z
https://git.frama-c.com/pub/frama-c/-/issues/1289
wrong interpretation when a bit-field receives the result of a function (csmith)
2021-02-22T13:26:14Z
Pascal Cuoq
wrong interpretation when a bit-field receives the result of a function (csmith)
ID0000819:
**This issue was created automatically from Mantis Issue 819. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000819:
**This issue was created automatically from Mantis Issue 819. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000819 | Frama-C | Plug-in > Eva | public | 2011-05-11 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | pascal | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20110201 | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
struct S { int b:31; } s;
int f(void)
{
return -1;
}
main(){
s.b = f();
Frama_C_dump_each();
}
[value] DUMPING STATE of file bitfield_receives_result.c line 10
s.b# ? {-1} misaligned 0%32
.[bits 31 to 31] ? {0}
=END OF DUMP==
https://git.frama-c.com/pub/frama-c/-/issues/1275
Serial conversions in function result (csmith)
2021-02-22T13:25:42Z
Pascal Cuoq
Serial conversions in function result (csmith)
ID0000798:
**This issue was created automatically from Mantis Issue 798. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000798:
**This issue was created automatically from Mantis Issue 798. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000798 | Frama-C | Plug-in > Eva | public | 2011-04-17 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | pascal | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20110201 | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
short x = -10;
int y, z, t;
unsigned short f(void)
{
return x;
}
unsigned short g(void)
{
unsigned short l = *(unsigned short*)&x;
return l;
}
main(){
y = *(unsigned short*)&x;
z = f();
t = g();
}
y and z are computed correctly, but t is wrong:
[value] Values for function main:
y IN {65526; }
z IN {65526; }
t IN {-10; }
https://git.frama-c.com/pub/frama-c/-/issues/1265
Value may be incorrect in presence of several ensures
2021-02-22T13:25:19Z
Julien Signoles
Value may be incorrect in presence of several ensures
ID0000689:
**This issue was created automatically from Mantis Issue 689. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000689:
**This issue was created automatically from Mantis Issue 689. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000689 | Frama-C | Plug-in > Eva | public | 2011-01-26 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | signoles | **Assigned To** | monate | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20101202-beta2 | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
If a function has 1 valid ensure and 1 invalid ensure, the GUI says that both ensures are invalid.
### Steps To Reproduce :
==== a.c ====
/*@ ensures \result == 0;
@ ensures \false;
@ */
int f(void) { return 0; }
void main(void) { f(); }
==============
$ frama-c-gui a.c
Then check the property status of both ensures.
https://git.frama-c.com/pub/frama-c/-/issues/1259
wrong treatment for const arrays in lib-entry mode
2021-02-22T14:02:50Z
David Delmas
wrong treatment for const arrays in lib-entry mode
ID0000759:
**This issue was created automatically from Mantis Issue 759. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000759:
**This issue was created automatically from Mantis Issue 759. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000759 | Frama-C | Plug-in > Eva | public | 2011-03-21 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | ddelmas | **Assigned To** | pascal | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20110201 | **Target Version** | Frama-C Oxygen-20120901 | **Fixed in Version** | Frama-C Oxygen-20120901 |
### Description :
With the attache source file,
frama-c fptr.c -lib-entry -main f -users
yields the below incorrect result:
[users] ====== DISPLAYING USERS ======
f: h0 h1
====== END OF USERS ==========
## Attachments
- [fptr.c](/uploads/076ddbe0115c99046256c2fb6f30d4c4/fptr.c)
https://git.frama-c.com/pub/frama-c/-/issues/1258
Unexpected error (Ival.Float_abstract.Bottom)
2023-11-27T14:01:56Z
mantis-gitlab-migration
Unexpected error (Ival.Float_abstract.Bottom)
ID0000752:
**This issue was created automatically from Mantis Issue 752. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000752:
**This issue was created automatically from Mantis Issue 752. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000752 | Frama-C | Plug-in > Eva | public | 2011-03-11 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | kerstin | **Assigned To** | pascal | **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 Nitrogen-20111001 |
### Description :
Crash if the 3 assertions are added to the program.
Unexpected error (Ival.Float_abstract.Bottom).
commandline: frama-c-gui -val -slevel 10 -main interp interp_bug.c
frama-c -val -slevel 10 -main interp interp_bug.c
## Attachments
- [interp_bug.c](/uploads/d959ec698d88e05db6586ff4c99a6246/interp_bug.c)
https://git.frama-c.com/pub/frama-c/-/issues/1256
Unsoundness in value analysis when bitfield initializer exceeds range (csmith)
2021-02-22T13:24:58Z
John Regher
Unsoundness in value analysis when bitfield initializer exceeds range (csmith)
ID0000721:
**This issue was created automatically from Mantis Issue 721. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000721:
**This issue was created automatically from Mantis Issue 721. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000721 | Frama-C | Plug-in > Eva | public | 2011-02-13 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | regehr | **Assigned To** | pascal | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20110201 | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
The attached program, analyzed like this:
toplevel.opt -val -slevel 25 foo_pp.c
causes Frama-C to emit this assertion:
assert(*(unsigned int*)&g_115 == 9362872);
However, running the program gives the value of g_115 as 23992 at the end of execution.
This is on Ubuntu 10.10 on x86.
## Attachments
- [foo_pp.c](/uploads/3cf8926b10c608456b4537cd51e7b18f/foo_pp.c)
https://git.frama-c.com/pub/frama-c/-/issues/1253
Incorrect states passed to value analysis callbacks in presence of slevel
2021-02-22T13:31:30Z
Boris Yakobowski
Incorrect states passed to value analysis callbacks in presence of slevel
ID0000732:
**This issue was created automatically from Mantis Issue 732. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000732:
**This issue was created automatically from Mantis Issue 732. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000732 | Frama-C | Plug-in > Eva | public | 2011-02-20 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | yakobowski | **Assigned To** | pascal | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20110201 | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
Execute the following program with options '-val -slevel n' for n between 1 and 10001.
int p[20000];
void main () {
for (int j=0;j<10000;j++)
p[j]=1;
}
Inspecting the values of the variable j in the gui reveals ranges of the form [n..10000], which is clearly incorrect.
Also, there is a big gap in the execution time between a fully symbolic evaluation (-slevel 10001) and a partial one (eg. -slevel 10000). This seems to be related to superposing the states in the callbacks.
### Additional Information :
The bug appears between the svn revisions 11262 and 11385.
## Attachments
- ![5000](/uploads/815345649598c607d8e593513c99a542/5000.png)
https://git.frama-c.com/pub/frama-c/-/issues/1248
possible unsoundness bug
2023-05-05T02:36:31Z
John Regher
possible unsoundness bug
ID0000717:
**This issue was created automatically from Mantis Issue 717. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000717:
**This issue was created automatically from Mantis Issue 717. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000717 | Frama-C | Plug-in > Eva | public | 2011-02-12 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | regehr | **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 Nitrogen-20111001 |
### Description :
This is on Ubuntu 10.10 on x86.
Analyzing the attached program like this:
toplevel.opt -val -slevel 24 foo_pp.c
Gives output including:
*(unsigned char*)((unsigned char*)&g_8+30) == 0
However, running the program leaves the value 243 in this byte.
## Attachments
- [foo_pp.c](/uploads/d4618293170dad277408009f857c0c3d/foo_pp.c)
https://git.frama-c.com/pub/frama-c/-/issues/1247
possible unsoundness in r11866
2021-02-22T13:24:39Z
John Regher
possible unsoundness in r11866
ID0000718:
**This issue was created automatically from Mantis Issue 718. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000718:
**This issue was created automatically from Mantis Issue 718. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000718 | Frama-C | Plug-in > Eva | public | 2011-02-12 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | regehr | **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 Nitrogen-20111001 |
### Description :
Analyzing the attached program like this:
~/z/frama-c/bin/toplevel.opt -val -slevel 46 foo_pp.c
Gives this assertion:
*(int*)&g_23 == -10
However, running the program gives value "-9" instead.
## Attachments
- [foo_pp.c](/uploads/df59ba5d2cd54d534cdf2e0f4299ed62/foo_pp.c)
https://git.frama-c.com/pub/frama-c/-/issues/1238
Value analysis: bad type conversion plus unassigned fields in a struct leads ...
2021-02-22T13:24:25Z
mantis-gitlab-migration
Value analysis: bad type conversion plus unassigned fields in a struct leads to crash
ID0001477:
**This issue was created automatically from Mantis Issue 1477. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001477:
**This issue was created automatically from Mantis Issue 1477. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001477 | Frama-C | Plug-in > Eva | public | 2013-09-04 | 2014-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | djs52 | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130601 | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
The attached code crashes value analysis for me (with frama-c -val testcase.c):
[kernel] preprocessing with "gcc -C -E -I. testcase.c"
[value] Analyzing a complete application starting at main
[value] Computing initial state
testcase.c:3:[kernel] warning: overflow in conversion of - 1.0f (-1.) from floating-point to integer.
assert -1 < -1.0f < 256;
[kernel] Current source was: testcase.c:3
The full backtrace is:
Called from file "src/value/initial_state.ml", line 498, characters 14-70
Called from file "list.ml", line 74, characters 24-34
Called from file "src/value/initial_state.ml", line 461, characters 10-1023
Called from file "src/value/initial_state.ml", line 590, characters 20-70
Called from file "list.ml", line 69, characters 12-15
Called from file "src/value/initial_state.ml", line 565, characters 6-1023
Called from file "src/value/initial_state.ml", line 617, characters 13-23
Called from file "src/project/state_builder.ml", line 394, characters 17-21
Called from file "src/value/eval_funs.ml", line 313, characters 14-39
Called from file "src/value/eval_funs.ml", line 564, characters 11-40
Re-raised at file "src/value/eval_funs.ml", line 580, characters 47-50
Called from file "src/project/state_builder.ml", line 839, characters 9-13
Re-raised at file "src/project/state_builder.ml", line 847, characters 15-18
Called from file "src/value/register.ml", line 46, characters 4-24
Called from file "queue.ml", line 134, characters 6-20
Called from file "src/kernel/boot.ml", line 37, characters 4-20
Called from file "src/kernel/cmdline.ml", line 732, characters 2-9
Called from file "src/kernel/cmdline.ml", line 212, characters 4-8
Unexpected error (File "src/memory_state/lmap.ml", line 289, characters 18-24: Assertion failed).
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Fluorine-20130601.
Note that a version and a backtrace alone often do not contain enough
information to understand the bug. Guidelines for reporting bugs are at:
http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelines
## Attachments
- [testcase.c](/uploads/e8ac990612384bf1ede4018d69ea375e/testcase.c)
https://git.frama-c.com/pub/frama-c/-/issues/1221
pointer comparable assert generated between void* and unsigned long
2021-02-22T13:23:55Z
Dillon Pariente
pointer comparable assert generated between void* and unsigned long
ID0001559:
**This issue was created automatically from Mantis Issue 1559. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001559:
**This issue was created automatically from Mantis Issue 1559. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001559 | Frama-C | Plug-in > Eva | public | 2013-11-19 | 2014-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dpariente | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130601 | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
[STANCE]
The following code:
/*------------------------------------------*/
typedef unsigned long size_t;
struct apr_file_t;
typedef struct apr_file_t apr_file_t;
struct apr_file_t {char *fname ;};
int apr_file_write(apr_file_t *thefile, unsigned long *nbytes);
int apr_file_write_full(apr_file_t *thefile, unsigned long nbytes, unsigned long *bytes_written)
{ int status;
unsigned long a;
a = nbytes;
status = apr_file_write(thefile,& a);
nbytes -= a;
if (! (nbytes > (unsigned long)0)) return 0;
return 1;
}
/*------------------------------------------*/
analyzed by:
frama-c.exe -val -main apr_file_write_full -lib-entry foo.c -no-unicode
generates an assert:
[kernel] warning: pointer comparison:
assert \pointer_comparable((void *)nbytes, (unsigned long)0);
which, once the project is pretty-printed (-print -ocode ...),
yields an error on the generated C file:
[kernel] user error: no such predicate or logic function \pointer_comparable(void *, unsigned long) in annotation.
(... indeed it might be an issue at Kernel level!)
## Attachments
- [patch-ptr-comparable](/uploads/93c9deb5551e847fe57e42df72977385/patch-ptr-comparable)
https://git.frama-c.com/pub/frama-c/-/issues/1211
validity of a field defined in an abstract struct typedef
2021-02-22T13:30:31Z
Dillon Pariente
validity of a field defined in an abstract struct typedef
ID0001486:
**This issue was created automatically from Mantis Issue 1486. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001486:
**This issue was created automatically from Mantis Issue 1486. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001486 | Frama-C | Plug-in > Eva | public | 2013-09-26 | 2014-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dpariente | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130501 | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
[STANCE]
The small source code snippet is extracted from an Apache server module.
//------------------------------------
struct core_dir_config { int server_signature; } core_dir_config;
typedef struct core_dir_config core_dir_config;
struct request_rec { struct ap_conf_vector_t *per_dir_config; } request_rec;
typedef struct request_rec request_rec;
//@ requires \valid(r->per_dir_config);
const char * app(request_rec *r)
{
core_dir_config *conf;
conf = (core_dir_config *)(((void **)(r->per_dir_config))[0]);
if (conf->server_signature == 1) { return ""; }
return " ";
}
//------------------------------------
When analyzed by:
frama-c -val -main app bug.c -lib-entry -no-unicode
Value generates an error:
$ Internal error 835; debug info:
{{ NULL -> {0}; S_r -> {0} }} (size:<32>)
Is it "abstract struct type" related?
Is there any workaround?
## Attachments
- [patch-stance](/uploads/e7a7207756d1fab4453eae629c1694c0/patch-stance)
https://git.frama-c.com/pub/frama-c/-/issues/1209
Interpretation of @ assigns \result;
2023-05-16T12:35:51Z
mantis-gitlab-migration
Interpretation of @ assigns \result;
ID0001448:
**This issue was created automatically from Mantis Issue 1448. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001448:
**This issue was created automatically from Mantis Issue 1448. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001448 | Frama-C | Plug-in > Eva | public | 2013-06-20 | 2014-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Anne | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130501 | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
Sorry for the title which is not very informative, but here is the problem :
in this example :
//@ assigns \result;
extern char * get_ptr (void);
int main (void) { char * p = get_ptr (); int x = p ? 0 : 1; return x; }
The value analysis tells me that the else branch is dead, so x is always 0.
If I change the assigns property into :
//@ assigns \result \from \nothing;
The problem disappears.
https://git.frama-c.com/pub/frama-c/-/issues/1204
Smarter access to array of struct of array
2021-02-22T13:23:20Z
Pascal Cuoq
Smarter access to array of struct of array
ID0001044:
**This issue was created automatically from Mantis Issue 1044. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001044:
**This issue was created automatically from Mantis Issue 1044. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001044 | Frama-C | Plug-in > Eva | public | 2011-12-10 | 2014-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
Smarter access to array of struct of array
## Attachments
- [test1.c](/uploads/c77a0f373169ebe36d95a11954412e2c/test1.c)
https://git.frama-c.com/pub/frama-c/-/issues/1186
Assertion failure in Ival.scale_div
2021-02-22T13:22:35Z
Boris Yakobowski
Assertion failure in Ival.scale_div
ID0001584:
**This issue was created automatically from Mantis Issue 1584. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001584:
**This issue was created automatically from Mantis Issue 1584. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001584 | Frama-C | Plug-in > Eva | public | 2013-12-09 | 2014-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | yakobowski | **Assigned To** | pascal | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
(Csmith-found program, reduced by creduce)
To be analyzed with -slevel 4.
Interesting part of the backtrace:
Called from file "src/ai/ival.ml", line 1011, characters 3-123
Called from file "src/ai/ival.ml", line 1166, characters 2-35
Called from file "src/ai/ival.ml", line 2370, characters 20-48
## Attachments
- [small3.i](/uploads/5eae9a679e659d4b5d94d6604e24c457/small3.i)
https://git.frama-c.com/pub/frama-c/-/issues/1178
uninitialized value can be passed through pointer, through return, but not t...
2021-02-22T13:22:22Z
Jochen Burghardt
uninitialized value can be passed through pointer, through return, but not through function argument
ID0001447:
**This issue was created automatically from Mantis Issue 1447. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001447:
**This issue was created automatically from Mantis Issue 1447. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001447 | Frama-C | Plug-in > Eva | public | 2013-06-13 | 2014-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130501 | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
Running "frama-c -val ftest.c" on the attached program doesn't produce any warning, although the uninitialized value of variable "undf" is passed to variable "i" and "k" via assignment to a pointer and via return in line 7 and 9, respectively.
If it is passed also to variable "j" via function argument (uncomment line 8 to do this), a warning is issued, as expected, even although "j" is never used.
I would have expected similar behavior in all 3 cases, preferrable issuing always a warning.
## Attachments
- [ftest.c](/uploads/0fe3a52d968a24b302d37eb327e5b80f/ftest.c)
https://git.frama-c.com/pub/frama-c/-/issues/1160
The post-conditon of [gets] got status invalid
2021-02-22T13:21:34Z
mantis-gitlab-migration
The post-conditon of [gets] got status invalid
ID0001435:
**This issue was created automatically from Mantis Issue 1435. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001435:
**This issue was created automatically from Mantis Issue 1435. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001435 | Frama-C | Plug-in > Eva | public | 2013-05-30 | 2014-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Anne | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130501 | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
When using 'gets' from Frama-C include files, the value analysis gives :
:/usr/local/share/frama-c/libc/stdio.h:225:
[value] Function gets: postcondition got status invalid.
I don't really understand how Value can say something about the post-condition of an undefined function, but anyway, then I get "This call never terminates".
It seems that a fix is to add :
@ assigns \result \from s, *__fc_stdin;
but maybe it could be more correct to also add :
@ assigns *__fc_stdin \from *__fc_stdin ;
### Additional Information :
Example :
$ frama-c -val toto.c -cpp-extra-args="-I`frama-c -print-path`/libc -nostdinc"
#include <stdio.h>
void main () {
char line[100];
char * p = gets (line);
}
https://git.frama-c.com/pub/frama-c/-/issues/1157
Logging just enough information for failed pre-conditions
2022-10-03T08:07:55Z
Pascal Cuoq
Logging just enough information for failed pre-conditions
ID0001415:
**This issue was created automatically from Mantis Issue 1415. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001415:
**This issue was created automatically from Mantis Issue 1415. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001415 | Frama-C | Plug-in > Eva | public | 2013-05-03 | 2014-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **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 Neon-20140301 |
### Description :
There was a bit of a discussion over an analysis made on an example provided by a StackOverflow user:
http://stackoverflow.com/a/16356519/139746
The current message is:
.../libc/string.h:54:[value] Function memcpy: precondition got status invalid.
That is a bit frustrating. The localization of the call to memcpy() can be found just above in the log:
[value] computing for function memcpy <- main.
Called from mem.c:13.
but the exact nature of the detected issue is only printed as a reference to libc/string.h, a file that the user did not even provide emself.
There are at least two solutions suggested by the discussion:
- annotate the libc preconditions with nice labels, and when a pre-condition fails, print any label it may have, or
- print the entire ACSL pre-condition that failed, including any label it may have.
https://git.frama-c.com/pub/frama-c/-/issues/1152
strange warning "postcondition got status invalid"
2022-08-29T14:56:07Z
Jochen Burghardt
strange warning "postcondition got status invalid"
ID0001369:
**This issue was created automatically from Mantis Issue 1369. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001369:
**This issue was created automatically from Mantis Issue 1369. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001369 | Frama-C | Plug-in > Eva | public | 2013-02-15 | 2014-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Oxygen-20120901 | **Target Version** | Frama-C Neon-20140301 | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
Running "frama-c -val ftest.c" on the attached program produces a "[value] Function foo: postcondition got status invalid" in line 6, although the ensures clause looks quite reasonable. (I don't understand the notion of a "postcondition status": shouldn't the postconditions of a function be satisfied automatically if all its preconditions are?) The warning disappears if the ensures clause in line 5 is removed or an appropriate function body (e.g. the one commented out at the end of line 6) is added.
## Attachments
- [ftest.c](/uploads/0c897adefea2db69ea93598a19ce19bc/ftest.c)
https://git.frama-c.com/pub/frama-c/-/issues/1141
Unbound value Base.get_varinfo (Neon)
2021-02-22T13:21:03Z
Dillon Pariente
Unbound value Base.get_varinfo (Neon)
ID0001691:
**This issue was created automatically from Mantis Issue 1691. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001691:
**This issue was created automatically from Mantis Issue 1691. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001691 | Frama-C | Plug-in > Eva | public | 2014-03-13 | 2014-03-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dpariente | **Assigned To** | yakobowski | **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** | - |
### Description :
[STANCE]
Base.get_varinfo disappeared from the API.
What can replace it?