diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2020-02-03 10:52:53 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2020-02-03 10:52:53 +0100 |
| commit | 7dca7590aa212806ee939244b253a6a067f34bfc (patch) | |
| tree | 1449c8a386c23ab0a8d443ac46ebccb39a8630e9 /backend/Duplicateaux.ml | |
| parent | 326bdc281c60ac826129b0a0fda33dc17d8498fa (diff) | |
| download | compcert-kvx-7dca7590aa212806ee939244b253a6a067f34bfc.tar.gz compcert-kvx-7dca7590aa212806ee939244b253a6a067f34bfc.zip | |
Added flag to desactivate condition inversion
Diffstat (limited to 'backend/Duplicateaux.ml')
| -rw-r--r-- | backend/Duplicateaux.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/backend/Duplicateaux.ml b/backend/Duplicateaux.ml index 2dd07b76..84daa329 100644 --- a/backend/Duplicateaux.ml +++ b/backend/Duplicateaux.ml @@ -557,7 +557,8 @@ let rec invert_iconds_trace code = function let rec invert_iconds code = function | [] -> code | t :: ts -> - let code' = invert_iconds_trace code t + let code' = if !Clflags.option_finvertcond then invert_iconds_trace code t + else code in invert_iconds code' ts (* For now, identity function *) |