[acl2/acl2] f45014: VL: start toward statement tests

0 views
Skip to first unread message

GitHub

unread,
Nov 12, 2015, 8:04:10 AM11/12/15
to acl2-...@googlegroups.com
Branch: refs/heads/testing
Home: https://github.com/acl2/acl2
Commit: f450146155cca5e28250276eb7997593fad1afba
https://github.com/acl2/acl2/commit/f450146155cca5e28250276eb7997593fad1afba
Author: Jared C. Davis <jared....@gmail.com>
Date: 2015-11-12 (Thu, 12 Nov 2015)

Changed paths:
M books/centaur/vl/loader/parser/tests/base.lisp
M books/centaur/vl/loader/parser/tests/statements.lisp

Log Message:
-----------
VL: start toward statement tests

This is still terribly incomplete, for now I mainly just want some
tests of call statements since I'm about to go muck with their parser.


Commit: 3ef38a999f7d87ea89ef82e14c50846125c1cc1c
https://github.com/acl2/acl2/commit/3ef38a999f7d87ea89ef82e14c50846125c1cc1c
Author: Jared C. Davis <jared....@gmail.com>
Date: 2015-11-12 (Thu, 12 Nov 2015)

Changed paths:
M books/std/typed-lists/signed-byte-listp.lisp
M books/std/typed-lists/unsigned-byte-listp.lisp

Log Message:
-----------
Better names in (un)signed-byte-listp books

Some of these theorems were using "bytes" as the name of the width
argument to signed/unsigned-byte-p, which was really confusing. Thanks
to David Hardin for pointing this out.


Commit: c62afc3e8bd30417524851beb99e471ebb35e22a
https://github.com/acl2/acl2/commit/c62afc3e8bd30417524851beb99e471ebb35e22a
Author: Jared C. Davis <jared....@gmail.com>
Date: 2015-11-12 (Thu, 12 Nov 2015)

Changed paths:
R books/centaur/vl/lint/lint-stmt-rewrite.lisp
M books/centaur/vl/lint/lucid.lisp
M books/centaur/vl/lint/suppress-warnings.lisp
M books/centaur/vl/loader/parser/statements.lisp
M books/centaur/vl/loader/parser/tests/base.lisp
M books/centaur/vl/loader/parser/tests/statements.lisp
M books/centaur/vl/mlib/fmt.lisp
M books/centaur/vl/mlib/json.lisp
M books/centaur/vl/mlib/stmt-tools.lisp
M books/centaur/vl/mlib/writer.lisp
M books/centaur/vl/parsetree.lisp
M books/centaur/vl/transforms/annotate/type-disambiguation.lisp

Log Message:
-----------
Extend VL support for subroutine calls statements

We now can parse things like void'(...) and otherwise do slightly
better with calls of tasks/functions in statements. None of this
is really supported in SV yet.


Compare: https://github.com/acl2/acl2/compare/e073a4418ccb...c62afc3e8bd3

GitHub

unread,
Nov 12, 2015, 11:13:23 AM11/12/15
to acl2-...@googlegroups.com
Branch: refs/heads/master
Reply all
Reply to author
Forward
0 new messages