aboutsummaryrefslogtreecommitdiffstats
path: root/cfrontend/C2C.ml
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2017-12-11 08:18:44 +0100
committerBernhard Schommer <bernhardschommer@gmail.com>2017-12-11 08:18:44 +0100
commitefe33ff4c85a309833a0302fd09a531c317b7ae1 (patch)
treef52d54cd91296093cb7c481c32b3caa5d91b82fc /cfrontend/C2C.ml
parentd56beade63aa995461cad3e33d918738a9facff2 (diff)
downloadcompcert-kvx-efe33ff4c85a309833a0302fd09a531c317b7ae1.tar.gz
compcert-kvx-efe33ff4c85a309833a0302fd09a531c317b7ae1.zip
Correct test for noinline. Bug 22642
Diffstat (limited to 'cfrontend/C2C.ml')
-rw-r--r--cfrontend/C2C.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index 2b3b50bf..173764e3 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -1153,7 +1153,7 @@ let convertFundef loc env fd =
fd.fd_locals in
let body' = convertStmt env fd.fd_body in
let id' = intern_string fd.fd_name.name in
- let noinline = Cutil.find_custom_attributes ["noinline";"__noinline__"] fd.fd_attrib = [] in
+ let noinline = Cutil.find_custom_attributes ["noinline";"__noinline__"] fd.fd_attrib <> [] in
let inline = if noinline || fd.fd_vararg then (* PR#15 *)
Noinline
else if fd.fd_inline then