Goose  Diff

Differences From Artifact [eb4c342346]:

• File bs/verify/value.cpp — part of check-in [b1d4853b7f] at 2023-05-31 21:34:19 on branch trunk — Lifetimes: implemented verifier's z3 representation (user: zlodo size: 22253)

To Artifact [05b81fc021]:

• File bs/verify/value.cpp — part of check-in [08898dae70] at 2023-06-17 10:15:09 on branch trunk —
  • Remove MemLoc, it's redundant with cir::Address
  • Added compîlation time sequence type
  • Partially handle sequence type in the verifier (to be completed later)
  • Added "SelectPath" builtin type for adress paths
  (user: zlodo size: 22249)

653
654
655
656
657
658
659
660

661
662
663
664
665
666
667

653
654
655
656
657
658
659

660
661
662
663
664
665
666
667

-
+

        b.push( Z3Val
        {
            tc.memLocCtor()(
                ltExpr,
                z3::concat( pathExpr, GetZ3Context().int_val( instr.memberIndex() ).unit() )
            ),

            *EIRToValue( GetValueType< builtins::MemLoc >() ),
            *EIRToValue( GetValueType< cir::Address >() ),
            instr.locationId()
        } );

        return true;
    }

    bool BuildZ3Op( Builder& b, const GhostCall& instr )