diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-05-08 07:07:25 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-05-08 07:07:25 +0000 |
| commit | c45fc2431ea70e0cb5a80e65d0ac99f91e94693e (patch) | |
| tree | dfc11f4507c6ddaab96074382d8406dbc4031f60 /cparser/Ceval.ml | |
| parent | 67e74f6f1a24247bfcd3d6c165a2d6cd45c83b06 (diff) | |
| download | compcert-kvx-c45fc2431ea70e0cb5a80e65d0ac99f91e94693e.tar.gz compcert-kvx-c45fc2431ea70e0cb5a80e65d0ac99f91e94693e.zip | |
Added pass CleanupLabels to remove unreferenced labels in a proved way.
ia32/PrintAsm.ml: simplified accordingly; other PrintAsm.ml to be fixed.
ia32/Asm.v: Pmov_ri can undef flags (if translated to xor)
cparser/Ceval.ml: treat ~ in constant exprs
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1647 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'cparser/Ceval.ml')
| -rw-r--r-- | cparser/Ceval.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/cparser/Ceval.ml b/cparser/Ceval.ml index 16305039..87b50e04 100644 --- a/cparser/Ceval.ml +++ b/cparser/Ceval.ml @@ -116,6 +116,7 @@ let unop env op tyres ty v = | Oplus, TInt _, I n -> I n | Oplus, TFloat _, F n -> F n | Olognot, _, _ -> if boolean_value v then I 0L else I 1L + | Onot, _, I n -> I (Int64.lognot n) | _ -> raise Notconst in cast env ty tyres res |