aboutsummaryrefslogtreecommitdiffstats
path: root/x86
diff options
context:
space:
mode:
authorCyril SIX <cyril.six@kalray.eu>2020-05-04 16:35:45 +0200
committerCyril SIX <cyril.six@kalray.eu>2020-05-04 16:35:45 +0200
commitc22a1828063756fdc11876993e6f1e2ca3bba04d (patch)
treef1d61e5ae919097062343e9309d1b96b6ca80dd1 /x86
parent4f6c5833a149d0659f4bffaaeb464cd9864b3a9b (diff)
downloadcompcert-kvx-c22a1828063756fdc11876993e6f1e2ca3bba04d.tar.gz
compcert-kvx-c22a1828063756fdc11876993e6f1e2ca3bba04d.zip
Adding copyrights
Diffstat (limited to 'x86')
-rw-r--r--x86/CSE2deps.v12
-rw-r--r--x86/CSE2depsproof.v12
-rw-r--r--x86/DuplicateOpcodeHeuristic.ml14
3 files changed, 38 insertions, 0 deletions
diff --git a/x86/CSE2deps.v b/x86/CSE2deps.v
index f4d9e254..a4b47a5c 100644
--- a/x86/CSE2deps.v
+++ b/x86/CSE2deps.v
@@ -1,3 +1,15 @@
+(* *************************************************************)
+(* *)
+(* The Compcert verified compiler *)
+(* *)
+(* David Monniaux CNRS, VERIMAG *)
+(* *)
+(* Copyright VERIMAG. All rights reserved. *)
+(* This file is distributed under the terms of the INRIA *)
+(* Non-Commercial License Agreement. *)
+(* *)
+(* *************************************************************)
+
Require Import BoolEqual Coqlib.
Require Import AST Integers Floats.
Require Import Values Memory Globalenvs Events.
diff --git a/x86/CSE2depsproof.v b/x86/CSE2depsproof.v
index 1e913254..fd088962 100644
--- a/x86/CSE2depsproof.v
+++ b/x86/CSE2depsproof.v
@@ -1,3 +1,15 @@
+(* *************************************************************)
+(* *)
+(* The Compcert verified compiler *)
+(* *)
+(* David Monniaux CNRS, VERIMAG *)
+(* *)
+(* Copyright VERIMAG. All rights reserved. *)
+(* This file is distributed under the terms of the INRIA *)
+(* Non-Commercial License Agreement. *)
+(* *)
+(* *************************************************************)
+
Require Import Coqlib Maps Errors Integers Floats Lattice Kildall.
Require Import AST Linking.
Require Import Memory Registers Op RTL Maps.
diff --git a/x86/DuplicateOpcodeHeuristic.ml b/x86/DuplicateOpcodeHeuristic.ml
index 2ec314c1..38702e1b 100644
--- a/x86/DuplicateOpcodeHeuristic.ml
+++ b/x86/DuplicateOpcodeHeuristic.ml
@@ -1,3 +1,17 @@
+(* *************************************************************)
+(* *)
+(* The Compcert verified compiler *)
+(* *)
+(* Sylvain Boulmé Grenoble-INP, VERIMAG *)
+(* David Monniaux CNRS, VERIMAG *)
+(* Cyril Six Kalray *)
+(* *)
+(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *)
+(* This file is distributed under the terms of the INRIA *)
+(* Non-Commercial License Agreement. *)
+(* *)
+(* *************************************************************)
+
(* open Camlcoq *)
open Op
open Integers