aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--mppa_k1c/Machregs.v2
-rw-r--r--test/monniaux/binary_search/binary_search.c2
2 files changed, 2 insertions, 2 deletions
diff --git a/mppa_k1c/Machregs.v b/mppa_k1c/Machregs.v
index f36962f3..823b13e9 100644
--- a/mppa_k1c/Machregs.v
+++ b/mppa_k1c/Machregs.v
@@ -209,7 +209,7 @@ Global Opaque
Definition two_address_op (op: operation) : bool :=
match op with
- | Ocast32unsigned | Omadd | Omaddimm _ | Omaddl | Omaddlimm _ | Oselect _ | Oselectl _ | Oselectf _ | Oselectfs _ => true
+ | Omadd | Omaddimm _ | Omaddl | Omaddlimm _ | Oselect _ | Oselectl _ | Oselectf _ | Oselectfs _ => true
| _ => false
end.
diff --git a/test/monniaux/binary_search/binary_search.c b/test/monniaux/binary_search/binary_search.c
index 9b54f28d..1fbc37b8 100644
--- a/test/monniaux/binary_search/binary_search.c
+++ b/test/monniaux/binary_search/binary_search.c
@@ -4,7 +4,7 @@
#include "../clock.h"
typedef int data;
-typedef int index;
+typedef unsigned index;
int my_bsearch (data *a, index n, data x) {
index i = 0, j = n - 1;