frama-c issues
https://git.frama-c.com/pub/frama-c/-/issues
2021-02-22T13:58:10Z
https://git.frama-c.com/pub/frama-c/-/issues/2396
Wrong postconditions are "valid according to value analysis"
2021-02-22T13:58:10Z
Guillaume Melquiond
Wrong postconditions are "valid according to value analysis"
ID0000372:
**This issue was created automatically from Mantis Issue 372. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000372:
**This issue was created automatically from Mantis Issue 372. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000372 | Frama-C | Plug-in > Eva | public | 2010-01-13 | 2010-04-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | gmelquio | **Assigned To** | virgile | **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 Boron-20100401 |
### Description :
/*@ ensures \result == 1; */
int main() {
return 0;
}
When clicking on the "ensures" clause, Frama-C GUI (r7298) reports:
This is an ensures clause.
Status: Valid according to value analysis
https://git.frama-c.com/pub/frama-c/-/issues/2391
Failure("Function 'From.find_deps_no_transitivity' not registered yet")
2021-02-22T13:58:03Z
mantis-gitlab-migration
Failure("Function 'From.find_deps_no_transitivity' not registered yet")
ID0000392:
**This issue was created automatically from Mantis Issue 392. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000392:
**This issue was created automatically from Mantis Issue 392. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000392 | Frama-C | Plug-in > Eva | public | 2010-02-03 | 2010-04-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | djs52 | **Assigned To** | pascal | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090902 | **Target Version** | - | **Fixed in Version** | Frama-C Boron-20100401 |
### Description :
Attempting value analysis on a large code base, using -mem-exec to exclude some difficult functions. Running frama-c -val -mem-exec ... seems to complete without error; frama-c-gui with the same options fails with
Unexpected error (Failure("Function 'From.find_deps_no_transitivity' not registered yet"))
https://git.frama-c.com/pub/frama-c/-/issues/412
Incorrect location of warnings emitted by value analysis
2021-02-22T13:57:59Z
Virgile Prevosto
Incorrect location of warnings emitted by value analysis
ID0000772:
**This issue was created automatically from Mantis Issue 772. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000772:
**This issue was created automatically from Mantis Issue 772. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000772 | Frama-C | Plug-in > Eva | public | 2011-03-30 | 2016-08-02 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | virgile | **Assigned To** | yakobowski | **Resolution** | won't fix |
| **Priority** | low | **Severity** | tweak | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | - |
### Description :
On the code below, frama-c -val -main f t.c will report an out of bound read on line 2. It should be line 3.
------------- t.c
void f (int* x) {
int a = 3 +
*x;
}
-----------------
https://git.frama-c.com/pub/frama-c/-/issues/2325
error in analyzing xen 4.0.0 code
2021-02-22T13:56:34Z
mantis-gitlab-migration
error in analyzing xen 4.0.0 code
ID0000516:
**This issue was created automatically from Mantis Issue 516. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000516:
**This issue was created automatically from Mantis Issue 516. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000516 | Frama-C | Plug-in > Eva | public | 2010-06-19 | 2010-12-10 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | amkhalid | **Assigned To** | pascal | **Resolution** | unable to reproduce |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
[kernel] Parsing stage early
[kernel] Parsing stage extending
[kernel] Parsing stage extended
[kernel] Parsing stage exiting
[kernel] Parsing stage loading
[kernel] Parsing stage configuring
[kernel] preprocessing with "gcc -C -E -I. -I/home/ak729/xen-4.0.0/xen/include/ /home/ak729/xen-4.0.0/xen/common/kernel.c"
/home/ak729/xen-4.0.0/xen/include/public/domctl.h:51:[kernel] user error: syntax error
[kernel] The full backtrace is:
[kernel] Raised at file "cil/src/frontc/frontc.ml", line 209, characters 9-28
[kernel] Called from file "cil/src/frontc/frontc.ml", line 124, characters 13-38
[kernel] Called from file "cil/src/frontc/frontc.ml", line 263, characters 13-32
[kernel] Called from file "src/kernel/file.ml", line 546, characters 27-46
[kernel] Called from file "src/kernel/file.ml", line 582, characters 16-23
[kernel] Re-raised at file "src/kernel/file.ml", line 585, characters 52-55
[kernel] Called from file "list.ml", line 74, characters 24-34
[kernel] Called from file "src/kernel/file.ml", line 579, characters 6-314
[kernel] Called from file "src/kernel/file.ml", line 1027, characters 12-30
[kernel] Called from file "src/kernel/file.ml", line 1108, characters 4-27
[kernel] Called from file "src/kernel/ast.ml", line 57, characters 29-45
[kernel] Called from file "src/project/computation.ml", line 108, characters 17-21
[kernel] Called from file "src/kernel/file.ml", line 1147, characters 12-22
[kernel] Called from file "src/project/project.ml", line 432, characters 12-15
[kernel] Re-raised at file "src/project/project.ml", line 437, characters 10-11
[kernel] Called from file "src/kernel/boot.ml", line 44, characters 33-47
[kernel] Called from file "src/kernel/cmdline.ml", line 170, characters 4-8
[kernel]
[kernel] Unexpected error (Parsing.Parse_error).
[kernel] Please report as 'crash' at http://bts.frama-c.com
https://git.frama-c.com/pub/frama-c/-/issues/543
Widen hints for a variable should not influence the values for other variables
2021-02-22T13:55:57Z
Boris Yakobowski
Widen hints for a variable should not influence the values for other variables
ID0000876:
**This issue was created automatically from Mantis Issue 876. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000876:
**This issue was created automatically from Mantis Issue 876. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000876 | Frama-C | Plug-in > Eva | public | 2011-07-04 | 2016-01-26 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | yakobowski | **Assigned To** | yakobowski | **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 Magnesium |
### Description :
With the widen hint below, Value finds the range i ? [30..127] for i. Without the hint, the completely precise value {30} is found. The hint for 'next' should not degrade the results for 'i'.
int max = 25;
int next = 0;
void main () {
/*@ loop pragma WIDEN_HINTS next, 24; */
for (int i=0;i<30;i++) {
int vsize = max;
int vnext = next;
if(vsize > vnext)
next++;
}
}
https://git.frama-c.com/pub/frama-c/-/issues/2235
star_star dump issue
2021-02-22T13:54:32Z
mantis-gitlab-migration
star_star dump issue
ID0000746:
**This issue was created automatically from Mantis Issue 746. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000746:
**This issue was created automatically from Mantis Issue 746. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000746 | Frama-C | Plug-in > Eva | public | 2011-03-05 | 2011-03-07 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | haihao | **Assigned To** | pascal | **Resolution** | no change required |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Boron-20100401 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Hi,
Recently I used Frama-C to analyze the input/output information for each C function. However, I found for some functions, there are many inputs (more than 200, but most of them are similar).
Here is one sample input, and hope that you could help me figure out why these are generated by Frama-C.
##star_star_star_xx_pointer_0nth__inner_pointer_0nth__field[bits 0 to 549755813887]## xx_pointer is one of pointers used in a function, inner_pointer is a field of structure, pointed by xx_pointer, while field is a field of structure, pointed by inner_pointer.
Since there are many similar inputs, I am wondering whether they are really inputs for a function.
Any comments are welcome!
Thanks,
Haihao
### Additional Information :
I used a simple file to reproduce similar issue. Please tell me how to understand the star_star dump infomation. Thanks.
## Attachments
- [frama.c](/uploads/bc1a19580ec11baf490aed779ca30833/frama.c)
https://git.frama-c.com/pub/frama-c/-/issues/2226
How to break down the fields in strcuture (nested structures)
2021-02-22T13:54:14Z
mantis-gitlab-migration
How to break down the fields in strcuture (nested structures)
ID0000760:
**This issue was created automatically from Mantis Issue 760. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000760:
**This issue was created automatically from Mantis Issue 760. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000760 | Frama-C | Plug-in > Eva | public | 2011-03-22 | 2011-03-22 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | haihao | **Assigned To** | pascal | **Resolution** | no change required |
| **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 Carbon-20110201 |
### Description :
Hi,
Frama-C value analysis could provide the detailed input and output. I am wondering whether users could use Frama-C to get the break-down fields of a structure if there is a nested structure.
Thanks, Haihao
### Additional Information :
Hi Pascal, I am sorry that I could find a suitable discussion place to let me ask the question, so I post the question here.
Sorry for the inconvenience.
Haihao
https://git.frama-c.com/pub/frama-c/-/issues/2223
Base.create_varinfo has no with_alarms arguments
2021-02-22T13:54:11Z
Benjamin Monate
Base.create_varinfo has no with_alarms arguments
ID0000773:
**This issue was created automatically from Mantis Issue 773. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000773:
**This issue was created automatically from Mantis Issue 773. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000773 | Frama-C | Plug-in > Eva | public | 2011-03-30 | 2011-03-30 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | monate | **Assigned To** | pascal | **Resolution** | no change required |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Thus Kernel.warning ~current:true ~once:true
"Periodic variable %s of period %d@."
name
will be emitted even if it is called by a function in eval.ml which is supposed to honor its with_alarms argument.
https://git.frama-c.com/pub/frama-c/-/issues/2192
assert-clause recommended by tool doesn't make warning vanish
2021-02-22T13:53:20Z
Jochen Burghardt
assert-clause recommended by tool doesn't make warning vanish
ID0000863:
**This issue was created automatically from Mantis Issue 863. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000863:
**This issue was created automatically from Mantis Issue 863. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000863 | Frama-C | Plug-in > Eva | public | 2011-06-10 | 2011-06-10 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | pascal | **Resolution** | no change required |
| **Priority** | normal | **Severity** | text | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20110201 | **Target Version** | - | **Fixed in Version** | - |
### Description :
When running "frama-c -val ftest.c" on the attached program, I get the messages:
ftest.c:4:[value] Assertion got status unknown.
ftest.c:5:[kernel] warning: out of bounds read. assert \valid(argv+0);
However, the assertion recommended in the above warning is already in the code (in line 4); so I'd expect the warning to have vanished.
## Attachments
- [ftest.c](/uploads/fab2960212e81ebd8c8d79b441cd5ac2/ftest.c)
https://git.frama-c.com/pub/frama-c/-/issues/2189
Option -val-signed-overflow-alarms misses some overflow
2021-02-22T13:53:16Z
Boris Yakobowski
Option -val-signed-overflow-alarms misses some overflow
ID0000893:
**This issue was created automatically from Mantis Issue 893. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000893:
**This issue was created automatically from Mantis Issue 893. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000893 | Frama-C | Plug-in > Eva | public | 2011-07-26 | 2011-07-26 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | yakobowski | **Assigned To** | pascal | **Resolution** | no change required |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20110201 | **Target Version** | - | **Fixed in Version** | - |
### Description :
The value analysis does not emit an alarm on c++, even with option -val-signed-overflow-alarms. This is because c+1 is done on an int, which is cast back into unsigned char afterwards.
void main () {
signed char c=0;
while(1) c++;
}
https://git.frama-c.com/pub/frama-c/-/issues/2184
Bogus uninitialized value messages for trivial safe program
2021-02-22T13:53:09Z
mantis-gitlab-migration
Bogus uninitialized value messages for trivial safe program
ID0000920:
**This issue was created automatically from Mantis Issue 920. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000920:
**This issue was created automatically from Mantis Issue 920. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000920 | Frama-C | Plug-in > Eva | public | 2011-08-11 | 2011-08-11 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jrrk100 | **Assigned To** | pascal | **Resolution** | no change required |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20110201 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Using the following command line:
frama-c -cpp-extra-args="-I`frama-c -print-share-path`/libc -nostdinc" `frama-c -print-share-path`/libc/fc_runtime.c -unspecified-access -val junk.c
Bogus uninitialized value messages were produced for a trivial safe program.
The attached program was extracted from a larger whole to demonstrate the issue.
### Additional Information :
junk.c:18:[value] entering loop for the first time
junk.c:19:[value] assigning non deterministic value for the first time
junk.c:19:[kernel] warning: out of bounds write. assert \valid(ptr);
junk.c:22:[value] Function print: precondition got status valid
junk.c:10:[value] entering loop for the first time
junk.c:10:[kernel] warning: accessing uninitialized left-value *ptr: assert(Ook)
junk.c:11:[kernel] warning: accessing uninitialized left-value *tmp: assert(Ook)
junk.c:10:[kernel] warning: out of bounds read. assert \valid(ptr);
junk.c:11:[kernel] warning: out of bounds read. assert \valid(tmp);
## Attachments
- [junk.c](/uploads/600421e2ff0cf80bf55ec15e23d2c405/junk.c)
https://git.frama-c.com/pub/frama-c/-/issues/2180
strange value-set for loop-variable in presence of flexible array
2021-02-22T13:53:05Z
Jochen Burghardt
strange value-set for loop-variable in presence of flexible array
ID0000924:
**This issue was created automatically from Mantis Issue 924. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000924:
**This issue was created automatically from Mantis Issue 924. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000924 | Frama-C | Plug-in > Eva | public | 2011-08-12 | 2011-08-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | pascal | **Resolution** | no change required |
| **Priority** | normal | **Severity** | text | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20110201 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Analyzing the attached program with "frama-c -val ftest.c -main f -no-unicode -slevel 1000" reports "i IN {0; 1; 2; }", which seems a too small set.
When "n" is replaced by e.g. "9" in line 1 (col.19 only) and 4, the computed set "i IN {9; }" seems ok.
When instead "a[i]" is replaced by "i" in line 5, the computed set "i IN [0..2147483647]" seems ok, too. (Only in this case, messages like "[value] Semantic level unrolling superposing up to ..." are printed - is this ok?)
If arrays with non-constants upper-bound expressions are not supported, a corresponding warning should be emitted for line 1.
## Attachments
- [ftest.c](/uploads/0c15bbc66390644d25e8124e8714f21a/ftest.c)
https://git.frama-c.com/pub/frama-c/-/issues/2164
Incorrect results with low slevel
2021-02-22T13:52:35Z
Boris Yakobowski
Incorrect results with low slevel
ID0000844:
**This issue was created automatically from Mantis Issue 844. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000844:
**This issue was created automatically from Mantis Issue 844. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000844 | Frama-C | Plug-in > Eva | public | 2011-05-28 | 2011-10-10 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **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 :
The following program is correct and always terminates. However, with no slevel, the value analysis incorrectly states that main and memset do not terminate.
(Analyzed with -value -slevel 0)
void* memset (void* dest, int val, unsigned int len) {
unsigned char *ptr = (unsigned char*)dest;
while (len-- > 0) {
*ptr++ = val;
}
return dest;
}
extern int k;
void main () {
int v;
int x = k ? 2 : 3;
memset(&v,42,x);
}
https://git.frama-c.com/pub/frama-c/-/issues/2158
Value analysis crashes in lib-entry mode with peculiar context
2021-02-22T13:52:25Z
David Delmas
Value analysis crashes in lib-entry mode with peculiar context
ID0000820:
**This issue was created automatically from Mantis Issue 820. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000820:
**This issue was created automatically from Mantis Issue 820. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000820 | Frama-C | Plug-in > Eva | public | 2011-05-11 | 2011-10-10 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | ddelmas | **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 :
A crash occurs with command :
frama-c -val -lib-entry -main F -context-width 1 -context-depth 0 crash_align.c
### Additional Information :
The analysis does not crash with -context-depth 1.
## Attachments
- [crash_align.c](/uploads/27c1eb98ff6f0ccd59f2698b84ba9167/crash_align.c)
https://git.frama-c.com/pub/frama-c/-/issues/2137
Use of Cabs2cil.fresh_global
2021-02-22T13:51:59Z
Boris Yakobowski
Use of Cabs2cil.fresh_global
ID0000680:
**This issue was created automatically from Mantis Issue 680. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000680:
**This issue was created automatically from Mantis Issue 680. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000680 | Frama-C | Plug-in > Eva | public | 2011-01-20 | 2011-10-10 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | yakobowski | **Assigned To** | pascal | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20101202-beta2 | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
A few functions in the value analysis (Eval.initialize_var_using_type, Eval.return_value, Eval.compute_call), as well as Builtins.frama_c_alloc_infinite call the function Cabs2cil.fresh_global. Since it is a global hashtable that is never reset, successive executions of the value analysis will yield different results over time. This causes convergence problems for, eg. fixpoint-based plugins.
https://git.frama-c.com/pub/frama-c/-/issues/2122
Valid access to literal w_chart string address considered invalid
2021-02-22T13:51:34Z
Benjamin Monate
Valid access to literal w_chart string address considered invalid
ID0000949:
**This issue was created automatically from Mantis Issue 949. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000949:
**This issue was created automatically from Mantis Issue 949. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000949 | Frama-C | Plug-in > Eva | public | 2011-09-02 | 2011-10-10 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | monate | **Assigned To** | pascal | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | Frama-C GIT, precise the release id | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
#include <stddef.h>
int main() {
// String literals are lvalues
char (*p)[4] = &("bar");
wchar_t (*q)[4] = &(L"foO");
if((*p)[1] != 'a') return 1;
if((*q)[1] != 'o') return 2;
return 0;
}
return 0 when gcc'ed but frama-c -val ends with
tests/cil/string.c:10:[kernel] warning: out of bounds read. assert \valid(&(*q)[1]);
https://git.frama-c.com/pub/frama-c/-/issues/2106
if (p < valid_address) seems to take the else branch although p == NULL
2021-02-22T13:51:07Z
Pascal Cuoq
if (p < valid_address) seems to take the else branch although p == NULL
ID0000753:
**This issue was created automatically from Mantis Issue 753. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000753:
**This issue was created automatically from Mantis Issue 753. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000753 | Frama-C | Plug-in > Eva | public | 2011-03-11 | 2011-10-10 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **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** | - |
### Description :
Obtained result:
The else branch appears feasible.
Expected result:
[value] Values for function main:
NON TERMINATING FUNCTION
## Attachments
- [test.c](/uploads/09bea72dde5791648719bac4b6ca87ff/test.c)
https://git.frama-c.com/pub/frama-c/-/issues/2102
Wrong result when subtle promotions involved in x86_32 (csmith)
2021-02-22T13:51:02Z
Pascal Cuoq
Wrong result when subtle promotions involved in x86_32 (csmith)
ID0000994:
**This issue was created automatically from Mantis Issue 994. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000994:
**This issue was created automatically from Mantis Issue 994. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000994 | Frama-C | Plug-in > Eva | public | 2011-10-21 | 2011-10-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | pascal | **Resolution** | no change required |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Nitrogen-20111001 | **Target Version** | - | **Fixed in Version** | - |
### Description :
main(){
int i = ( ((short int) (-27963)) ^ 2UL ) <= 0xE945F009BC071553LL;
return i;
}
~/ppc/bin/toplevel.opt -print r.c -val -machdep x86_64 -print
...
i ? {0}
(correct)
~/ppc/bin/toplevel.opt -print r.c -val -machdep x86_32 -print
...
i ? {1}
(incorrect)
https://git.frama-c.com/pub/frama-c/-/issues/2032
Feedback about value analysis degeneration
2021-02-22T13:49:21Z
mantis-gitlab-migration
Feedback about value analysis degeneration
ID0001221:
**This issue was created automatically from Mantis Issue 1221. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001221:
**This issue was created automatically from Mantis Issue 1221. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001221 | Frama-C | Plug-in > Eva | public | 2012-06-26 | 2012-07-03 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Anne | **Assigned To** | pascal | **Resolution** | no change required |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Nitrogen-20111001 | **Target Version** | - | **Fixed in Version** | - |
### Description :
It would be great to have more information about the reasons why the value analysis degenerates in some cases. For instance :
$ frama-c -val toto.c
with :
int main (int argc, char * argv []) {
char * s1 = argv[1];
char * s2 = argv[2];
return 0;
}
gives :
toto.c:2:[kernel] warning: out of bounds read. assert \valid(argv+1);
toto.c:3:[kernel] warning: out of bounds read. assert \valid(argv+2);
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
[value] Values for function main:
NON TERMINATING FUNCTION
I know now that I have to use -context-width, but it is not easy to guess from the value analysis output, especially if we don't know if the function doesn't terminate for other reasons... Would it be possible to give the first statement where the state is BOTTOM for instance : this would be a hint.
https://git.frama-c.com/pub/frama-c/-/issues/1992
Imprecise result on almost deterministic program
2021-02-22T13:48:08Z
Boris Yakobowski
Imprecise result on almost deterministic program
ID0001074:
**This issue was created automatically from Mantis Issue 1074. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001074:
**This issue was created automatically from Mantis Issue 1074. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001074 | Frama-C | Plug-in > Eva | public | 2012-01-28 | 2012-09-19 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | yakobowski | **Assigned To** | pascal | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Nitrogen-20111001 | **Target Version** | - | **Fixed in Version** | Frama-C Oxygen-20120901 |
### Description :
----- memsetff.c --------
int t[10];
void main (char c) {
for (int i=0;i<sizeof(t);i++)
((char*)t)[i]=0xFF;
Frama_C_show_each(t[1]);
if(c)
t[1] = 1;
}
------------------------
To be tested with
frama-c -val memsetff.c -precise-unions -big-ints-hex 0x10 -slevel 100000
(-precise-unions has not effect in this case)
The obtained possible values for t[1] are [1] ? [--..--], which is over-approximated.