From 5a632954c85e8b2b5afea124e4fc83f39c5d3598 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Tue, 1 Jun 2021 14:37:07 +0200 Subject: [BROKEN] Merge with v3.9 : something broken for __builtin_expect in cfrontend/C2C.ml --- exportclight/Clightdefs.v | 43 ++++++++++++++++++++++++++++--------------- exportclight/Clightgen.ml | 9 +++++---- exportclight/Clightnorm.ml | 9 +++++---- exportclight/ExportClight.ml | 13 ++++++++----- 4 files changed, 46 insertions(+), 28 deletions(-) (limited to 'exportclight') diff --git a/exportclight/Clightdefs.v b/exportclight/Clightdefs.v index 8af920df..708be1cb 100644 --- a/exportclight/Clightdefs.v +++ b/exportclight/Clightdefs.v @@ -6,10 +6,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) @@ -18,6 +19,8 @@ From Coq Require Import Ascii String List ZArith. From compcert Require Import Integers Floats Maps Errors AST Ctypes Cop Clight. +(** ** Short names for types *) + Definition tvoid := Tvoid. Definition tschar := Tint I8 Signed noattr. Definition tuchar := Tint I8 Unsigned noattr. @@ -56,6 +59,8 @@ Definition talignas (n: N) (ty: type) := Definition tvolatile_alignas (n: N) (ty: type) := tattr {| attr_volatile := true; attr_alignas := Some n |} ty. +(** ** Constructor for programs and compilation units *) + Definition wf_composites (types: list composite_definition) : Prop := match build_composite_env types with OK _ => True | Error _ => False end. @@ -81,6 +86,8 @@ Definition mkprogram (types: list composite_definition) prog_comp_env := ce; prog_comp_env_eq := EQ |}. +(** ** Encoding character strings as positive numbers *) + (** The following encoding of character strings as positive numbers must be kept consistent with the OCaml function [Camlcoq.pos_of_string]. *) @@ -169,17 +176,6 @@ Fixpoint ident_of_string (s: string) : ident := | String c s => append_char_pos c (ident_of_string s) end. -(** A convenient notation [$ "ident"] to force evaluation of - [ident_of_string "ident"] *) - -Ltac ident_of_string s := - let x := constr:(ident_of_string s) in - let y := eval compute in x in - exact y. - -Notation "$ s" := (ltac:(ident_of_string s)) - (at level 1, only parsing) : string_scope. - (** The inverse conversion, from encoded strings to strings *) Section DECODE_BITS. @@ -289,3 +285,20 @@ Proof. intros. rewrite <- (string_of_ident_of_string s1), <- (string_of_ident_of_string s2). congruence. Qed. + +(** ** Notations *) + +Module ClightNotations. + +(** A convenient notation [$ "ident"] to force evaluation of + [ident_of_string "ident"] *) + +Ltac ident_of_string s := + let x := constr:(ident_of_string s) in + let y := eval compute in x in + exact y. + +Notation "$ s" := (ltac:(ident_of_string s)) + (at level 1, only parsing) : clight_scope. + +End ClightNotations. diff --git a/exportclight/Clightgen.ml b/exportclight/Clightgen.ml index 5e27370e..44c76cc6 100644 --- a/exportclight/Clightgen.ml +++ b/exportclight/Clightgen.ml @@ -6,10 +6,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) diff --git a/exportclight/Clightnorm.ml b/exportclight/Clightnorm.ml index a6158b60..88d44c08 100644 --- a/exportclight/Clightnorm.ml +++ b/exportclight/Clightnorm.ml @@ -6,10 +6,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) diff --git a/exportclight/ExportClight.ml b/exportclight/ExportClight.ml index 7604175e..474a1bd8 100644 --- a/exportclight/ExportClight.ml +++ b/exportclight/ExportClight.ml @@ -6,10 +6,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) @@ -455,8 +456,10 @@ let print_composite_definition p (Composite(id, su, m, a)) = let prologue = "\ From Coq Require Import String List ZArith.\n\ From compcert Require Import Coqlib Integers Floats AST Ctypes Cop Clight Clightdefs.\n\ +Import Clightdefs.ClightNotations.\n\ Local Open Scope Z_scope.\n\ -Local Open Scope string_scope.\n" +Local Open Scope string_scope.\n\ +Local Open Scope clight_scope.\n" (* Naming the compiler-generated temporaries occurring in the program *) -- cgit