		Search-engine friendly clone of the ACL2 documentation.

Json-encoders

Vl-jp-constint

Signature
(vl-jp-constint x &key (ps 'ps)) → ps
Arguments: x — Guard (vl-value-p x).

Note that we always encode the value as a string. This is because it is quite common for Verilog constants to run into the hundreds of bits, but the JSON standard doesn't really ever say how big of numbers must be supported and JSON implementations often use machine integers which could not hold such large values.

Definitions and Theorems

Function: vl-jp-constint-fn

(defun vl-jp-constint-fn (x ps)
  (declare (xargs :stobjs (ps)))
  (declare (xargs :guard (vl-value-p x)))
  (declare (xargs :guard (equal (vl-value-kind x) :vl-constint)))
  (let ((__function__ 'vl-jp-constint))
    (declare (ignorable __function__))
    (jp-object
         :tag (jp-sym (vl-value-kind x))
         :origwidth (jp-nat (vl-constint->origwidth x))
         :value (jp-bignat (vl-constint->value x))
         :origsign (jp-str (symbol-name (vl-constint->origsign x)))
         :wasunsized (jp-bool (vl-constint->wasunsized x)))))