diff options
Diffstat (limited to 'kvx/lib/RTLpathSE_theory.v')
| -rw-r--r-- | kvx/lib/RTLpathSE_theory.v | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/kvx/lib/RTLpathSE_theory.v b/kvx/lib/RTLpathSE_theory.v index dcdc54b5..3573ddbb 100644 --- a/kvx/lib/RTLpathSE_theory.v +++ b/kvx/lib/RTLpathSE_theory.v @@ -1716,7 +1716,8 @@ Proof. constructor; eauto. congruence. Qed. -Fixpoint seval_builtin_sval ge sp bsv rs0 m0 := match bsv with +Fixpoint seval_builtin_sval ge sp bsv rs0 m0 := + match bsv with | BA sv => SOME v <- seval_sval ge sp sv rs0 m0 IN Some (BA v) | BA_splitlong sv1 sv2 => SOME v1 <- seval_builtin_sval ge sp sv1 rs0 m0 IN @@ -1736,7 +1737,8 @@ Fixpoint seval_builtin_sval ge sp bsv rs0 m0 := match bsv with | BA_addrglobal id ptr => Some (BA_addrglobal id ptr) end. -Fixpoint seval_list_builtin_sval ge sp lbsv rs0 m0 := match lbsv with +Fixpoint seval_list_builtin_sval ge sp lbsv rs0 m0 := + match lbsv with | nil => Some nil | bsv::lbsv => SOME v <- seval_builtin_sval ge sp bsv rs0 m0 IN SOME lv <- seval_list_builtin_sval ge sp lbsv rs0 m0 IN |