[sledge] Global initializers do not contain registers

Summary:
The initializers of globals are constant expressions, and therefore
contain no registers. This change adds an assertion to make this
existing invariant explicit.

Differential Revision: D29441160

fbshipit-source-id: 4da4e74d1
master
Josh Berdine 4 years ago committed by Facebook GitHub Bot
parent 063ddb5784
commit ee4bb29cc4

@ -18,8 +18,10 @@ let pp ppf {name; init; loc} =
let invariant g =
let@ () = Invariant.invariant [%here] g [%sexp_of: t] in
match Global.typ g.name with
( match Global.typ g.name with
| Pointer {elt} -> assert (Option.is_none g.init || Typ.is_sized elt)
| _ -> assert false
| _ -> assert false ) ;
Option.iter g.init ~f:(fun init ->
Exp.fold_regs init () ~f:(fun _ () -> assert false) )
let mk ?init name loc = {name; init; loc} |> check invariant

Loading…
Cancel
Save