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

11 files changed, 36 insertions, 14 deletions

diff --git a/cparser/Errors.ml b/cparser/Cerrors.ml
index 188531e..188531e 100644
--- a/cparser/Errors.ml
+++ b/cparser/Cerrors.ml
diff --git a/cparser/Errors.mli b/cparser/Cerrors.mli
index 557fb14..557fb14 100644
--- a/cparser/Errors.mli
+++ b/cparser/Cerrors.mli
diff --git a/cparser/Cparser.mllib b/cparser/Cparser.mllib
new file mode 100644
index 0000000..c5dc513
--- /dev/null
+++ b/cparser/Cparser.mllib
@@ -0,0 +1,21 @@
+Cerrors
+Cabs
+Cabshelper
+Parse_aux
+Parser
+Lexer
+Machine
+Env
+Cprint
+Cutil
+Ceval
+Cleanup
+Builtins
+Elab
+Rename
+Transform
+Unblock
+StructReturn
+Bitfields
+PackedStructs
+Parse
diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml
index eb3f063..4856c01 100644
--- a/cparser/Cutil.ml
+++ b/cparser/Cutil.ml
@@ -16,7 +16,7 @@
 (* Operations on C types and abstract syntax *)
 
 open Printf
-open Errors
+open Cerrors
 open C
 open Env
 open Machine
diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index f9b70c4..2473cf2 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -16,7 +16,7 @@
 (* Elaboration from Cabs parse tree to C simplified, typed syntax tree *)
 
 open Format
-open Errors
+open Cerrors
 open Machine
 open Cabs
 open Cabshelper
@@ -29,13 +29,13 @@ open Env
 (* Error reporting  *)
 
 let fatal_error loc fmt =
-  Errors.fatal_error ("%a: Error:@ " ^^ fmt) format_cabsloc loc
+  Cerrors.fatal_error ("%a: Error:@ " ^^ fmt) format_cabsloc loc
 
 let error loc fmt =
-  Errors.error ("%a: Error:@ " ^^ fmt) format_cabsloc loc
+  Cerrors.error ("%a: Error:@ " ^^ fmt) format_cabsloc loc
 
 let warning loc fmt =
-  Errors.warning ("%a: Warning:@ " ^^ fmt) format_cabsloc loc
+  Cerrors.warning ("%a: Warning:@ " ^^ fmt) format_cabsloc loc
 
 (* Error reporting for Env functions *)
 
diff --git a/cparser/PackedStructs.ml b/cparser/PackedStructs.ml
index f926ece..0dbc7cb 100644
--- a/cparser/PackedStructs.ml
+++ b/cparser/PackedStructs.ml
@@ -20,7 +20,7 @@ open Machine
 open C
 open Cutil
 open Env
-open Errors
+open Cerrors
 open Transform
 
 type field_info = {
diff --git a/cparser/Parse.ml b/cparser/Parse.ml
index 0fc85bf..2a144e2 100644
--- a/cparser/Parse.ml
+++ b/cparser/Parse.ml
@@ -39,15 +39,15 @@ let parse_transformations s =
   !t
 
 let preprocessed_file transfs name sourcefile =
-  Errors.reset();
+  Cerrors.reset();
   let t = parse_transformations transfs in
   let ic = open_in sourcefile in
   let p =
     try
       transform_program t (Elab.elab_preprocessed_file name ic)
     with Parsing.Parse_error ->
-           Errors.error "Error during parsing"; []
-       | Errors.Abort ->
+           Cerrors.error "Error during parsing"; []
+       | Cerrors.Abort ->
            [] in
   close_in ic;
-  if Errors.check_errors() then None else Some p
+  if Cerrors.check_errors() then None else Some p
diff --git a/cparser/Parse_aux.ml b/cparser/Parse_aux.ml
index 6592245..0600261 100755
--- a/cparser/Parse_aux.ml
+++ b/cparser/Parse_aux.ml
@@ -14,7 +14,7 @@
 (* *********************************************************************)
 
 open Format
-open Errors
+open Cerrors
 open Cabshelper
 
 (* Report parsing errors *)
diff --git a/cparser/Rename.ml b/cparser/Rename.ml
index 76c3c12..034df24 100644
--- a/cparser/Rename.ml
+++ b/cparser/Rename.ml
@@ -83,8 +83,8 @@ let ident env id =
   try
     IdentMap.find id env.re_id
   with Not_found ->
-    Errors.fatal_error "Internal error: Rename: %s__%d unbound" 
-                       id.name id.stamp
+    Cerrors.fatal_error "Internal error: Rename: %s__%d unbound" 
+                        id.name id.stamp
 
 let rec typ env = function
   | TPtr(ty, a) -> TPtr(typ env ty, a)
diff --git a/cparser/Unblock.ml b/cparser/Unblock.ml
index fa304b7..abdc5d5 100644
--- a/cparser/Unblock.ml
+++ b/cparser/Unblock.ml
@@ -20,7 +20,7 @@
 
 open C
 open Cutil
-open Errors
+open Cerrors
 
 (* Convert an initializer to a list of assignments.
    Prepend those assignments to the given statement. *)
diff --git a/cparser/libCparser.clib b/cparser/libCparser.clib
new file mode 100644
index 0000000..1b55150
--- /dev/null
+++ b/cparser/libCparser.clib
@@ -0,0 +1 @@
+cparser/uint64.o