Rules for executing assignment expressions to identifier expressions.
The first one is used in the large symbolic execution.
The second one is for the new modular proof approach.
Theorem:
(defthm exec-expr-asg-ident (implies (and (syntaxp (quotep e)) (equal (expr-kind e) :binary) (equal (binop-kind (expr-binary->op e)) :asg) (not (zp limit)) (equal e1 (expr-binary->arg1 e)) (equal (expr-kind e1) :ident) (equal val+compst1 (exec-expr-call-or-pure (expr-binary->arg2 e) compst fenv (1- limit))) (equal val (mv-nth 0 val+compst1)) (equal compst1 (mv-nth 1 val+compst1)) (valuep val) (valuep (read-var (expr-ident->get e1) compst1))) (equal (exec-expr-asg e compst fenv limit) (write-var (expr-ident->get e1) val compst1))))
Theorem:
(defthm exec-expr-asg-ident-via-object (implies (and (syntaxp (quotep e)) (equal (expr-kind e) :binary) (equal (binop-kind (expr-binary->op e)) :asg) (not (zp limit)) (equal e1 (expr-binary->arg1 e)) (equal (expr-kind e1) :ident) (equal val+compst1 (exec-expr-call-or-pure (expr-binary->arg2 e) compst fenv (1- limit))) (equal val (mv-nth 0 val+compst1)) (equal compst1 (mv-nth 1 val+compst1)) (valuep val) (equal objdes (objdesign-of-var (expr-ident->get e1) compst1)) objdes) (equal (exec-expr-asg e compst fenv limit) (write-object objdes val compst1))))