Merge of the nonstrict-ops branch:

- Most RTL operators now evaluate to Some Vundef instead of None
  when undefined behavior occurs.
- More aggressive instruction selection.
- "Bertotization" of pattern-matchings now implemented by a proper preprocessor.
- Cast optimization moved to cfrontend/Cminorgen; removed backend/CastOptim.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1790 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 5 insertions, 10 deletions

diff --git a/backend/LTL.v b/backend/LTL.v
index 5ed0a8fd..422b0e0a 100644
--- a/backend/LTL.v
+++ b/backend/LTL.v
@@ -207,18 +207,13 @@ Inductive step: state -> trace -> state -> Prop :=
       external_call ef ge (map rs args) m t v m' ->
       step (State s f sp pc rs m)
          t (State s f sp pc' (Locmap.set res v rs) m')
-  | exec_Lcond_true:
-      forall s f sp pc rs m cond args ifso ifnot,
+  | exec_Lcond:
+      forall s f sp pc rs m cond args ifso ifnot b pc',
       (fn_code f)!pc = Some(Lcond cond args ifso ifnot) ->
-      eval_condition cond (map rs args) m = Some true ->
+      eval_condition cond (map rs args) m = Some b ->
+      pc' = (if b then ifso else ifnot) ->
       step (State s f sp pc rs m)
-        E0 (State s f sp ifso (undef_temps rs) m)
-  | exec_Lcond_false:
-      forall s f sp pc rs m cond args ifso ifnot,
-      (fn_code f)!pc = Some(Lcond cond args ifso ifnot) ->
-      eval_condition cond (map rs args) m = Some false ->
-      step (State s f sp pc rs m)
-        E0 (State s f sp ifnot (undef_temps rs) m)
+        E0 (State s f sp pc' (undef_temps rs) m)
   | exec_Ljumptable:
       forall s f sp pc rs m arg tbl n pc',
       (fn_code f)!pc = Some(Ljumptable arg tbl) ->