Add -Ofixed_int and -Ofixed_bits to assume fixed-precision ints and bitvectors in C

Assumes a Sail C library that has functions with the right types to
support this. Currently lib/int128 supports the -Ofixed_int option,
which was previously -Oint128.

Add a version of Sail C library that can be built with -nostdlib and
-ffreestanding, assuming the above options. Currently just a header
file without any implementation, but with the right types

1 files changed, 10 insertions, 0 deletions

diff --git a/src/slice.ml b/src/slice.ml
index 427d5913..0011bb4d 100644
--- a/src/slice.ml
+++ b/src/slice.ml
@@ -173,6 +173,15 @@ let add_def_to_graph graph def =
        IdSet.iter (fun id -> graph := G.add_edge self (Type id) !graph) (typ_ids typ)
     | LEXP_memory (id, _) ->
        graph := G.add_edge self (Function id) !graph
+    | LEXP_id id ->
+       begin match Env.lookup_id id env with
+       | Register _ -> graph := G.add_edge self (Register id) !graph
+       | Enum _ -> graph := G.add_edge self (Constructor id) !graph
+       | _ ->
+          if IdSet.mem id (Env.get_toplevel_lets env) then
+            graph := G.add_edge self (Letbind id) !graph
+          else ()
+       end
     | _ -> ()
     end;
     LEXP_aux (lexp_aux, annot)
@@ -204,6 +213,7 @@ let add_def_to_graph graph def =
     E_aux (e_aux, annot)
   in
   let rw_exp self = { id_exp_alg with e_aux = (fun (e_aux, annot) -> scan_exp self e_aux annot);
+                                      lEXP_aux = (fun (l_aux, annot) -> scan_lexp self l_aux annot);
                                       pat_alg = rw_pat self } in
 
   let rewriters self =