Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | - Revised non-overflow constraints on memory injections so that | xleroy | 2012-07-23 | 1 | -0/+1 |
| | | | | | | | | | | injections compose (Values, Memdata, Memory) - Memory chunks: Mfloat64 now has alignment 8; introduced Mfloat64al32 that works like old Mfloat64 (i.e. has alignment 4); simplified handling of memcpy builtin accordingly. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1983 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e | ||||
* | Added volatile_read_global and volatile_store_global builtins. | xleroy | 2012-01-15 | 1 | -0/+6 |
| | | | | | | | Finished updating IA32 and ARM ports. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1792 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e | ||||
* | Forgot to add new file | xleroy | 2011-06-14 | 1 | -0/+40 |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1673 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e |