frama-c issues
https://git.frama-c.com/pub/frama-c/-/issues
2021-02-22T14:03:55Z
https://git.frama-c.com/pub/frama-c/-/issues/1897
Extern function vs extern variable to get a random value
2021-02-22T14:03:55Z
mantis-gitlab-migration
Extern function vs extern variable to get a random value
ID0001372:
**This issue was created automatically from Mantis Issue 1372. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001372:
**This issue was created automatically from Mantis Issue 1372. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001372 | Frama-C | Plug-in > Eva | public | 2013-02-20 | 2013-04-19 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Anne | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Oxygen-20120901 | **Target Version** | - | **Fixed in Version** | Frama-C Fluorine-20130401 |
### Description :
I am trying to build an environment to represent the inputs of the application that I study with the value analysis. I tried different things :
~~~~~~~~~~~~~
1/ double v = ext_double; assert (v <= 100);
with the global variable : extern double ext_double;
gives what I want: v ? [-1.79769313486e+308 .. 100.]
~~~~~~~~~~~~~
2/ double v = rand_double (); assert (v <= 100);
with:
//@ assigns \result \from \nothing;
extern double rand_double ();
gives a warning that I don't understand:
toto.c:25:[value] warning: converting value to float: assert(Ook)
and doesn't use the assert (?):
v ? [--..--]
~~~~~~~~~~~~~
3/ double v = rand_double_post (); assert (v <= 100);
with:
//@ assigns \result \from \nothing; ensures \result <= 100;
extern double rand_double_post ();
gives the same warning twice:
toto.c:21:[value] warning: converting value to float: assert(Ook)
toto.c:25:[value] warning: converting value to float: assert(Ook)
and doesn't work either:
v ? [--..--]
~~~~~~~~~~~~~
4/ double v = rand_double_var (); assert (v <= 100);
with:
extern double rand_double_var () { return ext_double; }
gives no warning, and works as expected:
v ? [-1.79769313486e+308 .. 100.]
~~~~~~~~~~~~~
Shouldn't the four initializations give the same results ?
Sorry if it is about something that I didn't understand...
### Additional Information :
With the attached file, see previous results with the command:
$ frama-c -val toto.c -cpp-extra-args="-DT=1"
with different values of T (1 to 4).
## Attachments
- [toto.c](/uploads/9e28b543bd0896a04a18d16dd7ead4cf/toto.c)
https://git.frama-c.com/pub/frama-c/-/issues/1891
Crash with Invalid argument for Frama_C_alloc_size function
2021-02-22T13:45:09Z
mantis-gitlab-migration
Crash with Invalid argument for Frama_C_alloc_size function
ID0001302:
**This issue was created automatically from Mantis Issue 1302. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001302:
**This issue was created automatically from Mantis Issue 1302. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001302 | Frama-C | Plug-in > Eva | public | 2012-11-14 | 2013-04-19 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Anne | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Oxygen-20120901 | **Target Version** | - | **Fixed in Version** | Frama-C Fluorine-20130401 |
### Description :
$ frama-c toto.c -val
gives :
[value] user error: Invalid argument for Frama_C_alloc_size function
(...)
Unexpected error (Kernel_function.No_Definition).
Please report as 'crash' at http://bts.frama-c.com/.
It seems ok that the value analysis doesn't know what to do with this example,
but I guess it shouldn't 'crash'...
## Attachments
- [toto.c](/uploads/1511017492714bdf46e6978e5cd2caca/toto.c)
https://git.frama-c.com/pub/frama-c/-/issues/1884
Locations.valid_enumerate_bits enumerate invalid bits
2021-02-22T13:44:59Z
Boris Yakobowski
Locations.valid_enumerate_bits enumerate invalid bits
ID0001264:
**This issue was created automatically from Mantis Issue 1264. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001264:
**This issue was created automatically from Mantis Issue 1264. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001264 | Frama-C | Plug-in > Eva | public | 2012-08-08 | 2013-04-19 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | yakobowski | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | low | **Severity** | tweak | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Nitrogen-20111001 | **Target Version** | - | **Fixed in Version** | Frama-C Fluorine-20130401 |
### Description :
The program below shows that valid_enumerate_bits can return Top intervals, even on bases where the validity is completely known. This defeats the purpose of the function, and can cause very subtle bugs with the "default" flag in Offsetmap_bitwise.
---------- many.c ----------------
struct s {
int f1;
int f2;
};
struct s t[10][10];
void main() {
for (int i=0; i<10; i++) {
for (int j=0; j<10; j++) {
t[i][j].f1 = 1;
}
}
}
-------------------------------------
Command-line: frama-c -val many.c -out -plevel 80 -slevel 50
This combination of slevel/plevel will result in only one " more than foo elements to enumerate. Approximating." message, caused by the Out plugin.
----------------------------------------
Output:
[inout] Out (internal) for function main:
t[..]; i; j
The expected output is t[0..9][0..9]; i; j
### Additional Information :
The problem lies either in valid_enumerate_bits itself, or in Lattice_Interval_Set.from_ival_int
https://git.frama-c.com/pub/frama-c/-/issues/1864
warning for unreachable program point
2021-02-22T13:44:30Z
mantis-gitlab-migration
warning for unreachable program point
ID0001425:
**This issue was created automatically from Mantis Issue 1425. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001425:
**This issue was created automatically from Mantis Issue 1425. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001425 | Frama-C | Plug-in > Eva | public | 2013-05-23 | 2013-05-23 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Anne | **Assigned To** | yakobowski | **Resolution** | no change required |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | N/A |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130401 | **Target Version** | - | **Fixed in Version** | - |
### Description :
It might be interesting that the Value analysis emit a message when it detect that the program point after a loop or a call is unreachable.
Just an idea...
### Additional Information :
Example:
void may_be_infinite (int c) {
int x = 0;
if (c > 0) {
while (1) ;
x = 1; // <-- unreachable
}
}
void main (int cond) {
int r = 0;
if (cond > 0) {
may_be_infinite (cond);
r = 1; // <-- unreachable
}
else {
may_be_infinite (cond);
r = 2;
}
}
https://git.frama-c.com/pub/frama-c/-/issues/1863
"Loss of precision" message after shift
2021-02-22T13:44:29Z
mantis-gitlab-migration
"Loss of precision" message after shift
ID0001423:
**This issue was created automatically from Mantis Issue 1423. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001423:
**This issue was created automatically from Mantis Issue 1423. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001423 | Frama-C | Plug-in > Eva | public | 2013-05-22 | 2013-05-23 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dhekir | **Assigned To** | yakobowski | **Resolution** | no change required |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130401 | **Target Version** | - | **Fixed in Version** | - |
### Description :
If I use Frama-C to analyze the following program:
int a[2];
int main() {
int i = &(a[0]);
int j = i >> 8;
return 0;
}
The value analysis reports the following:
[kernel] preprocessing with "gcc -C -E -I. test.c"
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
a[0..1] ? {0}
test.c:5:[kernel] warning: Operation {{ &a }} >> {8} incurs a loss of precision
test.c:5:[value] Assigning imprecise value to j.
The imprecision originates from Arithmetic {test.c:5}
[value] Recording results for main
[value] done for function main
Is this expected? Shouldn't there be a message in line 4? I'm sorry if my understanding of the C standard is incorrect, but I believe the warning could be made in a more clear way, or maybe it could reference line 4 to help the user see the original source of the problem.
https://git.frama-c.com/pub/frama-c/-/issues/1861
Different signed_overflow assert with rte + val
2021-02-22T13:44:26Z
mantis-gitlab-migration
Different signed_overflow assert with rte + val
ID0001424:
**This issue was created automatically from Mantis Issue 1424. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001424:
**This issue was created automatically from Mantis Issue 1424. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001424 | Frama-C | Plug-in > Eva | public | 2013-05-22 | 2013-05-23 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Anne | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130401 | **Target Version** | - | **Fixed in Version** | Frama-C Fluorine-20130501 |
### Description :
I use -rte to generate annotations, and then -val to check them,
and usually, Value doesn't emit new annotations for 'signed_overflow' RTE.
But in this case :
int main (int x) {
int a;
if (0 <= x)
a = x;
else
a = - x;
return a;
}
RTE generates : /*@ assert rte: signed_overflow: -2147483648 ? x; */
Value validates it : [value] Assertion got status valid.
but then emits an unchecked annotation :
/*@ assert Value: signed_overflow: -x ? 2147483647; */
It looks strange, doesn't it.
### Additional Information :
I was expected to have no "Value:signed_overflow" properties after rte.
Am I wrong ?
https://git.frama-c.com/pub/frama-c/-/issues/1848
Some Value assert are not in the log file
2021-02-22T13:44:08Z
mantis-gitlab-migration
Some Value assert are not in the log file
ID0001426:
**This issue was created automatically from Mantis Issue 1426. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001426:
**This issue was created automatically from Mantis Issue 1426. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001426 | Frama-C | Plug-in > Eva | public | 2013-05-23 | 2013-05-30 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Anne | **Assigned To** | yakobowski | **Resolution** | unable to reproduce |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130401 | **Target Version** | - | **Fixed in Version** | - |
### Description :
When running a value analysis, I usually redirect stdout in a file and use :
grep warning val.log
to analyze the results.
But I just remarked that some 'assert' are generated by Value (can see them in the GUI or in the '-report' results) but are not printed in the log file.
In my example, they are Assertion 'Value,is_nan_or_infinite' normally logged as:
"warning: non-finite double value"
### Additional Information :
Sorry : don't have time to build an example today.
I'll try to do it later if you need it.
https://git.frama-c.com/pub/frama-c/-/issues/1835
unexpected stack overflow in value analysis
2021-02-22T13:43:42Z
Jochen Burghardt
unexpected stack overflow in value analysis
ID0001374:
**This issue was created automatically from Mantis Issue 1374. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001374:
**This issue was created automatically from Mantis Issue 1374. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001374 | Frama-C | Plug-in > Eva | public | 2013-02-25 | 2013-08-26 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | yakobowski | **Resolution** | unable to reproduce |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Oxygen-20120901 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running 'frama-c -cpp-command "{{many cpp options}}" -no-unicode -pp-annot -slevel 300 -val-ignore-recursive-calls {{27 c files}}' caused an unexpected stack overflow after computing for about 18 hours and writing a 3.6 GB log file.
Unfortunately, I cannot provide the C sources; they were about 9400 lines (total), distributed to 27 C files.
I attach the backtrace log; it seemingly contains a loop starting at line 168 (bottommost repeated line in log file: 'Called from file "src/value/eval_funs.ml", line 86, characters 9-32').
Due to the long run-time it is also impossible to boil-down the code causing the stack overflow.
## Attachments
- [backtrace.log](/uploads/fe06fe6f08cc1f5b8ee840e9b655e56e/backtrace.log)
- [stackoverflow.ml](/uploads/600855f22566fe97f823e83e1400b864/stackoverflow.ml)
- [calledFuncs.txt](/uploads/81bda206000422b768f369d905e3dd36/calledFuncs.txt)
https://git.frama-c.com/pub/frama-c/-/issues/1824
speed of value analysis while use the "-lib-entry" and "main" and "-val-use-s...
2021-02-22T13:43:23Z
mantis-gitlab-migration
speed of value analysis while use the "-lib-entry" and "main" and "-val-use-spec" option for value analysis
ID0001593:
**This issue was created automatically from Mantis Issue 1593. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001593:
**This issue was created automatically from Mantis Issue 1593. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001593 | Frama-C | Plug-in > Eva | public | 2014-01-12 | 2014-01-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Yibiao | **Assigned To** | yakobowski | **Resolution** | no change required |
| **Priority** | low | **Severity** | trivial | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
With "-lib-entry", all global variables in the ast file will be initialized for a initial state in value analysis.
But I think it will largely impact on the speed of value analysis. Especially when I am using the "-val-use-spec" option for all the functions which called by the main function, there will be many global variables might not useful for value analysis. So in fact, I think we can only initialize all the global variables which only used in the main function for improving the speed of value analysis.
https://git.frama-c.com/pub/frama-c/-/issues/1823
value analysis crashed after I the ast was modified in a new project
2021-02-22T13:43:22Z
mantis-gitlab-migration
value analysis crashed after I the ast was modified in a new project
ID0001585:
**This issue was created automatically from Mantis Issue 1585. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001585:
**This issue was created automatically from Mantis Issue 1585. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001585 | Frama-C | Plug-in > Eva | public | 2013-12-11 | 2014-01-14 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Yibiao | **Assigned To** | yakobowski | **Resolution** | no change required |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130601 | **Target Version** | - | **Fixed in Version** | - |
### Description :
I am writing a script to transform all call stmt of using
function pointer to a regular call stm inspired by Virgile 's insert_stmt script.
I am not only transform the ast, but also want to do the value analysis in the modified ast.
When I load my script, it was crashed in value analysis process.
frama-c -load-script transfer.ml pfunc.c
### Additional Information :
attached is the files for the command line:
1. transfer.ml
2. pfun.c
The command line used here is:
frama-c -load-script transfer.ml pfunc.c
## Attachments
- [transform.zip](/uploads/2abd9a339b9545b2644e8a0fdf2a860d/transform.zip)
- [transfer.ml](/uploads/00c38a0785a1499e84354a205cc6c753/transfer.ml)
https://git.frama-c.com/pub/frama-c/-/issues/1815
Incompatibility between -inout-callwise and failing built-ins.
2021-02-22T13:43:12Z
Pascal Cuoq
Incompatibility between -inout-callwise and failing built-ins.
ID0001637:
**This issue was created automatically from Mantis Issue 1637. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001637:
**This issue was created automatically from Mantis Issue 1637. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001637 | Frama-C | Plug-in > Eva | public | 2014-01-30 | 2014-02-06 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | yakobowski | **Resolution** | won't fix |
| **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 :
The test below, called with the corresponding commandline, causes a crash.
$ cat tests/misc/outside_builtin_callwise.i
/* run.config
OPT: -inout-callwise -val-builtin strlen:Frama_C_strlen -val t.c
*/
int strlen ()
{
return 0;
}
int main ()
{
strlen(); // note that we pass the wrong number of arguments,
// causing Db.Value.Outside_builtin_possibilities to be raised.
}
The causes appears to be that Value tells Inout that strlen is the sort of function that is analyzed as built-in and that inout should analyze from specs instead of code, although the built-in failed and strlen() was actually analyzed from code.
If this diagnostic is correctish, a solution might be for Value to pass a boolean to registered hooks instead of having them call a function !Db.Value.use_spec_instead_of_definition that does not know the answer. This could be solved with a change of API on the side of Value.
____________
Crash:
[kernel] Current source was: tests/misc/outside_builtin_callwise.i:12
The full backtrace is:
Raised at file "pervasives.ml", line 20, characters 22-33
Called from file "src/inout/operational_inputs.ml", line 576, characters 31-56
Called from file "src/inout/operational_inputs.ml", line 327, characters 30-47
Called from file "src/inout/operational_inputs.ml", line 325, characters 15-939
Called from file "src/inout/operational_inputs.ml", line 380, characters 34-59
Called from file "cil/src/ext/dataflows.ml", line 310, characters 12-42
Called from file "cil/src/ext/dataflows.ml", line 318, characters 19-30
Called from file "cil/src/ext/dataflows.ml", line 319, characters 5-14
Called from unknown location
Called from unknown location
Called from unknown location
Called from file "src/inout/operational_inputs.ml", line 600, characters 16-69
Called from file "queue.ml", line 134, characters 6-20
Called from file "src/value/eval_slevel.ml", line 198, characters 5-326
Called from file "src/value/eval_funs.ml", line 78, characters 2-27
Called from file "src/value/eval_funs.ml", line 307, characters 8-61
Called from file "src/value/eval_funs.ml", line 380, characters 10-110
Called from file "src/value/eval_funs.ml", line 659, characters 11-40
Re-raised at file "src/value/eval_funs.ml", line 678, characters 47-50
Called from file "src/project/state_builder.ml", line 841, characters 9-13
Re-raised at file "src/project/state_builder.ml", line 849, characters 15-18
Called from file "src/value/register.ml", line 83, 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 735, characters 2-9
Called from file "src/kernel/cmdline.ml", line 214, characters 4-8
Unexpected error (Failure("hd")).
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Fluorine-20130601+dev.
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
https://git.frama-c.com/pub/frama-c/-/issues/1810
strange warning "extracting bits of a pointer"
2021-02-22T13:42:58Z
Jochen Burghardt
strange warning "extracting bits of a pointer"
ID0001364:
**This issue was created automatically from Mantis Issue 1364. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001364:
**This issue was created automatically from Mantis Issue 1364. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001364 | Frama-C | Plug-in > Eva | public | 2013-02-12 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | tweak | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Oxygen-20120901 | **Target Version** | - | **Fixed in Version** | Frama-C Fluorine-20130401 |
### Description :
Running "frama-c -val ftest.c" on the attached program causes a
"[kernel] warning: extracting bits of a pointer"
for line 13, where neither any pointer nor any bit operation is present in the code. The warning vanishes if
(1) the field "int a" in line 3 is removed from the struct _s,
(2) the field "char *b" in line 4 is removed from the struct _s, or
(3) the "extern" is removed from the declaration of "s" in line 10.
Except for (2), no such action touches any pointer or bit operation.
## Attachments
- [ftest.c](/uploads/e58a21fc9403889db8c62e24e4c036dd/ftest.c)
https://git.frama-c.com/pub/frama-c/-/issues/1794
interest for a built-in memset function
2021-02-22T13:42:12Z
David Delmas
interest for a built-in memset function
ID0000915:
**This issue was created automatically from Mantis Issue 915. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000915:
**This issue was created automatically from Mantis Issue 915. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000915 | Frama-C | Plug-in > Eva | public | 2011-08-05 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | ddelmas | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20110201 | **Target Version** | - | **Fixed in Version** | Frama-C Fluorine-20130401 |
### Description :
The following command produces perfectly precise results on the attached example:
frama-c frama-c-lib.c $(frama-c -print-path)/libc.c -val -cpp-command 'gcc -C -E -I$(frama-c -print-path)' -main F1
On the contrary, analysing -main F2 instead of F1 yields unprecise results, unless unrolling is used. It would be of great interest, both for precision and performance, to have a Frama-C built-in for the memset library function, at least in the frequent case where the abstract value of the second parameter is just the {0} singleton.
## Attachments
- [frama-c-lib.c](/uploads/e577d1fc9149baf49243e6655cbf56e1/frama-c-lib.c)
https://git.frama-c.com/pub/frama-c/-/issues/1781
Evaluation in the logic can cause crashes
2021-02-22T13:41:34Z
Boris Yakobowski
Evaluation in the logic can cause crashes
ID0001000:
**This issue was created automatically from Mantis Issue 1000. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001000:
**This issue was created automatically from Mantis Issue 1000. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001000 | Frama-C | Plug-in > Eva | public | 2011-10-25 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | yakobowski | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | unable to reproduce |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Nitrogen-20111001 | **Target Version** | - | **Fixed in Version** | Frama-C Oxygen-20120901 |
### Description :
Evaluation in the logic sometimes causes the warning "using size of void". Worse, this can lead to crashes, as e.g. do_cast raises assert false when it encounters something of type void.
It is not clear how one goes from something that has type void* to something that has type void, but this definitely happens.
### Steps To Reproduce :
This example can be used to cause the apparition of the warning
frama-c -val -then -print
void main (int i) {
int x=1;
while(1)
Frama_C_memcpy((void *)&x, (void const*)&x, i);
}
The generated assertion cast the pointer to void*, then does arithmetic on it. This is incorrect.
https://git.frama-c.com/pub/frama-c/-/issues/1775
Slicing generates empty program (csmith)
2021-02-22T13:41:22Z
Pascal Cuoq
Slicing generates empty program (csmith)
ID0000968:
**This issue was created automatically from Mantis Issue 968. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000968:
**This issue was created automatically from Mantis Issue 968. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000968 | Frama-C | Plug-in > Eva | public | 2011-09-19 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
Le programme slicé s.15102009.9.s.c, obtenu avec la commande slice_src_dest.sh, est vide.
## Attachments
- [968.tgz](/uploads/fea68ec0d3896dea3c5b3f70667d2011/968.tgz)
https://git.frama-c.com/pub/frama-c/-/issues/1761
Cash in value analysis of sliced project
2021-02-22T14:03:42Z
Patrick Baudin
Cash in value analysis of sliced project
ID0000791:
**This issue was created automatically from Mantis Issue 791. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000791:
**This issue was created automatically from Mantis Issue 791. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000791 | Frama-C | Plug-in > Eva | public | 2011-04-13 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | patrick | **Assigned To** | pascal | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
Unexpected error (File "src/kernel/cilE.ml", line 268, characters 68-74: Assertion failed).
### Additional Information :
Revision: 12829
Command:
frama-c bug.c -slice-return send -then-on 'Slicing export' -val
file bug.c
/*@ assigns *p \from \empty;
assigns \result ; */
int scanf (char const *, int * p);
/*@ assigns \nothing ; */
int send (int x) {
return x;
}
void main(void) {
int input;
scanf("%d",&input);
send (input);
}
https://git.frama-c.com/pub/frama-c/-/issues/1754
Print addresses in hexadecimal
2021-02-22T13:40:20Z
Boris Yakobowski
Print addresses in hexadecimal
ID0000730:
**This issue was created automatically from Mantis Issue 730. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000730:
**This issue was created automatically from Mantis Issue 730. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000730 | Frama-C | Plug-in > Eva | public | 2011-02-18 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | yakobowski | **Assigned To** | pascal | **Resolution** | fixed |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20110201 | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
It would be really helpful to have an option that asks the value analysis to print memory addresses in hexadecimal instead of base 10 integers.
That is, print eg. NULL[117445956..117445959] as NULL[0x7001544-7001547]. I think this would also be fine for smaller offsets.
I tried to do the change myself, but Big_int.to_hex_string (or anything equivalent) does not exists... Ideas are welcome.
https://git.frama-c.com/pub/frama-c/-/issues/1738
Superfluous ';' in value analysis output
2021-02-22T13:39:48Z
Boris Yakobowski
Superfluous ';' in value analysis output
ID0000634:
**This issue was created automatically from Mantis Issue 634. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000634:
**This issue was created automatically from Mantis Issue 634. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000634 | Frama-C | Plug-in > Eva | public | 2010-12-03 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | yakobowski | **Assigned To** | pascal | **Resolution** | fixed |
| **Priority** | none | **Severity** | tweak | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Boron-20100401 | **Target Version** | - | **Fixed in Version** | Frama-C Carbon-20101201-beta1 |
### Description :
The pretty-printer for the Locations.Zone.t prints '; ' even after the last location, causing not so pretty outputs when the location contains a single zone.
(This case is very frequent for Lmap_bitwise obtained outputs.) The attached patch corrects this.
### Additional Information :
Will require to update our various manuals after being applied.
## Attachments
- [patch-pretty-locations.diff](/uploads/a37923daa4398f209fd4511ef6b6f6a5/patch-pretty-locations.diff)
https://git.frama-c.com/pub/frama-c/-/issues/1694
Comparing a function pointer will NULL might raise incorrect warning
2021-02-22T13:38:17Z
Boris Yakobowski
Comparing a function pointer will NULL might raise incorrect warning
ID0000472:
**This issue was created automatically from Mantis Issue 472. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000472:
**This issue was created automatically from Mantis Issue 472. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000472 | Frama-C | Plug-in > Eva | public | 2010-05-07 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | yakobowski | **Assigned To** | pascal | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Boron-20100401 | **Target Version** | - | **Fixed in Version** | Frama-C Carbon-20101201-beta1 |
### Description :
In the code below, the value analysis flags the comparison of fun with the NULL pointer as requiring a comparability assertion, while a comparison with the NULL pointer is always legal.
void f(void);
void g(void);
extern int j;
int main (void) {
void (*fun)(void);
int* p;
if(j) fun = f; else fun = g;
if (fun == 0) return 0; else return 1;
}
(The problem does not appear if 'fun' is a pointer to only one function, or when comparing non-functional pointers.)
https://git.frama-c.com/pub/frama-c/-/issues/1658
Precise widening when a loop condition involves a char or short
2021-02-22T14:04:43Z
Pascal Cuoq
Precise widening when a loop condition involves a char or short
ID0000325:
**This issue was created automatically from Mantis Issue 325. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000325:
**This issue was created automatically from Mantis Issue 325. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000325 | Frama-C | Plug-in > Eva | public | 2009-11-07 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | pascal | **Resolution** | fixed |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090902 | **Target Version** | - | **Fixed in Version** | Frama-C Boron-20100401 |
### Description :
> Depending the type of i, the range is not the same.
> The range of i in the loop is [0..10] (for int) or [0..15] for char or
> short.
_____
void main(void)
{
char i=0;
int j=0;
while (i<10) i++;
while (j<10) j++;
}
[value] ====== VALUES COMPUTED ======
[value] Values for function main:
i IN {10; 11; 12; 13; 14; 15; }
j IN {10; }
_____
Note that the AST for the two loops is different:
i = (char)0;
j = 0;
while ((int )i < 10) {i = (char )((int )i + 1);}
while (j < 10) {j ++;}
CIL transforms the code thus because the standard
specifies that operators such as ++ do not operate on
types smaller than int, and that values of these types
are implicitly promoted to int in these conditions.
Meanwhile, in the absence of any loop-related
option, the value analysis tries to keep computations
short at the price of precision by using a technique
called "widening". In order to limit the loss of precision,
however, various heuristics are used, including a
syntactic one for the j loop that recognizes that
j IN [0..10] is a good candidate for the loop invariant.
These heuristic does not currently recognize the condition
((int )i < 10) as one where it would be valuable to try
the same kind of invariant.