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...