Removed CMinor import. Bug 20992

9 files changed, 3 insertions, 1379 deletions

diff --git a/.gitignore b/.gitignore
index fd993627..1d1ff9df 100644
--- a/.gitignore
+++ b/.gitignore
@@ -38,9 +38,6 @@ arm/SelectOp.v
 arm/SelectLong.v
 backend/SelectDiv.v
 backend/SplitLong.v
-backend/CMlexer.ml
-backend/CMparser.ml
-backend/CMparser.mli
 cparser/Parser.v
 cparser/Lexer.ml
 cparser/pre_parser.ml
@@ -53,7 +50,6 @@ cparser/handcrafted.messages.raw
 cparser/deLexer
 cparser/tests/generated/*.c
 cparser/tests/generated/*.err
-backend/CMparser.automaton
 lib/Readconfig.ml
 lib/Tokenize.ml
 lib/Responsefile.ml
diff --git a/LICENSE b/LICENSE
index 0151a7fa..2353de49 100644
--- a/LICENSE
+++ b/LICENSE
@@ -36,11 +36,6 @@ option) any later version:
   cfrontend/Ctyping.v
   
   backend/Cminor.v
-  backend/CMlexer.mli
-  backend/CMlexer.mll
-  backend/CMparser.mly
-  backend/CMtypecheck.ml
-  backend/CMtypecheck.mli
 
   arm/Archi.v
   ia32/Archi.v
diff --git a/Makefile.extr b/Makefile.extr
index fb19dd00..a1c2ef7c 100644
--- a/Makefile.extr
+++ b/Makefile.extr
@@ -54,8 +54,6 @@ extraction/%.cmx: WARNINGS +=-w -20-27-32..34-39-41-44..45
 extraction/%.cmo: WARNINGS +=-w -20-27-32..34-39-41-44..45
 cparser/pre_parser.cmx: WARNINGS += -w -41
 cparser/pre_parser.cmo: WARNINGS += -w -41
-backend/CMparser.cmx: WARNINGS += -w -41
-backend/CMparser.cmo: WARNINGS += -w -41
 
 COMPFLAGS+=-g $(INCLUDES) $(MENHIR_INCLUDES) $(WARNINGS)
 
@@ -74,10 +72,9 @@ OCAMLDEP=ocamldep$(DOTOPT) -slash $(INCLUDES)
 OCAMLLEX=ocamllex -q
 MODORDER=tools/modorder .depend.extr
 
-PARSERS=backend/CMparser.mly cparser/pre_parser.mly
-LEXERS=backend/CMlexer.mll cparser/Lexer.mll \
-       lib/Tokenize.mll lib/Readconfig.mll \
-       lib/Responsefile.mll
+PARSERS=cparser/pre_parser.mly
+LEXERS=cparser/Lexer.mll lib/Tokenize.mll \
+	     lib/Readconfig.mll lib/Responsefile.mll
 
 LIBS=str.cmxa unix.cmxa $(MENHIR_LIBS)
 LIBS_BYTE=$(patsubst %.cmxa,%.cma,$(patsubst %.cmx,%.cmo,$(LIBS)))
@@ -132,7 +129,6 @@ clean:
 	rm -f $(EXECUTABLES)
 	rm -f $(GENERATED)
 	for d in $(DIRS); do rm -f $$d/*.cm[iotx] $$d/*cmti $$d/*.o; done
-	rm -f backend/CMparser.automaton
 	$(MAKE) -C cparser clean
 
 # Generation of .depend.extr
diff --git a/backend/CMlexer.mli b/backend/CMlexer.mli
deleted file mode 100644
index c6afb72c..00000000
--- a/backend/CMlexer.mli
+++ /dev/null
@@ -1,17 +0,0 @@
-(* *********************************************************************)
-(*                                                                     *)
-(*              The Compcert verified compiler                         *)
-(*                                                                     *)
-(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
-(*                                                                     *)
-(*  Copyright Institut National de Recherche en Informatique et en     *)
-(*  Automatique.  All rights reserved.  This file is distributed       *)
-(*  under the terms of the GNU General Public License as published by  *)
-(*  the Free Software Foundation, either version 2 of the License, or  *)
-(*  (at your option) any later version.  This file is also distributed *)
-(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
-(*                                                                     *)
-(* *********************************************************************)
-
-val token: Lexing.lexbuf -> CMparser.token
-exception Error of string
diff --git a/backend/CMlexer.mll b/backend/CMlexer.mll
deleted file mode 100644
index 65f244b5..00000000
--- a/backend/CMlexer.mll
+++ /dev/null
@@ -1,180 +0,0 @@
-(* *********************************************************************)
-(*                                                                     *)
-(*              The Compcert verified compiler                         *)
-(*                                                                     *)
-(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
-(*                                                                     *)
-(*  Copyright Institut National de Recherche en Informatique et en     *)
-(*  Automatique.  All rights reserved.  This file is distributed       *)
-(*  under the terms of the GNU General Public License as published by  *)
-(*  the Free Software Foundation, either version 2 of the License, or  *)
-(*  (at your option) any later version.  This file is also distributed *)
-(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
-(*                                                                     *)
-(* *********************************************************************)
-
-{
-open CMparser
-exception Error of string
-}
-
-let blank = [' ' '\009' '\012' '\010' '\013']
-let floatlit =
- ("-"? (['0'-'9'] ['0'-'9' '_']*
-  ('.' ['0'-'9' '_']* )?
-  (['e' 'E'] ['+' '-']? ['0'-'9'] ['0'-'9' '_']*)? )) | "inf" | "nan"
-let ident = ['A'-'Z' 'a'-'z' '_'] ['A'-'Z' 'a'-'z' '_' '$' '0'-'9']*
-let qident = '\'' [ ^ '\'' ]+ '\''
-let temp = "$" ['1'-'9'] ['0'-'9']*
-let intlit = "-"? ( ['0'-'9']+ | "0x" ['0'-'9' 'a'-'f' 'A'-'F']+
-                               | "0o" ['0'-'7']+ | "0b" ['0'-'1']+ )
-let stringlit = "\"" [ ^ '"' ] * '"'
-
-rule token = parse
-  | blank +      { token lexbuf }
-  | "/*"         { comment lexbuf; token lexbuf }
-  | "absf" { ABSF }
-  | "&" { AMPERSAND }
-  | "&l" { AMPERSANDL }
-  | "!"    { BANG }
-  | "!="    { BANGEQUAL }
-  | "!=f"    { BANGEQUALF }
-  | "!=l"    { BANGEQUALL }
-  | "!=lu"    { BANGEQUALLU }
-  | "!=u"    { BANGEQUALU }
-  | "|"     { BAR }
-  | "|l"     { BARL }
-  | "builtin" { BUILTIN }
-  | "^"     { CARET }
-  | "^l"     { CARETL }
-  | "case"  { CASE }
-  | ":"    { COLON }
-  | ","    { COMMA }
-  | "default" { DEFAULT }
-  | "else"    { ELSE }
-  | "="    { EQUAL }
-  | "=="    { EQUALEQUAL }
-  | "==f"    { EQUALEQUALF }
-  | "==l"    { EQUALEQUALL }
-  | "==lu"    { EQUALEQUALLU }
-  | "==u"    { EQUALEQUALU }
-  | "exit"    { EXIT }
-  | "extern"    { EXTERN }
-  | "float"    { FLOAT }
-  | "float32"    { FLOAT32 }
-  | "float64"    { FLOAT64 }
-  | "floatofint"    { FLOATOFINT }
-  | "floatofintu"    { FLOATOFINTU }
-  | "floatoflong"  { FLOATOFLONG }
-  | "floatoflongu" { FLOATOFLONGU }
-  | "goto"  { GOTO }
-  | ">"    { GREATER }
-  | ">f"    { GREATERF }
-  | ">l"    { GREATERL }
-  | ">lu"    { GREATERLU }
-  | ">u"    { GREATERU }
-  | ">="    { GREATEREQUAL }
-  | ">=f"    { GREATEREQUALF }
-  | ">=l"    { GREATEREQUALL }
-  | ">=lu"    { GREATEREQUALLU }
-  | ">=u"    { GREATEREQUALU }
-  | ">>"    { GREATERGREATER }
-  | ">>u"    { GREATERGREATERU }
-  | ">>l"    { GREATERGREATERL }
-  | ">>lu"    { GREATERGREATERLU }
-  | "if"    { IF }
-  | "int"    { INT }
-  | "int16"    { INT16 }
-  | "int16s"    { INT16S }
-  | "int16u"    { INT16U }
-  | "int32"    { INT32 }
-  | "int64"    { INT64 }
-  | "int8"    { INT8 }
-  | "int8s"    { INT8S }
-  | "int8u"    { INT8U }
-  | "intoffloat"    { INTOFFLOAT }
-  | "intuoffloat"    { INTUOFFLOAT }
-  | "intoflong"   { INTOFLONG }
-  | "{"    { LBRACE }
-  | "{{"    { LBRACELBRACE }
-  | "["    { LBRACKET }
-  | "<"    { LESS }
-  | "<u"    { LESSU }
-  | "<l"    { LESSL }
-  | "<lu"    { LESSLU }
-  | "<f"    { LESSF }
-  | "<="    { LESSEQUAL }
-  | "<=u"    { LESSEQUALU }
-  | "<=f"    { LESSEQUALF }
-  | "<=l"    { LESSEQUALL }
-  | "<=lu"    { LESSEQUALLU }
-  | "<<"    { LESSLESS }
-  | "<<l"    { LESSLESSL }
-  | "long"    { LONG }
-  | "longofint" { LONGOFINT }
-  | "longofintu" { LONGOFINTU }
-  | "longoffloat" { LONGOFFLOAT }
-  | "longuoffloat" { LONGUOFFLOAT }
-  | "loop"    { LOOP }
-  | "("    { LPAREN }
-  | "match" { MATCH }
-  | "-"    { MINUS }
-  | "->"    { MINUSGREATER }
-  | "-f"    { MINUSF }
-  | "-s"    { MINUSS }
-  | "-l"    { MINUSL }
-  | "%"    { PERCENT }
-  | "%l"    { PERCENTL }
-  | "%lu"    { PERCENTLU }
-  | "%u"    { PERCENTU }
-  | "+"    { PLUS }
-  | "+f"    { PLUSF }
-  | "+s"    { PLUSS }
-  | "+l"    { PLUSL }
-  | "}"    { RBRACE }
-  | "}}"    { RBRACERBRACE }
-  | "]"    { RBRACKET }
-  | "readonly" { READONLY }
-  | "return"    { RETURN }
-  | "runtime"    { RUNTIME }
-  | ")"    { RPAREN }
-  | ";"    { SEMICOLON }
-  | "/"    { SLASH }
-  | "/f"    { SLASHF }
-  | "/s"    { SLASHS }
-  | "/l"    { SLASHL }
-  | "/lu"    { SLASHLU }
-  | "/u"    { SLASHU }
-  | "single" { SINGLE }
-  | "singleofint" { SINGLEOFINT }
-  | "stack"    { STACK }
-  | "*" { STAR }
-  | "*f"    { STARF }
-  | "*s"    { STARS }
-  | "*l"    { STARL }
-  | "switch"    { SWITCH }
-  | "switchl"    { SWITCHL }
-  | "tailcall"  { TAILCALL }
-  | "~"    { TILDE }
-  | "~l"    { TILDEL }
-  | "var"    { VAR }
-  | "void"    { VOID }
-  | "volatile" { VOLATILE }
-  | "while" { WHILE }
-
-  | intlit"LL"  { let s = Lexing.lexeme lexbuf in
-                LONGLIT(Int64.of_string(String.sub s 0 (String.length s - 2))) }
-  | intlit    { INTLIT(Int32.of_string(Lexing.lexeme lexbuf)) }
-  | floatlit     { FLOATLIT(float_of_string(Lexing.lexeme lexbuf)) }
-  | stringlit { let s = Lexing.lexeme lexbuf in
-                STRINGLIT(String.sub s 1 (String.length s - 2)) }
-  | ident | temp  { IDENT(Lexing.lexeme lexbuf) }
-  | qident    { let s = Lexing.lexeme lexbuf in
-                IDENT(String.sub s 1 (String.length s - 2)) }
-  | eof      { EOF }
-  | _        { raise(Error("illegal character `" ^ Char.escaped (Lexing.lexeme_char lexbuf 0) ^ "'")) }
-
-and comment = parse
-    "*/"     { () }
-  | eof      { raise(Error "unterminated comment") }
-  | _        { comment lexbuf }
diff --git a/backend/CMparser.mly b/backend/CMparser.mly
deleted file mode 100644
index 64943f0b..00000000
--- a/backend/CMparser.mly
+++ /dev/null
@@ -1,732 +0,0 @@
-/* *********************************************************************/
-/*                                                                     */
-/*              The Compcert verified compiler                         */
-/*                                                                     */
-/*          Xavier Leroy, INRIA Paris-Rocquencourt                     */
-/*                                                                     */
-/*  Copyright Institut National de Recherche en Informatique et en     */
-/*  Automatique.  All rights reserved.  This file is distributed       */
-/*  under the terms of the GNU General Public License as published by  */
-/*  the Free Software Foundation, either version 2 of the License, or  */
-/*  (at your option) any later version.  This file is also distributed */
-/*  under the terms of the INRIA Non-Commercial License Agreement.     */
-/*                                                                     */
-/* *********************************************************************/
-
-/* Note that this compiles a superset of the language defined by the AST,
-   including function calls in expressions, matches, while statements, etc. */
-
-%{
-open Datatypes
-open Camlcoq
-open BinNums
-open Integers
-open AST
-open Cminor
-
-(** Parsing external functions *)
-
-type ef_token =
-  | EFT_tok of string
-  | EFT_int of int32
-  | EFT_string of string
-  | EFT_chunk of memory_chunk
-
-let mkef sg toks =
-  match toks with
-  | [EFT_tok "extern"; EFT_string s] ->
-      EF_external(coqstring_of_camlstring s, sg)
-  | [EFT_tok "builtin"; EFT_string s] ->
-      EF_builtin(coqstring_of_camlstring s, sg)
-  | [EFT_tok "runtime"; EFT_string s] ->
-      EF_runtime(coqstring_of_camlstring s, sg)
-  | [EFT_tok "volatile"; EFT_tok "load"; EFT_chunk c] ->
-      EF_vload c
-  | [EFT_tok "volatile"; EFT_tok "store"; EFT_chunk c] ->
-      EF_vstore c
-  | [EFT_tok "malloc"] ->
-      EF_malloc
-  | [EFT_tok "free"] ->
-      EF_free
-  | [EFT_tok "memcpy"; EFT_tok "size"; EFT_int sz; EFT_tok "align"; EFT_int al] ->
-      EF_memcpy(Z.of_sint32 sz, Z.of_sint32 al)
-  | [EFT_tok "annot"; EFT_string txt] ->
-      EF_annot(coqstring_of_camlstring txt, sg.sig_args)
-  | [EFT_tok "annot_val"; EFT_string txt] ->
-      if sg.sig_args = [] then raise Parsing.Parse_error;
-      EF_annot_val(coqstring_of_camlstring txt, List.hd sg.sig_args)
-  | [EFT_tok "inline_asm"; EFT_string txt] ->
-      EF_inline_asm(coqstring_of_camlstring txt, sg, [])
-  | _ ->
-      raise Parsing.Parse_error
-
-(** Naming function calls in expressions *)
-
-type rexpr =
-  | Rvar of ident
-  | Rconst of constant
-  | Runop of unary_operation * rexpr
-  | Rbinop of binary_operation * rexpr * rexpr
-  | Rload of memory_chunk * rexpr
-  | Rcall of signature * rexpr * rexpr list
-  | Rbuiltin of signature * ef_token list * rexpr list
-
-let temp_counter = ref 0
-
-let temporaries = ref []
-
-let mktemp () =
-  incr temp_counter;
-  let n = Printf.sprintf "__t%d" !temp_counter in
-  let id = intern_string n in
-  temporaries := id :: !temporaries;
-  id
-
-let convert_accu = ref []
-
-let rec convert_rexpr = function
-  | Rvar id -> Evar id
-  | Rconst c -> Econst c
-  | Runop(op, e1) -> Eunop(op, convert_rexpr e1)
-  | Rbinop(op, e1, e2) ->
-      let c1 = convert_rexpr e1 in
-      let c2 = convert_rexpr e2 in
-      Ebinop(op, c1, c2)
-  | Rload(chunk, e1) -> Eload(chunk, convert_rexpr e1)
-  | Rcall(sg, e1, el) ->
-      let c1 = convert_rexpr e1 in
-      let cl = convert_rexpr_list el in
-      let t = mktemp() in
-      convert_accu := Scall(Some t, sg, c1, cl) :: !convert_accu;
-      Evar t
-  | Rbuiltin(sg, pef, el) ->
-      let ef = mkef sg pef in
-      let cl = convert_rexpr_list el in
-      let t = mktemp() in
-      convert_accu := Sbuiltin(Some t, ef, cl) :: !convert_accu;
-      Evar t
-
-and convert_rexpr_list = function
-  | [] -> []
-  | e1 :: el ->
-      let c1 = convert_rexpr e1 in
-      let cl = convert_rexpr_list el in
-      c1 :: cl
-
-let rec prepend_seq stmts last =
-  match stmts with
-  | [] -> last
-  | s1 :: sl -> prepend_seq sl (Sseq(s1, last))
-
-let mkeval e =
-  convert_accu := [];
-  match e with
-  | Rcall(sg, e1, el) ->
-      let c1 = convert_rexpr e1 in
-      let cl = convert_rexpr_list el in
-      prepend_seq !convert_accu (Scall(None, sg, c1, cl))
-  | Rbuiltin(sg, pef, el) ->
-      let ef = mkef sg pef in
-      let cl = convert_rexpr_list el in
-      prepend_seq !convert_accu (Sbuiltin(None, ef, cl))
-  | _ ->
-      ignore (convert_rexpr e);
-      prepend_seq !convert_accu Sskip
-
-let mkassign id e =
-  convert_accu := [];
-  match e with
-  | Rcall(sg, e1, el) ->
-      let c1 = convert_rexpr e1 in
-      let cl = convert_rexpr_list el in
-      prepend_seq !convert_accu (Scall(Some id, sg, c1, cl))
-  | Rbuiltin(sg, pef, el) ->
-      let ef = mkef sg pef in
-      let cl = convert_rexpr_list el in
-      prepend_seq !convert_accu (Sbuiltin(Some id, ef, cl))
-  | _ ->
-      let c = convert_rexpr e in
-      prepend_seq !convert_accu (Sassign(id, c))
-
-let mkstore chunk e1 e2 =
-  convert_accu := [];
-  let c1 = convert_rexpr e1 in
-  let c2 = convert_rexpr e2 in
-  prepend_seq !convert_accu (Sstore(chunk, c1, c2))
-
-let mkifthenelse e s1 s2 =
-  convert_accu := [];
-  let c = convert_rexpr e in
-  prepend_seq !convert_accu (Sifthenelse(c, s1, s2))
-
-let mkreturn_some e =
-  convert_accu := [];
-  let c = convert_rexpr e in
-  prepend_seq !convert_accu (Sreturn (Some c))
-
-let mktailcall sg e1 el =
-  convert_accu := [];
-  let c1 = convert_rexpr e1 in
-  let cl = convert_rexpr_list el in
-  prepend_seq !convert_accu (Stailcall(sg, c1, cl))
-
-let mkwhile expr body =
-  Sblock (Sloop (mkifthenelse expr body (Sexit O)))
-
-(** Other constructors *)
-
-let intconst n =
-  Rconst(Ointconst(coqint_of_camlint n))
-
-let longconst n =
-  Rconst(Olongconst(coqint_of_camlint64 n))
-
-let exitnum n = Nat.of_int32 n
-
-let mkswitch islong convert expr (cases, dfl) =
-  convert_accu := [];
-  let c = convert_rexpr expr in
-  let rec mktable = function
-  | [] -> []
-  | (key, exit) :: rem ->
-      (convert key, exitnum exit) :: mktable rem in
-  prepend_seq !convert_accu (Sswitch(islong, c, mktable cases, exitnum dfl))
-
-(***
-   match (a) { case 0: s0; case 1: s1; case 2: s2; }  --->
-
-   block {
-   block {
-   block {
-   block {
-     switch(a) { case 0: exit 0; case 1: exit 1; default: exit 2; }
-   }; s0; exit 2;
-   }; s1; exit 1;
-   }; s2;
-   }
-
-   Note that matches are assumed to be exhaustive
-***)
-
-let mkmatch_aux expr cases =
-  let ncases = List.length cases in
-  let rec mktable n = function
-    | [] -> assert false
-    | [key, action] -> []
-    | (key, action) :: rem ->
-        (coqint_of_camlint key, Nat.of_int n)
-        :: mktable (n + 1) rem in
-  let sw =
-    Sswitch(false, expr, mktable 0 cases, Nat.of_int (ncases - 1)) in
-  let rec mkblocks body n = function
-    | [] -> assert false
-    | [key, action] ->
-        Sblock(Sseq(body, action))
-    | (key, action) :: rem ->
-        mkblocks
-          (Sblock(Sseq(body, Sseq(action, Sexit (Nat.of_int n)))))
-          (n - 1)
-          rem in
-  mkblocks (Sblock sw) (ncases - 1) cases
-
-let mkmatch expr cases =
-  convert_accu := [];
-  let c = convert_rexpr expr in
-  let s =
-    match cases with
-    | [] -> Sskip (* ??? *)
-    | [key, action] -> action
-    | _ -> mkmatch_aux c cases in
-  prepend_seq !convert_accu s
-
-%}
-
-%token ABSF
-%token AMPERSAND
-%token AMPERSANDL
-%token BANG
-%token BANGEQUAL
-%token BANGEQUALF
-%token BANGEQUALU
-%token BANGEQUALL
-%token BANGEQUALLU
-%token BAR
-%token BARL
-%token BUILTIN
-%token CARET
-%token CARETL
-%token CASE
-%token COLON
-%token COMMA
-%token DEFAULT
-%token ELSE
-%token EQUAL
-%token EQUALEQUAL
-%token EQUALEQUALF
-%token EQUALEQUALU
-%token EQUALEQUALL
-%token EQUALEQUALLU
-%token EOF
-%token EXIT
-%token EXTERN
-%token FLOAT
-%token FLOAT32
-%token FLOAT64
-%token <float> FLOATLIT
-%token FLOATOFINT
-%token FLOATOFINTU
-%token FLOATOFLONG
-%token FLOATOFLONGU
-%token GOTO
-%token GREATER
-%token GREATERF
-%token GREATERU
-%token GREATERL
-%token GREATERLU
-%token GREATEREQUAL
-%token GREATEREQUALF
-%token GREATEREQUALU
-%token GREATEREQUALL
-%token GREATEREQUALLU
-%token GREATERGREATER
-%token GREATERGREATERU
-%token GREATERGREATERL
-%token GREATERGREATERLU
-%token <string> IDENT
-%token IF
-%token INT
-%token INT16
-%token INT16S
-%token INT16U
-%token INT32
-%token INT64
-%token INT8
-%token INT8S
-%token INT8U
-%token <int32> INTLIT
-%token INTOFFLOAT
-%token INTUOFFLOAT
-%token INTOFLONG
-%token LBRACE
-%token LBRACELBRACE
-%token LBRACKET
-%token LESS
-%token LESSU
-%token LESSF
-%token LESSL
-%token LESSLU
-%token LESSEQUAL
-%token LESSEQUALU
-%token LESSEQUALF
-%token LESSEQUALL
-%token LESSEQUALLU
-%token LESSLESS
-%token LESSLESSL
-%token LONG
-%token <int64> LONGLIT
-%token LONGOFINT
-%token LONGOFINTU
-%token LONGOFFLOAT
-%token LONGUOFFLOAT
-%token LOOP
-%token LPAREN
-%token MATCH
-%token MINUS
-%token MINUSF
-%token MINUSS
-%token MINUSL
-%token MINUSGREATER
-%token PERCENT
-%token PERCENTU
-%token PERCENTL
-%token PERCENTLU
-%token PLUS
-%token PLUSF
-%token PLUSS
-%token PLUSL
-%token RBRACE
-%token RBRACERBRACE
-%token RBRACKET
-%token READONLY
-%token RETURN
-%token RPAREN
-%token RUNTIME
-%token SEMICOLON
-%token SINGLE
-%token SINGLEOFINT
-%token SLASH
-%token SLASHF
-%token SLASHS
-%token SLASHU
-%token SLASHL
-%token SLASHLU
-%token STACK
-%token STAR
-%token STARF
-%token STARS
-%token STARL
-%token <string> STRINGLIT
-%token SWITCH
-%token SWITCHL
-%token TILDE
-%token TILDEL
-%token TAILCALL
-%token VAR
-%token VOID
-%token VOLATILE
-%token WHILE
-
-/* Precedences from low to high */
-%nonassoc p_THEN
-%nonassoc ELSE
-%left BAR BARL
-%left CARET CARETL
-%left AMPERSAND AMPERSANDL
-%left EQUALEQUAL BANGEQUAL LESS LESSEQUAL GREATER GREATEREQUAL EQUALEQUALU BANGEQUALU LESSU LESSEQUALU GREATERU GREATEREQUALU EQUALEQUALF BANGEQUALF LESSF LESSEQUALF GREATERF GREATEREQUALF EQUALEQUALL BANGEQUALL LESSL LESSEQUALL GREATERL GREATEREQUALL EQUALEQUALLU BANGEQUALLU LESSLU LESSEQUALLU GREATERLU GREATEREQUALLU
-%left LESSLESS GREATERGREATER GREATERGREATERU LESSLESSL GREATERGREATERL GREATERGREATERLU
-%left PLUS PLUSF PLUSS PLUSL MINUS MINUSF MINUSS MINUSL
-%left STAR SLASH PERCENT STARF STARS SLASHF SLASHS SLASHU PERCENTU STARL SLASHL SLASHLU PERCENTL PERCENTLU
-%nonassoc BANG TILDE TILDEL p_uminus ABSF INTOFFLOAT INTUOFFLOAT FLOATOFINT FLOATOFINTU SINGLEOFINT INT8S INT8U INT16S INT16U FLOAT32 FLOAT64 INTOFLONG LONGOFINT LONGOFINTU LONGOFFLOAT LONGUOFFLOAT FLOATOFLONG FLOATOFLONGU
-%left LPAREN
-
-/* Entry point */
-
-%start prog
-%type <Cminor.program> prog
-
-%%
-
-/* Programs */
-
-prog:
-   EQUAL STRINGLIT global_declarations EOF
-      { { prog_defs = List.rev $3;
-          prog_public = List.map fst $3;  (* FIXME *)
-          prog_main = intern_string $2; } }
-
-|  global_declarations EOF
-      { { prog_defs = List.rev $1;
-          prog_public = List.map fst $1;  (* FIXME *)
-          prog_main = intern_string "main" } }
-;
-
-global_declarations:
-    /* empty */                                 { [] }
-  | global_declarations global_declaration      { $2 :: $1 }
-;
-
-global_declaration:
-    proc
-      { $1 }
-  | VAR STRINGLIT LBRACKET INTLIT RBRACKET  /* old style */
-      { (intern_string $2,
-         Gvar{gvar_info = (); gvar_init = [Init_space(Z.of_sint32 $4)];
-              gvar_readonly = false; gvar_volatile = false}) }
-  | VAR STRINGLIT is_readonly is_volatile LBRACE init_data_list RBRACE
-       { (intern_string $2,
-          Gvar{gvar_info = (); gvar_init = List.rev $6;
-               gvar_readonly = $3; gvar_volatile = $4; } ) }
-;
-
-is_readonly:
-  /* empty */          { false }
-  | READONLY           { true }
-
-is_volatile:
-  /* empty */          { false }
-  |  VOLATILE          { true }
-
-init_data_list:
-    /* empty */                                 { [] }
-   | init_data_list_1                           { $1 }
- ;
-
-init_data_list_1:
-     init_data                                   { [$1] }
-   | init_data_list_1 COMMA init_data            { $3 :: $1 }
- ;
-
-init_data:
-     INT8 INTLIT                                 { Init_int8 (coqint_of_camlint $2) }
-   | INT16 INTLIT                                { Init_int16 (coqint_of_camlint $2) }
-   | INT32 INTLIT                                { Init_int32 (coqint_of_camlint $2) }
-   | INT INTLIT                                  { Init_int32 (coqint_of_camlint $2) }
-   | INTLIT                                      { Init_int32 (coqint_of_camlint $1) }
-   | LONGLIT                                     { Init_int64 (coqint_of_camlint64 $1) }
-   | INT64 LONGLIT                               { Init_int64 (coqint_of_camlint64 $2) }
-   | FLOAT32 FLOATLIT                            { Init_float32 (coqfloat_of_camlfloat $2) }
-   | FLOAT64 FLOATLIT                            { Init_float64 (coqfloat_of_camlfloat $2) }
-   | FLOAT FLOATLIT                              { Init_float64 (coqfloat_of_camlfloat $2) }
-   | FLOATLIT                                    { Init_float64 (coqfloat_of_camlfloat $1) }
-   | LBRACKET INTLIT RBRACKET                    { Init_space (Z.of_sint32 $2) }
-   | INTLIT LPAREN STRINGLIT RPAREN              { Init_addrof (intern_string $3, coqint_of_camlint $1) }
- ;
-
-/* Procedures */
-
-proc:
-    STRINGLIT LPAREN parameters RPAREN COLON signature
-    LBRACE
-      stack_declaration
-      var_declarations
-      stmt_list
-    RBRACE
-      { let tmp = !temporaries in
-        temporaries := [];
-        temp_counter := 0;
-        (intern_string $1,
-        Gfun(Internal { fn_sig = $6;
-                        fn_params = List.rev $3;
-                        fn_vars = List.rev (tmp @ $9);
-                        fn_stackspace = $8;
-                        fn_body = $10 })) }
-  | EXTERN STRINGLIT COLON signature
-      { (intern_string $2, Gfun(External(EF_external(coqstring_of_camlstring $2,$4)))) }
-  | EXTERN STRINGLIT EQUAL eftoks COLON signature
-      { (intern_string $2, Gfun(External(mkef $6 $4))) }
-;
-
-signature:
-    type_
-               { {sig_args = []; sig_res = Some $1; sig_cc = cc_default} }
-  | VOID
-               { {sig_args = []; sig_res = None; sig_cc = cc_default} }
-  | type_ MINUSGREATER signature
-               { let s = $3 in {s with sig_args = $1 :: s.sig_args} }
-;
-
-parameters:
-    /* empty */                                 { [] }
-  | parameter_list                              { $1 }
-;
-
-parameter_list:
-    IDENT                                       { intern_string $1 :: [] }
-  | parameter_list COMMA IDENT                  { intern_string $3 :: $1 }
-;
-
-stack_declaration:
-    /* empty */                                 { Z0 }
-  | STACK INTLIT SEMICOLON                      { Z.of_sint32 $2 }
-;
-
-var_declarations:
-    /* empty */                                 { [] }
-  | var_declarations var_declaration            { $2 @ $1 }
-;
-
-var_declaration:
-    VAR parameter_list SEMICOLON                { $2 }
-;
-
-/* Statements */
-
-stmt:
-    expr SEMICOLON                              { mkeval $1 }
-  | IDENT EQUAL expr SEMICOLON                  { mkassign (intern_string $1) $3 }
-  | memory_chunk LBRACKET expr RBRACKET EQUAL expr SEMICOLON
-                                                { mkstore $1 $3 $6 }
-  | IF LPAREN expr RPAREN stmts ELSE stmts      { mkifthenelse $3 $5 $7 }
-  | IF LPAREN expr RPAREN stmts %prec p_THEN    { mkifthenelse $3 $5 Sskip }
-  | LOOP stmts                                  { Sloop($2) }
-  | LBRACELBRACE stmt_list RBRACERBRACE         { Sblock($2) }
-  | EXIT SEMICOLON                              { Sexit O }
-  | EXIT INTLIT SEMICOLON                       { Sexit (exitnum $2) }
-  | RETURN SEMICOLON                            { Sreturn None }
-  | RETURN expr SEMICOLON                       { mkreturn_some $2 }
-  | SWITCH LPAREN expr RPAREN LBRACE switch_cases RBRACE
-                                         { mkswitch false Z.of_uint32 $3 $6 }
-  | SWITCHL LPAREN expr RPAREN LBRACE switchl_cases RBRACE
-                                         { mkswitch true Z.of_uint64 $3 $6 }
-  | MATCH LPAREN expr RPAREN LBRACE match_cases RBRACE
-                                                { mkmatch $3 $6 }
-  | TAILCALL expr LPAREN expr_list RPAREN COLON signature SEMICOLON
-                                                { mktailcall $7 $2 $4 }
-  | WHILE LPAREN expr RPAREN stmts              { mkwhile $3 $5 }
-  | IDENT COLON stmts                           { Slabel (intern_string $1,$3) }
-  | GOTO IDENT SEMICOLON                        { Sgoto(intern_string $2) }
-;
-
-stmts:
-    LBRACE stmt_list RBRACE                     { $2 }
-  | stmt                                        { $1 }
-;
-
-stmt_list:
-    /* empty */                                 { Sskip }
-  | stmt stmt_list                              { Sseq($1, $2) }
-;
-
-switch_cases:
-    DEFAULT COLON EXIT INTLIT SEMICOLON
-           { ([], $4) }
-  | CASE INTLIT COLON EXIT INTLIT SEMICOLON switch_cases
-           { let (cases, dfl) = $7 in (($2, $5) :: cases, dfl) }
-;
-
-switchl_cases:
-    DEFAULT COLON EXIT INTLIT SEMICOLON
-           { ([], $4) }
-  | CASE LONGLIT COLON EXIT INTLIT SEMICOLON switchl_cases
-           { let (cases, dfl) = $7 in (($2, $5) :: cases, dfl) }
-;
-
-match_cases:
-    /* empty */                                 { [] }
-  | CASE INTLIT COLON stmt_list match_cases     { ($2, $4) :: $5 }
-;
-
-/* Expressions */
-
-expr:
-    LPAREN expr RPAREN                          { $2 }
-  | IDENT                                       { Rvar(intern_string $1) }
-  | INTLIT                                      { intconst $1 }
-  | LONGLIT                                     { longconst $1 }
-  | FLOATLIT                                    { Rconst(Ofloatconst (coqfloat_of_camlfloat $1)) }
-  | STRINGLIT                                   { Rconst(Oaddrsymbol(intern_string $1, Int.zero)) }
-  | AMPERSAND INTLIT                            { Rconst(Oaddrstack(coqint_of_camlint $2)) }
-  | MINUS expr    %prec p_uminus                { Runop(Onegint, $2) }
-  | MINUSF expr   %prec p_uminus                { Runop(Onegf, $2) }
-  | MINUSS expr   %prec p_uminus                { Runop(Onegfs, $2) }
-  | ABSF expr                                   { Runop(Oabsf, $2) }
-  | INTOFFLOAT expr                             { Runop(Ointoffloat, $2) }
-  | INTUOFFLOAT expr                            { Runop(Ointuoffloat, $2) }
-  | FLOATOFINT expr                             { Runop(Ofloatofint, $2) }
-  | SINGLEOFINT expr                            { Runop(Osingleofint, $2) }
-  | FLOATOFINTU expr                            { Runop(Ofloatofintu, $2) }
-  | TILDE expr                                  { Runop(Onotint, $2) }
-  | BANG expr                                   { Rbinop(Ocmpu Ceq, $2, intconst 0l) }
-  | INT8S expr                                  { Runop(Ocast8signed, $2) }
-  | INT8U expr                                  { Runop(Ocast8unsigned, $2) }
-  | INT16S expr                                 { Runop(Ocast16signed, $2) }
-  | INT16U expr                                 { Runop(Ocast16unsigned, $2) }
-  | FLOAT32 expr                                { Runop(Osingleoffloat, $2) }
-  | FLOAT64 expr                                { Runop(Ofloatofsingle, $2) }
-  | MINUSL expr %prec p_uminus                  { Runop(Onegl, $2) }
-  | TILDEL expr                                 { Runop(Onotl, $2) }
-  | INTOFLONG expr                              { Runop(Ointoflong, $2) }
-  | LONGOFINT expr                              { Runop(Olongofint, $2) }
-  | LONGOFINTU expr                             { Runop(Olongofintu, $2) }
-  | LONGOFFLOAT expr                            { Runop(Olongoffloat, $2) }
-  | LONGUOFFLOAT expr                           { Runop(Olonguoffloat, $2) }
-  | FLOATOFLONG expr                            { Runop(Ofloatoflong, $2) }
-  | FLOATOFLONGU expr                           { Runop(Ofloatoflongu, $2) }
-  | expr PLUS expr                              { Rbinop(Oadd, $1, $3) }
-  | expr MINUS expr                             { Rbinop(Osub, $1, $3) }
-  | expr STAR expr                              { Rbinop(Omul, $1, $3) }
-  | expr SLASH expr                             { Rbinop(Odiv, $1, $3) }
-  | expr PERCENT expr                           { Rbinop(Omod, $1, $3) }
-  | expr SLASHU expr                            { Rbinop(Odivu, $1, $3) }
-  | expr PERCENTU expr                          { Rbinop(Omodu, $1, $3) }
-  | expr AMPERSAND expr                         { Rbinop(Oand, $1, $3) }
-  | expr BAR expr                               { Rbinop(Oor, $1, $3) }
-  | expr CARET expr                             { Rbinop(Oxor, $1, $3) }
-  | expr LESSLESS expr                          { Rbinop(Oshl, $1, $3) }
-  | expr GREATERGREATER expr                    { Rbinop(Oshr, $1, $3) }
-  | expr GREATERGREATERU expr                   { Rbinop(Oshru, $1, $3) }
-  | expr PLUSL expr                             { Rbinop(Oaddl, $1, $3) }
-  | expr MINUSL expr                            { Rbinop(Osubl, $1, $3) }
-  | expr STARL expr                             { Rbinop(Omull, $1, $3) }
-  | expr SLASHL expr                            { Rbinop(Odivl, $1, $3) }
-  | expr PERCENTL expr                          { Rbinop(Omodl, $1, $3) }
-  | expr SLASHLU expr                           { Rbinop(Odivlu, $1, $3) }
-  | expr PERCENTLU expr                         { Rbinop(Omodlu, $1, $3) }
-  | expr AMPERSANDL expr                        { Rbinop(Oandl, $1, $3) }
-  | expr BARL expr                              { Rbinop(Oorl, $1, $3) }
-  | expr CARETL expr                            { Rbinop(Oxorl, $1, $3) }
-  | expr LESSLESSL expr                         { Rbinop(Oshll, $1, $3) }
-  | expr GREATERGREATERL expr                   { Rbinop(Oshrl, $1, $3) }
-  | expr GREATERGREATERLU expr                  { Rbinop(Oshrlu, $1, $3) }
-  | expr PLUSF expr                             { Rbinop(Oaddf, $1, $3) }
-  | expr PLUSS expr                             { Rbinop(Oaddfs, $1, $3) }
-  | expr MINUSF expr                            { Rbinop(Osubf, $1, $3) }
-  | expr MINUSS expr                            { Rbinop(Osubfs, $1, $3) }
-  | expr STARF expr                             { Rbinop(Omulf, $1, $3) }
-  | expr STARS expr                             { Rbinop(Omulfs, $1, $3) }
-  | expr SLASHF expr                            { Rbinop(Odivf, $1, $3) }
-  | expr SLASHS expr                            { Rbinop(Odivfs, $1, $3) }
-  | expr EQUALEQUAL expr                        { Rbinop(Ocmp Ceq, $1, $3) }
-  | expr BANGEQUAL expr                         { Rbinop(Ocmp Cne, $1, $3) }
-  | expr LESS expr                              { Rbinop(Ocmp Clt, $1, $3) }
-  | expr LESSEQUAL expr                         { Rbinop(Ocmp Cle, $1, $3) }
-  | expr GREATER expr                           { Rbinop(Ocmp Cgt, $1, $3) }
-  | expr GREATEREQUAL expr                      { Rbinop(Ocmp Cge, $1, $3) }
-  | expr EQUALEQUALU expr                       { Rbinop(Ocmpu Ceq, $1, $3) }
-  | expr BANGEQUALU expr                        { Rbinop(Ocmpu Cne, $1, $3) }
-  | expr LESSU expr                             { Rbinop(Ocmpu Clt, $1, $3) }
-  | expr LESSEQUALU expr                        { Rbinop(Ocmpu Cle, $1, $3) }
-  | expr GREATERU expr                          { Rbinop(Ocmpu Cgt, $1, $3) }
-  | expr GREATEREQUALU expr                     { Rbinop(Ocmpu Cge, $1, $3) }
-  | expr EQUALEQUALL expr                       { Rbinop(Ocmpl Ceq, $1, $3) }
-  | expr BANGEQUALL expr                        { Rbinop(Ocmpl Cne, $1, $3) }
-  | expr LESSL expr                             { Rbinop(Ocmpl Clt, $1, $3) }
-  | expr LESSEQUALL expr                        { Rbinop(Ocmpl Cle, $1, $3) }
-  | expr GREATERL expr                          { Rbinop(Ocmpl Cgt, $1, $3) }
-  | expr GREATEREQUALL expr                     { Rbinop(Ocmpl Cge, $1, $3) }
-  | expr EQUALEQUALLU expr                      { Rbinop(Ocmplu Ceq, $1, $3) }
-  | expr BANGEQUALLU expr                       { Rbinop(Ocmplu Cne, $1, $3) }
-  | expr LESSLU expr                            { Rbinop(Ocmplu Clt, $1, $3) }
-  | expr LESSEQUALLU expr                       { Rbinop(Ocmplu Cle, $1, $3) }
-  | expr GREATERLU expr                         { Rbinop(Ocmplu Cgt, $1, $3) }
-  | expr GREATEREQUALLU expr                    { Rbinop(Ocmplu Cge, $1, $3) }
-  | expr EQUALEQUALF expr                       { Rbinop(Ocmpf Ceq, $1, $3) }
-  | expr BANGEQUALF expr                        { Rbinop(Ocmpf Cne, $1, $3) }
-  | expr LESSF expr                             { Rbinop(Ocmpf Clt, $1, $3) }
-  | expr LESSEQUALF expr                        { Rbinop(Ocmpf Cle, $1, $3) }
-  | expr GREATERF expr                          { Rbinop(Ocmpf Cgt, $1, $3) }
-  | expr GREATEREQUALF expr                     { Rbinop(Ocmpf Cge, $1, $3) }
-  | memory_chunk LBRACKET expr RBRACKET         { Rload($1, $3) }
-  | expr LPAREN expr_list RPAREN COLON signature{ Rcall($6, $1, $3) }
-  | BUILTIN eftoks LPAREN expr_list RPAREN COLON signature{ Rbuiltin($7, $2, $4) }
-;
-
-expr_list:
-    /* empty */                                 { [] }
-  | expr_list_1                                 { $1 }
-;
-
-expr_list_1:
-    expr                                        { $1 :: [] }
-  | expr COMMA expr_list_1                      { $1 :: $3 }
-;
-
-memory_chunk:
-    INT8S                                       { Mint8signed }
-  | INT8U                                       { Mint8unsigned }
-  | INT16S                                      { Mint16signed }
-  | INT16U                                      { Mint16unsigned }
-  | INT32                                       { Mint32 }
-  | INT64                                       { Mint64 }
-  | INT                                         { Mint32 }
-  | FLOAT32                                     { Mfloat32 }
-  | FLOAT64                                     { Mfloat64 }
-  | FLOAT                                       { Mfloat64 }
-;
-
-/* Types */
-
-type_:
-    INT                                         { Tint }
-  | FLOAT                                       { Tfloat }
-  | LONG                                        { Tlong }
-  | SINGLE                                      { Tsingle }
-;
-
-/* External functions */
-
-eftok:
-    IDENT                                       { EFT_tok $1 }
-  | STRINGLIT                                   { EFT_string $1 }
-  | INTLIT                                      { EFT_int $1 }
-  | VOLATILE                                    { EFT_tok "volatile" }
-  | EXTERN                                      { EFT_tok "extern" }
-  | BUILTIN                                     { EFT_tok "builtin" }
-  | RUNTIME                                     { EFT_tok "runtime" }
-  | memory_chunk                                { EFT_chunk $1 }
-;
-
-eftoks:
-    eftok eftoks                                { $1 :: $2 }
-  | /*empty*/                                   { [] }
-;
diff --git a/backend/CMtypecheck.ml b/backend/CMtypecheck.ml
deleted file mode 100644
index cd0d25dc..00000000
--- a/backend/CMtypecheck.ml
+++ /dev/null
@@ -1,350 +0,0 @@
-(* *********************************************************************)
-(*                                                                     *)
-(*              The Compcert verified compiler                         *)
-(*                                                                     *)
-(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
-(*                                                                     *)
-(*  Copyright Institut National de Recherche en Informatique et en     *)
-(*  Automatique.  All rights reserved.  This file is distributed       *)
-(*  under the terms of the GNU General Public License as published by  *)
-(*  the Free Software Foundation, either version 2 of the License, or  *)
-(*  (at your option) any later version.  This file is also distributed *)
-(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
-(*                                                                     *)
-(* *********************************************************************)
-
-(* A type-checker for Cminor *)
-
-(* FIXME: proper support for type Tsingle *)
-
-open Printf
-open Camlcoq
-open AST
-open PrintAST
-open Cminor
-
-exception Error of string
-
-type ty = Base of typ | Var of ty option ref
-
-let newvar () = Var (ref None)
-let tint = Base Tint
-let tfloat = Base Tfloat
-let tlong = Base Tlong
-let tsingle = Base Tsingle
-let tany32 = Base Tany32
-let tany64 = Base Tany64
-
-let ty_of_typ = function
-  | Tint -> tint
-  | Tfloat -> tfloat
-  | Tlong -> tlong
-  | Tsingle -> tsingle
-  | Tany32 -> tany32
-  | Tany64 -> tany64
-
-let ty_of_sig_args tyl = List.map ty_of_typ tyl
-
-let rec repr t =
-  match t with
-  | Base _ -> t
-  | Var r -> match !r with None -> t | Some t' -> repr t'
-
-let unify t1 t2 =
-  match (repr t1, repr t2) with
-  | Base b1, Base b2 ->
-      if b1 <> b2 then
-        raise (Error (sprintf "Expected type %s, actual type %s\n"
-                              (name_of_type b1) (name_of_type b2)))
-  | Base b, Var r -> r := Some (Base b)
-  | Var r, Base b -> r := Some (Base b)
-  | Var r1, Var r2 -> if r1 != r2 then r1 := Some (Var r2)
-
-let unify_list l1 l2 =
-  let ll1 = List.length l1 and ll2 = List.length l2 in
-  if ll1 <> ll2 then
-    raise (Error (sprintf "Arity mismatch: expected %d, actual %d\n" ll1 ll2));
-  List.iter2 unify l1 l2
-
-let type_var env id =
-  try
-    List.assoc id env
-  with Not_found ->
-    raise (Error (sprintf "Unbound variable %s\n" (extern_atom id)))
-
-let type_constant = function
-  | Ointconst _ -> tint
-  | Ofloatconst _ -> tfloat
-  | Osingleconst _ -> tsingle
-  | Olongconst _ -> tlong
-  | Oaddrsymbol _ -> tint
-  | Oaddrstack _ -> tint
-
-let type_unary_operation = function
-  | Ocast8signed -> tint, tint
-  | Ocast16signed -> tint, tint
-  | Ocast8unsigned -> tint, tint
-  | Ocast16unsigned -> tint, tint
-  | Onegint -> tint, tint
-  | Onotint -> tint, tint
-  | Onegf -> tfloat, tfloat
-  | Oabsf -> tfloat, tfloat
-  | Onegfs -> tsingle, tsingle
-  | Oabsfs -> tsingle, tsingle
-  | Osingleoffloat -> tfloat, tsingle
-  | Ofloatofsingle -> tsingle, tfloat
-  | Ointoffloat -> tfloat, tint
-  | Ointuoffloat -> tfloat, tint
-  | Ofloatofint -> tint, tfloat
-  | Ofloatofintu -> tint, tfloat
-  | Ointofsingle -> tsingle, tint
-  | Ointuofsingle -> tsingle, tint
-  | Osingleofint -> tint, tsingle
-  | Osingleofintu -> tint, tsingle
-  | Onegl -> tlong, tlong
-  | Onotl -> tlong, tlong
-  | Ointoflong -> tlong, tint
-  | Olongofint -> tint, tlong
-  | Olongofintu -> tint, tlong
-  | Olongoffloat -> tfloat, tlong
-  | Olonguoffloat -> tfloat, tlong
-  | Ofloatoflong -> tlong, tfloat
-  | Ofloatoflongu -> tlong, tfloat
-  | Olongofsingle -> tsingle, tlong
-  | Olonguofsingle -> tsingle, tlong
-  | Osingleoflong -> tlong, tfloat
-  | Osingleoflongu -> tlong, tfloat
-
-let type_binary_operation = function
-  | Oadd -> tint, tint, tint
-  | Osub -> tint, tint, tint
-  | Omul -> tint, tint, tint
-  | Odiv -> tint, tint, tint
-  | Odivu -> tint, tint, tint
-  | Omod -> tint, tint, tint
-  | Omodu -> tint, tint, tint
-  | Oand -> tint, tint, tint
-  | Oor -> tint, tint, tint
-  | Oxor -> tint, tint, tint
-  | Oshl -> tint, tint, tint
-  | Oshr -> tint, tint, tint
-  | Oshru -> tint, tint, tint
-  | Oaddf -> tfloat, tfloat, tfloat
-  | Osubf -> tfloat, tfloat, tfloat
-  | Omulf -> tfloat, tfloat, tfloat
-  | Odivf -> tfloat, tfloat, tfloat
-  | Oaddfs -> tsingle, tsingle, tsingle
-  | Osubfs -> tsingle, tsingle, tsingle
-  | Omulfs -> tsingle, tsingle, tsingle
-  | Odivfs -> tsingle, tsingle, tsingle
-  | Oaddl -> tlong, tlong, tlong
-  | Osubl -> tlong, tlong, tlong
-  | Omull -> tlong, tlong, tlong
-  | Odivl -> tlong, tlong, tlong
-  | Odivlu -> tlong, tlong, tlong
-  | Omodl -> tlong, tlong, tlong
-  | Omodlu -> tlong, tlong, tlong
-  | Oandl -> tlong, tlong, tlong
-  | Oorl -> tlong, tlong, tlong
-  | Oxorl -> tlong, tlong, tlong
-  | Oshll -> tlong, tint, tlong
-  | Oshrl -> tlong, tint, tlong
-  | Oshrlu -> tlong, tint, tlong
-  | Ocmp _ -> tint, tint, tint
-  | Ocmpu _ -> tint, tint, tint
-  | Ocmpf _ -> tfloat, tfloat, tint
-  | Ocmpfs _ -> tsingle, tsingle, tint
-  | Ocmpl _ -> tlong, tlong, tint
-  | Ocmplu _ -> tlong, tlong, tint
-
-let name_of_unary_operation = PrintCminor.name_of_unop
-
-let name_of_binary_operation = PrintCminor.name_of_binop
-
-let type_chunk = function
-  | Mint8signed -> tint
-  | Mint8unsigned -> tint
-  | Mint16signed -> tint
-  | Mint16unsigned -> tint
-  | Mint32 -> tint
-  | Mint64 -> tlong
-  | Mfloat32 -> tsingle
-  | Mfloat64 -> tfloat
-  | Many32 -> tany32
-  | Many64 -> tany64
-
-let name_of_chunk = PrintAST.name_of_chunk
-
-let rec type_expr env lenv e =
-  match e with
-  | Evar id ->
-      type_var env id
-  | Econst cst ->
-      type_constant cst
-  | Eunop(op, e1) ->
-      let te1 = type_expr env lenv e1 in
-      let (targ, tres) = type_unary_operation op in
-      begin try
-        unify targ te1
-      with Error s ->
-        raise (Error (sprintf "In application of operator %s:\n%s"
-                              (name_of_unary_operation op) s))
-      end;
-      tres
-  | Ebinop(op, e1, e2) ->
-      let te1 = type_expr env lenv e1 in
-      let te2 = type_expr env lenv e2 in
-      let (targ1, targ2, tres) = type_binary_operation op in
-      begin try
-        unify targ1 te1; unify targ2 te2
-      with Error s ->
-        raise (Error (sprintf "In application of operator %s:\n%s"
-                              (name_of_binary_operation op) s))
-      end;
-      tres
-  | Eload(chunk, e) ->
-      let te = type_expr env lenv e in
-      begin try
-        unify tint te
-      with Error s ->
-        raise (Error (sprintf "In load %s:\n%s"
-                              (name_of_chunk chunk) s))
-      end;
-      type_chunk chunk
-
-and type_exprlist env lenv el =
-  match el with
-  | [] -> []
-  | e1 :: et ->
-      let te1 = type_expr env lenv e1 in
-      let tet = type_exprlist env lenv et in
-      (te1 :: tet)
-
-and type_condexpr env lenv e =
-  let te = type_expr env lenv e in
-  begin try
-    unify tint te
-  with Error s ->
-    raise (Error (sprintf "In condition:\n%s" s))
-  end
-
-let rec type_stmt env blk ret s =
-  match s with
-  | Sskip -> ()
-  | Sassign(id, e1) ->
-      let tid = type_var env id in
-      let te1 = type_expr env [] e1 in
-      begin try
-        unify tid te1
-      with Error s ->
-        raise (Error (sprintf "In assignment to %s:\n%s" (extern_atom id) s))
-      end
-  | Sstore(chunk, e1, e2) ->
-      let te1 = type_expr env [] e1 in
-      let te2 = type_expr env [] e2 in
-      begin try
-        unify tint te1;
-        unify (type_chunk chunk) te2
-      with Error s ->
-        raise (Error (sprintf "In store %s:\n%s"
-                              (name_of_chunk chunk) s))
-      end
-  | Scall(optid, sg, e1, el) ->
-      let te1 = type_expr env [] e1 in
-      let tel = type_exprlist env [] el in
-      begin try
-        unify tint te1;
-        unify_list (ty_of_sig_args sg.sig_args) tel;
-        let ty_res =
-          match sg.sig_res with
-          | None -> tint (*???*)
-          | Some t -> ty_of_typ t in
-        begin match optid with
-        | None -> ()
-        | Some id -> unify (type_var env id) ty_res
-        end
-      with Error s ->
-        raise (Error (sprintf "In call:\n%s" s))
-      end
-  | Sbuiltin(optid, ef, el) ->
-      let sg = ef_sig ef in
-      let tel = type_exprlist env [] el in
-      begin try
-        unify_list (ty_of_sig_args sg.sig_args) tel;
-        let ty_res =
-          match sg.sig_res with
-          | None -> tint (*???*)
-          | Some t -> ty_of_typ t in
-        begin match optid with
-        | None -> ()
-        | Some id -> unify (type_var env id) ty_res
-        end
-      with Error s ->
-        raise (Error (sprintf "In builtin call:\n%s" s))
-      end
-  | Sseq(s1, s2) ->
-      type_stmt env blk ret s1;
-      type_stmt env blk ret s2
-  | Sifthenelse(ce, s1, s2) ->
-      type_condexpr env [] ce;
-      type_stmt env blk ret s1;
-      type_stmt env blk ret s2
-  | Sloop s1 ->
-      type_stmt env blk ret s1
-  | Sblock s1 ->
-      type_stmt env (blk + 1) ret s1
-  | Sexit n ->
-      if Nat.to_int n >= blk then
-        raise (Error (sprintf "Bad exit(%d)\n" (Nat.to_int n)))
-  | Sswitch(islong, e, cases, deflt) ->
-      unify (type_expr env [] e) (if islong then tlong else tint)
-  | Sreturn None ->
-      begin match ret with
-      | None -> ()
-      | Some tret -> raise (Error ("return without argument"))
-      end
-  | Sreturn (Some e) ->
-      begin match ret with
-      | None -> raise (Error "return with argument")
-      | Some tret ->
-          begin try
-            unify (type_expr env [] e) (ty_of_typ tret)
-          with Error s ->
-            raise (Error (sprintf "In return:\n%s" s))
-          end
-      end
-  | Stailcall(sg, e1, el) ->
-      let te1 = type_expr env [] e1 in
-      let tel = type_exprlist env [] el in
-      begin try
-        unify tint te1;
-        unify_list (ty_of_sig_args sg.sig_args) tel
-      with Error s ->
-        raise (Error (sprintf "In tail call:\n%s" s))
-      end
-  | Slabel(lbl, s1) ->
-      type_stmt env blk ret s1
-  | Sgoto lbl ->
-      ()
-
-let rec env_of_vars idl =
-  match idl with
-  | [] -> []
-  | id1 :: idt -> (id1, newvar()) :: env_of_vars idt
-
-let type_function id f =
-  try
-    type_stmt
-       (env_of_vars f.fn_vars @ env_of_vars f.fn_params)
-       0 f.fn_sig.sig_res f.fn_body
-  with Error s ->
-    raise (Error (sprintf "In function %s:\n%s" (extern_atom id) s))
-
-let type_globdef (id, gd) =
-  match gd with
-  | Gfun(Internal f) -> type_function id f
-  | Gfun(External ef) -> ()
-  | Gvar v -> ()
-
-let type_program p =
-  List.iter type_globdef p.prog_defs; p
diff --git a/backend/CMtypecheck.mli b/backend/CMtypecheck.mli
deleted file mode 100644
index 44c76544..00000000
--- a/backend/CMtypecheck.mli
+++ /dev/null
@@ -1,19 +0,0 @@
-(* *********************************************************************)
-(*                                                                     *)
-(*              The Compcert verified compiler                         *)
-(*                                                                     *)
-(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
-(*                                                                     *)
-(*  Copyright Institut National de Recherche en Informatique et en     *)
-(*  Automatique.  All rights reserved.  This file is distributed       *)
-(*  under the terms of the GNU General Public License as published by  *)
-(*  the Free Software Foundation, either version 2 of the License, or  *)
-(*  (at your option) any later version.  This file is also distributed *)
-(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
-(*                                                                     *)
-(* *********************************************************************)
-
-exception Error of string
-
-val type_program: Cminor.program -> Cminor.program
-
diff --git a/driver/Driver.ml b/driver/Driver.ml
index 1a6c47d5..6a4970eb 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -74,49 +74,6 @@ let compile_c_file sourcename ifile ofile =
   let ast = parse_c_file sourcename ifile in
   compile_c_ast sourcename ast ofile
 
-(* From Cminor to asm *)
-
-let compile_cminor_file ifile ofile =
-  (* Prepare to dump RTL, Mach, etc, if requested *)
-  let set_dest dst opt ext =
-    dst := if !opt then Some (output_filename ifile ".cm" ext)
-                   else None in
-  set_dest PrintRTL.destination option_drtl ".rtl";
-  set_dest Regalloc.destination_alloctrace option_dalloctrace ".alloctrace";
-  set_dest PrintLTL.destination option_dltl ".ltl";
-  set_dest PrintMach.destination option_dmach ".mach";
-  Sections.initialize();
-  let ic = open_in ifile in
-  let lb = Lexing.from_channel ic in
-  (* Parse cminor *)
-  let cm =
-    try CMtypecheck.type_program (CMparser.prog CMlexer.token lb)
-    with Parsing.Parse_error ->
-           eprintf "File %s, character %d: Syntax error\n"
-                   ifile (Lexing.lexeme_start lb);
-           exit 2
-       | CMlexer.Error msg ->
-           eprintf "File %s, character %d: %s\n"
-                   ifile (Lexing.lexeme_start lb) msg;
-           exit 2
-       | CMtypecheck.Error msg ->
-           eprintf "File %s, type-checking error:\n%s"
-                   ifile msg;
-           exit 2 in
-  (* Convert to Asm *)
-  let asm =
-    match Compiler.apply_partial
-               (Compiler.transf_cminor_program cm)
-               Asmexpand.expand_program with
-    | Errors.OK asm ->
-        asm
-    | Errors.Error msg ->
-        eprintf "%s: %a" ifile print_error msg;
-        exit 2 in
-  (* Print Asm in text form *)
-  let oc = open_out ofile in
-  PrintAsm.print_program oc asm;
-  close_out oc
 
 (* Processing of a .c file *)
 
@@ -185,25 +142,6 @@ let process_i_file sourcename =
     objname
   end
 
-(* Processing of a .cm file *)
-
-let process_cminor_file sourcename =
-  ensure_inputfile_exists sourcename;
-  if !option_S then begin
-    compile_cminor_file sourcename
-                        (output_filename ~final:true sourcename ".cm" ".s");
-    ""
-  end else begin
-    let asmname =
-      if !option_dasm
-      then output_filename sourcename ".cm" ".s"
-      else Filename.temp_file "compcert" ".s" in
-    compile_cminor_file sourcename asmname;
-    let objname = output_filename ~final: !option_c sourcename ".cm" ".o" in
-    assemble asmname objname;
-    if not !option_dasm then safe_remove asmname;
-    objname
-  end
 
 (* Processing of .S and .s files *)
 
@@ -259,7 +197,6 @@ let usage_string =
 Recognized source files:
   .c             C source file
   .i or .p       C source file that should not be preprocessed
-  .cm            Cminor source file
   .s             Assembly file
   .S or .sx      Assembly file that must be preprocessed
   .o             Object file
@@ -485,8 +422,6 @@ let cmdline_actions =
       push_action process_i_file s; incr num_source_files; incr num_input_files);
   Suffix ".p", Self (fun s ->
       push_action process_i_file s; incr num_source_files; incr num_input_files);
-  Suffix ".cm", Self (fun s ->
-      push_action process_cminor_file s; incr num_source_files; incr num_input_files);
   Suffix ".s", Self (fun s ->
       push_action process_s_file s; incr num_source_files; incr num_input_files);
   Suffix ".S", Self (fun s ->