Rules about push-frame.
In exec-fun, a scope is initialized and a frame is pushed with that scope. Here we provide two theorems to turn that into a canonical representation. Assuming that init-scope is rewritten to a nest of omap::update calls (as it is, because we use rules for init-scope that do that), the two theorems below move the variables into add-var calls, and finally turn push-frame into add-frame.
During symbolic execution,
the values stored into a scope never have flexible array members.
This is because init-scope removes them, if present.
During symbolic execution, these values will satisfy that predicate,
making the application of remove-flexible-array-member
in the omap::update nest disappear,
which justifies its absence
in the left side of
Theorem:
(defthm push-frame-of-one-empty-scope (equal (push-frame (frame fun (list nil)) compst) (add-frame fun compst)))
Theorem:
(defthm push-frame-of-one-nonempty-scope (implies (and (identp var) (valuep val) (scopep scope) (not (flexible-array-member-p val))) (equal (push-frame (frame fun (list (omap::update var val scope))) compst) (add-var var val (push-frame (frame fun (list scope)) compst)))))