aboutsummaryrefslogtreecommitdiffstats
path: root/driver
diff options
context:
space:
mode:
authorXavier Leroy <xavierleroy@users.noreply.github.com>2022-11-09 17:55:28 +0100
committerGitHub <noreply@github.com>2022-11-09 17:55:28 +0100
commitabe1f24dfb2b1b67dfeeaf3513e6d3d534f7df32 (patch)
tree2befd6d99593d99f1d0fd0ef520dd8bce0ebf86e /driver
parente637a49e7a963683a4337b742c0adc0e1f93f139 (diff)
parent5a9f24b4e739b6ef830f526845dd4d1557d0adee (diff)
downloadcompcert-abe1f24dfb2b1b67dfeeaf3513e6d3d534f7df32.tar.gz
compcert-abe1f24dfb2b1b67dfeeaf3513e6d3d534f7df32.zip
Merge pull request #459 from AbsInt/full-switch
Handle Duff's device and other unstructured `switch` statements
Diffstat (limited to 'driver')
-rw-r--r--driver/Clflags.ml1
-rw-r--r--driver/CommonOptions.ml4
-rw-r--r--driver/Frontend.ml14
3 files changed, 11 insertions, 8 deletions
diff --git a/driver/Clflags.ml b/driver/Clflags.ml
index 8fbda738..995be34d 100644
--- a/driver/Clflags.ml
+++ b/driver/Clflags.ml
@@ -20,6 +20,7 @@ let option_fstruct_passing = ref false
let option_fvararg_calls = ref true
let option_funprototyped = ref true
let option_fpacked_structs = ref false
+let option_funstructured_switch = ref false
let option_ffpu = ref true
let option_ffloatconstprop = ref 2
let option_ftailcalls = ref true
diff --git a/driver/CommonOptions.ml b/driver/CommonOptions.ml
index 2a3bd740..773c5c7d 100644
--- a/driver/CommonOptions.ml
+++ b/driver/CommonOptions.ml
@@ -35,7 +35,7 @@ let version_options tool_name =
let all_language_support_options = [
option_flongdouble;
option_fstruct_passing; option_fvararg_calls; option_funprototyped;
- option_fpacked_structs; option_finline_asm
+ option_fpacked_structs; option_finline_asm; option_funstructured_switch
]
let f_opt name ref =
@@ -65,6 +65,7 @@ let language_support_options =
@ f_opt "struct-passing" option_fstruct_passing
@ f_opt "vararg-calls" option_fvararg_calls
@ f_opt "unprototyped" option_funprototyped
+ @ f_opt "unstructured-switch" option_funstructured_switch
@ f_opt "packed-structs" option_fpacked_structs
@ f_opt "inline-asm" option_finline_asm
@@ -78,6 +79,7 @@ let language_support_help =
-fstruct-return Like -fstruct-passing (deprecated)
-fvararg-calls Support calls to variable-argument functions [on]
-funprototyped Support calls to old-style functions without prototypes [on]
+ -funstructured-switch Support non-structured 'switch' statements [off]
-fpacked-structs Emulate packed structs [off]
-finline-asm Support inline 'asm' statements [off]
-fall Activate all language support options above
diff --git a/driver/Frontend.ml b/driver/Frontend.ml
index 5d45306d..c8131662 100644
--- a/driver/Frontend.ml
+++ b/driver/Frontend.ml
@@ -79,14 +79,14 @@ let parse_c_file sourcename ifile =
Debug.init_compile_unit sourcename;
Sections.initialize();
CPragmas.reset();
- (* Simplification options *)
- let simplifs =
- "b" (* blocks: mandatory *)
- ^ (if !option_fstruct_passing then "s" else "")
- ^ (if !option_fpacked_structs then "p" else "")
- in
(* Parsing and production of a simplified C AST *)
- let ast = Parse.preprocessed_file simplifs 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 *)