Merge pull request #93 from AbsInt/separate-compilation

This pull request implements "approach A" to separate compilation in CompCert from the paper

Lightweight verification of separate compilation
by Jeehoon Kang, Yoonseung Kim, Chung-Kil Hur, Derek Dreyer, Viktor Vafeiadis,
POPL 2016, pages 178-190

In a nutshell, semantic preservation is still stated and proved in terms of a whole C program and a whole assembly program. However, the whole C program can be the result of syntactic linking of several C compilation units, each unit being separated compiled by CompCert to produce assembly unit, and these assembly units being linked together to produce the whole assembly program.

This way, the statement of semantic preservation and its proof now take into account the fact that each compilation unit is compiled separately, knowing only a fragment of the whole program (i.e. the current compilation unit) rather than the whole program.

1 files changed, 4 insertions, 19 deletions

diff --git a/backend/Allocation.v b/backend/Allocation.v
index 7534e23f..6a6c1eb6 100644
--- a/backend/Allocation.v
+++ b/backend/Allocation.v
@@ -12,26 +12,11 @@
 
 (** Register allocation by external oracle and a posteriori validation. *)
 
-Require Import FSets.
-Require FSetAVLplus.
+Require Import FSets FSetAVLplus.
+Require Import Coqlib Ordered Maps Errors Integers Floats.
+Require Import AST Lattice Kildall Memdata.
 Require Archi.
-Require Import Coqlib.
-Require Import Ordered.
-Require Import Errors.
-Require Import Maps.
-Require Import Lattice.
-Require Import AST.
-Require Import Integers.
-Require Import Floats.
-Require Import Memdata.
-Require Import Op.
-Require Import Registers.
-Require Import RTL.
-Require Import Kildall.
-Require Import Locations.
-Require Import Conventions.
-Require Import RTLtyping.
-Require Import LTL.
+Require Import Op Registers RTL Locations Conventions RTLtyping LTL.
 
 (** The validation algorithm used here is described in
   "Validating register allocation and spilling",