Replace cast{8,16}{signed,unsigned} with zero_ext and sign_ext.
lib/Integers.v: added more properties for ARM port. lib/Coqlib.v: added more properties for division and powers of 2. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@928 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Showing
- backend/Cminor.v 4 additions, 4 deletionsbackend/Cminor.v
- backend/Constprop.v 8 additions, 8 deletionsbackend/Constprop.v
- backend/Op.v 12 additions, 12 deletionsbackend/Op.v
- backend/PPC.v 2 additions, 2 deletionsbackend/PPC.v
- backend/PPCgen.v 1 addition, 1 deletionbackend/PPCgen.v
- backend/PPCgenproof.v 2 additions, 2 deletionsbackend/PPCgenproof.v
- backend/PPCgenproof1.v 8 additions, 7 deletionsbackend/PPCgenproof1.v
- backend/Selectionproof.v 12 additions, 8 deletionsbackend/Selectionproof.v
- cfrontend/Cminorgenproof.v 8 additions, 8 deletionscfrontend/Cminorgenproof.v
- cfrontend/Csem.v 4 additions, 4 deletionscfrontend/Csem.v
- common/Mem.v 10 additions, 10 deletionscommon/Mem.v
- common/Values.v 40 additions, 40 deletionscommon/Values.v
- extraction/.depend 9 additions, 3 deletionsextraction/.depend
- lib/Coqlib.v 86 additions, 0 deletionslib/Coqlib.v
- lib/Integers.v 638 additions, 258 deletionslib/Integers.v
Loading
Please register or sign in to comment