Modified:
/branches/1.0/guru/carraway/Datatype.java
/branches/1.0/lib/word.g
=======================================
--- /branches/1.0/guru/carraway/Datatype.java Sun Aug 14 10:36:45 2011
+++ /branches/1.0/guru/carraway/Datatype.java Tue Aug 16 13:11:10 2011
@@ -254,6 +254,7 @@
if (R != null)
for (int j = 0; j < jend; j++) {
String v = R.vars[j].toString(ctxt);
+ //ctxt.cw.print(" if (x->"+v+" != "+v+")");
ctxt.cw.println(" x->"+v+" = "+v+";");
}
ctxt.cw.println(" return x;");
=======================================
--- /branches/1.0/lib/word.g Wed Jul 27 10:47:09 2011
+++ /branches/1.0/lib/word.g Tue Aug 16 13:11:10 2011
@@ -410,6 +410,10 @@
}
END.
+Define primitive word_inc_wrap : Fun(w:word).word <<END
+#define gword_inc_wrap(c) (c+1)
+END.
+
Define word_inc_tot :=
foralli(b:word).
abbrev r = terminates (bv_inc spec wordlen b) by bv_inc_tot in
@@ -424,7 +428,7 @@
Total word_inc word_inc_tot.
-Define word_inc2 :=
+Define primitive word_inc2 :=
fun(b:word).
match (word_inc b) with
mk_word_inc_t b' carry =>
@@ -432,7 +436,17 @@
ff => b'
| tt => abort word
end
- end.
+ end
+<<END
+#include <limits.h>
+inline unsigned int gword_inc2(unsigned int c) {
+ if (c == UINT_MAX) {
+ fprintf(stderr,"Overflow from word_inc2.\n");
+ exit(1);
+ }
+ return (c+1);
+}
+END.
Define word_inc2_word_inc
: Forall(w w':word)(u:{ w' = (word_inc2 w) }).