[acl2/acl2] e8ba4e: VL/SV: preliminary support for parameters of unpac...

[GitHub]

Branch: refs/heads/testing
Home: https://github.com/acl2/acl2
Commit: e8ba4e2d70781320315d5cb2bd34bb2546a2dd1b
https://github.com/acl2/acl2/commit/e8ba4e2d70781320315d5cb2bd34bb2546a2dd1b
Author: Sol Swords <ssw...@centtech.com>
Date: 2016-11-30 (Wed, 30 Nov 2016)

Changed paths:
M books/centaur/sv/vl/elaborate.lisp
M books/centaur/sv/vl/expr.lisp
A books/centaur/sv/vl/literal.lisp
M books/centaur/sv/vl/vl-svstmt.lisp
M books/centaur/vl/loader/parser/paramdecls.lisp
A books/centaur/vl/mlib/arithclass.lisp
M books/centaur/vl/mlib/datatype-tools.lisp
M books/centaur/vl/mlib/hid-tools.lisp
M books/centaur/vl/mlib/mocktype.lisp
M books/centaur/vl/mlib/selfsize.lisp
M books/centaur/vl/mlib/typedecide.lisp
M books/centaur/vl/transforms/unparam/override.lisp

Log Message:
-----------
VL/SV: preliminary support for parameters of unpacked type


Commit: 57db8607361097fc7128a3b18f982b2a3b2ac16b
https://github.com/acl2/acl2/commit/57db8607361097fc7128a3b18f982b2a3b2ac16b
Author: Sol Swords <ssw...@centtech.com>
Date: 2016-11-30 (Wed, 30 Nov 2016)

Changed paths:
M acl2-fns.lisp
M acl2.lisp
M apply-raw.lisp
M axioms.lisp
M books/acl2s/cgen/with-timeout-raw.lsp
M books/acl2s/cgen/with-timeout.lisp
M books/centaur/defrstobj/sketch.lsp
M books/centaur/fty/bitstruct.lisp
M books/centaur/gl/tutorial.lisp
M books/centaur/quicklisp/top.lisp
M books/centaur/sv/cosims/run.lsp
M books/centaur/vl/lint/lucid.lisp
M books/centaur/vl/transforms/addnames.lisp
M books/doc/relnotes.lisp
M books/misc/bash.lisp
M books/misc/check-acl2-exports.lisp
M books/misc/expander.lisp
M books/misc/file-io.lisp
M books/projects/paco/database.lisp
M books/projects/paco/type-set.lisp
R books/projects/x86isa/proofs/dissertation-examples/powOfTwo.lisp
A books/projects/x86isa/proofs/powOfTwo/acl2-customization.lsp
A books/projects/x86isa/proofs/powOfTwo/cert.acl2
A books/projects/x86isa/proofs/powOfTwo/powOfTwo.lisp
M books/projects/x86isa/proofs/top.lisp
A books/projects/x86isa/tools/execution/examples/powOfTwo64.c
A books/projects/x86isa/tools/execution/examples/prefixSum.c
M books/projects/x86isa/utils/utilities.lisp
M books/projects/x86isa/x86-images/x86isa.png
M books/std/util/define.lisp
M books/system/doc/acl2-doc.lisp
A books/system/tests/cached-fn-inst.lisp
M books/tools/removable-runes.lisp
M books/tools/remove-hyps.lisp
M books/workshops/2011/krug-et-al/support/MinVisor/setup-nested-page-tables.lisp
M doc.lisp
M emacs/emacs-acl2.el
M hons-raw.lisp
M memoize-raw.lisp
M memoize.lisp
M other-events.lisp
M proof-builder-b.lisp

Log Message:
-----------
Merge remote-tracking branch 'remotes/origin/testing'


Commit: f218fdeba2ab2464baec14b0dadb8466a4b9bc26
https://github.com/acl2/acl2/commit/f218fdeba2ab2464baec14b0dadb8466a4b9bc26
Author: Sol Swords <ssw...@centtech.com>
Date: 2016-11-30 (Wed, 30 Nov 2016)

Changed paths:
M books/centaur/sv/failtest/Makefile

Log Message:
-----------
mark a few vl failtests as failing


Compare: https://github.com/acl2/acl2/compare/6df548e3b25e...f218fdeba2ab

[GitHub]

Branch: refs/heads/master

Commit: 5ac65ea25b851965b61a0cf7ffbf995d99181f0c
https://github.com/acl2/acl2/commit/5ac65ea25b851965b61a0cf7ffbf995d99181f0c

Author: Sol Swords <ssw...@centtech.com>
Date: 2016-11-30 (Wed, 30 Nov 2016)

Changed paths:

A books/centaur/sv/cosims/paramarray/spec.sv
A books/centaur/sv/cosims/paramarray2/spec.sv

Log Message:
-----------
add vl/sv cosims testing new feature


Commit: 0c45828592f6a1c96685f0f3e19013b6e29a9048
https://github.com/acl2/acl2/commit/0c45828592f6a1c96685f0f3e19013b6e29a9048
Author: David L. Rager <rag...@gmail.com>

Date: 2016-11-30 (Wed, 30 Nov 2016)

Changed paths:

M books/projects/sat/proof-checker-array/farray.lisp

Log Message:
-----------
Merge commit '8656f238c04bb220cb7af86faac40b7b9b7b7d0b' into HEAD


Compare: https://github.com/acl2/acl2/compare/8656f238c04b...0c45828592f6