checklink: first import of Valentin Robert's validator for asm and link

cparser: renamed Errors to Cerrors; removed packing into Cparser.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1856 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

5 files changed, 11 insertions, 40 deletions

diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index 6386445..508c414 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -15,12 +15,9 @@
 
 open Printf
 
-module CompcertErrors = Errors (* avoid shadowing by Cparser.Errors *)
-
-open Cparser
-open Cparser.C
-open Cparser.Env
-open Cparser.Builtins
+open C
+open Env
+open Builtins
 
 open Camlcoq
 open AST
@@ -222,12 +219,12 @@ let make_builtin_memcpy args =
   | Econs(dst, Econs(src, Econs(sz, Econs(al, Enil)))) ->
       let sz1 =
         match Initializers.constval sz with
-        | CompcertErrors.OK(Vint n) -> camlint_of_coqint n
+        | Errors.OK(Vint n) -> camlint_of_coqint n
         | _ -> error "ill-formed __builtin_memcpy_aligned (3rd argument must be 
 a constant)"; 0l in
       let al1 =
         match Initializers.constval al with
-        | CompcertErrors.OK(Vint n) -> camlint_of_coqint n
+        | Errors.OK(Vint n) -> camlint_of_coqint n
         | _ -> error "ill-formed __builtin_memcpy_aligned (4th argument must be 
 a constant)"; 0l in
       let fn = register_inlined_memcpy sz1 al1 in
@@ -249,7 +246,7 @@ let convertAttr a = List.mem AVolatile a
 
 let convertIkind = function
   | C.IBool -> (Unsigned, IBool)
-  | C.IChar -> ((if (!Cparser.Machine.config).Cparser.Machine.char_signed
+  | C.IChar -> ((if (!Machine.config).Machine.char_signed
                  then Signed else Unsigned), I8)
   | C.ISChar -> (Signed, I8)
   | C.IUChar -> (Unsigned, I8)
@@ -725,9 +722,9 @@ let convertFundecl env (sto, id, ty, optinit) =
 
 let string_of_errmsg msg =
   let string_of_err = function
-  | CompcertErrors.MSG s -> camlstring_of_coqstring s
-  | CompcertErrors.CTX i -> extern_atom i
-  | CompcertErrors.CTXL i -> "" (* should not happen *)
+  | Errors.MSG s -> camlstring_of_coqstring s
+  | Errors.CTX i -> extern_atom i
+  | Errors.CTXL i -> "" (* should not happen *)
   in String.concat "" (List.map string_of_err msg)
 
 let rec convertInit env init =
@@ -749,8 +746,8 @@ and convertInitList env il =
 let convertInitializer env ty i =
   match Initializers.transl_init (convertTyp env ty) (convertInit env i)
   with
-  | CompcertErrors.OK init -> init
-  | CompcertErrors.Error msg ->
+  | Errors.OK init -> init
+  | Errors.Error msg ->
       error (sprintf "Initializer is not a compile-time constant (%s)"
                      (string_of_errmsg msg)); []
 
diff --git a/cfrontend/CPragmas.ml b/cfrontend/CPragmas.ml
index 4b4c0f1..63bd3f9 100644
--- a/cfrontend/CPragmas.ml
+++ b/cfrontend/CPragmas.ml
@@ -17,7 +17,6 @@
 
 open Printf
 open Camlcoq
-open Cparser
 
 (* #pragma section *)
 
diff --git a/cfrontend/Cparser.mllib b/cfrontend/Cparser.mllib
deleted file mode 100644
index e942137..0000000
--- a/cfrontend/Cparser.mllib
+++ /dev/null
@@ -1 +0,0 @@
-Cparser
diff --git a/cfrontend/Cparser.mlpack b/cfrontend/Cparser.mlpack
deleted file mode 100644
index b59e30f..0000000
--- a/cfrontend/Cparser.mlpack
+++ /dev/null
@@ -1,23 +0,0 @@
-cparser/C
-cparser/Errors
-cparser/Cabs
-cparser/Cabshelper
-cparser/Parse_aux
-cparser/Parser
-cparser/Lexer
-cparser/Machine
-cparser/Env
-cparser/Cprint
-cparser/Cutil
-cparser/Ceval
-cparser/Cleanup
-cparser/Builtins
-cparser/Elab
-cparser/Rename
-cparser/Transform
-cparser/Unblock
-cparser/StructReturn
-cparser/Bitfields
-cparser/PackedStructs
-cparser/Parse
-
diff --git a/cfrontend/libCparser.clib b/cfrontend/libCparser.clib
deleted file mode 100644
index 1b55150..0000000
--- a/cfrontend/libCparser.clib
+++ /dev/null
@@ -1 +0,0 @@
-cparser/uint64.o