aboutsummaryrefslogtreecommitdiff
path: root/checker
diff options
context:
space:
mode:
Diffstat (limited to 'checker')
-rw-r--r--checker/analyze.ml22
-rw-r--r--checker/check.ml4
-rw-r--r--checker/check.mli4
-rw-r--r--checker/checkInductive.ml4
-rw-r--r--checker/checkInductive.mli4
-rw-r--r--checker/checkTypes.ml4
-rw-r--r--checker/checkTypes.mli4
-rw-r--r--checker/check_stat.ml4
-rw-r--r--checker/check_stat.mli4
-rw-r--r--checker/checker.ml4
-rw-r--r--checker/checker.mli4
-rw-r--r--checker/coqchk.mli4
-rw-r--r--checker/mod_checking.mli4
-rw-r--r--checker/safe_checking.ml4
-rw-r--r--checker/safe_checking.mli4
-rw-r--r--checker/validate.ml4
-rw-r--r--checker/validate.mli4
-rw-r--r--checker/values.ml4
-rw-r--r--checker/values.mli4
-rw-r--r--checker/votour.ml4
-rw-r--r--checker/votour.mli4
21 files changed, 60 insertions, 42 deletions
diff --git a/checker/analyze.ml b/checker/analyze.ml
index 91137a0ce2..94acba6b05 100644
--- a/checker/analyze.ml
+++ b/checker/analyze.ml
@@ -25,6 +25,12 @@ let code_codepointer = 0x10
let code_infixpointer = 0x11
let code_custom = 0x12
let code_block64 = 0x13
+let code_shared64 = 0x14
+let code_string64 = 0x15
+let code_double_array64_big = 0x16
+let code_double_array64_little = 0x17
+let code_custom_len = 0x18
+let code_custom_fixed = 0x19
[@@@ocaml.warning "-37"]
type code_descr =
@@ -48,8 +54,14 @@ type code_descr =
| CODE_INFIXPOINTER
| CODE_CUSTOM
| CODE_BLOCK64
+| CODE_SHARED64
+| CODE_STRING64
+| CODE_DOUBLE_ARRAY64_BIG
+| CODE_DOUBLE_ARRAY64_LITTLE
+| CODE_CUSTOM_LEN
+| CODE_CUSTOM_FIXED
-let code_max = 0x13
+let code_max = 0x19
let magic_number = "\132\149\166\190"
@@ -342,7 +354,8 @@ let parse_object chan =
let addr = input_int32u chan in
for _i = 0 to 15 do ignore (input_byte chan); done;
RCode addr
- | CODE_CUSTOM ->
+ | CODE_CUSTOM
+ | CODE_CUSTOM_FIXED ->
begin match input_cstring chan with
| "_j" -> Rint64 (input_intL chan)
| s -> Printf.eprintf "Unhandled custom code: %s" s; assert false
@@ -356,6 +369,11 @@ let parse_object chan =
| CODE_DOUBLE_ARRAY8_LITTLE
| CODE_DOUBLE_ARRAY32_BIG
| CODE_INFIXPOINTER
+ | CODE_SHARED64
+ | CODE_STRING64
+ | CODE_DOUBLE_ARRAY64_BIG
+ | CODE_DOUBLE_ARRAY64_LITTLE
+ | CODE_CUSTOM_LEN
-> Printf.eprintf "Unhandled code %04x\n%!" data; assert false
let parse chan =
diff --git a/checker/check.ml b/checker/check.ml
index 4ac5c56732..bb3255338f 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/checker/check.mli b/checker/check.mli
index 7f0340b193..bb19f09d2e 100644
--- a/checker/check.mli
+++ b/checker/check.mli
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/checker/checkInductive.ml b/checker/checkInductive.ml
index c4c6d9bb4f..a1d5aedb01 100644
--- a/checker/checkInductive.ml
+++ b/checker/checkInductive.ml
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/checker/checkInductive.mli b/checker/checkInductive.mli
index c5f8dec1a4..54e8911366 100644
--- a/checker/checkInductive.mli
+++ b/checker/checkInductive.mli
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/checker/checkTypes.ml b/checker/checkTypes.ml
index 2f1c690aca..626ed5f250 100644
--- a/checker/checkTypes.ml
+++ b/checker/checkTypes.ml
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/checker/checkTypes.mli b/checker/checkTypes.mli
index 9ef6ff017c..95e7dabf2e 100644
--- a/checker/checkTypes.mli
+++ b/checker/checkTypes.mli
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/checker/check_stat.ml b/checker/check_stat.ml
index 8854a23dd5..ee7170df48 100644
--- a/checker/check_stat.ml
+++ b/checker/check_stat.ml
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/checker/check_stat.mli b/checker/check_stat.mli
index c636327553..8796bcda76 100644
--- a/checker/check_stat.mli
+++ b/checker/check_stat.mli
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/checker/checker.ml b/checker/checker.ml
index 5f93148be6..0522d43417 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/checker/checker.mli b/checker/checker.mli
index bbfefb22c0..d0a18b5416 100644
--- a/checker/checker.mli
+++ b/checker/checker.mli
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/checker/coqchk.mli b/checker/coqchk.mli
index d0712f8075..eeb4eb64bd 100644
--- a/checker/coqchk.mli
+++ b/checker/coqchk.mli
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/checker/mod_checking.mli b/checker/mod_checking.mli
index d29d1861f4..58eb135b50 100644
--- a/checker/mod_checking.mli
+++ b/checker/mod_checking.mli
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/checker/safe_checking.ml b/checker/safe_checking.ml
index a913d53bd6..524ffbc022 100644
--- a/checker/safe_checking.ml
+++ b/checker/safe_checking.ml
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/checker/safe_checking.mli b/checker/safe_checking.mli
index 205777272d..21566555d4 100644
--- a/checker/safe_checking.mli
+++ b/checker/safe_checking.mli
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/checker/validate.ml b/checker/validate.ml
index 6ffc43394b..66367cb002 100644
--- a/checker/validate.ml
+++ b/checker/validate.ml
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/checker/validate.mli b/checker/validate.mli
index 584ea6ed95..9ddc510e4a 100644
--- a/checker/validate.mli
+++ b/checker/validate.mli
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/checker/values.ml b/checker/values.ml
index cba96e6636..12f7135cdf 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/checker/values.mli b/checker/values.mli
index 15d307ee29..ced7de4719 100644
--- a/checker/values.mli
+++ b/checker/values.mli
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/checker/votour.ml b/checker/votour.ml
index 452809f7bb..a83ba20dd6 100644
--- a/checker/votour.ml
+++ b/checker/votour.ml
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/checker/votour.mli b/checker/votour.mli
index d0712f8075..eeb4eb64bd 100644
--- a/checker/votour.mli
+++ b/checker/votour.mli
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 19:01:34 +0000