diff options
Diffstat (limited to 'cfrontend')
-rw-r--r-- | cfrontend/Cop.v | 3 | ||||
-rw-r--r-- | cfrontend/Cshmgenproof.v | 1 | ||||
-rw-r--r-- | cfrontend/Ctyping.v | 1 | ||||
-rw-r--r-- | cfrontend/SimplLocalsproof.v | 3 |
4 files changed, 0 insertions, 8 deletions
diff --git a/cfrontend/Cop.v b/cfrontend/Cop.v index 4e572277..b6b75abe 100644 --- a/cfrontend/Cop.v +++ b/cfrontend/Cop.v @@ -273,7 +273,6 @@ Definition sem_cast (v: val) (t1 t2: type) : option val := | cast_case_p2bool => match v with | Vint i => Some (Vint (cast_int_int IBool Signed i)) - | Vptr _ _ => Some (Vint Int.one) | _ => None end | cast_case_l2l => @@ -391,7 +390,6 @@ Definition bool_val (v: val) (t: type) : option bool := | bool_case_p => match v with | Vint n => Some (negb (Int.eq n Int.zero)) - | Vptr b ofs => Some true | _ => None end | bool_case_l => @@ -426,7 +424,6 @@ Definition sem_notbool (v: val) (ty: type) : option val := | bool_case_p => match v with | Vint n => Some (Val.of_bool (Int.eq n Int.zero)) - | Vptr _ _ => Some Vfalse | _ => None end | bool_case_l => diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v index 7f61c657..847e4856 100644 --- a/cfrontend/Cshmgenproof.v +++ b/cfrontend/Cshmgenproof.v @@ -333,7 +333,6 @@ Proof. econstructor; split. econstructor; eauto with cshm. simpl. eauto. unfold Val.cmpu, Val.cmpu_bool. simpl. destruct (Int.eq i Int.zero); simpl; constructor. - exists Vtrue; split. econstructor; eauto with cshm. constructor. (* long *) econstructor; split. econstructor; eauto with cshm. simpl. unfold Val.cmpl. simpl. eauto. destruct (Int64.eq i Int64.zero); simpl; constructor. diff --git a/cfrontend/Ctyping.v b/cfrontend/Ctyping.v index 43d34007..bdeeff2a 100644 --- a/cfrontend/Ctyping.v +++ b/cfrontend/Ctyping.v @@ -1390,7 +1390,6 @@ Proof. destruct (Float.cmp Ceq f Float.zero); constructor; auto with ty. destruct (Float32.cmp Ceq f Float32.zero); constructor; auto with ty. destruct (Int.eq i Int.zero); constructor; auto with ty. - constructor; auto with ty. destruct (Int64.eq i Int64.zero); constructor; auto with ty. - (* notint *) unfold sem_notint in SEM; DestructCases; auto with ty. diff --git a/cfrontend/SimplLocalsproof.v b/cfrontend/SimplLocalsproof.v index 5cf59d94..3364ec6a 100644 --- a/cfrontend/SimplLocalsproof.v +++ b/cfrontend/SimplLocalsproof.v @@ -267,11 +267,8 @@ Proof. constructor. simpl. destruct (Float32.cmp Ceq f Float32.zero); auto. constructor. simpl. destruct (Float.cmp Ceq f Float.zero); auto. constructor. simpl. destruct (Int.eq i Int.zero); auto. - constructor; auto. constructor. simpl. destruct (Int.eq i Int.zero); auto. - constructor; auto. constructor. simpl. destruct (Int.eq i Int.zero); auto. - constructor; auto. (* long *) destruct ty; try (destruct f); try discriminate. destruct v; inv H. constructor. |