From 5df29e2caa1ec95a3ddbcaf49d686998b0696855 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Wed, 10 Jan 2018 10:32:43 +0100 Subject: Change README to markdown. --- exportclight/README | 34 ---------------------------------- 1 file changed, 34 deletions(-) delete mode 100644 exportclight/README (limited to 'exportclight/README') diff --git a/exportclight/README b/exportclight/README deleted file mode 100644 index 3fd8c0ae..00000000 --- a/exportclight/README +++ /dev/null @@ -1,34 +0,0 @@ - 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