frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2021-02-22T13:48:05Zhttps://git.frama-c.com/pub/frama-c/-/issues/1991"volatile" ignored2021-02-22T13:48:05ZJochen Burghardt"volatile" ignoredID0001076:
**This issue was created automatically from Mantis Issue 1076. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001076:
**This issue was created automatically from Mantis Issue 1076. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001076 | Frama-C | Plug-in > Eva | public | 2012-01-30 | 2012-09-19 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | pascal | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Nitrogen-20111001 | **Target Version** | - | **Fixed in Version** | Frama-C Oxygen-20120901 |
### Description :
Running "frama-c -val exm22.c" on the attached program produces the output "a in {0}". Running the same command after deleting the initialization of "a" in line 2 reports a run-time error (uninitialized variable access) in line 3. Both would be ok if "a" wasn't declared "volatile".
In contrast to the 1st analysis result, the value-analysis manual says on p.43: "the analyzer does not assume that the value read from a volatile variable is identical to the last value written there."
## Attachments
- [exm22.c](/uploads/5b074d5dffdf6094f94afe4ac0b33a0d/exm22.c)https://git.frama-c.com/pub/frama-c/-/issues/1980Warnings in presence of Top floats2021-02-22T13:47:47ZBoris YakobowskiWarnings in presence of Top floatsID0000997:
**This issue was created automatically from Mantis Issue 997. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000997:
**This issue was created automatically from Mantis Issue 997. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000997 | Frama-C | Plug-in > Eva | public | 2011-10-23 | 2012-09-19 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | yakobowski | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Nitrogen-20111001 | **Target Version** | - | **Fixed in Version** | Frama-C Oxygen-20120901 |
### Description :
Consider the following program analyzed with
frama-c -val -absolute-valid-range 0-100
const short max = 255;
const short min = 0;
extern float u[256];
float main () {
short r;
float f = *((float *)18);
// assert -3.40282346639e+38 <= f <= 3.40282346639e+38;
int j = 2; // To be able to see the value of f in the gui
if(f >= max) r = max;
else if (f <= min) r = min;
else r = f + 0.5;
return u[r];
}
The results are not optimal, as the access to u[r] is not proven correct. The reason is as follows: with a "normal" float, the reductions within the 'if' take place normally, and r belongs to [0..255]. However, here we have a Topint inside a float, and the reduction does not happen.
If we activate the assertion to help the user, the result is worse: the assertion is incorrectly proven correct, as the conversion to a finite float happens before the truth value of the assertion is computed. Moreover, since the assertion is "correct", no reduction by the assertion occurs, and the access to u[r] is still not correct.https://git.frama-c.com/pub/frama-c/-/issues/1979Invalid handling of shift of pointer address2021-02-22T13:47:44ZBoris YakobowskiInvalid handling of shift of pointer addressID0001001:
**This issue was created automatically from Mantis Issue 1001. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001001:
**This issue was created automatically from Mantis Issue 1001. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001001 | Frama-C | Plug-in > Eva | public | 2011-10-27 | 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 :
The behavior of the value analysis is incorrect on the following example, which is valid according to the norm.
char t[10];
int main () {
int r = (unsigned long)t << 8;
return r;
}https://git.frama-c.com/pub/frama-c/-/issues/1944Strings in value analysis results2021-02-22T13:46:57Zmantis-gitlab-migrationStrings in value analysis resultsID0001191:
**This issue was created automatically from Mantis Issue 1191. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001191:
**This issue was created automatically from Mantis Issue 1191. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001191 | Frama-C | Plug-in > Eva | public | 2012-06-08 | 2012-11-18 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Anne | **Assigned To** | pascal | **Resolution** | won't fix |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Nitrogen-20111001 | **Target Version** | - | **Fixed in Version** | - |
### Description :
String constant are nicely printed in value analysis results, but other strings are not (see additional information). Wouldn't it be possible (I mean: not too much work) to also print nicely the known variable strings ?
### Additional Information :
For the file :
int main (void) {
char toto[] = "bonjour";
char * titi = "coucou";
char * ptoto = toto;
char * ptiti = titi;
return 0;
}
$ frama-c -val toto.c
[value] Values for function main:
toto[0] ? {98}
[1] ? {111}
[2] ? {110}
[3] ? {106}
[4] ? {111}
[5] ? {117}
[6] ? {114}
[7] ? {0}
titi ? {{ &"coucou" }}
ptoto ? {{ &toto }}
ptiti ? {{ &"coucou" }}
It would be nice to have toto ? {"bonjour"} when there is only one possible value. (I understand that if some of the character can have several values, you cannot enumerate all the possible strings...)https://git.frama-c.com/pub/frama-c/-/issues/1914Alignment of global character arrays2021-02-22T13:45:59ZDavid DelmasAlignment of global character arraysID0000873:
**This issue was created automatically from Mantis Issue 873. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000873:
**This issue was created automatically from Mantis Issue 873. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000873 | Frama-C | Plug-in > Eva | public | 2011-06-28 | 2013-02-22 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **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** | - |
### Description :
With the attached source file,
$ frama-c tab_char.c -val
produces the (correct) output :
[value] Called Frama_C_show_each_Alignment(
{{ &"WARNING: address possibly non word aligned" ;}},
{{ &t ;}})
However, adding options -machdep ppc_32_diab does not change this output, although character arrays have a default alignment of 4 with the Diab C cross-compiler for PowerPC.
It would be useful to have -machdep ppc_32_diab take this specific feature into account.
## Attachments
- [tab_char.c](/uploads/1b6648205d05612a39c5e0f2dfdcbe24/tab_char.c)https://git.frama-c.com/pub/frama-c/-/issues/1891Crash with Invalid argument for Frama_C_alloc_size function2021-02-22T13:45:09Zmantis-gitlab-migrationCrash with Invalid argument for Frama_C_alloc_size functionID0001302:
**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/1884Locations.valid_enumerate_bits enumerate invalid bits2021-02-22T13:44:59ZBoris YakobowskiLocations.valid_enumerate_bits enumerate invalid bitsID0001264:
**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_inthttps://git.frama-c.com/pub/frama-c/-/issues/1864warning for unreachable program point2021-02-22T13:44:30Zmantis-gitlab-migrationwarning for unreachable program pointID0001425:
**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 shift2021-02-22T13:44:29Zmantis-gitlab-migration"Loss of precision" message after shiftID0001423:
**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/1861Different signed_overflow assert with rte + val2021-02-22T13:44:26Zmantis-gitlab-migrationDifferent signed_overflow assert with rte + valID0001424:
**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/1389suggest to use "NULL" rather than "&NULL" for null pointer2021-02-22T13:44:22ZJochen Burghardtsuggest to use "NULL" rather than "&NULL" for null pointerID0001066:
**This issue was created automatically from Mantis Issue 1066. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001066:
**This issue was created automatically from Mantis Issue 1066. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001066 | Frama-C | Plug-in > Eva | public | 2012-01-19 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | pascal | **Resolution** | fixed |
| **Priority** | normal | **Severity** | trivial | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Nitrogen-20111001 | **Target Version** | - | **Fixed in Version** | Frama-C Oxygen-20120901 |
### Description :
Running "frama-c -val exm4.c -no-unicode" on the attached program produces an output "p IN {{ &NULL ; &n }}", which is unusual and confusing for a C-programmer. I'd prefer to get "p IN {{ NULL ; &n }}" instead, which also resembles the C code in line 4 of the program.
From p.26 of file "value-analysis-Nitrogen-20111001.pdf", I understand that (void*)0, which I consider an absolute address, handled in the 2nd item under "A set of addresses", should be denoted as "NULL+0". The notation "&NULL", on the other hand, could be subsumed only under the 1st item on p.26, which seems to indicate that "NULL" denotes some variable. So I consider the output on exm4.c to be inconsistent with the explanations on p.26. The same applies to the use of "&NULL" on p.51 and later in the manual.
## Attachments
- [exm4.c](/uploads/b1ce66eefcc2c74cab2007322c4be3f0/exm4.c)https://git.frama-c.com/pub/frama-c/-/issues/1848Some Value assert are not in the log file2021-02-22T13:44:08Zmantis-gitlab-migrationSome Value assert are not in the log fileID0001426:
**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/1835unexpected stack overflow in value analysis2021-02-22T13:43:42ZJochen Burghardtunexpected stack overflow in value analysisID0001374:
**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/1824speed of value analysis while use the "-lib-entry" and "main" and "-val-use-s...2021-02-22T13:43:23Zmantis-gitlab-migrationspeed of value analysis while use the "-lib-entry" and "main" and "-val-use-spec" option for value analysisID0001593:
**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/1823value analysis crashed after I the ast was modified in a new project2021-02-22T13:43:22Zmantis-gitlab-migrationvalue analysis crashed after I the ast was modified in a new projectID0001585:
**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/1815Incompatibility between -inout-callwise and failing built-ins.2021-02-22T13:43:12ZPascal CuoqIncompatibility 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_guidelineshttps://git.frama-c.com/pub/frama-c/-/issues/1810strange warning "extracting bits of a pointer"2021-02-22T13:42:58ZJochen Burghardtstrange 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/1320File "src/memory_state/lmap.ml", line 931, characters 22-28: Assertion failed2021-02-22T13:42:52ZBenjamin MonateFile "src/memory_state/lmap.ml", line 931, characters 22-28: Assertion failedID0000889:
**This issue was created automatically from Mantis Issue 889. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000889:
**This issue was created automatically from Mantis Issue 889. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000889 | Frama-C | Plug-in > Eva | public | 2011-07-25 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | monate | **Assigned To** | pascal | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
frama-c /usr/local/share/frama-c/libc/fc_runtime.c main.i protocol.i util.i -val -quiet
crashes the value analysis.
## Attachments
- [main.i](/uploads/f310746c6649373aefea3edc9602f483/main.i)
- [util.i](/uploads/15ac5f03bcc13cfed5c759fbc47a64fc/util.i)
- [protocol.i](/uploads/9753b8a9322f329b2774dc0429fc793b/protocol.i)https://git.frama-c.com/pub/frama-c/-/issues/1794interest for a built-in memset function2021-02-22T13:42:12ZDavid Delmasinterest for a built-in memset functionID0000915:
**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/1781Evaluation in the logic can cause crashes2021-02-22T13:41:34ZBoris YakobowskiEvaluation in the logic can cause crashesID0001000:
**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.