Actions
Feature #9895
closedDisabling single exit point
Start date:
10/28/2019
Due date:
% Done:
0%
Estimated time:
Published in build:
Description
By default (or just with command line options listed below) Frama-C (CIL) translates code of all functions so that there is a single exit point in each function always. This may help for some analyses within Frama-C, but for 3rd party users of outputted code this transformation is redundant. Perhaps, there is some option (or it can be implemented) to disable such the behavior.
toplevel.opt "-no-autoload-plugins" "-no-findlib" "-machdep" "gcc_x86_64" "-c11" "-kernel-warn-key" "CERT:MSC:38=active" "-remove-unused-inline-functions" "-remove-unused-static-functions" "-no-annot" "-keep-logical-operators" "-aggressive-merging" "-print" "-print-lines" "-no-print-annot" "-ocode" "cil.i" ...
Updated by Mikhail Mandrykin over 4 years ago
- Status changed from New to Open
Added an experimental option "-no-single-return" that disables single-return transformation in commit df584314.
Updated by Evgeny Novikov over 4 years ago
For me it works. Can we close the issue?
Actions