/seL4-l4v-10.1.1/HOL4/examples/HolCheck/ |
H A D | holCheck.sig | 4 val holCheck : modelTools.model -> modelTools.model
|
H A D | holCheckLib.sig | 6 type model = modelTools.model type 8 val holCheck : model -> model 12 val empty_model : model 14 val set_init : Term.term -> model -> model 15 val set_trans : (string * Term.term) list -> model -> model 16 val set_flag_ric : bool -> model [all...] |
H A D | modelTools.sig | 6 type model type 9 val empty_model : model 11 val get_init : model -> Term.term 12 val get_trans : model ->(string * Term.term) list 13 val get_flag_ric : model -> bool 14 val get_name : model -> string option 15 val get_vord : model -> string list option 16 val get_state : model -> Term.term option 17 val get_props : model -> (string * Term.term) list 18 val get_results : model [all...] |
H A D | modelTools.sml | 2 (* this contains all info about the model, including the properties to be checked, and th eventual results *) 21 type model = {init: term option, type 37 fun get_name (m:model) = #name(m) 38 fun get_init (m:model) = valOf (#init(m)) 39 fun get_trans (m:model) = valOf (#trans(m)) 40 fun get_flag_ric (m:model) = valOf (#ric(m)) 41 fun get_vord (m:model) = #vord(m) 42 fun get_state (m:model) = #state(m) 43 fun get_props (m:model) = valOf (#props(m)) 44 fun get_results (m:model) [all...] |
/seL4-l4v-10.1.1/seL4/include/arch/x86/arch/machine/ |
H A D | timer.h | 16 #include <arch/model/statedata.h>
|
/seL4-l4v-10.1.1/seL4/src/config/ |
H A D | default_domain.c | 12 #include <model/statedata.h>
|
/seL4-l4v-10.1.1/HOL4/src/metis/ |
H A D | mlibModel.sig | 13 (* The parts of the model that are fixed and cannot be perturbed *) 14 (* Note: a model of size N has integer elements 0...N-1 *) 34 type model type 37 val new : parameters -> model 38 val size : model -> int 41 val evaluate_term : model -> term -> int 42 val evaluate_formula : model -> formula -> bool 44 (* Check whether a random grounding of a formula is satisfied by the model *) 45 val check : model -> formula -> bool 46 val checkn : model [all...] |
/seL4-l4v-10.1.1/seL4/include/model/ |
H A D | smp.h | 18 #include <arch/model/statedata.h> 19 #include <model/statedata.h>
|
/seL4-l4v-10.1.1/seL4/src/model/ |
H A D | preemption.c | 12 #include <model/preemption.h> 13 #include <model/statedata.h>
|
H A D | smp.c | 14 #include <model/smp.h>
|
/seL4-l4v-10.1.1/l4v/spec/cspec/c/ |
H A D | config_sched.c | 12 #include <model/statedata.h>
|
/seL4-l4v-10.1.1/seL4/include/arch/x86/arch/model/ |
H A D | smp.h | 18 #include <arch/model/statedata.h> 19 #include <model/statedata.h> 20 #include <model/smp.h> 21 #include <mode/model/smp.h>
|
/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/ |
H A D | Model.sig | 16 (* A model of size N has integer elements 0...N-1. *) 26 (* The parts of the model that are fixed. *) 55 (* Renaming fixed model parts. *) 67 (* Standard fixed model parts. *) 202 type model type 206 val new : parameters -> model 208 val size : model -> int 211 (* Interpreting terms and formulas in the model. *) 214 val interpretFunction : model -> Term.functionName * element list -> element 216 val interpretRelation : model [all...] |
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/ |
H A D | Model.sig | 16 (* A model of size N has integer elements 0...N-1. *) 26 (* The parts of the model that are fixed. *) 55 (* Renaming fixed model parts. *) 67 (* Standard fixed model parts. *) 202 type model type 206 val new : parameters -> model 208 val size : model -> int 211 (* Interpreting terms and formulas in the model. *) 214 val interpretFunction : model -> Term.functionName * element list -> element 216 val interpretRelation : model [all...] |
/seL4-l4v-10.1.1/seL4/src/arch/x86/machine/ |
H A D | cpu_identification.c | 14 /** @file Support routines for identifying the processor family, model, etc 15 * on INTEL x86 processors, as well as attempting to determine the model string. 57 uint8_t family, model; member in struct:family_model 65 * require you to take into account an additional extended family and model 84 * Additionally, even though the Intel manuals say to adjust the model 96 ci->display.model = (ci->display.extended_model << 4u) + original.model; 98 ci->display.model = original.model; 107 * the family and model ID [all...] |
/seL4-l4v-10.1.1/seL4/include/arch/arm/arch/model/ |
H A D | statedata.h | 16 #include <model/statedata.h>
|
/seL4-l4v-10.1.1/isabelle/src/Tools/VSCode/src/ |
H A D | vscode_resources.scala | 50 (_, model) <- models.iterator 51 blob <- model.get_blob 52 } yield (model.node_name -> blob)).toMap) 66 sealed case class Caret(file: JFile, model: Document_Model, offset: Text.Offset) 68 def node_name: Document.Node.Name = model.node_name 134 case Some(model) => Some(model.content.text) 142 case Some(model) => f(Scan.char_reader(model.content.text)) 156 case Some(model) [all...] |
H A D | preview_panel.scala | 29 case Some(model) => 30 val snapshot = model.snapshot()
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/VSCode/src/ |
H A D | vscode_resources.scala | 50 (_, model) <- models.iterator 51 blob <- model.get_blob 52 } yield (model.node_name -> blob)).toMap) 66 sealed case class Caret(file: JFile, model: Document_Model, offset: Text.Offset) 68 def node_name: Document.Node.Name = model.node_name 134 case Some(model) => Some(model.content.text) 142 case Some(model) => f(Scan.char_reader(model.content.text)) 156 case Some(model) [all...] |
H A D | preview_panel.scala | 29 case Some(model) => 30 val snapshot = model.snapshot()
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/hoare-triple/ |
H A D | temporalScript.sml | 33 SPEC_1 model pre code post err <=> 34 TEMPORAL model code 40 val INIT = `?to_set next instr less allow. model = (to_set,next,instr,less,allow)` 44 `SPEC model pre code post <=> 45 TEMPORAL model code (T_IMPLIES (NOW pre) (EVENTUALLY (NOW post)))`, 54 `TEMPORAL model code (ALWAYS p) <=> TEMPORAL model code p`, 74 `TEMPORAL model code (T_IMPLIES p1 (NEXT p2)) ==> 75 TEMPORAL model code (T_IMPLIES p1 (EVENTUALLY p2))`, 82 ``SPEC_1 model pr [all...] |
/seL4-l4v-10.1.1/seL4/src/plat/pc99/machine/ |
H A D | hardware.c | 14 #include <arch/model/statedata.h> 99 if (model_info->model == valid_models[i]) { 111 if (model_info->model == NEHALEM_1_MODEL_ID || 112 model_info->model == NEHALEM_2_MODEL_ID || 113 model_info->model == NEHALEM_3_MODEL_ID) { 120 /* We just found the matching model, so no point continuing the search */
|
/seL4-l4v-10.1.1/seL4/src/arch/x86/32/model/ |
H A D | statedata.c | 12 #include <mode/model/statedata.h>
|
/seL4-l4v-10.1.1/seL4/include/arch/arm/arch/ |
H A D | benchmark_overflowHandler.h | 19 #include <model/statedata.h>
|
/seL4-l4v-10.1.1/seL4/include/arch/arm/armv/armv6/armv/ |
H A D | context_switch.h | 15 #include <mode/model/statedata.h>
|