		Search-engine friendly clone of the ACL2 documentation.

Vl-lucidocc

Vl-lucidocc-tail

An occurrence of an identifier with something fancy.

This is a product type, introduced by deftagsum in support of vl-lucidocc.

Fields

ctx — vl-context1
ss — vl-scopestack

We use this to record occurrences of a variable where there is additional indexing or some kind of struct field referencing. For instance, if we have a variable, myinst, which is an instruction_t structure, then we might have reads or writes of individual fields, like myinst.opcode or myinst.arg1. We don't currently record what the tail is or analyze it in any sensible way, but this at least allows us to see that something has been read/written.

Subtopics

Vl-lucidocc-tail->ctx: Get the ctx field from a vl-lucidocc-tail.
Make-vl-lucidocc-tail: Basic constructor macro for vl-lucidocc-tail structures.
Vl-lucidocc-tail->ss: Get the ss field from a vl-lucidocc-tail.
Change-vl-lucidocc-tail: Modifying constructor for vl-lucidocc-tail structures.