diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-01-07 10:30:16 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-01-07 10:30:16 +0000 |
| commit | 8e5f68c1a6d921a46bb817fe0a82fca1c3494dde (patch) | |
| tree | 2cec8321fd218a49c6cc8ec70b9f9d37634ef43f /driver | |
| parent | 578cc2a54897e0c89425a56df7a173bebeee2382 (diff) | |
Update Cminor parser and printer so that the parser can parse the whole Cminor language and can reparse the output of the printer.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2090 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'driver')
| -rw-r--r-- | driver/Interp.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/driver/Interp.ml b/driver/Interp.ml index 9031042..63d51a4 100644 --- a/driver/Interp.ml +++ b/driver/Interp.ml @@ -69,12 +69,12 @@ let print_event p = function print_eventval res | Event_vload(chunk, id, ofs, res) -> fprintf p "volatile load %s[&%s%+ld] -> %a" - (PrintCminor.name_of_chunk chunk) + (PrintAST.name_of_chunk chunk) (extern_atom id) (camlint_of_coqint ofs) print_eventval res | Event_vstore(chunk, id, ofs, arg) -> fprintf p "volatile store %s[&%s%+ld] <- %a" - (PrintCminor.name_of_chunk chunk) + (PrintAST.name_of_chunk chunk) (extern_atom id) (camlint_of_coqint ofs) print_eventval arg | Event_annot(text, args) -> |