diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2021-06-01 14:37:07 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2021-06-01 14:37:07 +0200 |
| commit | 5a632954c85e8b2b5afea124e4fc83f39c5d3598 (patch) | |
| tree | d53323083adec47d3338a04b516265c634806bea /backend | |
| parent | a298e55fdc51cce92a8b39280643b623d7d991a8 (diff) | |
| download | compcert-kvx-5a632954c85e8b2b5afea124e4fc83f39c5d3598.tar.gz compcert-kvx-5a632954c85e8b2b5afea124e4fc83f39c5d3598.zip | |
[BROKEN] Merge with v3.9 : something broken for __builtin_expect in cfrontend/C2C.ml
Diffstat (limited to 'backend')
| -rw-r--r-- | backend/Cminor.v | 9 | ||||
| -rw-r--r-- | backend/JsonAST.ml | 8 | ||||
| -rw-r--r-- | backend/NeedDomain.v | 2 | ||||
| -rw-r--r-- | backend/PrintCminor.ml | 9 |
4 files changed, 18 insertions, 10 deletions
diff --git a/backend/Cminor.v b/backend/Cminor.v index e585dc13..829adca0 100644 --- a/backend/Cminor.v +++ b/backend/Cminor.v @@ -6,10 +6,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) diff --git a/backend/JsonAST.ml b/backend/JsonAST.ml index a55bfa0c..2e70aae7 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; diff --git a/backend/NeedDomain.v b/backend/NeedDomain.v index fc1ae16d..62b8ff90 100644 --- a/backend/NeedDomain.v +++ b/backend/NeedDomain.v @@ -737,7 +737,7 @@ Lemma store_argument_sound: Proof. intros. assert (UNDEF: list_forall2 memval_lessdef - (list_repeat (size_chunk_nat chunk) Undef) + (List.repeat Undef (size_chunk_nat chunk)) (encode_val chunk w)). { rewrite <- (encode_val_length chunk w). diff --git a/backend/PrintCminor.ml b/backend/PrintCminor.ml index 051225a4..9ca0e3a0 100644 --- a/backend/PrintCminor.ml +++ b/backend/PrintCminor.ml @@ -6,10 +6,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) |