		Search-engine friendly clone of the ACL2 documentation.

Lucid

Vl-lucidstate

State for the lucid transform.

This is a product type introduced by defprod.

Fields

Main database mapping keys to their use/set occurrences.

modportsp — booleanp

Should we issue warnings for modports? It generally will only make sense to do this before unparameterization has taken place, because unparameterization can change the names of interfaces and our argresolve handling drops the arg.modport stuff in a way that makes this too hard to handle.

paramsp — booleanp

Should we issue warnings for parameters? It generally will only make sense to do this before unparameterization has taken place, because unparameterization should generally get rid of any sensible parameters.

generatesp — booleanp

Should we include multidrive warnings in generates? It will generally only make sense to do this after unparameterization, because until then things like

if (condition) assign foo = 1;
                   else assign foo = 0;

may appear to be multiple assignments to foo, even though they never happen at the same time.

warnings — vl-warninglist

Subtopics

Vl-lucidstate-p: Recognizer for vl-lucidstate structures.
Vl-lucidctx: Info about a usage/setting of an identifier
Vl-lucidstate-fix: Fixing function for vl-lucidstate structures.
Vl-lucidval: Use/set information about a single variable.
Vl-lucidocc: Record of an occurrence of an identifier.
Vl-lucidkey: A single key in the lucid database.
Vl-lucidstate-equiv: Basic equivalence relation for vl-lucidstate structures.
Make-vl-lucidstate: Basic constructor macro for vl-lucidstate structures.
Vl-lucidstate->warnings: Get the warnings field from a vl-lucidstate.
Vl-lucidstate->modportsp: Get the modportsp field from a vl-lucidstate.
Vl-lucidstate->generatesp: Get the generatesp field from a vl-lucidstate.
Vl-luciddb-count
Change-vl-lucidstate: Modifying constructor for vl-lucidstate structures.
Vl-lucidstate->paramsp: Get the paramsp field from a vl-lucidstate.
Vl-lucidstate->db: Get the db field from a vl-lucidstate.
Vl-lucidocc->ctx
Vl-lucidocc->ss
Vl-luciddb: The main lucid database. Binds keys (scopestack/item pairs) to information about how they have been used.
Vl-lucidocclist: A list of vl-lucidocc-p objects.
Vl-lucidkeylist: A list of vl-lucidkey-p objects.