From a5ffc59246b09a389e5f8cbc2f217e323e76990f Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Mon, 13 Jun 2011 18:11:19 +0000
Subject: Revised handling of annotation statements, and more generally
 built-in functions, and more generally external functions

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1672 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 backend/Lineartyping.v | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'backend/Lineartyping.v')

diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v
index ef6194c0..390b6302 100644
--- a/backend/Lineartyping.v
+++ b/backend/Lineartyping.v
@@ -93,6 +93,12 @@ Inductive wt_instr : instruction -> Prop :=
       mreg_type res = proj_sig_res (ef_sig ef) ->
       arity_ok (ef_sig ef).(sig_args) = true ->
       wt_instr (Lbuiltin ef args res)
+  | wt_Lannot:
+      forall ef args,
+      List.map Loc.type args = (ef_sig ef).(sig_args) ->
+      ef_reloads ef = false ->
+      locs_acceptable args ->
+      wt_instr (Lannot ef args)
   | wt_Llabel:
       forall lbl,
       wt_instr (Llabel lbl)
-- 
cgit