| /seL4-l4v-10.1.1/HOL4/polyml/libpolyml/ |
| H A D | Makefile.in | 251 RECURSIVE_TARGETS = all-recursive check-recursive cscopelist-recursive \
942 check-am: all-am
943 check: check-recursive
1053 .PHONY: $(am__recursive_targets) CTAGS GTAGS TAGS all all-am check \
1054 check-am clean clean-generic clean-libLTLIBRARIES \
|
| /seL4-l4v-10.1.1/HOL4/polyml/mlsource/MLCompiler/CodeTree/ |
| H A D | CODETREE_REMOVE_REDUNDANT.sml | 85 So, we check to see whether the result of recursive use has added anything to the
|
| H A D | CODETREE_SIMPLIFIER.sml | 73 is really only a check that the reversed and forward lists
126 to know the size of the item on this platform. We have to make this check
423 (* Build andalso tree to check each byte. For the null string this simply returns "true". *)
780 (* We have to make a special check here that we are not passing in the function
1234 (* When checking for a constant we need to check that there are no bindings.
|
| /seL4-l4v-10.1.1/isabelle/src/Pure/PIDE/ |
| H A D | document.scala | 494 def prune(check: Change => Boolean, retain: Int): Option[(List[Change], History)] =
496 val n = undo_list.iterator.zipWithIndex.find(p => check(p._1)).get._2 + 1
|
| /seL4-l4v-10.1.1/HOL4/polyml/basis/ |
| H A D | Array.sml | 132 check would fail. *)
|
| H A D | TopLevelPolyML.sml | 207 val _ = readToEscape("", #",") (* Should be empty - check? *)
209 val _ = readToEscape("", #"r") (* Should be empty - check? *)
1076 (* Get the current parse tree and check the ID matches *)
1341 (* No exception in compiler: run the code and check that it
|
| H A D | Vector.sml | 57 g.c. performance and causes equality to check for value equality
|
| H A D | Real.sml | 184 precision and then check for overflow if necessary. *)
405 for the number of digits raises Size. The tests also check
|
| H A D | Thread.sml | 353 (* If we are now handling interrupts asynchronously check whether
501 shortly afterwards. The check for !m = 0w1 is an optimisation and nearly
|
| H A D | FinalPolyML.sml | 1083 Otherwise we look at the dependency list and check those. If the result
1084 of that check is that one of the dependencies is newer than the object
1087 them, generating a new dependency list. That is why we don't check the
1805 check the debugging state using getCurrentStack which raises an
2121 (* Try actually loading the file. That way we really check we have a module. *)
|
| /seL4-l4v-10.1.1/l4v/isabelle/src/Pure/PIDE/ |
| H A D | document.scala | 494 def prune(check: Change => Boolean, retain: Int): Option[(List[Change], History)] =
496 val n = undo_list.iterator.zipWithIndex.find(p => check(p._1)).get._2 + 1
|
| /seL4-l4v-10.1.1/seL4/manual/parts/ |
| H A D | ipc.tex | 205 system call, the \apifunc{seL4\_Recv}{sel4_recv} system call does not check that the
|
| H A D | objects.tex | 201 \item[\apifunc{seL4\_NBRecv}{sel4_nbrecv}] is used by a thread to check for
254 polling to check any flags,
|
| /seL4-l4v-10.1.1/HOL4/src/IndDef/ |
| H A D | InductiveDefinition.sml | 732 (* check that tm has no extra type variables or free variables other than *)
751 (* check that there aren't duplicate names in the forall chain *)
|
| /seL4-l4v-10.1.1/HOL4/src/meson/src/ |
| H A D | mesonLib.sml | 307 then failwith "augment1: Occurs check"
338 if fol_free_in v t' then failwith "augment_insts: Occurs check"
|
| /seL4-l4v-10.1.1/HOL4/src/metis/ |
| H A D | folMapping.sml | 80 fun check s = assert (String.isPrefix p s) (ERR "dest_prefix" "") function
83 fn s => (check s; String.extract (s, size_p, NONE))
|
| /seL4-l4v-10.1.1/HOL4/src/pattern_matches/ |
| H A D | patternMatchesScript.sml | 652 (* Fancy redundancy check *)
934 This is handy for avoiding complicated procedures to check,
|
| /seL4-l4v-10.1.1/HOL4/examples/lambda/other-models/ |
| H A D | ncScript.sml | 661 (* Sanity check - try to prove Lemma 1.14 from Hindley and Seldin using *)
703 (* Sanity check: set of free variables is finite. This was a postulate *)
|
| /seL4-l4v-10.1.1/isabelle/src/Pure/Admin/ |
| H A D | build_status.scala | 441 result.error("Gnuplot failed for " + data_name + "/" + plot_name).check
|
| /seL4-l4v-10.1.1/isabelle/src/Pure/Tools/ |
| H A D | server.scala | 382 Isabelle_System.bash("chmod 600 " + File.bash_path(Data.database)).check
|
| /seL4-l4v-10.1.1/l4v/isabelle/src/Pure/Admin/ |
| H A D | build_status.scala | 441 result.error("Gnuplot failed for " + data_name + "/" + plot_name).check
|
| /seL4-l4v-10.1.1/l4v/isabelle/src/Pure/Tools/ |
| H A D | server.scala | 382 Isabelle_System.bash("chmod 600 " + File.bash_path(Data.database)).check
|
| /seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/m0/step/ |
| H A D | m0_stepLib.sml | 1053 fun check (l, s) thm = function
1073 then check (v, "is a Thumb-2 prefix")
1076 then check (v, "is not a Thumb-2 instruction")
|
| /seL4-l4v-10.1.1/HOL4/Manual/Description/ |
| H A D | holCheck.tex | 340 This property says that A has a winning strategy from the current state. Since we define success if the set of states satisfying the property contains the set of initial states, this suffices to check that A has a winning strategy. Cleaned up, this is the \ctl property \[ \mathbf{EG} (\textup{(A wins)} \lor (\textup{A to move} \land \mathbf{EF} (\textup{A wins})) \lor (\textup{B to move} \land \mathbf{AF} (\textup{A wins})))\] Intuitively, the property says that there exists a path from the current state such that at each step on that path either A has won the game, or it is A's turn and there exists at least one path in which A eventually wins the game, or it is not A's turn and on all paths A eventually wins the game.
536 For those familiar with model checking, this is \emph{not} assume-guarantee reasoning, nor does it use simulation pre-orders. It is considerably more simple: take a product Kripke structure, break up the components, model check each component, re-compose. Unlike assume-guarantee reasoning, this does not apply to properties that address truly global aspects of the system. Also, it is limited to synchronous systems. Nevertheless, there are some applications in hardware verification.
560 \hc{} implements a fully automatic abstraction refinement framework that is invisible to the user. A simple heuristic analysis is used to decide whether or not to apply abstraction for a given property. Sometimes the abstraction may make things worse. If \hc{} appears to be taking overly long on a property, the user may try redoing the check, after turning off abstraction. This can be done by calling \texttt{set\_flag\_abs} on the model. Turning abstraction on and off on a per-property basis is not supported yet.
|
| /seL4-l4v-10.1.1/HOL4/Manual/Translations/IT/Description/ |
| H A D | holCheck.tex | 340 This property says that A has a winning strategy from the current state. Since we define success if the set of states satisfying the property contains the set of initial states, this suffices to check that A has a winning strategy. Cleaned up, this is the \ctl property \[ \mathbf{EG} (\textup{(A wins)} \lor (\textup{A to move} \land \mathbf{EF} (\textup{A wins})) \lor (\textup{B to move} \land \mathbf{AF} (\textup{A wins})))\] Intuitively, the property says that there exists a path from the current state such that at each step on that path either A has won the game, or it is A's turn and there exists at least one path in which A eventually wins the game, or it is not A's turn and on all paths A eventually wins the game.
536 For those familiar with model checking, this is \emph{not} assume-guarantee reasoning, nor does it use simulation pre-orders. It is considerably more simple: take a product Kripke structure, break up the components, model check each component, re-compose. Unlike assume-guarantee reasoning, this does not apply to properties that address truly global aspects of the system. Also, it is limited to synchronous systems. Nevertheless, there are some applications in hardware verification.
560 \hc{} implements a fully automatic abstraction refinement framework that is invisible to the user. A simple heuristic analysis is used to decide whether or not to apply abstraction for a given property. Sometimes the abstraction may make things worse. If \hc{} appears to be taking overly long on a property, the user may try redoing the check, after turning off abstraction. This can be done by calling \texttt{set\_flag\_abs} on the model. Turning abstraction on and off on a per-property basis is not supported yet.
|