Project

General

Profile

Feature #9895

Disabling single exit point

Added by Evgeny Novikov 18 days ago. Updated 7 days ago.

Status:
Open
Priority:
High
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" ...

History

#1

Updated by Mikhail Mandrykin 14 days ago

  • Status changed from New to Open

Added an experimental option "-no-single-return" that disables single-return transformation in commit df584314.

#2

Updated by Evgeny Novikov 7 days ago

For me it works. Can we close the issue?

Also available in: Atom PDF