frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2022-09-28T14:07:01Zhttps://git.frama-c.com/pub/frama-c/-/issues/609Control dependencies between labelled instructuctions and the corresponding ...2022-09-28T14:07:01Zmantis-gitlab-migrationControl dependencies between labelled instructuctions and the corresponding goto statementID0001992:
**This issue was created automatically from Mantis Issue 1992. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001992:
**This issue was created automatically from Mantis Issue 1992. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001992 | Frama-C | Plug-in > pdg | public | 2014-11-25 | 2015-08-03 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | nguenaomer | **Assigned To** | maroneze | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | X68 | **OS** | Linux | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130601 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Issue1: Does the pdg of frama-c include the transitive closure of standard control and data dependency relation?
Issue2: I think that there is an error in the PDG (or only the dot version).
The PDG of the function below states that the "while_0_break" statement control the "goto while_0_break" when using the -simplify-cfg option. To me, it should be the converse. The same with Neon.
Note that Issue1 and Issue2 are related.
### Steps To Reproduce :
I executed the following commamds with the C code below
$frama-c -pdg example2.c -main transfer_func -pdg-dot pdg2 -simplify-cfg
$dot -Tpng -o pdg2.transfer_func.png pdg2.transfer_func.dot
int x1,x2 ;
void transfer_func(int time) {
int prod =1 ;
int k =1 ;
while (k<=10) {
if (time/k > prod) break ;
prod *= k;
k++ ;
}
x1++;
x2++;
}
Enclosed is the pdg.
## Attachments
- ![pdg2.transfer_func](/uploads/89e7e73de0bccff6146ec1bca3678b43/pdg2.transfer_func.png)Andre MaronezeAndre Maronezehttps://git.frama-c.com/pub/frama-c/-/issues/523FRama C Nitrogen Nitrogen-20111001 crash during pdg construction2021-02-22T14:01:40Zmantis-gitlab-migrationFRama C Nitrogen Nitrogen-20111001 crash during pdg constructionID0002211:
**This issue was created automatically from Mantis Issue 2211. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002211:
**This issue was created automatically from Mantis Issue 2211. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002211 | Frama-C | Plug-in > pdg | public | 2016-02-22 | 2016-02-22 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | lammyday | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | Linux | **OS Version** | Ubunutu 14.04 |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | - |
### Description :
Crash during pdg construction, due to unexpected error - (File "external/hptmap.ml)
### Additional Information :
Error Message:
[value] computing for function error <- readline <- do_define <- eval <-
eval_makefile.
Called from read.c:2391.
[value] Done for function error
[kernel] The full backtrace is:
Called from file "src/lib/binary_cache.ml", line 366, characters 14-21
Called from file "external/hptmap.ml", line 1107, characters 18-41
Called from file "src/memory_state/lmap.ml", line 818, characters 10-35
Called from file "src/value/current_table.ml", line 75, characters 9-57
Called from file "src/value/eval_stmts.ml", line 1136, characters 6-69
Called from file "cil/src/ext/dataflow.ml", line 305, characters 12-27
Called from file "cil/src/ext/dataflow.ml", line 497, characters 8-21
Called from file "cil/src/ext/dataflow.ml", line 501, characters 9-22
Called from file "src/value/eval_funs.ml", line 117, characters 14-37
Called from file "src/value/eval_funs.ml", line 478, characters 10-65
Called from file "src/value/eval_stmts.ml", line 866, characters 14-73
Called from file "src/value/eval_stmts.ml", line 885, characters 10-114
Called from file "src/value/eval_stmts.ml", line 918, characters 38-62
Called from file "list.ml", line 74, characters 24-34
Called from file "src/value/eval_stmts.ml", line 974, characters 26-79
Called from file "cil/src/ext/dataflow.ml", line 320, characters 29-47
Called from file "cil/src/ext/dataflow.ml", line 497, characters 8-21
Called from file "cil/src/ext/dataflow.ml", line 501, characters 9-22
Called from file "src/value/eval_funs.ml", line 117, characters 14-37
Called from file "src/value/eval_funs.ml", line 478, characters 10-65
Called from file "src/value/eval_stmts.ml", line 866, characters 14-73
Called from file "src/value/eval_stmts.ml", line 885, characters 10-114
Called from file "src/value/eval_stmts.ml", line 918, characters 38-62
Called from file "list.ml", line 74, characters 24-34
Called from file "src/value/eval_stmts.ml", line 974, characters 26-79
Called from file "cil/src/ext/dataflow.ml", line 320, characters 29-47
Called from file "cil/src/ext/dataflow.ml", line 497, characters 8-21
Called from file "cil/src/ext/dataflow.ml", line 501, characters 9-22
Called from file "src/value/eval_funs.ml", line 117, characters 14-37
Called from file "src/value/eval_funs.ml", line 478, characters 10-65
Called from file "src/value/eval_stmts.ml", line 866, characters 14-73
Called from file "src/value/eval_stmts.ml", line 885, characters 10-114
Called from file "src/value/eval_stmts.ml", line 918, characters 38-62
Called from file "list.ml", line 74, characters 24-34
Called from file "src/value/eval_stmts.ml", line 974, characters 26-79
Called from file "cil/src/ext/dataflow.ml", line 320, characters 29-47
Called from file "cil/src/ext/dataflow.ml", line 497, characters 8-21
Called from file "cil/src/ext/dataflow.ml", line 501, characters 9-22
Called from file "src/value/eval_funs.ml", line 117, characters 14-37
Called from file "src/value/eval_funs.ml", line 452, characters 6-69
Called from file "src/value/eval_funs.ml", line 556, characters 11-44
Re-raised at file "src/value/eval_funs.ml", line 572, characters 47-50
Called from file "src/project/state_builder.ml", line 1076, characters 9-13
Re-raised at file "src/project/state_builder.ml", line 1080, characters 15-18
Called from file "src/semantic_callgraph/register.ml", line 84, characters 7-24
Called from file "src/project/state_builder.ml", line 490, characters 17-21
Called from file "src/semantic_callgraph/register.ml", line 196, characters 51-65
Called from file "src/pdg/register.ml", line 145, characters 4-68
Called from file "queue.ml", line 134, characters 6-20
Called from file "src/kernel/boot.ml", line 36, characters 4-20
Called from file "src/kernel/cmdline.ml", line 723, characters 2-9
Called from file "src/kernel/cmdline.ml", line 200, characters 4-8
Unexpected error (File "external/hptmap.ml", line 1105, characters 14-20: Assertion failed).
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Nitrogen-20111001.
Note that a version and a backtrace alone often does not have 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
### Steps To Reproduce :
execute:
frama-c -pdg -dot-pdg graph -pdg-print read.i -main eval_makefile -val-ignore-recursive-calls
on gnu make utility repository:
5acda13ace0ae4443ed04c4f8a62512b00a2b656
obtainable at urs:
http://git.savannah.gnu.org/cgit/make.git/snapshot/make-5acda13ace0ae4443ed04c4f8a62512b00a2b656.tar.gzhttps://git.frama-c.com/pub/frama-c/-/issues/520FRama C Nitrogen Nitrogen-201110012021-02-22T14:01:40Zmantis-gitlab-migrationFRama C Nitrogen Nitrogen-20111001ID0002210:
**This issue was created automatically from Mantis Issue 2210. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002210:
**This issue was created automatically from Mantis Issue 2210. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002210 | Frama-C | Plug-in > pdg | public | 2016-02-22 | 2016-02-25 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | lammyday | **Assigned To** | yakobowski | **Resolution** | unable to reproduce |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | sometimes |
| **Platform** | - | **OS** | Linux | **OS Version** | Ubuntu 14.04 |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | - |
### Description :
Frama-c pdg crashed of an unexpected error(out of memeory) after a warning that it could not find a final state, or a final state was unreachable.
### Additional Information :
Error meesages from crash:
main.c:2313:[pdg] warning: no final state. Probably unreachable...
[pdg] done for function main
[kernel] The full backtrace is:
Raised by primitive operation at file "src/kernel/log.ml", line 197, characters 16-31
Called from file "format.ml", line 299, characters 4-28
Called from file "format.ml", line 428, characters 6-72
Called from file "format.ml", line 435, characters 6-24
Called from file "format.ml", line 1148, characters 10-28
Called from file "external/hptmap.ml", line 201, characters 3-15
Called from file "external/hptmap.ml", line 201, characters 3-15
Called from file "external/hptmap.ml", line 201, characters 3-15
Called from file "external/hptmap.ml", line 201, characters 3-15
Called from file "list.ml", line 69, characters 12-15
Called from file "src/pdg_types/pdgTypes.ml", line 584, characters 6-33
Called from file "format.ml", line 1157, characters 10-25
Called from file "format.ml", line 1157, characters 10-25
Called from file "src/pdg/register.ml", line 140, characters 8-63
Called from file "queue.ml", line 134, characters 6-20
Called from file "src/pdg/register.ml", line 145, characters 4-68
Called from file "queue.ml", line 134, characters 6-20
Called from file "src/kernel/boot.ml", line 36, characters 4-20
Called from file "src/kernel/cmdline.ml", line 723, characters 2-9
Called from file "src/kernel/cmdline.ml", line 200, characters 4-8
Unexpected error (Out of memory).
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Nitrogen-20111001.
Note that a version and a backtrace alone often does not have 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
### Steps To Reproduce :
execute:
"frama-c -pdg -dot-pdg graph -pdg-print main.i -main main -val-ignore-recursive-calls"
on the make gnu utility with git version: 036760a9fdb11849b6a43feec7ce294e7f77db2a
this is obtainable from this url:
http://git.savannah.gnu.org/cgit/make.git/snapshot/make-036760a9fdb11849b6a43feec7ce294e7f77db2a.tar.gzhttps://git.frama-c.com/pub/frama-c/-/issues/1206Stack overflow when computing a PDG2021-02-22T13:23:23ZJulien SignolesStack overflow when computing a PDGID0001436:
**This issue was created automatically from Mantis Issue 1436. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001436:
**This issue was created automatically from Mantis Issue 1436. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001436 | Frama-C | Plug-in > pdg | public | 2013-05-30 | 2014-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | signoles | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | urgent | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130501 | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
==== test.c ====
void __VERIFIER_assert(int cond) {
if (!(cond)) {
ERROR: goto ERROR;
}
return;
}
#define a (2)
int main(unsigned int loop1, unsigned int m1) {
int sn=0;
unsigned int x=0;
while(1){
sn = sn + a;
x++;
__VERIFIER_assert(sn==x*a || sn == 0);
}
}
==========
$ frama-c -pdg test.c
<skip value's trace>
[pdg] computing for function __VERIFIER_assert
[pdg] done for function __VERIFIER_assert
[pdg] computing for function main
[kernel] Current source was: sum03_safe.c:5
The full backtrace is:
Called from file "set.ml", line 216, characters 18-33
Called from file "list.ml", line 195, characters 17-20
Called from file "src/kernel/stmts_graph.ml", line 418, characters 6-65
Called from file "src/pdg/ctrlDpds.ml", line 217, characters 35-59
Called from file "list.ml", line 86, characters 24-34
Called from file "src/pdg/ctrlDpds.ml", line 237, characters 29-39
Called from file "src/pdg/ctrlDpds.ml", line 257, characters 22-31
Called from file "src/pdg/ctrlDpds.ml", line 261, characters 11-21
Called from file "src/pdg/ctrlDpds.ml", line 261, characters 11-21
Called from file "src/pdg/ctrlDpds.ml", line 261, characters 11-21
<skip the rest of the backrace>
### Additional Information :
Bug coming from Checkofv...