diff options
| author | Alasdair | 2020-05-21 15:30:43 +0100 |
|---|---|---|
| committer | Alasdair | 2020-05-21 15:30:43 +0100 |
| commit | 8320ddc4b19d622f8ab5ab8625dde45fccbf383b (patch) | |
| tree | 4ebd634581c6ffe6c5b61ad9437692a1856a81c6 /src/constant_fold.ml | |
| parent | 3311b7d4c5aeebacdbcd14602d7a8a75a9c1b258 (diff) | |
| parent | 92b0564856fb3e20a09bead04d5c1b21eed224e1 (diff) | |
Merge branch 'sail2' into mono-tweaks
Diffstat (limited to 'src/constant_fold.ml')
| -rw-r--r-- | src/constant_fold.ml | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/src/constant_fold.ml b/src/constant_fold.ml index 35417ac8..1c273df1 100644 --- a/src/constant_fold.ml +++ b/src/constant_fold.ml @@ -374,4 +374,10 @@ let () = ~name:"fix_registers" ~help:"Fix the value of specified registers, specified as a \ list of <register>=<value>. Can also fix a specific \ - register field as <register>.<field>=<value>." + register field as <register>.<field>=<value>. Note that \ + this is not used to set registers normally, but instead \ + fixes their value such that the constant folding rewrite \ + (which is subsequently invoked by this command) will \ + replace register reads with the fixed values. Requires a \ + target (c, lem, etc.), as the set of functions that can \ + be constant folded can differ on a per-target basis." |