Commit 19fd9866 authored by Bernhard Schommer's avatar Bernhard Schommer
Browse files

Merge github.com:AbsInt/CompCert

parents c7b0e1ec e24e4a93
All files in this distribution are part of the CompCert verified compiler.
The CompCert verified compiler is Copyright 2004, 2005, 2006, 2007,
2008, 2009, 2010, 2011, 2012, 2013, 2014, 2015 Institut National de
Recherche en Informatique et en Automatique (INRIA).
The CompCert verified compiler is Copyright by Institut National de
Recherche en Informatique et en Automatique (INRIA) and
AbsInt Angewandte Informatik GmbH.
The CompCert verified compiler is distributed under the terms of the
INRIA Non-Commercial License Agreement given below. This is a
non-free license that grants you the right to use the CompCert verified
compiler for educational, research or evaluation purposes only, but
prohibits commercial uses.
INRIA Non-Commercial License Agreement given below or under the terms
of a Software Usage Agreement of AbsInt Angewandte Informatik GmbH.
The latter is a separate contract document.
The INRIA Non-Commercial License Agreement is a non-free license that
grants you the right to use the CompCert verified compiler for
educational, research or evaluation purposes only, but prohibits
any commercial uses.
For commercial use you need a Software Usage Agreement from
AbsInt Angewandte Informatik GmbH.
The following files in this distribution are dual-licensed both under
the INRIA Non-Commercial License Agreement and under the Free Software
......
......@@ -74,7 +74,7 @@ let print_error oc msg =
let output_filename ?(final = false) source_file source_suffix output_suffix =
match !option_o with
| Some file when final -> file
| _ ->
| _ ->
Filename.basename (Filename.chop_suffix source_file source_suffix)
^ output_suffix
......@@ -127,7 +127,7 @@ let parse_c_file sourcename ifile =
let oc = open_out ofile in
Cprint.program (Format.formatter_of_out_channel oc) ast;
close_out oc
end;
end;
(* Conversion to Csyntax *)
let csyntax =
match Timing.time "CompCert C generation" C2C.convertProgram ast with
......@@ -176,7 +176,7 @@ let compile_c_ast sourcename csyntax ofile debug =
| Errors.Error msg ->
print_error stderr msg;
exit 2 in
(* Dump Asm in binary format *)
(* Dump Asm in binary format *)
if !option_sdump then
dump_asm asm (output_filename sourcename ".c" ".sdump");
(* Print Asm in text form *)
......@@ -219,7 +219,7 @@ let compile_cminor_file ifile ofile =
eprintf "File %s, character %d: Syntax error\n"
ifile (Lexing.lexeme_start lb);
exit 2
| CMlexer.Error msg ->
| CMlexer.Error msg ->
eprintf "File %s, character %d: %s\n"
ifile (Lexing.lexeme_start lb) msg;
exit 2
......@@ -361,7 +361,7 @@ let process_h_file sourcename =
end else begin
eprintf "Error: input file %s ignored (not in -E mode)\n" sourcename;
exit 2
end
end
(* Record actions to be performed after parsing the command line *)
......@@ -386,9 +386,12 @@ let explode_comma_option s =
| [] -> assert false
| hd :: tl -> tl
let version_string =
"The CompCert C verified compiler, version "^ Configuration.version ^ "\n"
let usage_string =
"The CompCert C verified compiler, version " ^ Configuration.version ^ "
Usage: ccomp [options] <source files>
version_string ^
"Usage: ccomp [options] <source files>
Recognized source files:
.c C source file
.i or .p C source file that should not be preprocessed
......@@ -464,6 +467,7 @@ General options:
-stdlib <dir> Set the path of the Compcert run-time library
-v Print external commands before invoking them
-timings Show the time spent in various compiler passes
-version Print the version string and exit
Interpreter mode:
-interp Execute given .c files using the reference interpreter
-quiet Suppress diagnostic messages for the interpreter
......@@ -475,6 +479,9 @@ Interpreter mode:
let print_usage_and_exit _ =
printf "%s" usage_string; exit 0
let print_version_and_exit _ =
printf "%s" version_string; exit 0
let language_support_options = [
option_fbitfields; option_flongdouble;
option_fstruct_return; option_fvararg_calls; option_funprototyped;
......@@ -497,13 +504,16 @@ let cmdline_actions =
(* Getting help *)
Exact "-help", Self print_usage_and_exit;
Exact "--help", Self print_usage_and_exit;
(* Getting version info *)
Exact "-version", Self print_version_and_exit;
Exact "--version", Self print_version_and_exit;
(* Processing options *)
Exact "-c", Set option_c;
Exact "-E", Set option_E;
Exact "-S", Set option_S;
Exact "-o", String(fun s -> option_o := Some s);
Prefix "-o", Self (fun s -> let s = String.sub s 2 ((String.length s) - 2) in
option_o := Some s);
option_o := Some s);
(* Preprocessing options *)
Exact "-I", String(fun s -> prepro_options := s :: "-I" :: !prepro_options);
Prefix "-I", Self(fun s -> prepro_options := s :: !prepro_options);
......@@ -549,7 +559,7 @@ let cmdline_actions =
Exact "-dmach", Set option_dmach;
Exact "-dasm", Set option_dasm;
Exact "-sdump", Set option_sdump;
(* General options *)
(* General options *)
Exact "-v", Set option_v;
Exact "-stdlib", String(fun s -> stdlib_path := s);
Exact "-timings", Set option_timings;
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment