aboutsummaryrefslogtreecommitdiffstats
path: root/driver/Frontend.ml
diff options
context:
space:
mode:
authorXavier Leroy <xavier.leroy@college-de-france.fr>2022-09-27 12:31:07 +0200
committerXavier Leroy <xavier.leroy@college-de-france.fr>2022-10-29 10:03:30 +0200
commita1dabb4792446538cce24eb87bcd3ccb3c09f18b (patch)
treeb74523469addfab9db6afc5ced3564ce267da4d7 /driver/Frontend.ml
parentdfc6b66ec21e148d29b2a6e8b5d77873a0a47511 (diff)
downloadcompcert-a1dabb4792446538cce24eb87bcd3ccb3c09f18b.tar.gz
compcert-a1dabb4792446538cce24eb87bcd3ccb3c09f18b.zip
Handle unstructured 'switch' statements such as Duff's device
- New elaboration pass: SwitchNorm - recognizes structured 'switch' statements and puts them in a normalized form; - if selected, transforms unstructured 'switch' statements into a structured switch with goto actions + the original switch body with appropriate labels and gotos. - C2C treatment of 'switch' statements is simplified accordingly. - New language support option `-funstructured-switch`. - Some tests were added (test/regression/switch3.c).
Diffstat (limited to 'driver/Frontend.ml')
-rw-r--r--driver/Frontend.ml12
1 files changed, 7 insertions, 5 deletions
diff --git a/driver/Frontend.ml b/driver/Frontend.ml
index 5132f730..c8131662 100644
--- a/driver/Frontend.ml
+++ b/driver/Frontend.ml
@@ -80,11 +80,13 @@ let parse_c_file sourcename ifile =
Sections.initialize();
CPragmas.reset();
(* Parsing and production of a simplified C AST *)
- let ast = Parse.preprocessed_file
- ~unblock: true
- ~struct_passing: !option_fstruct_passing
- ~packed_structs: !option_fpacked_structs
- sourcename ifile in
+ let ast =
+ Parse.preprocessed_file
+ ~unblock: true
+ ~switch_norm: (if !option_funstructured_switch then `Full else `Partial)
+ ~struct_passing: !option_fstruct_passing
+ ~packed_structs: !option_fpacked_structs
+ sourcename ifile in
(* Save C AST if requested *)
Cprint.print_if ast;
(* Conversion to Csyntax *)