From 578cc2a54897e0c89425a56df7a173bebeee2382 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 5 Jan 2013 09:59:26 +0000 Subject: 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 --- exportclight/README | 34 ++++++++++++++++++++++++++++++++++ 1 file changed, 34 insertions(+) create mode 100644 exportclight/README (limited to 'exportclight/README') diff --git a/exportclight/README b/exportclight/README new file mode 100644 index 00000000..3fd8c0ae --- /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] + +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 search for include files + -D define preprocessor macro + -U undefine preprocessor macro + -Wp, pass options to C preprocessor + -f activate emulation of the given C feature + -- cgit