| commit | 410f2f63218a98ee44e7c179b69308a3d0b3fca8 | |
| author | Sven Verdoolaege <skimo@kotnet.org> | |
| Mon, 31 Oct 2016 15:06:14 +0000 (31 16:06 +0100) | ||
| committer | Sven Verdoolaege <skimo@kotnet.org> | |
| Wed, 23 Nov 2016 10:36:05 +0000 (23 11:36 +0100) | ||
| tree | 58fae4ca14385bf3bdb394941b8686a6f9239b68 | treesnapshot (tar.gz zip) |
| parent | 059461503bf6d5c041a0dfaff0a2a8367bb3b119 | commitdiff |
pet_scop_from_pet_tree: take into account assumptions
The assumptions provided by the user in __pencil_assume/__builtin_assume
statements are collected in the context, but they were not otherwise exploited.
Exploit them during the extraction process as well.
In particular, use the assumptions to simplify expressions.
This simplification can in some cases eliminate some redundant
pieces and therefore also speed up the extraction process.
Tested-by: Samuel Thibault <samuel.thibault@inria.fr>
Signed-off-by: Sven Verdoolaege <skimo@kotnet.org>
The assumptions provided by the user in __pencil_assume/__builtin_assume
statements are collected in the context, but they were not otherwise exploited.
Exploit them during the extraction process as well.
In particular, use the assumptions to simplify expressions.
This simplification can in some cases eliminate some redundant
pieces and therefore also speed up the extraction process.
Tested-by: Samuel Thibault <samuel.thibault@inria.fr>
Signed-off-by: Sven Verdoolaege <skimo@kotnet.org>
| tests/assume.scop | diffblobblamehistory | |
| tests/assume3.c | [new file with mode: 0644] | blob |
| tests/assume3.scop | [new file with mode: 0644] | blob |
| tests/assume4.c | [new file with mode: 0644] | blob |
| tests/assume4.scop | [new file with mode: 0644] | blob |
| tests/assume5.c | [new file with mode: 0644] | blob |
| tests/assume5.scop | [new file with mode: 0644] | blob |
| tree2scop.c | diffblobblamehistory |