aboutsummaryrefslogtreecommitdiffstats
path: root/backend/Linear.v
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2015-04-02 16:25:25 +0200
committerBernhard Schommer <bernhardschommer@gmail.com>2015-04-02 16:25:25 +0200
commit170284b51766112e29d6bbfe519bad9f6da95269 (patch)
tree13a163ccee48cee0512a8af484b394623cdce030 /backend/Linear.v
parent2e30ad9698a6f24a8a746f68b30c235913006392 (diff)
parent959432fa13a899290db5236f93575a8bfdc13bb5 (diff)
downloadcompcert-kvx-170284b51766112e29d6bbfe519bad9f6da95269.tar.gz
compcert-kvx-170284b51766112e29d6bbfe519bad9f6da95269.zip
Merge branch 'master' into dwarf
Diffstat (limited to 'backend/Linear.v')
-rw-r--r--backend/Linear.v7
1 files changed, 4 insertions, 3 deletions
diff --git a/backend/Linear.v b/backend/Linear.v
index 56d1eb99..5d1fc0d8 100644
--- a/backend/Linear.v
+++ b/backend/Linear.v
@@ -42,7 +42,7 @@ Inductive instruction: Type :=
| Lcall: signature -> mreg + ident -> instruction
| Ltailcall: signature -> mreg + ident -> instruction
| Lbuiltin: external_function -> list mreg -> list mreg -> instruction
- | Lannot: external_function -> list loc -> instruction
+ | Lannot: external_function -> list (annot_arg loc) -> instruction
| Llabel: label -> instruction
| Lgoto: label -> instruction
| Lcond: condition -> list mreg -> label -> instruction
@@ -204,8 +204,9 @@ Inductive step: state -> trace -> state -> Prop :=
step (State s f sp (Lbuiltin ef args res :: b) rs m)
t (State s f sp b rs' m')
| exec_Lannot:
- forall s f sp rs m ef args b t v m',
- external_call' ef ge (map rs args) m t v m' ->
+ forall s f sp rs m ef args vl b t v m',
+ eval_annot_args ge rs sp m args vl ->
+ external_call ef ge vl m t v m' ->
step (State s f sp (Lannot ef args :: b) rs m)
t (State s f sp b rs m')
| exec_Llabel: