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 aef4ab77..7d7b6887 100644 --- a/aarch64/Archi.v +++ b/aarch64/Archi.v @@ -86,3 +86,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. |