diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2017-12-11 08:18:44 +0100 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2017-12-11 08:18:44 +0100 |
commit | efe33ff4c85a309833a0302fd09a531c317b7ae1 (patch) | |
tree | f52d54cd91296093cb7c481c32b3caa5d91b82fc | |
parent | d56beade63aa995461cad3e33d918738a9facff2 (diff) | |
download | compcert-efe33ff4c85a309833a0302fd09a531c317b7ae1.tar.gz compcert-efe33ff4c85a309833a0302fd09a531c317b7ae1.zip |
Correct test for noinline. Bug 22642
-rw-r--r-- | cfrontend/C2C.ml | 2 |
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 |