Put clighgen files in exportclight/

Short doc in exportclight/README



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

6 files changed, 99 insertions, 44 deletions

diff --git a/Makefile b/Makefile
index 716116c..9e04d95 100644
--- a/Makefile
+++ b/Makefile
@@ -33,6 +33,9 @@ OCB_OPTIONS_CHECKLINK=\
   $(OCB_OPTIONS) \
   -I checklink \
   -use-ocamlfind
+OCB_OPTIONS_CLIGHTGEN=\
+  $(OCB_OPTIONS) \
+  -I exportclight
 
 VPATH=$(DIRS)
 GPATH=$(DIRS)
@@ -154,13 +157,13 @@ cchecklink.byte: driver/Configuration.ml
 	$(OCAMLBUILD) $(OCB_OPTIONS_CHECKLINK) Validator.d.byte \
         && rm -f cchecklink.byte && $(SLN) _build/checklink/Validator.d.byte cchecklink.byte
 
-clightgen: extraction/STAMP driver/Configuration.ml
-	$(OCAMLBUILD) $(OCB_OPTIONS) Clightgen.native \
-        && rm -f clightgen && $(SLN) _build/driver/Clightgen.native clightgen
+clightgen: extraction/STAMP driver/Configuration.ml exportclight/Clightdefs.vo
+	$(OCAMLBUILD) $(OCB_OPTIONS_CLIGHTGEN) Clightgen.native \
+        && rm -f clightgen && $(SLN) _build/exportclight/Clightgen.native clightgen
 
-clightgen.byte: extraction/STAMP driver/Configuration.ml
-	$(OCAMLBUILD) $(OCB_OPTIONS) Clightgen.d.byte \
-        && rm -f clightgen.byte && $(SLN) _build/driver/Clightgen.d.byte clightgen.byte
+clightgen.byte: extraction/STAMP driver/Configuration.ml exportclight/Clightdefs.vo
+	$(OCAMLBUILD) $(OCB_OPTIONS_CLIGHTGEN) Clightgen.d.byte \
+        && rm -f clightgen.byte && $(SLN) _build/exportclight/Clightgen.d.byte clightgen.byte
 
 .PHONY: proof extraction ccomp ccomp.prof ccomp.byte runtime cchecklink cchecklink.byte clightgen clightgen.byte
 
@@ -222,7 +225,7 @@ endif
 	$(MAKE) -C runtime install
 
 clean:
