diff options
Diffstat (limited to 'riscV/Archi.v')
| -rw-r--r-- | riscV/Archi.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/riscV/Archi.v b/riscV/Archi.v index 9e561ca8..96f34276 100644 --- a/riscV/Archi.v +++ b/riscV/Archi.v @@ -72,3 +72,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. |