aboutsummaryrefslogtreecommitdiffstats
path: root/cparser/Elab.ml
diff options
context:
space:
mode:
authorBernhard Schommer <bschommer@users.noreply.github.com>2018-08-17 13:57:00 +0200
committerXavier Leroy <xavierleroy@users.noreply.github.com>2018-08-17 13:57:00 +0200
commit44c859e5ffd95498b6e0dc504a9fc54cef86aae8 (patch)
tree066e0f63c2b210b72413ade8850d51777363e99e /cparser/Elab.ml
parente108b274eda3739ff0d69efff626bb1c1dbcaed1 (diff)
downloadcompcert-kvx-44c859e5ffd95498b6e0dc504a9fc54cef86aae8.tar.gz
compcert-kvx-44c859e5ffd95498b6e0dc504a9fc54cef86aae8.zip
Earlier check for invalid asm outputs. (#130)
Since a non modifiable lvalue is an invalid asm output it should be checked earlier, otherwise this leads to a retyping error later. Bug 24285
Diffstat (limited to 'cparser/Elab.ml')
-rw-r--r--cparser/Elab.ml5
1 files changed, 5 insertions, 0 deletions
diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index d0de1058..cff9ed5b 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -2879,6 +2879,11 @@ let rec elab_stmt env ctx s =
let a = elab_cvspecs env cv_specs in
let s = elab_simple_string loc wide chars in
let outputs,env = mmap (elab_asm_operand ctx loc) env outputs in
+ List.iter
+ (fun (lbl, cst, e) ->
+ if not (is_modifiable_lvalue env e) then
+ error loc "asm output is not a modifiable l-value";)
+ outputs;
let inputs ,env= mmap (elab_asm_operand ctx loc) env inputs in
let flags = List.map (fun (w,c) -> elab_simple_string loc w c) flags in
{ sdesc = Sasm(a, s, outputs, inputs, flags);