-	rm -f $(patsubst %, %/*.vo, $(DIRS))
+	rm -f $(patsubst %, %/*.vo, $(DIRS) exportclight)
 	rm -f ccomp ccomp.byte cchecklink cchecklink.byte clightgen clightgen.byte
 	rm -rf _build
 	rm -rf doc/html doc/*.glob
diff --git a/_tags b/_tags
index 0653ec6..e87167e 100644
--- a/_tags
+++ b/_tags
@@ -1,4 +1,4 @@
 <driver/Driver.*{byte,native}>: use_unix,use_str,use_Cparser
-<driver/Clightgen.*{byte,native}>: use_unix,use_str,use_Cparser
+<exportclight/Clightgen.*{byte,native}>: use_unix,use_str,use_Cparser
 <checklink/*.ml>: pkg_bitstring,warn_error_A
 <checklink/Validator.*{byte,native}>: pkg_unix,pkg_str,pkg_bitstring,use_Cparser
diff --git a/exportclight/Clightdefs.v b/exportclight/Clightdefs.v
new file mode 100644
index 0000000..4c3c942
--- /dev/null
+++ b/exportclight/Clightdefs.v
@@ -0,0 +1,53 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              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.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** All imports and definitions used by .v Clight files generated by clightgen *)
+
+Require Export List.
+Require Export ZArith.
+Require Export Integers.
+Require Export Floats.
+Require Export AST.
+Require Export Ctypes.
+Require Export Cop.
+Require Export Clight.
+
+Definition tvoid := Tvoid.
+Definition tschar := Tint I8 Signed noattr.
+Definition tuchar := Tint I8 Unsigned noattr.
+Definition tshort := Tint I16 Signed noattr.
+Definition tushort := Tint I16 Unsigned noattr.
+Definition tint := Tint I32 Signed noattr.
+Definition tuint := Tint I32 Unsigned noattr.
+Definition tbool := Tint IBool Unsigned noattr.
+Definition tfloat := Tfloat F32 noattr.
+Definition tdouble := Tfloat F64 noattr.
+Definition tptr (t: type) := Tpointer t noattr.
+Definition tarray (t: type) (sz: Z) := Tarray t sz noattr.
+
+Definition volatile_attr := {| attr_volatile := true |}.
+
+Definition tvolatile (ty: type) :=
+  match ty with
+  | Tvoid => Tvoid
+  | Tint sz si a => Tint sz si volatile_attr
+  | Tfloat sz a => Tfloat sz volatile_attr
+  | Tpointer elt a => Tpointer elt volatile_attr
+  | Tarray elt sz a => Tarray elt sz volatile_attr
+  | Tfunction args res => Tfunction args res 
+  | Tstruct id fld a => Tstruct id fld volatile_attr
+  | Tunion id fld a => Tunion id fld volatile_attr
+  | Tcomp_ptr id a => Tcomp_ptr id volatile_attr
+  end.
diff --git a/driver/Clightgen.ml b/exportclight/Clightgen.ml
index 1805573..1805573 100644
--- a/driver/Clightgen.ml
+++ b/exportclight/Clightgen.ml
diff --git a/cfrontend/ExportClight.ml b/exportclight/ExportClight.ml
index d7a80a5..452693c 100644
--- a/cfrontend/ExportClight.ml
+++ b/exportclight/ExportClight.ml
@@ -480,45 +480,10 @@ let print_assertions p =
 (* The prologue *)
 
 let prologue = "\
-Require Import List.
-Require Import ZArith.
-Require Import Integers.
-Require Import Floats.
-Require Import AST.
-Require Import Ctypes.
-Require Import Cop.
-Require Import Clight.
+Require Import Clightdefs.
 
 Local Open Scope Z_scope.
 
-Definition tvoid := Tvoid.
-Definition tschar := Tint I8 Signed noattr.
-Definition tuchar := Tint I8 Unsigned noattr.
-Definition tshort := Tint I16 Signed noattr.
-Definition tushort := Tint I16 Unsigned noattr.
-Definition tint := Tint I32 Signed noattr.
-Definition tuint := Tint I32 Unsigned noattr.
-Definition tbool := Tint IBool Unsigned noattr.
-Definition tfloat := Tfloat F32 noattr.
-Definition tdouble := Tfloat F64 noattr.
-Definition tptr (t: type) := Tpointer t noattr.
-Definition tarray (t: type) (sz: Z) := Tarray t sz noattr.
-
-Definition volatile_attr := {| attr_volatile := true |}.
-
-Definition tvolatile (ty: type) :=
-  match ty with
-  | Tvoid => Tvoid
-  | Tint sz si a => Tint sz si volatile_attr
-  | Tfloat sz a => Tfloat sz volatile_attr
-  | Tpointer elt a => Tpointer elt volatile_attr
-  | Tarray elt sz a => Tarray elt sz volatile_attr
-  | Tfunction args res => Tfunction args res 
-  | Tstruct id fld a => Tstruct id fld volatile_attr
-  | Tunion id fld a => Tunion id fld volatile_attr
-  | Tcomp_ptr id a => Tcomp_ptr id volatile_attr
-  end.
-
 "
 
 (* All together *)
diff --git a/exportclight/README b/exportclight/README
new file mode 100644
index 0000000..3fd8c0a
--- /dev/null
+++ b/exportclight/README
@@ -0,0 +1,34 @@
+                        The clightgen tool
+                        ------------------
+
+OVERVIEW
+
+"clightgen" is an experimental tool that transforms C source files
+into Clight abstract syntax, pretty-printed in Coq format in .v files.
+These generated .v files can be loaded in a Coq session for
+interactive verification, typically.
+
+
+HOW TO BUILD
+
+Change to the top-level CompCert directory and issue
+
+          make clightgen
+
+
+USAGE
+
+        clightgen [options] <C source files>
+
+For each source file "src.c", its Clight abstract syntax is generated
+in "src.v".
+
+The options recognized are a subset of those of the CompCert compiler ccomp
+(see http://compcert.inria.fr/man/manual003.html for full documentation):
+
+   -I<dir>     search <dir> for include files
+   -D<symbol>  define preprocessor macro
+   -U<symbol>  undefine preprocessor macro
+   -Wp,<opts>  pass options to C preprocessor
+   -f<feature> activate emulation of the given C feature
+