diff options
Diffstat (limited to 'aarch64/Archi.v')
| -rw-r--r-- | aarch64/Archi.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/aarch64/Archi.v b/aarch64/Archi.v index 42500e70..7f39d1fa 100644 --- a/aarch64/Archi.v +++ b/aarch64/Archi.v @@ -88,3 +88,5 @@ Global Opaque ptr64 big_endian splitlong (** Whether to generate position-independent code or not *) Parameter pic_code: unit -> bool. + +Definition has_notrap_loads := false. |