4 files changed, 48 insertions, 3 deletions
diff --git a/mppa_k1c/SelectOp.v b/mppa_k1c/SelectOp.v
index fb7f476f..4d3d5ad0 100644
--- a/mppa_k1c/SelectOp.v
+++ b/mppa_k1c/SelectOp.v
@@ -720,7 +720,39 @@ Definition xor (e1: expr) (e2: expr) :=
 
 (** ** Integer logical negation *)
 
-Definition notint (e: expr) := xorimm Int.mone e.
+(** Original definition:
+<<
+Nondetfunction notint (e: expr) :=
+  match e with
+  | Eop Oand (e1:::e2:::Enil) => Eop Onand (e1:::e2:::Enil)
+  | Eop (Oandimm n) (e1:::Enil) => Eop (Onandimm n) (e1:::Enil)
+  | _ => xorimm Int.mone e
+  end.
+>>
+*)
+
+Inductive notint_cases: forall (e: expr), Type :=
+  | notint_case1: forall e1 e2, notint_cases (Eop Oand (e1:::e2:::Enil))
+  | notint_case2: forall n e1, notint_cases (Eop (Oandimm n) (e1:::Enil))
+  | notint_default: forall (e: expr), notint_cases e.
+
+Definition notint_match (e: expr) :=
+  match e as zz1 return notint_cases zz1 with
+  | Eop Oand (e1:::e2:::Enil) => notint_case1 e1 e2
+  | Eop (Oandimm n) (e1:::Enil) => notint_case2 n e1
+  | e => notint_default e
+  end.
+
+Definition notint (e: expr) :=
+  match notint_match e with
+  | notint_case1 e1 e2 => (* Eop Oand (e1:::e2:::Enil) *) 
+      Eop Onand (e1:::e2:::Enil)
+  | notint_case2 n e1 => (* Eop (Oandimm n) (e1:::Enil) *) 
+      Eop (Onandimm n) (e1:::Enil)
+  | notint_default e =>
+      xorimm Int.mone e
+  end.
+
 
 (** ** Integer division and modulus *)
 
diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp
index 14753871..4b64e495 100644
--- a/mppa_k1c/SelectOp.vp
+++ b/mppa_k1c/SelectOp.vp
@@ -275,7 +275,12 @@ Nondetfunction xor (e1: expr) (e2: expr) :=
 
 (** ** Integer logical negation *)
 
-Definition notint (e: expr) := xorimm Int.mone e.
+Nondetfunction notint (e: expr) :=
+  match e with
+  | Eop Oand (e1:::e2:::Enil) => Eop Onand (e1:::e2:::Enil)
+  | Eop (Oandimm n) (e1:::Enil) => Eop (Onandimm n) (e1:::Enil)
+  | _ => xorimm Int.mone e
+  end.
 
 (** ** Integer division and modulus *)
 
diff --git a/mppa_k1c/SelectOpproof.v b/mppa_k1c/SelectOpproof.v
index c5f05dcf..c14a622a 100644
--- a/mppa_k1c/SelectOpproof.v
+++ b/mppa_k1c/SelectOpproof.v
@@ -524,7 +524,12 @@ Qed.
 
 Theorem eval_notint: unary_constructor_sound notint Val.notint.
 Proof.
-  unfold notint; red; intros. rewrite Val.not_xor. apply eval_xorimm; auto.
+  assert (forall v, Val.lessdef (Val.notint (Val.notint v)) v).
+    destruct v; simpl; auto. rewrite Int.not_involutive; auto.
+  unfold notint; red; intros until x; case (notint_match a); intros; InvEval.
+  - TrivialExists; simpl; congruence.
+  - TrivialExists; simpl; congruence.
+  - apply eval_xorimm; assumption.
 Qed.
 
 Theorem eval_divs_base:
diff --git a/test/monniaux/nand/nand.c b/test/monniaux/nand/nand.c
new file mode 100644
index 00000000..002c2368
--- /dev/null
+++ b/test/monniaux/nand/nand.c
@@ -0,0 +1,3 @@
+unsigned not(unsigned x) {
+  return ~x;
+}