diff options
| author | Alasdair Armstrong | 2018-02-16 18:37:25 +0000 |
|---|---|---|
| committer | Alasdair Armstrong | 2018-02-16 18:38:51 +0000 |
| commit | 8403ad68b451f9d41baa52087af5fd7acef6bc58 (patch) | |
| tree | 0b8acb49371f471838b5e7298fea8cd2c0d1aa08 /lib | |
| parent | d864aa242ac00ecee08d6d2792a0803ba5450d86 (diff) | |
Add __TakeColdReset function to aarch64_no_vector
Turns out the __TakeColdReset function is actually in the v8.3 XML. I
went and looked for it, and it's there, it just wasn't being picked up
by ASL parser because it's not called from any instructions. I added a
new field to the json config files for ASL parser that can tell it
about any such special functions that it should guarantee to include.
Also fixed a bug in C loop compilation
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/smt.sail | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/lib/smt.sail b/lib/smt.sail index 702b82c6..24e0d148 100644 --- a/lib/smt.sail +++ b/lib/smt.sail @@ -15,11 +15,11 @@ val mod = { lem: "integerMod" } : forall 'n 'm. (atom('n), atom('m)) -> {'o, 'o = mod('n, 'm). atom('o)} -val abs = { +val abs_atom = { smt : "abs", ocaml: "abs_int", lem: "abs_int" -} : forall 'n. atom('n) -> {'o, 'o = abs('n). atom('o)} +} : forall 'n. atom('n) -> {'o, 'o = abs_atom('n). atom('o)} $ifdef TEST |