From daccc2928e6410c4e8c886ea7d019fd9a071b931 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 29 Mar 2015 19:57:16 +0200 Subject: Omission: forgot to treat pointer values in bool_of_val and sem_notbool. --- cfrontend/Cstrategy.v | 68 +++++++++++++++++++++++++-------------------------- 1 file changed, 34 insertions(+), 34 deletions(-) (limited to 'cfrontend/Cstrategy.v') diff --git a/cfrontend/Cstrategy.v b/cfrontend/Cstrategy.v index 3b0eb84f..b082ea56 100644 --- a/cfrontend/Cstrategy.v +++ b/cfrontend/Cstrategy.v @@ -122,7 +122,7 @@ with eval_simple_rvalue: expr -> val -> Prop := eval_simple_rvalue (Eaddrof l ty) (Vptr b ofs) | esr_unop: forall op r1 ty v1 v, eval_simple_rvalue r1 v1 -> - sem_unary_operation op v1 (typeof r1) = Some v -> + sem_unary_operation op v1 (typeof r1) m = Some v -> eval_simple_rvalue (Eunop op r1 ty) v | esr_binop: forall op r1 r2 ty v1 v2 v, eval_simple_rvalue r1 v1 -> eval_simple_rvalue r2 v2 -> @@ -249,33 +249,33 @@ Inductive estep: state -> trace -> state -> Prop := | step_seqand_true: forall f C r1 r2 ty k e m v, leftcontext RV RV C -> eval_simple_rvalue e m r1 v -> - bool_val v (typeof r1) = Some true -> + bool_val v (typeof r1) m = Some true -> estep (ExprState f (C (Eseqand r1 r2 ty)) k e m) E0 (ExprState f (C (Eparen r2 type_bool ty)) k e m) | step_seqand_false: forall f C r1 r2 ty k e m v, leftcontext RV RV C -> eval_simple_rvalue e m r1 v -> - bool_val v (typeof r1) = Some false -> + bool_val v (typeof r1) m = Some false -> estep (ExprState f (C (Eseqand r1 r2 ty)) k e m) E0 (ExprState f (C (Eval (Vint Int.zero) ty)) k e m) | step_seqor_true: forall f C r1 r2 ty k e m v, leftcontext RV RV C -> eval_simple_rvalue e m r1 v -> - bool_val v (typeof r1) = Some true -> + bool_val v (typeof r1) m = Some true -> estep (ExprState f (C (Eseqor r1 r2 ty)) k e m) E0 (ExprState f (C (Eval (Vint Int.one) ty)) k e m) | step_seqor_false: forall f C r1 r2 ty k e m v, leftcontext RV RV C -> eval_simple_rvalue e m r1 v -> - bool_val v (typeof r1) = Some false -> + bool_val v (typeof r1) m = Some false -> estep (ExprState f (C (Eseqor r1 r2 ty)) k e m) E0 (ExprState f (C (Eparen r2 type_bool ty)) k e m) | step_condition: forall f C r1 r2 r3 ty k e m v b, leftcontext RV RV C -> eval_simple_rvalue e m r1 v -> - bool_val v (typeof r1) = Some b -> + bool_val v (typeof r1) m = Some b -> estep (ExprState f (C (Econdition r1 r2 r3 ty)) k e m) E0 (ExprState f (C (Eparen (if b then r2 else r3) ty ty)) k e m) @@ -536,17 +536,17 @@ Definition invert_expr_prop (a: expr) (m: mem) : Prop := | Evalof (Eloc b ofs ty') ty => ty' = ty /\ exists t, exists v, deref_loc ge ty m b ofs t v | Eunop op (Eval v1 ty1) ty => - exists v, sem_unary_operation op v1 ty1 = Some v + exists v, sem_unary_operation op v1 ty1 m = Some v | Ebinop op (Eval v1 ty1) (Eval v2 ty2) ty => exists v, sem_binary_operation ge op v1 ty1 v2 ty2 m = Some v | Ecast (Eval v1 ty1) ty => exists v, sem_cast v1 ty1 ty = Some v | Eseqand (Eval v1 ty1) r2 ty => - exists b, bool_val v1 ty1 = Some b + exists b, bool_val v1 ty1 m = Some b | Eseqor (Eval v1 ty1) r2 ty => - exists b, bool_val v1 ty1 = Some b + exists b, bool_val v1 ty1 m = Some b | Econdition (Eval v1 ty1) r1 r2 ty => - exists b, bool_val v1 ty1 = Some b + exists b, bool_val v1 ty1 m = Some b | Eassign (Eloc b ofs ty1) (Eval v2 ty2) ty => exists v, exists m', exists t, ty = ty1 /\ sem_cast v2 ty2 ty1 = Some v /\ assign_loc ge ty1 m b ofs v t m' @@ -1695,27 +1695,27 @@ with eval_expr: env -> mem -> kind -> expr -> trace -> mem -> expr -> Prop := eval_expr e m RV (Ecast a ty) t m' (Ecast a' ty) | eval_seqand_true: forall e m a1 a2 ty t1 m' a1' v1 t2 m'' a2' v2 v, eval_expr e m RV a1 t1 m' a1' -> eval_simple_rvalue ge e m' a1' v1 -> - bool_val v1 (typeof a1) = Some true -> + bool_val v1 (typeof a1) m' = Some true -> eval_expr e m' RV a2 t2 m'' a2' -> eval_simple_rvalue ge e m'' a2' v2 -> sem_cast v2 (typeof a2) type_bool = Some v -> eval_expr e m RV (Eseqand a1 a2 ty) (t1**t2) m'' (Eval v ty) | eval_seqand_false: forall e m a1 a2 ty t1 m' a1' v1, eval_expr e m RV a1 t1 m' a1' -> eval_simple_rvalue ge e m' a1' v1 -> - bool_val v1 (typeof a1) = Some false -> + bool_val v1 (typeof a1) m' = Some false -> eval_expr e m RV (Eseqand a1 a2 ty) t1 m' (Eval (Vint Int.zero) ty) | eval_seqor_false: forall e m a1 a2 ty t1 m' a1' v1 t2 m'' a2' v2 v, eval_expr e m RV a1 t1 m' a1' -> eval_simple_rvalue ge e m' a1' v1 -> - bool_val v1 (typeof a1) = Some false -> + bool_val v1 (typeof a1) m' = Some false -> eval_expr e m' RV a2 t2 m'' a2' -> eval_simple_rvalue ge e m'' a2' v2 -> sem_cast v2 (typeof a2) type_bool = Some v -> eval_expr e m RV (Eseqor a1 a2 ty) (t1**t2) m'' (Eval v ty) | eval_seqor_true: forall e m a1 a2 ty t1 m' a1' v1, eval_expr e m RV a1 t1 m' a1' -> eval_simple_rvalue ge e m' a1' v1 -> - bool_val v1 (typeof a1) = Some true -> + bool_val v1 (typeof a1) m' = Some true -> eval_expr e m RV (Eseqor a1 a2 ty) t1 m' (Eval (Vint Int.one) ty) | eval_condition: forall e m a1 a2 a3 ty t1 m' a1' v1 t2 m'' a' v' b v, eval_expr e m RV a1 t1 m' a1' -> eval_simple_rvalue ge e m' a1' v1 -> - bool_val v1 (typeof a1) = Some b -> + bool_val v1 (typeof a1) m' = Some b -> eval_expr e m' RV (if b then a2 else a3) t2 m'' a' -> eval_simple_rvalue ge e m'' a' v' -> sem_cast v' (typeof (if b then a2 else a3)) ty = Some v -> eval_expr e m RV (Econdition a1 a2 a3 ty) (t1**t2) m'' (Eval v ty) @@ -1801,7 +1801,7 @@ with exec_stmt: env -> mem -> statement -> trace -> mem -> outcome -> Prop := t1 m1 out | exec_Sifthenelse: forall e m a s1 s2 t1 m1 v1 t2 m2 b out, eval_expression e m a t1 m1 v1 -> - bool_val v1 (typeof a) = Some b -> + bool_val v1 (typeof a) m1 = Some b -> exec_stmt e m1 (if b then s1 else s2) t2 m2 out -> exec_stmt e m (Sifthenelse a s1 s2) (t1**t2) m2 out @@ -1820,19 +1820,19 @@ with exec_stmt: env -> mem -> statement -> trace -> mem -> outcome -> Prop := E0 m Out_continue | exec_Swhile_false: forall e m a s t m' v, eval_expression e m a t m' v -> - bool_val v (typeof a) = Some false -> + bool_val v (typeof a) m' = Some false -> exec_stmt e m (Swhile a s) t m' Out_normal | exec_Swhile_stop: forall e m a s t1 m1 v t2 m2 out' out, eval_expression e m a t1 m1 v -> - bool_val v (typeof a) = Some true -> + bool_val v (typeof a) m1 = Some true -> exec_stmt e m1 s t2 m2 out' -> out_break_or_return out' out -> exec_stmt e m (Swhile a s) (t1**t2) m2 out | exec_Swhile_loop: forall e m a s t1 m1 v t2 m2 out1 t3 m3 out, eval_expression e m a t1 m1 v -> - bool_val v (typeof a) = Some true -> + bool_val v (typeof a) m1 = Some true -> exec_stmt e m1 s t2 m2 out1 -> out_normal_or_continue out1 -> exec_stmt e m2 (Swhile a s) t3 m3 out -> @@ -1842,7 +1842,7 @@ with exec_stmt: env -> mem -> statement -> trace -> mem -> outcome -> Prop := exec_stmt e m s t1 m1 out1 -> out_normal_or_continue out1 -> eval_expression e m1 a t2 m2 v -> - bool_val v (typeof a) = Some false -> + bool_val v (typeof a) m2 = Some false -> exec_stmt e m (Sdowhile a s) (t1 ** t2) m2 Out_normal | exec_Sdowhile_stop: forall e m s a t m1 out1 out, @@ -1854,7 +1854,7 @@ with exec_stmt: env -> mem -> statement -> trace -> mem -> outcome -> Prop := exec_stmt e m s t1 m1 out1 -> out_normal_or_continue out1 -> eval_expression e m1 a t2 m2 v -> - bool_val v (typeof a) = Some true -> + bool_val v (typeof a) m2 = Some true -> exec_stmt e m2 (Sdowhile a s) t3 m3 out -> exec_stmt e m (Sdowhile a s) (t1 ** t2 ** t3) m3 out @@ -1865,19 +1865,19 @@ with exec_stmt: env -> mem -> statement -> trace -> mem -> outcome -> Prop := (t1 ** t2) m2 out | exec_Sfor_false: forall e m s a2 a3 t m' v, eval_expression e m a2 t m' v -> - bool_val v (typeof a2) = Some false -> + bool_val v (typeof a2) m' = Some false -> exec_stmt e m (Sfor Sskip a2 a3 s) t m' Out_normal | exec_Sfor_stop: forall e m s a2 a3 t1 m1 v t2 m2 out1 out, eval_expression e m a2 t1 m1 v -> - bool_val v (typeof a2) = Some true -> + bool_val v (typeof a2) m1 = Some true -> exec_stmt e m1 s t2 m2 out1 -> out_break_or_return out1 out -> exec_stmt e m (Sfor Sskip a2 a3 s) (t1 ** t2) m2 out | exec_Sfor_loop: forall e m s a2 a3 t1 m1 v t2 m2 out1 t3 m3 t4 m4 out, eval_expression e m a2 t1 m1 v -> - bool_val v (typeof a2) = Some true -> + bool_val v (typeof a2) m1 = Some true -> exec_stmt e m1 s t2 m2 out1 -> out_normal_or_continue out1 -> exec_stmt e m2 a3 t3 m3 Out_normal -> @@ -1952,7 +1952,7 @@ CoInductive evalinf_expr: env -> mem -> kind -> expr -> traceinf -> Prop := evalinf_expr e m RV (Eseqand a1 a2 ty) t1 | evalinf_seqand_2: forall e m a1 a2 ty t1 m' a1' v1 t2, eval_expr e m RV a1 t1 m' a1' -> eval_simple_rvalue ge e m' a1' v1 -> - bool_val v1 (typeof a1) = Some true -> + bool_val v1 (typeof a1) m' = Some true -> evalinf_expr e m' RV a2 t2 -> evalinf_expr e m RV (Eseqand a1 a2 ty) (t1***t2) | evalinf_seqor: forall e m a1 a2 ty t1, @@ -1960,7 +1960,7 @@ CoInductive evalinf_expr: env -> mem -> kind -> expr -> traceinf -> Prop := evalinf_expr e m RV (Eseqor a1 a2 ty) t1 | evalinf_seqor_2: forall e m a1 a2 ty t1 m' a1' v1 t2, eval_expr e m RV a1 t1 m' a1' -> eval_simple_rvalue ge e m' a1' v1 -> - bool_val v1 (typeof a1) = Some false -> + bool_val v1 (typeof a1) m' = Some false -> evalinf_expr e m' RV a2 t2 -> evalinf_expr e m RV (Eseqor a1 a2 ty) (t1***t2) | evalinf_condition: forall e m a1 a2 a3 ty t1, @@ -1968,7 +1968,7 @@ CoInductive evalinf_expr: env -> mem -> kind -> expr -> traceinf -> Prop := evalinf_expr e m RV (Econdition a1 a2 a3 ty) t1 | evalinf_condition_2: forall e m a1 a2 a3 ty t1 m' a1' v1 t2 b, eval_expr e m RV a1 t1 m' a1' -> eval_simple_rvalue ge e m' a1' v1 -> - bool_val v1 (typeof a1) = Some b -> + bool_val v1 (typeof a1) m' = Some b -> evalinf_expr e m' RV (if b then a2 else a3) t2 -> evalinf_expr e m RV (Econdition a1 a2 a3 ty) (t1***t2) | evalinf_assign_left: forall e m a1 t1 a2 ty, @@ -2039,7 +2039,7 @@ with execinf_stmt: env -> mem -> statement -> traceinf -> Prop := execinf_stmt e m (Sifthenelse a s1 s2) t1 | execinf_Sifthenelse: forall e m a s1 s2 t1 m1 v1 t2 b, eval_expression e m a t1 m1 v1 -> - bool_val v1 (typeof a) = Some b -> + bool_val v1 (typeof a) m1 = Some b -> execinf_stmt e m1 (if b then s1 else s2) t2 -> execinf_stmt e m (Sifthenelse a s1 s2) (t1***t2) | execinf_Sreturn_some: forall e m a t, @@ -2050,12 +2050,12 @@ with execinf_stmt: env -> mem -> statement -> traceinf -> Prop := execinf_stmt e m (Swhile a s) t1 | execinf_Swhile_body: forall e m a s t1 m1 v t2, eval_expression e m a t1 m1 v -> - bool_val v (typeof a) = Some true -> + bool_val v (typeof a) m1 = Some true -> execinf_stmt e m1 s t2 -> execinf_stmt e m (Swhile a s) (t1***t2) | execinf_Swhile_loop: forall e m a s t1 m1 v t2 m2 out1 t3, eval_expression e m a t1 m1 v -> - bool_val v (typeof a) = Some true -> + bool_val v (typeof a) m1 = Some true -> exec_stmt e m1 s t2 m2 out1 -> out_normal_or_continue out1 -> execinf_stmt e m2 (Swhile a s) t3 -> @@ -2072,7 +2072,7 @@ with execinf_stmt: env -> mem -> statement -> traceinf -> Prop := exec_stmt e m s t1 m1 out1 -> out_normal_or_continue out1 -> eval_expression e m1 a t2 m2 v -> - bool_val v (typeof a) = Some true -> + bool_val v (typeof a) m2 = Some true -> execinf_stmt e m2 (Sdowhile a s) t3 -> execinf_stmt e m (Sdowhile a s) (t1***t2***t3) | execinf_Sfor_start_1: forall e m s a1 a2 a3 t1, @@ -2087,19 +2087,19 @@ with execinf_stmt: env -> mem -> statement -> traceinf -> Prop := execinf_stmt e m (Sfor Sskip a2 a3 s) t | execinf_Sfor_body: forall e m s a2 a3 t1 m1 v t2, eval_expression e m a2 t1 m1 v -> - bool_val v (typeof a2) = Some true -> + bool_val v (typeof a2) m1 = Some true -> execinf_stmt e m1 s t2 -> execinf_stmt e m (Sfor Sskip a2 a3 s) (t1***t2) | execinf_Sfor_next: forall e m s a2 a3 t1 m1 v t2 m2 out1 t3, eval_expression e m a2 t1 m1 v -> - bool_val v (typeof a2) = Some true -> + bool_val v (typeof a2) m1 = Some true -> exec_stmt e m1 s t2 m2 out1 -> out_normal_or_continue out1 -> execinf_stmt e m2 a3 t3 -> execinf_stmt e m (Sfor Sskip a2 a3 s) (t1***t2***t3) | execinf_Sfor_loop: forall e m s a2 a3 t1 m1 v t2 m2 out1 t3 m3 t4, eval_expression e m a2 t1 m1 v -> - bool_val v (typeof a2) = Some true -> + bool_val v (typeof a2) m1 = Some true -> exec_stmt e m1 s t2 m2 out1 -> out_normal_or_continue out1 -> exec_stmt e m2 a3 t3 m3 Out_normal -> -- cgit