aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--LICENSE21
-rw-r--r--cfrontend/C2C.ml27
-rw-r--r--checklink/Asm_printers.ml2
-rw-r--r--checklink/Check.ml2
-rw-r--r--cparser/Elab.ml1
-rw-r--r--driver/Driver.ml28
-rw-r--r--powerpc/Asm.v4
-rw-r--r--powerpc/Asmexpand.ml2
-rw-r--r--powerpc/TargetPrinter.ml4
-rw-r--r--[-rwxr-xr-x]test/compression/arcode.c0
-rw-r--r--[-rwxr-xr-x]test/compression/arcode.h0
-rw-r--r--[-rwxr-xr-x]test/compression/armain.c0
12 files changed, 67 insertions, 24 deletions
diff --git a/LICENSE b/LICENSE
index 21670791..5ffb39ab 100644
--- a/LICENSE
+++ b/LICENSE
@@ -1,14 +1,21 @@
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
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index 71328c71..96a497bc 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -897,6 +897,28 @@ let rec groupSwitch = function
let (fst, cases) = groupSwitch rem in
(Cutil.sseq s.sloc s fst, cases)
+(* Test whether the statement contains case and give an *)
+let rec contains_case s =
+ match s.sdesc with
+ | C.Sskip
+ | C.Sdo _
+ | C.Sbreak
+ | C.Scontinue
+ | C.Sswitch _ (* Stop at a switch *)
+ | C.Sgoto _
+ | C.Sreturn _
+ | C.Sdecl _
+ | C.Sasm _ -> ()
+ | C.Sseq (s1,s2)
+ | C.Sif(_,s1,s2) -> contains_case s1; contains_case s2
+ | C.Swhile (_,s1)
+ | C.Sdowhile (s1,_) -> contains_case s1
+ | C.Sfor (s1,e,s2,s3) -> contains_case s1; contains_case s2; contains_case s3
+ | C.Slabeled(C.Scase _, _) ->
+ unsupported "'case' outside of 'switch'"
+ | C.Slabeled(_,s) -> contains_case s
+ | C.Sblock b -> List.iter contains_case b
+
(** Annotations for line numbers *)
let add_lineno prev_loc this_loc s =
@@ -953,7 +975,10 @@ let rec convertStmt ploc env s =
| C.Sswitch(e, s1) ->
let (init, cases) = groupSwitch (flattenSwitch s1) in
if init.sdesc <> C.Sskip then
- warning "ignored code at beginning of 'switch'";
+ begin
+ warning "ignored code at beginning of 'switch'";
+ contains_case init
+ end;
let te = convertExpr env e in
add_lineno ploc s.sloc
(swrap (Ctyping.sswitch te
diff --git a/checklink/Asm_printers.ml b/checklink/Asm_printers.ml
index 43c974f2..c475d7da 100644
--- a/checklink/Asm_printers.ml
+++ b/checklink/Asm_printers.ml
@@ -289,7 +289,7 @@ let string_of_instruction = function
| Pstwu (i0, c1, i2) -> "Pstwu(" ^ string_of_ireg i0 ^ ", " ^ string_of_constant c1 ^ ", " ^ string_of_ireg i2 ^ ")"
| Pstwx (i0, i1, i2) -> "Pstwx(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")"
| Pstwx_a (i0, i1, i2) -> "Pstwx_a(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")"
-| Pstwxu (i0, i1, i2) -> "Pstwxu(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")"
+| Pstwux (i0, i1, i2) -> "Pstwux(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")"
| Pstwbrx (i0, i1, i2) -> "Pstwbrx(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")"
| Pstwcx_ (i0, i1, i2) -> "Pstwcx_(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")"
| Psubfc (i0, i1, i2) -> "Psubfc(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")"
diff --git a/checklink/Check.ml b/checklink/Check.ml
index 4924744c..bfd03c97 100644
--- a/checklink/Check.ml
+++ b/checklink/Check.ml
@@ -2130,7 +2130,7 @@ let rec compare_code ccode ecode pc: checker = fun fw ->
>>= recur_simpl
| _ -> error
end
- | Pstwxu(rd, r1, r2) ->
+ | Pstwux(rd, r1, r2) ->
begin match ecode with
| STWUX(rS, rA, rB) :: es ->
OK(fw)
diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index aa015b83..d6b79780 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -1817,6 +1817,7 @@ let enter_or_refine_ident local loc env s sto ty =
error loc "static redefinition of '%s' after non-static definition" s; sto
| Storage_static,_ -> Storage_static (* Static stays static *)
| Storage_extern,_ -> sto
+ | Storage_default,Storage_extern -> Storage_extern
| _,Storage_extern -> old_sto
| _,Storage_register
| Storage_register,_ -> Storage_register
diff --git a/driver/Driver.ml b/driver/Driver.ml
index 480cf665..805d5405 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -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;
diff --git a/powerpc/Asm.v b/powerpc/Asm.v
index d707b2b5..3fa7af31 100644
--- a/powerpc/Asm.v
+++ b/powerpc/Asm.v
@@ -260,7 +260,7 @@ Inductive instruction : Type :=
| Pstw: ireg -> constant -> ireg -> instruction (**r store 32-bit int *)
| Pstwu: ireg -> constant -> ireg -> instruction (**r store 32-bit int with update *)
| Pstwx: ireg -> ireg -> ireg -> instruction (**r same, with 2 index regs *)
- | Pstwxu: ireg -> ireg -> ireg -> instruction (**r same, with 2 index regs and update *)
+ | Pstwux: ireg -> ireg -> ireg -> instruction (**r same, with 2 index regs and update *)
| Pstw_a: ireg -> constant -> ireg -> instruction (**r store 32-bit quantity from int reg *)
| Pstwx_a: ireg -> ireg -> ireg -> instruction (**r same, with 2 index regs *)
| Pstwbrx: ireg -> ireg -> ireg -> instruction (**r store 32-bit int with reverse endianness *)
@@ -878,7 +878,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
| Pstfdu _ _ _
| Psthbrx _ _ _
| Pstwu _ _ _
- | Pstwxu _ _ _
+ | Pstwux _ _ _
| Psubfze _ _
| Psync
| Ptrap
diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml
index 7f413661..ec5a767f 100644
--- a/powerpc/Asmexpand.ml
+++ b/powerpc/Asmexpand.ml
@@ -427,7 +427,7 @@ let expand_instruction instr =
emit (Pstwu(GPR1, Cint(coqint_of_camlint adj), GPR1))
else begin
emit_loadimm GPR0 (coqint_of_camlint adj);
- emit (Pstwxu(GPR1, GPR1, GPR0))
+ emit (Pstwux(GPR1, GPR1, GPR0))
end;
emit (Pcfi_adjust (coqint_of_camlint sz));
if variadic then begin
diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml
index 3789d62e..2d47acb0 100644
--- a/powerpc/TargetPrinter.ml
+++ b/powerpc/TargetPrinter.ml
@@ -620,8 +620,8 @@ module Target (System : SYSTEM):TARGET =
fprintf oc " stwu %a, %a(%a)\n" ireg r1 constant c ireg r2
| Pstwx(r1, r2, r3) | Pstwx_a(r1, r2, r3) ->
fprintf oc " stwx %a, %a, %a\n" ireg r1 ireg r2 ireg r3
- | Pstwxu(r1, r2, r3) ->
- fprintf oc " stwxu %a, %a, %a\n" ireg r1 ireg r2 ireg r3
+ | Pstwux(r1, r2, r3) ->
+ fprintf oc " stwux %a, %a, %a\n" ireg r1 ireg r2 ireg r3
| Pstwbrx(r1, r2, r3) ->
fprintf oc " stwbrx %a, %a, %a\n" ireg r1 ireg r2 ireg r3
| Pstwcx_(r1, r2, r3) ->
diff --git a/test/compression/arcode.c b/test/compression/arcode.c
index f915cc25..f915cc25 100755..100644
--- a/test/compression/arcode.c
+++ b/test/compression/arcode.c
diff --git a/test/compression/arcode.h b/test/compression/arcode.h
index aac32080..aac32080 100755..100644
--- a/test/compression/arcode.h
+++ b/test/compression/arcode.h
diff --git a/test/compression/armain.c b/test/compression/armain.c
index 8f37c4ff..8f37c4ff 100755..100644
--- a/test/compression/armain.c
+++ b/test/compression/armain.c
generated by cgit (git 2.34.1) at 2024-07-03 00:23:22 +0000