diff options
| author | Lélio Brun <lelio.brun@inria.fr> | 2016-10-26 16:21:29 +0200 |
|---|---|---|
| committer | Lionel Rieg <lionel.rieg@univ-grenoble-alpes.fr> | 2020-04-21 01:08:58 +0200 |
| commit | 03b07d3f69fda4c32864fba9ecfff66aa23a2e67 (patch) | |
| tree | fec6b3a227b38571080e58d4a708b42d8328ade6 | |
| parent | 872236554ea25292f301a519767555200b48813a (diff) | |
| download | compcert-kvx-03b07d3f69fda4c32864fba9ecfff66aa23a2e67.tar.gz compcert-kvx-03b07d3f69fda4c32864fba9ecfff66aa23a2e67.zip | |
pretty printer for Clight
| -rw-r--r-- | cfrontend/PrintClight.ml | 6 | ||||
| -rw-r--r-- | common/Separation.v | 4 |
2 files changed, 3 insertions, 7 deletions
diff --git a/cfrontend/PrintClight.ml b/cfrontend/PrintClight.ml index 0e735d2d..7d4c47e5 100644 --- a/cfrontend/PrintClight.ml +++ b/cfrontend/PrintClight.ml @@ -30,11 +30,7 @@ open Clight not in the table of atoms. We print them as "$NNN" (a unique integer). *) -let temp_name (id: AST.ident) = - try - "$" ^ Hashtbl.find string_of_atom id - with Not_found -> - Printf.sprintf "$%d" (P.to_int id) +let temp_name (id: AST.ident) = (* "$" ^ Z.to_string (Z.Zpos id) *)extern_atom id (* Declarator (identifier + type) -- reuse from PrintCsyntax *) diff --git a/common/Separation.v b/common/Separation.v index 52c089a7..c4a46b6a 100644 --- a/common/Separation.v +++ b/common/Separation.v @@ -568,10 +568,10 @@ Lemma storev_rule2: forall chunk m m' b ofs v (spec1 spec: val -> Prop) P, m |= contains chunk b ofs spec1 ** P -> spec (Val.load_result chunk v) -> - Memory.Mem.storev chunk m (Vptr b (Int.repr ofs)) v = Some m' -> + Memory.Mem.storev chunk m (Vptr b (Ptrofs.repr ofs)) v = Some m' -> m' |= contains chunk b ofs spec ** P. Proof. - intros ** Hm Hspec Hstore. + intros * Hm Hspec Hstore. apply storev_rule with (1:=Hm) in Hspec. destruct Hspec as [m'' [Hmem Hspec]]. rewrite Hmem in Hstore. injection Hstore. |