| /seL4-l4v-10.1.1/HOL4/examples/HolCheck/ |
| H A D | decompScript.sml | 80 (* ASSERT: note also that this only works if the L are defined as \s p. p s; the 3rd and 4th assums *)
|
| H A D | cacheTools.sml | 649 (* ASSERT: mf = uniq mf (fv mf) [] *)
|
| H A D | cearTools.sml | 508 (* ASSERT: t must be a QBF *)
|
| H A D | muCheck.sml | 540 (* if ado then start from where we left off. ASSERT:ado==>Option.isSome bvtb *)
|
| /seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/arm8/model/ |
| H A D | arm8.sig | 382 exception ASSERT of string exception
|
| H A D | arm8.sml | 826 exception ASSERT of string exception
|
| H A D | arm8Script.sml | 364 [("ALIGNMENT_FAULT",[]),("ASSERT",[sTy]),("NoException",[]),
|
| /seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/m0/model/ |
| H A D | m0.sig | 148 exception ASSERT of string exception
|
| /seL4-l4v-10.1.1/HOL4/examples/acl2/examples/M1/ |
| H A D | PKGS.sml | 216 ("ASSERT" , "ACL2" , "COMMON-LISP"),
1198 ("ASSERT" , "ACL2-USER" , "COMMON-LISP"),
1199 ("ASSERT$" , "ACL2-USER" , "ACL2"),
3111 ("ASSERT" , "U" , "COMMON-LISP"),
3112 ("ASSERT$" , "U" , "ACL2"),
4947 ("ASSERT" , "ACL2-ASG" , "COMMON-LISP"),
4948 ("ASSERT$" , "ACL2-ASG" , "ACL2"),
6796 ("ASSERT" , "ACL2-AGP" , "COMMON-LISP"),
6797 ("ASSERT$" , "ACL2-AGP" , "ACL2"),
8645 ("ASSERT" , "ACL
[all...] |
| H A D | axioms.ml | 3063 "CDAADR") (mkpair (mksym "COMMON-LISP" "ASSERT") (mkpair (mksym "COMMON-LISP"
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/acl2/tests/inputs/ |
| H A D | PKGS.sml | 175 ("ASSERT" , "ACL2" , "COMMON-LISP"),
1157 ("ASSERT" , "ACL2-USER" , "COMMON-LISP"),
1158 ("ASSERT$" , "ACL2-USER" , "ACL2"),
3070 ("ASSERT" , "U" , "COMMON-LISP"),
3071 ("ASSERT$" , "U" , "ACL2"),
4906 ("ASSERT" , "ACL2-ASG" , "COMMON-LISP"),
4907 ("ASSERT$" , "ACL2-ASG" , "ACL2"),
6755 ("ASSERT" , "ACL2-AGP" , "COMMON-LISP"),
6756 ("ASSERT$" , "ACL2-AGP" , "ACL2"),
8604 ("ASSERT" , "ACL
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/arm/model/ |
| H A D | arm.sml | 1542 exception ASSERT of string exception
2389 | BitsN.B(0xF,_) => raise ASSERT "LookUpRName: n >= 0 and n <= 14"
2537 | _ => raise ASSERT "mem: size in {1, 2, 4, 8}";
2668 | _ => raise ASSERT "mem: size in {1, 2, 4, 8}";
2684 | _ => raise ASSERT "BigEndianReverse: n in {1, 2, 4, 8}";
2914 then raise ASSERT "SignedSatQ: M < N"
2929 then raise ASSERT "UnsignedSatQ: M < N"
2950 ( if shift = 0 then raise ASSERT "LSL_C" else ()
2963 ( if shift = 0 then raise ASSERT "LSR_C" else ()
2972 ( if shift = 0 then raise ASSERT "ASR_
[all...] |
| H A D | arm.sig | 377 exception ASSERT of string exception
|
| H A D | armScript.sml | 329 [("ASSERT",[sTy]),("AlignmentFault",[F32]),
1843 ("ASSERT",CTy"exception",
2244 ("ASSERT",CTy"exception",LS"mem: size in {1, 2, 4, 8}")),
2400 ("ASSERT",CTy"exception",
2431 ("ASSERT",CTy"exception",
3052 Call("ASSERT",CTy"exception",LS"SignedSatQ: M < N")),
3070 ("ASSERT",CTy"exception",LS"UnsignedSatQ: M < N")),
3122 Call("ASSERT",CTy"exception",LS"LSL_C")),
3149 Call("ASSERT",CTy"exception",LS"LSR_C")),
3176 Call("ASSERT",CT
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/acl2/ml/ |
| H A D | hol_defaxioms_proofsScript.sml | 2195 csym "BOOLE-NOR"; csym "CDAADR"; csym "ASSERT";
2792 csym "BOOLE-NOR"; csym "CDAADR"; csym "ASSERT";
|
| H A D | kpa-v2-9-3.ml | 937 ("ASSERT", "ACL2-USER", "COMMON-LISP"),
1915 ("ASSERT", "ACL2", "COMMON-LISP"),
|
| H A D | acl2_packageScript.sml | 1048 ("ASSERT", "ACL2-USER", "COMMON-LISP"),
2026 ("ASSERT", "ACL2", "COMMON-LISP"),
|
| H A D | defaxioms.lisp.trans.ml | 10551 "CDAADR") (mkpair (mksym "COMMON-LISP" "ASSERT") (mkpair (mksym "COMMON-LISP"
|
| /seL4-l4v-10.1.1/HOL4/examples/acl2/examples/acl2-hol-ltl-paper-example/ |
| H A D | acl2_packageScript.sml | 1048 ("ASSERT", "ACL2-USER", "COMMON-LISP"),
2026 ("ASSERT", "ACL2", "COMMON-LISP"),
|
| /seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/monadic-arm/ |
| H A D | armScript.sml | 289 [("ASSERT",[sTy]),("IMPLEMENTATION_DEFINED",[sTy]),("NoException",[]),
3119 ("ASSERT",CTy"exception",LS"LookUpRName: n >= 0 and n <= 14")))]))
3851 ("ASSERT",CTy"exception",
4313 ("ASSERT",CTy"exception",
4342 ("ASSERT",CTy"exception",
5359 Call("ASSERT",CTy"exception",LS"SignedSatQ: M < N")),
5377 Call("ASSERT",CTy"exception",LS"UnsignedSatQ: M < N")),
5411 Call("ASSERT",CTy"exception",LS"LSL_C")),MU(LU,qTy)),
5435 Call("ASSERT",CTy"exception",LS"LSR_C")),MU(LU,qTy)),
5458 Call("ASSERT",CT
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/acl2/tests/round-trip/gold/ |
| H A D | axioms.sml | 3063 "CDAADR") (mkpair (mksym "COMMON-LISP" "ASSERT") (mkpair (mksym "COMMON-LISP"
[all...] |