body of atomic cond belonging to an assume reproduced in sequence containing the assume
ID0002020: This issue was created automatically from Mantis Issue 2020. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002020 | Frama-C | Plug-in > pathcrawler | public | 2014-12-05 | 2015-03-17 |
| Reporter | nicky | Assigned To | muriel | Resolution | fixed |
| Priority | normal | Severity | major | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C GIT, precise the release id | Target Version | Frama-C GIT, precise the release id | Fixed in Version | Frama-C Sodium |
Description :
The ast_node.pl file generated for assert assume contains the following lines: ... ast_node(n(24), seq, [409,n(37),n(33),422,n(48),n(44)]). % assert_assume.c: l.16 ... ast_node(n(44), assume, [atomic_cond(n(53))]). % assert_assume.c: l.17 ... atomic_cond(n(53), [n(54), 429]). ... ast_node(n(54), seq, [422,n(48)]). % assert_assume.c: l.17
Steps To Reproduce :
cd pathcrawler/tests/AssertAssume frama-c -pc -pc-analyzer -lib-entry -main assert_assume assert_assume.c