diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-05-17 08:59:15 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-05-17 08:59:15 +0000 |
| commit | e9704f237a400630ba45ee65779123b054dc1d6c (patch) | |
| tree | 0366049e9fc00aa99299dabbd08454c3c2b06177 /arm | |
| parent | f692ee29c1ea8748120ca1a4cbb4cd7f1eb2531e (diff) | |
Update ARM port.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2254 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'arm')
| -rw-r--r-- | arm/Asmgenproof.v | 4 | ||||
| -rw-r--r-- | arm/PrintAsm.ml | 26 |
2 files changed, 14 insertions, 16 deletions
diff --git a/arm/Asmgenproof.v b/arm/Asmgenproof.v index aede0da..6899040 100644 --- a/arm/Asmgenproof.v +++ b/arm/Asmgenproof.v @@ -693,7 +693,7 @@ Opaque loadind. exploit loadind_int_correct. eexact C. intros [rs1 [P [Q R]]]. econstructor; split. eapply exec_straight_trans. eexact P. apply exec_straight_one. - simpl. rewrite R; auto with asmgen. unfold Mach.chunk_of_type in A. rewrite A. + simpl. rewrite R; auto with asmgen. unfold chunk_of_type in A. rewrite A. rewrite <- (sp_val _ _ _ AG). rewrite E. eauto. auto. split. Simpl. split. Simpl. @@ -896,7 +896,7 @@ Opaque loadind. rewrite <- H5 at 2; unfold fn_code. apply exec_straight_two with rs2 m2'. unfold exec_instr. rewrite C. fold sp. - rewrite <- (sp_val _ _ _ AG). unfold Mach.chunk_of_type in F. rewrite F. auto. + rewrite <- (sp_val _ _ _ AG). unfold chunk_of_type in F. rewrite F. auto. simpl. auto. simpl. unfold exec_store. change (rs2 IR14) with (rs0 IR14). rewrite Int.add_zero_l. simpl. unfold chunk_of_type in P. simpl in P. diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml index fafd1d5..a506bed 100644 --- a/arm/PrintAsm.ml +++ b/arm/PrintAsm.ml @@ -206,27 +206,19 @@ let print_location oc loc = let cfi_startproc oc = if Configuration.asm_supports_cfi then - match config with - | Linux -> fprintf oc " .cfi_startproc\n" - | Diab -> assert false + fprintf oc " .cfi_startproc\n" let cfi_endproc oc = if Configuration.asm_supports_cfi then - match config with - | Linux -> fprintf oc " .cfi_endproc\n" - | Diab -> assert false + fprintf oc " .cfi_endproc\n" let cfi_adjust oc delta = if Configuration.asm_supports_cfi then - match config with - | Linux -> fprintf oc " .cfi_adjust_cfa_offset %ld\n" delta - | Diab -> assert false + fprintf oc " .cfi_adjust_cfa_offset %ld\n" delta let cfi_rel_offset oc reg ofs = if Configuration.asm_supports_cfi then - match config with - | Linux -> fprintf oc " .cfi_rel_offset %s, %ld\n" reg ofs - | Diab -> assert false + fprintf oc " .cfi_rel_offset %s, %ld\n" reg ofs (* Built-ins. They come in two flavors: - annotation statements: take their arguments in registers or stack @@ -237,9 +229,15 @@ let cfi_rel_offset oc reg ofs = (* Handling of annotations *) +let re_file_line = Str.regexp "#line:\\(.*\\):\\([1-9][0-9]*\\)$" + let print_annot_stmt oc txt targs args = - fprintf oc "%s annotation: " comment; - PrintAnnot.print_annot_stmt preg "sp" oc txt targs args + if Str.string_match re_file_line txt 0 then begin + print_file_line oc (Str.matched_group 1 txt) (Str.matched_group 2 txt) + end else begin + fprintf oc "%s annotation: " comment; + PrintAnnot.print_annot_stmt preg "sp" oc txt targs args + end let print_annot_val oc txt args res = fprintf oc "%s annotation: " comment; |