		Search-engine friendly clone of the ACL2 documentation.

Vl-lint

Leftright-check

Check for strange expressions like A [op] A.

This is a heuristic for generating warnings, inspired by PVS Studio. It has found a few pretty minor things that we were able to clean up, and also found one interesting copy/paste bug.

We look for identical sub-expressions on the left and right of most binary operations, for instance A | A and A == A. It is usually pretty strange to write such an expression, and sometimes these indicate copy/paste errors. We do similar checking for the then- and else-branches of ?: operators.

We also look for part-selects that use the same expressions for both indices, e.g., foo[3:3], but these are somewhat more common and minor, and sometimes result from macros or parameterized modules, so we generally think these are pretty minor and uninteresting.

Subtopics

Vl-packagelist-leftright-check: (vl-packagelist-leftright-check x ss) maps vl-package-leftright-check across a list.
Vl-modulelist-leftright-check: (vl-modulelist-leftright-check x ss) maps vl-module-leftright-check across a list.
Vl-interfacelist-leftright-check: (vl-interfacelist-leftright-check x ss) maps vl-interface-leftright-check across a list.
Vl-collect-ac-args: Collect the nested arguments to an associative/commutative operator.
Vl-leftright-exprlist-duplicates: Optimized duplicate expression gatherer for leftright checking.
Vl-interface-leftright-check
Vl-package-leftright-check
Vl-module-leftright-check
Vl-expr-leftright-check1: Search for strange expressions like A [op] A.
Vl-expr-leftright-check
Vl-expr-indexy-via-ctx
Vl-ctxexprlist-leftright-check
Vl-design-leftright-check
Vl-ctxexprlist-leftright-check-nrev
Vl-op-ac-p: Recognizes the associative/commutative binary vl-op-ps.