/usr/share/acl2-6.3/books/misc/congruent-stobjs-test.cert is in acl2-books-certs 6.3-5.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 | (IN-PACKAGE "ACL2")
"ACL2 Version 6.3"
:BEGIN-PORTCULLIS-CMDS
:END-PORTCULLIS-CMDS
:EXPANSION-ALIST
((12 RECORD-EXPANSION (EVAL-FORM (UPDATE2 3 ST2)) (VALUE-TRIPLE :NIL)) (14 RECORD-EXPANSION (EVAL-FORM (UPDATE2 7 ST1)) (VALUE-TRIPLE :NIL)) (17 RECORD-EXPANSION (EVAL-FORM (SWAP-ST1-ST2 ST1 ST2)) (VALUE-TRIPLE :NIL)) (19 RECORD-EXPANSION (EVAL-FORM (SWAP-ST1-ST2 ST2 ST1)) (VALUE-TRIPLE :NIL)) (22 RECORD-EXPANSION (MUST-FAIL (DEFSTOBJ ST4 (REG3 :TYPE (ARRAY (UNSIGNED-BYTE 31) (8)) :INITIALLY 0) (PC3 :TYPE (UNSIGNED-BYTE 31) :INITIALLY 555) HALT3 :CONGRUENT-TO ST2)) (VALUE-TRIPLE (QUOTE T))) (23 RECORD-EXPANSION (MUST-FAIL (DEFSTOBJ ST4 (REG4 :TYPE (ARRAY (UNSIGNED-BYTE 31) (8)) :INITIALLY 0) (PC4 :TYPE (UNSIGNED-BYTE 30) :INITIALLY 555) HALT4 (MEM4 :TYPE (ARRAY (UNSIGNED-BYTE 31) (*MEM-SIZE*)) :INITIALLY 0 :RESIZABLE T) :CONGRUENT-TO ST1)) (VALUE-TRIPLE (QUOTE T))) (27 RECORD-EXPANSION (MUST-NOT-TRANSLATE (SWAP-ST1-ST2 ST1 ST1)) (VALUE-TRIPLE (QUOTE T))) (28 RECORD-EXPANSION (MUST-SUCCEED+ (MV-LET (ST1 ST2) (SWAP-ST1-ST2 ST2 ST1) (MV ST1 ST2))) (VALUE-TRIPLE (QUOTE T))) (29 RECORD-EXPANSION (MUST-SUCCEED+ (MV-LET (ST2 ST1) (SWAP-ST1-ST2 ST1 ST2) (MV ST1 ST2))) (VALUE-TRIPLE (QUOTE T))) (30 RECORD-EXPANSION (MUST-NOT-TRANSLATE (MV-LET (ST1 ST2) (SWAP-ST1-ST2 ST1 ST2) (MV ST1 ST2))) (VALUE-TRIPLE (QUOTE T))) (31 RECORD-EXPANSION (MUST-NOT-TRANSLATE (MV-LET (ST2 ST1) (SWAP-ST1-ST2 ST2 ST1) (MV ST1 ST2))) (VALUE-TRIPLE (QUOTE T))) (37 RECORD-EXPANSION (MUST-FAIL+ (WITH-GUARD-CHECKING T (UPDATE3 (QUOTE A) ST2))) (VALUE-TRIPLE :FAILED-AS-EXPECTED)) (38 RECORD-EXPANSION (MUST-FAIL+ (WITH-GUARD-CHECKING T (UPDATE3 (QUOTE A) ST1))) (VALUE-TRIPLE :FAILED-AS-EXPECTED)) (39 RECORD-EXPANSION (MUST-NOT-TRANSLATE (UPDATE3 3 (QUOTE B))) (VALUE-TRIPLE (QUOTE T))) (41 RECORD-EXPANSION (MUST-NOT-TRANSLATE (UPDATE4 3 ST1 ST1)) (VALUE-TRIPLE (QUOTE T))) (45 RECORD-EXPANSION (MUST-FAIL+ (WITH-GUARD-CHECKING T (TEST))) (VALUE-TRIPLE :FAILED-AS-EXPECTED)) (46 RECORD-EXPANSION (MAKE-EVENT (ER-PROGN (PRINT-GV) (VALUE (QUOTE (VALUE-TRIPLE :OK))))) (VALUE-TRIPLE :OK)) (49 RECORD-EXPANSION (MUST-SUCCEED+ (IF (HONS-ENABLEDP STATE) (MEMOIZE (QUOTE H)) (VALUE NIL))) (VALUE-TRIPLE (QUOTE T))) (50 RECORD-EXPANSION (MUST-SUCCEED+ (UPDATE-FLD 0 ST0)) (VALUE-TRIPLE (QUOTE T))) (51 RECORD-EXPANSION (MUST-SUCCEED+ (UPDATE-FLD 1 ST)) (VALUE-TRIPLE (QUOTE T))))
NIL
(("/usr/share/acl2-6.3/books/misc/congruent-stobjs-test.lisp" "congruent-stobjs-test" "congruent-stobjs-test" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1037617697) ("/usr/share/acl2-6.3/books/misc/eval.lisp" "eval" "eval" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1069973718))
708438032
|