Support for inlined built-ins.

AST: add ef_inline flag to external functions.
Selection: recognize calls to inlined built-ins and inline them as Sbuiltin.
CminorSel to Asm: added Sbuiltin/Ibuiltin instruction.
PrintAsm: adapted expansion of builtins.
C2Clight: adapted detection of builtins.
Conventions: refactored in a machine-independent part (backend/Conventions)
  and a machine-dependent part (ARCH/SYS/Conventions1).


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1356 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 23 insertions, 0 deletions

diff --git a/backend/Locations.v b/backend/Locations.v
index 295df28..c2fda9c 100644
--- a/backend/Locations.v
+++ b/backend/Locations.v
@@ -173,6 +173,18 @@ Module Loc.
     destruct s; destruct s0; intuition auto.
   Qed.
 
+  Lemma diff_reg_right:
+    forall l r, l <> R r -> diff (R r) l.
+  Proof.
+    intros. simpl. destruct l. congruence. auto.
+  Qed.
+
+  Lemma diff_reg_left:
+    forall l r, l <> R r -> diff l (R r).
+  Proof.
+    intros. apply diff_sym. apply diff_reg_right. auto.
+  Qed.
+
 (** [Loc.overlap l1 l2] returns [false] if [l1] and [l2] are different and
   non-overlapping, and [true] otherwise: either [l1 = l2] or they partially 
   overlap. *)
@@ -290,6 +302,14 @@ Module Loc.
     auto.
   Qed.
 
+  Lemma reg_notin:
+    forall r ll, ~(In (R r) ll) -> notin (R r) ll.
+  Proof.
+    induction ll; simpl; intros. auto. 
+    split. destruct a; auto. intuition congruence.
+    apply IHll. intuition.
+  Qed.
+
 (** [Loc.disjoint l1 l2] is true if the locations in list [l1]
   are different from all locations in list [l2]. *)
 
@@ -352,6 +372,9 @@ Module Loc.
   | norepet_cons:
       forall hd tl, notin hd tl -> norepet tl -> norepet (hd :: tl).
 
+(** [Loc.no_overlap l1 l2] holds if elements of [l1] never overlap partially
+  with elements of [l2]. *)
+
   Definition no_overlap (l1 l2 : list loc) :=
    forall r, In r l1 -> forall s, In s l2 ->  r = s \/ Loc.diff r s.