aboutsummaryrefslogtreecommitdiffstats
path: root/backend
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2020-11-10 19:15:16 +0100
committerXavier Leroy <xavier.leroy@college-de-france.fr>2021-04-29 09:13:25 +0200
commitd54fef19ae19df47dc9e0d64afdb6a110f5ecdb2 (patch)
treeb0aad2de3668459e1cfddccd59c4189b521966ba /backend
parent868da35cd23d47e8c027967148518497f921f829 (diff)
downloadcompcert-kvx-d54fef19ae19df47dc9e0d64afdb6a110f5ecdb2.tar.gz
compcert-kvx-d54fef19ae19df47dc9e0d64afdb6a110f5ecdb2.zip
Emit no entry for variables without init in json.
Variables without init do not generated any assembly code so no entry in the json AST should be generated. They correspond to extern variables without initializer that are defined in another compilation unit. Bug 30112
Diffstat (limited to 'backend')
-rw-r--r--backend/JsonAST.ml8
1 files changed, 7 insertions, 1 deletions
diff --git a/backend/JsonAST.ml b/backend/JsonAST.ml
index d218e567..8ab874b1 100644
--- a/backend/JsonAST.ml
+++ b/backend/JsonAST.ml
@@ -114,11 +114,17 @@ let pp_program pp pp_inst prog =
let prog_vars,prog_funs = List.fold_left (fun (vars,funs) (ident,def) ->
match def with
| Gfun (Internal f) ->
+ (* No assembly is generated for non static inline functions *)
if not (atom_is_iso_inline_definition ident) then
vars,(ident,f)::funs
else
vars,funs
- | Gvar v -> (ident,v)::vars,funs
+ | Gvar v ->
+ (* No assembly is generated for variables without init *)
+ if v.gvar_init <> [] then
+ (ident,v)::vars,funs
+ else
+ vars, funs
| _ -> vars,funs) ([],[]) prog.prog_defs in
pp_jobject_start pp;
pp_jmember ~first:true pp "Global Variables" (pp_jarray pp_vardef) prog_vars;