| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (2159 entries) |
| Instance Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (55 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (33 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (8 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (953 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (20 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (161 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (4 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (48 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (670 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (33 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (90 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (36 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (48 entries) |
Global Index
A
Abs [module, in veric.juicy_mem_ops]AbsPrimcom [inductive, in veric.juicy_mem_ops]
AbsPrimcom_free [constructor, in veric.juicy_mem_ops]
AbsPrimcom_alloc [constructor, in veric.juicy_mem_ops]
AbsPrimcom_store [constructor, in veric.juicy_mem_ops]
AbsPrimexpr [inductive, in veric.juicy_mem_ops]
abstract [instance, in veric.juicy_mem_ops]
access_cohere [definition, in veric.juicy_mem]
access_at [definition, in veric.juicy_mem]
address [definition, in veric.local]
address_mapsto_zeros_eq [lemma, in veric.seplog]
address_mapsto_zeros' [definition, in veric.seplog]
address_mapsto_zeros [definition, in veric.seplog]
address_mapsto_VALspec_range [lemma, in veric.seplog]
address_mapsto_exists [lemma, in veric.seplog]
address_mapsto_exists' [lemma, in veric.juicy_mem_lemmas]
address_mapsto_overlap [lemma, in veric.res_predicates]
address_mapsto_precise [lemma, in veric.res_predicates]
address_mapsto_VALspec_range [lemma, in veric.res_predicates]
address_mapsto_exists [lemma, in veric.res_predicates]
address_mapsto_VALspec [lemma, in veric.res_predicates]
address_mapsto_splittable [lemma, in veric.res_predicates]
address_mapsto_old_parametric [lemma, in veric.res_predicates]
address_mapsto_fun [lemma, in veric.res_predicates]
address_mapsto'_mapsto [lemma, in veric.res_predicates]
address_mapsto' [definition, in veric.res_predicates]
address_mapsto [definition, in veric.res_predicates]
address_mapsto_old [definition, in veric.res_predicates]
address_mapsto_can_store [lemma, in veric.semax_straight]
address_mapsto_zeros [definition, in veric.SeparationLogic]
address_mapsto [definition, in veric.SeparationLogic]
add_variables_nextblock [lemma, in veric.initialize]
add_globals_hack [lemma, in veric.initial_world]
adr_range_zle_fact [lemma, in veric.juicy_mem]
adr_range_inv [lemma, in veric.juicy_mem]
adr_range_eq_block [lemma, in veric.juicy_mem]
adr_inv [lemma, in veric.juicy_mem]
adr_inv0 [lemma, in veric.juicy_mem]
adr_range_split_lem3 [lemma, in veric.assert_lemmas]
adr_range_split_lem2 [lemma, in veric.assert_lemmas]
adr_range_split_lem1 [lemma, in veric.assert_lemmas]
adr_range_zle_zlt [lemma, in veric.juicy_mem_lemmas]
adr_range_divide [lemma, in veric.initial_world]
ADR_VAL0.kind [axiom, in veric.rmaps]
ADR_VAL0.some_address [axiom, in veric.rmaps]
ADR_VAL0.address [axiom, in veric.rmaps]
ADR_VAL0 [module, in veric.rmaps]
ADR_VAL.valid_join [axiom, in veric.rmaps]
ADR_VAL.valid_empty [axiom, in veric.rmaps]
ADR_VAL.valid [axiom, in veric.rmaps]
ADR_VAL.kind [axiom, in veric.rmaps]
ADR_VAL.some_address [axiom, in veric.rmaps]
ADR_VAL.address [axiom, in veric.rmaps]
ADR_VAL [module, in veric.rmaps]
after_alloc [definition, in veric.juicy_mem]
after_alloc'_ok [lemma, in veric.juicy_mem]
after_alloc'_valid [lemma, in veric.juicy_mem]
after_alloc' [definition, in veric.juicy_mem]
age_laterR [lemma, in veric.semax_lemmas]
age_core [lemma, in veric.semax_call]
age_twin' [lemma, in veric.semax_call]
age_jm_phi [lemma, in veric.juicy_mem]
age_jm_dry [lemma, in veric.juicy_mem]
age_safe [lemma, in veric.juicy_extspec]
age_resource_decay [lemma, in veric.juicy_extspec]
age1_resource_decay [lemma, in veric.semax_lemmas]
age1_juicy_mem_Some [lemma, in veric.juicy_mem]
age1_juicy_mem_None2 [lemma, in veric.juicy_mem]
age1_juicy_mem_None1 [lemma, in veric.juicy_mem]
age1_juicy_mem_unpack'' [lemma, in veric.juicy_mem]
age1_juicy_mem_unpack' [lemma, in veric.juicy_mem]
age1_juicy_mem_unpack [lemma, in veric.juicy_mem]
age1_juicy_mem [definition, in veric.juicy_mem]
age1_constructive_joins_eq [lemma, in veric.juicy_mem]
age1_joinx [lemma, in veric.juicy_mem]
alloc_vars_lemma [lemma, in veric.semax_call]
alloc_vars_lookup [lemma, in veric.semax_call]
alloc_juicy_variables_e [lemma, in veric.semax_call]
alloc_juicy_variables [definition, in veric.semax_call]
alloc_dry_updated_on [lemma, in veric.juicy_mem]
alloc_dry_unchanged_on [lemma, in veric.juicy_mem]
alloc_cohere [definition, in veric.juicy_mem]
alloc_variables_fun [lemma, in veric.Clight_lemmas]
alloc_Gfun_inflate [lemma, in veric.initialize]
alloc_global_inflate_same [lemma, in veric.initialize]
alloc_global_access [lemma, in veric.initialize]
alloc_global_beyond2 [lemma, in veric.initialize]
alloc_global_old [lemma, in veric.initial_world]
alloc_globals_rev_nextblock [lemma, in veric.initial_world]
alloc_globals_rev_eq [lemma, in veric.initial_world]
alloc_globals_app [lemma, in veric.initial_world]
alloc_globals_rev [definition, in veric.initial_world]
alloc_variables_mem_wd [lemma, in veric.Clight_coop]
alloc_variables_forward [lemma, in veric.Clight_coop]
allowedValCast [definition, in veric.expr]
allowed_val_cast_sound [lemma, in veric.expr]
allowed_val_cast_sound [lemma, in veric.expr_lemmas]
all_assertions_computable [definition, in veric.semax_lemmas]
all_VALs [definition, in veric.juicy_mem]
all_initializers_aligned [definition, in veric.initialize]
all_initializers_aligned [definition, in veric.SeparationLogic]
always [definition, in veric.expr]
andb_if [lemma, in veric.expr]
and_FF [lemma, in veric.semax_lemmas]
and_True [lemma, in veric.expr]
and_False [lemma, in veric.expr]
another_hackfun_lemma [lemma, in veric.initialize]
any_environ [definition, in veric.expr]
approx_map_idem [lemma, in veric.juicy_mem]
approx_eq_i [lemma, in veric.res_predicates]
approx_oo_approx'' [lemma, in veric.semax_prog]
arglist [definition, in veric.semax]
arglist [definition, in veric.SeparationLogic]
arg_type [constructor, in veric.expr]
assert [definition, in veric.seplog]
assert_safe_last' [lemma, in veric.semax_lemmas]
assert_safe_adj' [lemma, in veric.semax_lemmas]
assert_safe_adj [lemma, in veric.semax_lemmas]
assert_safe_last [lemma, in veric.semax_lemmas]
assert_truth [lemma, in veric.assert_lemmas]
assert_safe [definition, in veric.semax]
assert_lemmas [library]
assign_loc_fun [lemma, in veric.Clight_lemmas]
assign_loc_mem_wd [lemma, in veric.Clight_coop]
assign_loc_forward [lemma, in veric.Clight_coop]
assoc_list_get [definition, in veric.semax]
B
BAdd [constructor, in veric.local]base [library]
believe [definition, in veric.semax]
believepred [definition, in veric.semax]
believe_internal [definition, in veric.semax]
believe_internal_ [definition, in veric.semax]
believe_external [definition, in veric.semax]
beyond_block [definition, in veric.initialize]
binarithType [definition, in veric.expr]
binary_operation_val_valid [lemma, in veric.Clight_coop]
bind_ret [definition, in veric.seplog]
bind_args [definition, in veric.seplog]
bind_parameters_fun [lemma, in veric.Clight_lemmas]
bind_ret [definition, in veric.SeparationLogic]
binop [inductive, in veric.local]
binopDenote [definition, in veric.local]
binop_lemmas [library]
blockslice_mpred_rmap [definition, in veric.initialize]
blockslice_mpred [definition, in veric.initialize]
blockslice_rmap [definition, in veric.initialize]
blocks_match [definition, in veric.semax_straight]
blocks_match [definition, in veric.SeparationLogic]
blockwise_valid [lemma, in veric.compcert_rmaps]
boolT [definition, in veric.res_predicates]
bool_val_Cnot [lemma, in veric.semax_lemmas]
bool_of_valf [definition, in veric.Clight_lemmas]
bool_type [definition, in veric.expr]
bool_type [definition, in veric.SeparationLogic]
boxy_jam [lemma, in veric.res_predicates]
break_cont [definition, in veric.Clight_new]
break_strip_CC [lemma, in veric.Clight_sim]
break_strip [lemma, in veric.Clight_sim]
break_cont_skip [lemma, in veric.Clight_sim]
build_call_temp_env [lemma, in veric.semax_call]
bytes_writable_readable [lemma, in veric.compcert_rmaps]
bytes_readable_dec [lemma, in veric.compcert_rmaps]
bytes_writable_dec [lemma, in veric.compcert_rmaps]
bytes_readable [definition, in veric.compcert_rmaps]
bytes_writable [definition, in veric.compcert_rmaps]
C
call_cont_app_cons [lemma, in veric.semax_lemmas]call_cont_app_nil [lemma, in veric.semax_lemmas]
call_cont_current_function [lemma, in veric.semax_call]
call_cont_idem [lemma, in veric.semax_call]
call_cont_nonnil [lemma, in veric.Clight_new]
call_cont [definition, in veric.Clight_new]
call_strip' [lemma, in veric.Clight_sim]
call_strip [lemma, in veric.Clight_sim]
can_alloc_variables' [lemma, in veric.semax_call]
can_alloc_variables [lemma, in veric.semax_call]
can_age_jm [lemma, in veric.juicy_mem]
can_age1_juicy_mem [lemma, in veric.juicy_mem]
cast_expropt [definition, in veric.semax_call]
cast_no_change [lemma, in veric.expr_lemmas]
cast_no_val_change [definition, in veric.expr_lemmas]
cast_exists [lemma, in veric.expr_lemmas]
cast_int_long_nonzero [lemma, in veric.binop_lemmas]
cast_expropt [definition, in veric.SeparationLogic]
cat_prefix_empty [lemma, in veric.semax_lemmas]
CC [module, in veric.Clight_sim]
CCstep [definition, in veric.Clight_sim]
CCstep_to_CC_step_1 [lemma, in veric.Clight_sim]
CC_step_fun [lemma, in veric.Clight_sim]
CC_step_to_step [lemma, in veric.Clight_sim]
CC_atExternal_isExternal [lemma, in veric.Clight_sim]
CC_step_to_CCstep [lemma, in veric.Clight_sim]
CC_core_sem [definition, in veric.Clight_sim]
CC_at_external_halted_excl [lemma, in veric.Clight_sim]
CC_corestep_not_halted [lemma, in veric.Clight_sim]
CC_safely_halted [definition, in veric.Clight_sim]
CC_corestep_not_at_external [lemma, in veric.Clight_sim]
CC_step [definition, in veric.Clight_sim]
CC_initial_core [definition, in veric.Clight_sim]
CC_after_external [definition, in veric.Clight_sim]
CC_at_external [definition, in veric.Clight_sim]
CC_core_to_CC_state_inj [lemma, in veric.Clight_sim]
CC_core_CC_state_4 [lemma, in veric.Clight_sim]
CC_core_CC_state_3 [lemma, in veric.Clight_sim]
CC_core_CC_state_2 [lemma, in veric.Clight_sim]
CC_core_CC_state_1 [lemma, in veric.Clight_sim]
CC_state_to_CC_core [definition, in veric.Clight_sim]
CC_core_to_CC_state [definition, in veric.Clight_sim]
CC_core_Returnstate [constructor, in veric.Clight_sim]
CC_core_Callstate [constructor, in veric.Clight_sim]
CC_core_State [constructor, in veric.Clight_sim]
CC_core [inductive, in veric.Clight_sim]
cc_step_fun [lemma, in veric.Clight_sim]
CC_trans [library]
CC_implies_FW [library]
check_pl_long [definition, in veric.expr]
check_pp_int [definition, in veric.expr]
check_pl_long' [definition, in veric.binop_lemmas]
check_pp_int' [definition, in veric.binop_lemmas]
claims [definition, in veric.semax]
classify_shift_eq [lemma, in veric.binop_lemmas]
classify_shift' [definition, in veric.binop_lemmas]
classify_add_eq [lemma, in veric.binop_lemmas]
classify_add' [definition, in veric.binop_lemmas]
classify_cmp_eq [lemma, in veric.binop_lemmas]
classify_cmp' [definition, in veric.binop_lemmas]
classify_sub_eq [lemma, in veric.binop_lemmas]
classify_sub' [definition, in veric.binop_lemmas]
Clightnew_Clight_sim [lemma, in veric.Clight_sim]
Clightnew_Clight_sim_eq [lemma, in veric.Clight_sim]
Clightnew_Clight_sim_eq_noOrder [lemma, in veric.Clight_sim]
Clightnew_Clight_sim_eq_noOrder_SSplusConclusion [lemma, in veric.Clight_sim]
CLIGHT_SEPARATION_LOGIC.semax_extract_prop [axiom, in veric.SeparationLogic]
CLIGHT_SEPARATION_LOGIC.semax_frame [axiom, in veric.SeparationLogic]
CLIGHT_SEPARATION_LOGIC.semax_pre_post [axiom, in veric.SeparationLogic]
CLIGHT_SEPARATION_LOGIC.semax_skip [axiom, in veric.SeparationLogic]
CLIGHT_SEPARATION_LOGIC.semax_store [axiom, in veric.SeparationLogic]
CLIGHT_SEPARATION_LOGIC.semax_load [axiom, in veric.SeparationLogic]
CLIGHT_SEPARATION_LOGIC.semax_ptr_compare [axiom, in veric.SeparationLogic]
CLIGHT_SEPARATION_LOGIC.semax_set_forward [axiom, in veric.SeparationLogic]
CLIGHT_SEPARATION_LOGIC.semax_set [axiom, in veric.SeparationLogic]
CLIGHT_SEPARATION_LOGIC.semax_call_ext [axiom, in veric.SeparationLogic]
CLIGHT_SEPARATION_LOGIC.semax_fun_id [axiom, in veric.SeparationLogic]
CLIGHT_SEPARATION_LOGIC.semax_return [axiom, in veric.SeparationLogic]
CLIGHT_SEPARATION_LOGIC.semax_call [axiom, in veric.SeparationLogic]
CLIGHT_SEPARATION_LOGIC.corable_func_ptr [axiom, in veric.SeparationLogic]
CLIGHT_SEPARATION_LOGIC.func_ptr [axiom, in veric.SeparationLogic]
CLIGHT_SEPARATION_LOGIC.semax_loop [axiom, in veric.SeparationLogic]
CLIGHT_SEPARATION_LOGIC.semax_continue [axiom, in veric.SeparationLogic]
CLIGHT_SEPARATION_LOGIC.semax_break [axiom, in veric.SeparationLogic]
CLIGHT_SEPARATION_LOGIC.seq_assoc [axiom, in veric.SeparationLogic]
CLIGHT_SEPARATION_LOGIC.semax_seq [axiom, in veric.SeparationLogic]
CLIGHT_SEPARATION_LOGIC.semax_ifthenelse [axiom, in veric.SeparationLogic]
CLIGHT_SEPARATION_LOGIC.semax_func_cons_ext [axiom, in veric.SeparationLogic]
CLIGHT_SEPARATION_LOGIC.semax_external_FF [axiom, in veric.SeparationLogic]
CLIGHT_SEPARATION_LOGIC.semax_external [axiom, in veric.SeparationLogic]
CLIGHT_SEPARATION_LOGIC.semax_func_cons [axiom, in veric.SeparationLogic]
CLIGHT_SEPARATION_LOGIC.semax_body_params_ok [definition, in veric.SeparationLogic]
CLIGHT_SEPARATION_LOGIC.semax_func_nil [axiom, in veric.SeparationLogic]
CLIGHT_SEPARATION_LOGIC.semax_prog [definition, in veric.SeparationLogic]
CLIGHT_SEPARATION_LOGIC.semax_func [axiom, in veric.SeparationLogic]
CLIGHT_SEPARATION_LOGIC.semax_body [definition, in veric.SeparationLogic]
CLIGHT_SEPARATION_LOGIC.semax_extensionality_Delta [axiom, in veric.SeparationLogic]
CLIGHT_SEPARATION_LOGIC.extract_exists [axiom, in veric.SeparationLogic]
CLIGHT_SEPARATION_LOGIC.semax [axiom, in veric.SeparationLogic]
CLIGHT_SEPARATION_LOGIC [module, in veric.SeparationLogic]
Clight_sim [library]
Clight_lemmas [library]
Clight_coop [library]
Clight_new [library]
closed_wrt_vars [definition, in veric.seplog]
closed_wrt_modvars [definition, in veric.semax]
closed_wrt_modvars [definition, in veric.SeparationLogic]
closed_wrt_vars [definition, in veric.SeparationLogic]
cl_corestep_fun' [lemma, in veric.semax_lemmas]
cl_corestep_fun [lemma, in veric.Clight_new]
cl_core_sem [definition, in veric.Clight_new]
cl_after_at_external_excl [lemma, in veric.Clight_new]
cl_corestep_not_halted [lemma, in veric.Clight_new]
cl_corestep_not_at_external [lemma, in veric.Clight_new]
cl_initial_core [definition, in veric.Clight_new]
cl_init_mem [definition, in veric.Clight_new]
cl_safely_halted [definition, in veric.Clight_new]
cl_step [inductive, in veric.Clight_new]
cl_after_external [definition, in veric.Clight_new]
cl_at_external [definition, in veric.Clight_new]
cl_coop_sem [definition, in veric.Clight_coop]
cl_coop_core_sem [definition, in veric.Clight_coop]
cl_coopstep_not_halted [lemma, in veric.Clight_coop]
cl_coopstep_not_at_external [lemma, in veric.Clight_coop]
cl_forward [lemma, in veric.Clight_coop]
CminorgenproofSIM [library]
Cminor_CompcertSemantics [library]
cmp_ptr_no_mem [definition, in veric.expr]
cmp_ptr_no_mem [definition, in veric.SeparationLogic]
Cnot [definition, in veric.semax_lemmas]
CompCert_AV.valid_join [lemma, in veric.compcert_rmaps]
CompCert_AV.valid_empty [lemma, in veric.compcert_rmaps]
CompCert_AV.valid [definition, in veric.compcert_rmaps]
CompCert_AV.kind [definition, in veric.compcert_rmaps]
CompCert_AV.some_address [definition, in veric.compcert_rmaps]
CompCert_AV.address [definition, in veric.compcert_rmaps]
CompCert_AV [module, in veric.compcert_rmaps]
compcert_rmaps [library]
components_join_joins [lemma, in veric.juicy_mem_lemmas]
compute_list_norepet_e [lemma, in veric.expr]
compute_list_norepet [definition, in veric.expr]
ConcPrimcom [inductive, in veric.juicy_mem_ops]
ConcPrimcom_free [constructor, in veric.juicy_mem_ops]
ConcPrimcom_alloc [constructor, in veric.juicy_mem_ops]
ConcPrimcom_store [constructor, in veric.juicy_mem_ops]
ConcPrimexpr [inductive, in veric.juicy_mem_ops]
concrete [instance, in veric.juicy_mem_ops]
concurrency_extension [library]
config_det [definition, in veric.local]
constructive_age1_join [lemma, in veric.juicy_mem]
construct_rho [definition, in veric.expr]
cons_app' [lemma, in veric.semax_lemmas]
cons_app [lemma, in veric.semax_lemmas]
cont [definition, in veric.Clight_new]
contains_Lsh_e [lemma, in veric.semax_call]
contents_cohere [definition, in veric.juicy_mem]
contents_at [definition, in veric.juicy_mem]
contents_cohere_join_sub [lemma, in veric.juicy_mem_lemmas]
continue_cont [definition, in veric.Clight_new]
continue_cont_is [lemma, in veric.Clight_sim]
continue_cont_skip [lemma, in veric.Clight_sim]
control_suffix_safe [lemma, in veric.semax_lemmas]
control_as_safe_le [lemma, in veric.semax_lemmas]
control_as_safe [definition, in veric.semax_lemmas]
cont' [inductive, in veric.Clight_new]
coopstep [definition, in veric.Clight_coop]
coop_forward [lemma, in veric.Clight_coop]
coop_mem_wd [lemma, in veric.Clight_coop]
corable_fun_assert [lemma, in veric.assert_lemmas]
corable_jam [lemma, in veric.assert_lemmas]
corable_funassert [lemma, in veric.assert_lemmas]
corable_imp [lemma, in veric.assert_lemmas]
corable_prop [lemma, in veric.assert_lemmas]
corable_exp [lemma, in veric.assert_lemmas]
corable_allp [lemma, in veric.assert_lemmas]
corable_orp [lemma, in veric.assert_lemmas]
corable_andp [lemma, in veric.assert_lemmas]
corable_pureat [lemma, in veric.assert_lemmas]
corestate [inductive, in veric.Clight_new]
corestep_preservation_lemma [lemma, in veric.semax_lemmas]
core_load_fun [lemma, in veric.assert_lemmas]
core_load_load [lemma, in veric.juicy_mem_lemmas]
core_load_load' [lemma, in veric.juicy_mem_lemmas]
core_load_valid [lemma, in veric.juicy_mem_lemmas]
core_load_getN [lemma, in veric.juicy_mem_lemmas]
core_load' [definition, in veric.res_predicates]
core_load [definition, in veric.res_predicates]
core_inflate_initial_mem [lemma, in veric.semax_prog]
Cross_rmap_aux [instance, in veric.compcert_rmaps]
CSharpminor_CompcertSemantics [library]
CT [constructor, in veric.compcert_rmaps]
CTat [definition, in veric.res_predicates]
ctl [inductive, in veric.local]
ctl_erase [inductive, in veric.local]
ct_count [definition, in veric.res_predicates]
current_function [definition, in veric.Clight_new]
current_function_find_label_ls [lemma, in veric.Clight_sim]
current_function_find_label [lemma, in veric.Clight_sim]
current_function_call_cont [lemma, in veric.Clight_sim]
current_function_strip [lemma, in veric.Clight_sim]
Cveric [instance, in veric.SeparationLogic]
D
Dbool [definition, in veric.assert_lemmas]decode_byte_val [lemma, in veric.seplog]
decode_val_getN_lem1 [lemma, in veric.initialize]
dec_skip [lemma, in veric.semax_lemmas]
dec_continue [lemma, in veric.Clight_sim]
dec_skip [lemma, in veric.Clight_sim]
dec_pure [lemma, in veric.initial_world]
Delta1 [definition, in veric.expr_lemmas]
Delta1 [definition, in veric.semax_prog]
denote_tc_assert_andp [lemma, in veric.expr]
denote_tc_assert [definition, in veric.expr]
denote_tc_initialized [definition, in veric.expr]
denote_tc_nodivover [definition, in veric.expr]
denote_tc_samebase [definition, in veric.expr]
denote_tc_Zle [definition, in veric.expr]
denote_tc_Zge [definition, in veric.expr]
denote_tc_igt [definition, in veric.expr]
denote_tc_nonzero [definition, in veric.expr]
denote_tc_iszero [definition, in veric.expr]
denote_tc_assert'_andp'_e [lemma, in veric.binop_lemmas]
denote_tc_assert_orp' [lemma, in veric.binop_lemmas]
denote_tc_assert_andp' [lemma, in veric.binop_lemmas]
denote_tc_assert_andp [lemma, in veric.binop_lemmas]
denote_tc_assert_orp'' [lemma, in veric.binop_lemmas]
denote_tc_assert_andp'' [lemma, in veric.binop_lemmas]
denote_tc_assert_iszero' [lemma, in veric.binop_lemmas]
denote_tc_assert_iszero [lemma, in veric.binop_lemmas]
denote_tc_assert_orp [lemma, in veric.binop_lemmas]
denote_tc_assert'_eq [lemma, in veric.binop_lemmas]
denote_tc_assert' [definition, in veric.binop_lemmas]
den_isBinOpR [lemma, in veric.binop_lemmas]
deref_loc_fun [lemma, in veric.Clight_lemmas]
deref_byvalue [constructor, in veric.expr]
deref_noload [definition, in veric.expr]
deref_loc_val_valid [lemma, in veric.Clight_coop]
derives_skip [lemma, in veric.semax_lemmas]
deterministic_rel [definition, in veric.local]
dryspec [definition, in veric.NullExtension]
dryspec [definition, in veric.SequentialClight]
dry_noperm_juicy_nonreadable [lemma, in veric.juicy_mem]
E
EBinop [constructor, in veric.local]ef_exit [definition, in veric.Clight_sim]
EK_return [constructor, in veric.expr]
EK_continue [constructor, in veric.expr]
EK_break [constructor, in veric.expr]
EK_normal [constructor, in veric.expr]
elements_remove [lemma, in veric.semax_call]
empty_program_ok [lemma, in veric.semax_lemmas]
empty_genv [definition, in veric.semax_lemmas]
empty_function [definition, in veric.Clight_new]
empty_retainer [definition, in veric.juicy_mem]
empty_environ [definition, in veric.semax]
empty_tycontext [definition, in veric.expr]
empty_environ [definition, in veric.expr]
empty_rmap_valid [lemma, in veric.res_predicates]
empty_environ [definition, in veric.expr_lemmas]
empty_tenv [definition, in veric.expr_lemmas]
empty_genv [definition, in veric.expr_lemmas]
entry_tempenv [definition, in veric.semax_prog]
environ [inductive, in veric.expr]
environ_lemmas [library]
env_set [definition, in veric.expr]
EPrim [constructor, in veric.local]
eqb_type_refl [lemma, in veric.expr]
eqb_type_true [lemma, in veric.expr]
eqb_fieldlist [definition, in veric.expr]
eqb_typelist [definition, in veric.expr]
eqb_type [definition, in veric.expr]
eqb_signedness [definition, in veric.expr]
eqb_intsize [definition, in veric.expr]
eqb_ident [definition, in veric.expr]
eqb_floatsize [definition, in veric.expr]
eqb_attr [definition, in veric.expr]
eqb_type_false [lemma, in veric.environ_lemmas]
eqb_type_eq [lemma, in veric.environ_lemmas]
EqDec_kind [instance, in veric.compcert_rmaps]
EqDec_memval [instance, in veric.base]
EqDec_type [instance, in veric.base]
EqDec_byte [instance, in veric.base]
EqDec_ident [instance, in veric.base]
EqDec_exitkind [instance, in veric.expr]
equiv_e2 [lemma, in veric.Clight_lemmas]
equiv_e1 [lemma, in veric.Clight_lemmas]
eq_block_lem [lemma, in veric.Clight_lemmas]
eq_mod_blockslice [definition, in veric.initialize]
erase_KSeq [constructor, in veric.local]
erase_KStop [constructor, in veric.local]
erase_SWhile [constructor, in veric.local]
erase_SIfte [constructor, in veric.local]
erase_SSeq [constructor, in veric.local]
erase_SSkip [constructor, in veric.local]
erase_SPrimcom [constructor, in veric.local]
erase_EPrim [constructor, in veric.local]
erase_EBinop [constructor, in veric.local]
erase_EUnop [constructor, in veric.local]
erase_EVal [constructor, in veric.local]
ErasureCorollaries [section, in veric.local]
Espec [definition, in veric.NullExtension]
EUnop [constructor, in veric.local]
EVal [constructor, in veric.local]
eval_lvalue_fun [lemma, in veric.Clight_lemmas]
eval_exprlist_fun [lemma, in veric.Clight_lemmas]
eval_expr_fun [lemma, in veric.Clight_lemmas]
eval_expr_lvalue_fun [lemma, in veric.Clight_lemmas]
eval_id_other [lemma, in veric.expr]
eval_id_same [lemma, in veric.expr]
eval_expropt [definition, in veric.expr]
eval_exprlist [definition, in veric.expr]
eval_lvalue [definition, in veric.expr]
eval_expr [definition, in veric.expr]
eval_cast [definition, in veric.expr]
eval_cast_struct [definition, in veric.expr]
eval_cast_l2bool [definition, in veric.expr]
eval_cast_f2l [definition, in veric.expr]
eval_cast_l2f [definition, in veric.expr]
eval_cast_l2i [definition, in veric.expr]
eval_cast_i2l [definition, in veric.expr]
eval_cast_p2bool [definition, in veric.expr]
eval_cast_f2bool [definition, in veric.expr]
eval_cast_f2i [definition, in veric.expr]
eval_cast_i2f [definition, in veric.expr]
eval_cast_f2f [definition, in veric.expr]
eval_cast_l2l [definition, in veric.expr]
eval_cast_i2i [definition, in veric.expr]
eval_cast_neutral [definition, in veric.expr]
eval_var [definition, in veric.expr]
eval_field [definition, in veric.expr]
eval_binop [definition, in veric.expr]
eval_unop [definition, in veric.expr]
eval_id [definition, in veric.expr]
eval_cast_sem_cast [lemma, in veric.expr_lemmas]
eval_lvalue_relate [lemma, in veric.expr_lemmas]
eval_expr_relate [lemma, in veric.expr_lemmas]
eval_both_relate [lemma, in veric.expr_lemmas]
eval_binop_relate_fail [lemma, in veric.expr_lemmas]
eval_lvalue_ptr [lemma, in veric.expr_lemmas]
eval_deref_loc_val_valid [lemma, in veric.Clight_coop]
eval_lvalue_val_valid [lemma, in veric.Clight_coop]
eval_expr_val_valid [lemma, in veric.Clight_coop]
eval_expr_lvalue_valid_aux [lemma, in veric.Clight_coop]
Events2 [library]
eventval_list_match_fun [lemma, in veric.Clight_lemmas]
ewand_TT_emp [lemma, in veric.semax_lemmas]
exec_skips'_CC [lemma, in veric.Clight_sim]
exec_skips_CC [lemma, in veric.Clight_sim]
exec_skips' [lemma, in veric.Clight_sim]
exec_skips [lemma, in veric.Clight_sim]
existential_ret_assert [definition, in veric.seplog]
existential_ret_assert [definition, in veric.SeparationLogic]
Exists_dec [lemma, in veric.initialize]
exitkind [inductive, in veric.expr]
exit_tycontext_eqv [lemma, in veric.semax_lemmas]
exit_tycon_sub [lemma, in veric.semax_lemmas]
exit_syscall_number [definition, in veric.Clight_new]
exit_tycon [definition, in veric.semax]
exit_cont [definition, in veric.semax]
exit_tycon [definition, in veric.SeparationLogic]
expr [inductive, in veric.local]
expr [library]
ExpressionErasure [section, in veric.local]
ExpressionErasure.F [variable, in veric.local]
ExpressionErasure.G [variable, in veric.local]
ExpressionErasure.GF [variable, in veric.local]
ExpressionErasure.primexpr_safety [variable, in veric.local]
ExpressionErasure.primexpr_erasure [variable, in veric.local]
ExpressionErasure.S' [variable, in veric.local]
ExpressionErasure.W [variable, in veric.local]
ExpressionErasure.world_erase [variable, in veric.local]
Expressions [section, in veric.local]
Expressions.G [variable, in veric.local]
Expressions.W [variable, in veric.local]
exprEval [definition, in veric.local]
exprEval' [definition, in veric.local]
exprlist_eval [lemma, in veric.semax_call]
expr_false [definition, in veric.seplog]
expr_true [definition, in veric.seplog]
expr_closed_wrt_vars [definition, in veric.expr]
expr_safety [lemma, in veric.local]
expr_erasure [lemma, in veric.local]
expr_erase_pure_expr [lemma, in veric.local]
expr_erase [inductive, in veric.local]
expr_wellformed [definition, in veric.local]
expr_lemmas [library]
ExtCall [constructor, in veric.Clight_new]
extend_tc_value [lemma, in veric.seplog]
extend_tc_lvalue [lemma, in veric.seplog]
extend_tc_exprlist [lemma, in veric.seplog]
extend_tc_expr [lemma, in veric.seplog]
extend_tc_temp_id [lemma, in veric.seplog]
extend_tc_temp_id_load [lemma, in veric.seplog]
extend_prop [lemma, in veric.seplog]
extensible_core_load' [lemma, in veric.assert_lemmas]
extensible_jam [definition, in veric.res_predicates]
extensions [section, in veric.semax_lemmas]
extensions [section, in veric.semax_call]
extensions [section, in veric.semax_loop]
extensions [section, in veric.semax_straight]
extern_retainer_neq_top [lemma, in veric.juicy_mem]
extern_retainer_neq_bot [lemma, in veric.juicy_mem]
extern_retainer [definition, in veric.juicy_mem]
extern_retainer [definition, in veric.SeparationLogic]
extract_exists_pre [lemma, in veric.semax_lemmas]
extract_exists [lemma, in veric.semax_lemmas]
ext_spec_post' [definition, in veric.semax]
ext_spec_pre' [definition, in veric.semax]
F
False_and [lemma, in veric.expr]False_or [lemma, in veric.binop_lemmas]
filter_seq_call_cont [lemma, in veric.semax_lemmas]
filter_seq_current_function [lemma, in veric.semax_lemmas]
filter_seq [definition, in veric.semax_lemmas]
filter_genv [definition, in veric.expr]
filter_genv_zero_ofs [lemma, in veric.expr_lemmas]
final_state [inductive, in veric.Clight_sim]
find_label_prefix2 [lemma, in veric.semax_lemmas]
find_label_ls_prefix2' [lemma, in veric.semax_lemmas]
find_label_prefix2' [lemma, in veric.semax_lemmas]
find_label_ls_None [lemma, in veric.semax_lemmas]
find_label_None [lemma, in veric.semax_lemmas]
find_label_ls_prefix [lemma, in veric.semax_lemmas]
find_label_prefix [lemma, in veric.semax_lemmas]
find_label_ls [definition, in veric.Clight_new]
find_label [definition, in veric.Clight_new]
find_id_rev [lemma, in veric.initialize]
find_symbol_globalenv [lemma, in veric.initial_world]
find_symbol_add_globals [lemma, in veric.initial_world]
find_id_e [lemma, in veric.initial_world]
find_id_i [lemma, in veric.initial_world]
find_id [definition, in veric.initial_world]
fixup_join [lemma, in veric.compcert_rmaps]
fixup_splitting_valid [lemma, in veric.compcert_rmaps]
fixup_splitting [definition, in veric.compcert_rmaps]
fmap_option [definition, in veric.juicy_mem]
fn_funsig [definition, in veric.semax]
fn_funsig [definition, in veric.SeparationLogic]
fold_right_rev_left [lemma, in veric.initial_world]
forallb_rev [lemma, in veric.initialize]
force_ptr [definition, in veric.expr]
force_val [definition, in veric.expr]
force_valid_pointers [definition, in veric.semax_straight]
frame_loop1 [lemma, in veric.seplog]
frame_for1 [lemma, in veric.seplog]
frame_normal [lemma, in veric.seplog]
frame_ret_assert [definition, in veric.seplog]
frame_ret_assert [definition, in veric.SeparationLogic]
free [section, in veric.juicy_mem]
freeable_blocks [definition, in veric.semax_call]
free_list_juicy_mem_lem [lemma, in veric.semax_call]
free_list_juicy_mem_ext [lemma, in veric.semax_call]
free_juicy_mem_ext [lemma, in veric.semax_call]
free_list_juicy_mem [definition, in veric.semax_call]
free_list_free [lemma, in veric.semax_call]
free_not_freeable_eq [lemma, in veric.juicy_mem]
free_juicy_mem [definition, in veric.juicy_mem]
free_nadr_range_eq [lemma, in veric.juicy_mem]
free_smaller_None [lemma, in veric.juicy_mem]
free.b [variable, in veric.juicy_mem]
free.FREE [variable, in veric.juicy_mem]
free.hi [variable, in veric.juicy_mem]
free.jm [variable, in veric.juicy_mem]
free.lo [variable, in veric.juicy_mem]
free.m' [variable, in veric.juicy_mem]
fst_split [lemma, in veric.semax_call]
fst_split_fullshare_not_top [lemma, in veric.juicy_mem]
fst_split_fullshare_not_bot [lemma, in veric.juicy_mem]
fst_match_fdecs [lemma, in veric.semax_prog]
fullempty_after_alloc [lemma, in veric.juicy_mem]
FUN [constructor, in veric.compcert_rmaps]
funassert [definition, in veric.seplog]
funassert_update_tycon [lemma, in veric.semax_loop]
funassert_exit_tycon [lemma, in veric.semax_loop]
funassert_rho [lemma, in veric.semax_prog]
funassert_initial_core [lemma, in veric.semax_prog]
function_pointer_aux [lemma, in veric.semax_call]
function_body_ret_assert [definition, in veric.seplog]
function_body_ret_assert [definition, in veric.SeparationLogic]
func_tycontext'_eqv [lemma, in veric.semax_lemmas]
func_at_func_at' [lemma, in veric.semax_call]
func_ptr [definition, in veric.semax_call]
func_at' [definition, in veric.seplog]
func_at [definition, in veric.seplog]
func_tycontext' [definition, in veric.semax]
func_tycontext [definition, in veric.expr]
func_tycontext_t_sound [lemma, in veric.expr_lemmas]
func_tycontext_v_sound [lemma, in veric.expr_lemmas]
func_tycontext_v_denote [definition, in veric.expr_lemmas]
func_tycontext_t_denote [definition, in veric.expr_lemmas]
funsig [definition, in veric.base]
funsig [definition, in veric.SeparationLogic]
funspec [inductive, in veric.expr]
FUNspec [definition, in veric.res_predicates]
funspecs [definition, in veric.expr]
FUNspec_parametric [lemma, in veric.res_predicates]
fun_assert [definition, in veric.seplog]
fun_assert_contractive [lemma, in veric.res_predicates]
fun_assert [definition, in veric.res_predicates]
G
GenericSemantics [record, in veric.local]GenericSemanticsElaboration [section, in veric.local]
genviron [definition, in veric.expr]
getVAL [lemma, in veric.compcert_rmaps]
get_result [definition, in veric.seplog]
get_result1 [definition, in veric.seplog]
get_var_type [definition, in veric.expr]
get_typed_int [lemma, in veric.expr_lemmas]
get_result [definition, in veric.SeparationLogic]
get_result1 [definition, in veric.SeparationLogic]
ge_of [definition, in veric.expr]
GF [inductive, in veric.juicy_mem_ops]
GF_wellformed [lemma, in veric.local]
ghost [library]
ghostp [definition, in veric.ghost]
ghostp_unique_andp [lemma, in veric.ghost]
ghostp_unique_sepcon [lemma, in veric.ghost]
GHOSTspec [definition, in veric.ghost]
globals_only [definition, in veric.seplog]
globals_only [definition, in veric.SeparationLogic]
global_initializers [lemma, in veric.initialize]
Global_var [constructor, in veric.expr]
Global_func [constructor, in veric.expr]
global_spec [inductive, in veric.expr]
globtype [definition, in veric.expr]
globvars2pred [definition, in veric.initialize]
globvars2pred [definition, in veric.SeparationLogic]
globvars2pred_rev [lemma, in veric.initialize]
globvar2pred [definition, in veric.initialize]
globvar2pred [definition, in veric.SeparationLogic]
glob_types [definition, in veric.expr]
glob_types_join_labeled [lemma, in veric.expr_lemmas]
glob_types_update_tycon [lemma, in veric.expr_lemmas]
glob_types_update_dist [lemma, in veric.expr_lemmas]
guard [definition, in veric.semax]
guard_environ_sub [lemma, in veric.semax_lemmas]
guard_safe_adj [lemma, in veric.semax_lemmas]
guard_environ_eqv [lemma, in veric.semax_lemmas]
guard_environ_put_te' [lemma, in veric.semax_lemmas]
guard_environ_e1 [lemma, in veric.semax]
guard_environ [definition, in veric.semax]
G0 [definition, in veric.semax_lemmas]
H
hackfun [definition, in veric.initialize]hackfun_beyond_block [lemma, in veric.initialize]
hackfun_sep [lemma, in veric.initialize]
HG [inductive, in veric.juicy_mem_ops]
HG_wellformed [lemma, in veric.local]
HO_pred_eq_i1 [lemma, in veric.semax_prog]
HO_pred_eq [definition, in veric.semax_prog]
I
idset [definition, in veric.expr]idset0 [definition, in veric.expr]
idset1 [definition, in veric.expr]
id_in_list_false [lemma, in veric.expr]
id_in_list_true [lemma, in veric.expr]
id_in_list [definition, in veric.expr]
id_for_lift [definition, in veric.lift]
if_E_true [lemma, in veric.Clight_coop]
if_E_false [lemma, in veric.Clight_coop]
immed_safe1 [constructor, in veric.local]
immed_safe0 [constructor, in veric.local]
immed_safe [inductive, in veric.local]
inflate [section, in veric.juicy_mem]
inflate_free_resource_decay [lemma, in veric.juicy_mem]
inflate_store_resource_nodecay [lemma, in veric.juicy_mem]
inflate_free [definition, in veric.juicy_mem]
inflate_store [definition, in veric.juicy_mem]
inflate_alloc [definition, in veric.juicy_mem]
inflate_initial_mem_all_VALs [lemma, in veric.juicy_mem]
inflate_initial_mem_level [lemma, in veric.juicy_mem]
inflate_initial_mem [definition, in veric.juicy_mem]
inflate_initial_mem'_valid [lemma, in veric.juicy_mem]
inflate_initial_mem'_fmap [lemma, in veric.juicy_mem]
inflate_initial_mem' [definition, in veric.juicy_mem]
inflate_initial_mem_empty [lemma, in veric.juicy_mem_lemmas]
inflate.m [variable, in veric.juicy_mem]
inflate.phi [variable, in veric.juicy_mem]
initblocksize [definition, in veric.initial_world]
initblocksize [definition, in veric.SeparationLogic]
initblocksize_name [lemma, in veric.initial_world]
initialize [library]
initialized [definition, in veric.expr]
initialized_tycontext_eqv [lemma, in veric.semax_lemmas]
initialized_sub [lemma, in veric.expr_lemmas]
initialized_ne [lemma, in veric.expr_lemmas]
initialized_tycontext_evolve [lemma, in veric.environ_lemmas]
initializers_aligned [definition, in veric.initialize]
initializers_aligned [definition, in veric.SeparationLogic]
initializer_aligned [definition, in veric.initialize]
initializer_aligned [definition, in veric.SeparationLogic]
initial_state [inductive, in veric.Clight_sim]
initial_mem_all_VALs [lemma, in veric.juicy_mem]
initial_mem_level [lemma, in veric.juicy_mem]
initial_mem [definition, in veric.juicy_mem]
initial_mem.IOK [variable, in veric.juicy_mem]
initial_rmap_ok [definition, in veric.juicy_mem]
initial_mem.w [variable, in veric.juicy_mem]
initial_mem.m [variable, in veric.juicy_mem]
initial_mem [section, in veric.juicy_mem]
initial_mem_core [lemma, in veric.juicy_mem_lemmas]
initial_core_rev [lemma, in veric.initialize]
initial_jm [definition, in veric.initial_world]
initial_core_ok [lemma, in veric.initial_world]
initial_core [definition, in veric.initial_world]
initial_core' [definition, in veric.initial_world]
initial_world [library]
init_jmem [definition, in veric.juicy_extspec]
init_datalist_hack [lemma, in veric.initialize]
init_data_list_lem [lemma, in veric.initialize]
init_data_list_size_app [lemma, in veric.initialize]
init_data_lem [lemma, in veric.initialize]
init_data_list_size_pos [lemma, in veric.initialize]
init_data_list2pred [definition, in veric.initialize]
init_data2pred [definition, in veric.initialize]
init_data_list2pred [definition, in veric.SeparationLogic]
init_data_list_size [definition, in veric.SeparationLogic]
init_data_size [definition, in veric.SeparationLogic]
init_data2pred [definition, in veric.SeparationLogic]
insert_idset [definition, in veric.expr]
intersection_splittable [lemma, in veric.res_predicates]
int_eq_true [lemma, in veric.binop_lemmas]
invalid_lvalue [constructor, in veric.expr]
invalid_struct_field [constructor, in veric.expr]
invalid_field_access [constructor, in veric.expr]
invalid_expression [constructor, in veric.expr]
invalid_cast_result [constructor, in veric.expr]
invalid_cast [constructor, in veric.expr]
inv_find_symbol_fun [lemma, in veric.Clight_lemmas]
in_map_fst [lemma, in veric.initial_world]
In_fst_split [lemma, in veric.environ_lemmas]
in_prog_vars_in_prog_defs [lemma, in veric.semax_prog]
in_prog_funct_in_prog_defs [lemma, in veric.semax_prog]
in_prog_funct'_in [lemma, in veric.semax_prog]
isBinOpResultType [definition, in veric.expr]
isCastR [lemma, in veric.expr_lemmas]
isCastResultType [definition, in veric.expr]
isExternalCallState [definition, in veric.Clight_sim]
isptr [definition, in veric.expr]
isSome [definition, in veric.expr]
isUnOpResultType [definition, in veric.expr]
isVAL [definition, in veric.compcert_rmaps]
isVAL_dec [lemma, in veric.compcert_rmaps]
isVAL_i [lemma, in veric.compcert_rmaps]
is_neutral_cast [definition, in veric.expr]
is_numeric_type [definition, in veric.expr]
is_pointer_type [definition, in veric.expr]
is_float_type [definition, in veric.expr]
is_long_type [definition, in veric.expr]
is_int_type [definition, in veric.expr]
is_scalar_type [definition, in veric.expr]
is_comparison [definition, in veric.expr]
is_ptr_type [definition, in veric.expr_lemmas]
is_true_false [lemma, in veric.binop_lemmas]
is_true_true [lemma, in veric.binop_lemmas]
is_true_dec [lemma, in veric.local]
is_true [definition, in veric.local]
is_comparison [definition, in veric.SeparationLogic]
Iveric [instance, in veric.SeparationLogic]
J
jam [definition, in veric.res_predicates]jam_noat_splittable [lemma, in veric.res_predicates]
jam_noat_splittable_aux [lemma, in veric.res_predicates]
jam_vacuous [definition, in veric.res_predicates]
jam_false [lemma, in veric.res_predicates]
jam_true [lemma, in veric.res_predicates]
JE_exit_hered [projection, in veric.juicy_extspec]
JE_post_hered [projection, in veric.juicy_extspec]
JE_pre_hered [projection, in veric.juicy_extspec]
JE_spec [projection, in veric.juicy_extspec]
jminit_fdecs_match [projection, in veric.juicy_extspec]
jminit_defs_no_dups [projection, in veric.juicy_extspec]
jminit_init_mem [projection, in veric.juicy_extspec]
jminit_lev [projection, in veric.juicy_extspec]
jminit_G [projection, in veric.juicy_extspec]
jminit_prog [projection, in veric.juicy_extspec]
jminit_m [projection, in veric.juicy_extspec]
jm_init_package [record, in veric.juicy_extspec]
join_tycon_labeled_eqv [lemma, in veric.semax_lemmas]
join_tycontext_eqv [lemma, in veric.semax_lemmas]
join_sub_share_top [lemma, in veric.semax_lemmas]
join_share_of [lemma, in veric.compcert_rmaps]
Join_pk [definition, in veric.compcert_rmaps]
join_upto_beyond_block [lemma, in veric.initialize]
join_only_blocks [lemma, in veric.initialize]
join_tycon_same [lemma, in veric.expr]
join_tycon_labeled [definition, in veric.expr]
join_tycon [definition, in veric.expr]
join_te [definition, in veric.expr]
join_te' [definition, in veric.expr]
join_te_denote2 [lemma, in veric.expr_lemmas]
join_te_eqv [lemma, in veric.expr_lemmas]
join_te_denote [lemma, in veric.environ_lemmas]
jsafeN [definition, in veric.semax]
jstep [definition, in veric.juicy_extspec]
jstep_not_halted [lemma, in veric.juicy_extspec]
jstep_not_at_external [lemma, in veric.juicy_extspec]
JuicyMemOps [module, in veric.juicy_mem_ops]
JuicyMemOps.after_alloc_alloc_cohere [lemma, in veric.juicy_mem_ops]
JuicyMemOps.after_alloc_max_access_cohere [lemma, in veric.juicy_mem_ops]
JuicyMemOps.after_alloc_access_cohere [lemma, in veric.juicy_mem_ops]
JuicyMemOps.after_alloc_contents_cohere [lemma, in veric.juicy_mem_ops]
JuicyMemOps.juicy_mem_free_succeeds [lemma, in veric.juicy_mem_ops]
JuicyMemOps.juicy_mem_free [definition, in veric.juicy_mem_ops]
JuicyMemOps.juicy_mem_alloc_succeeds [lemma, in veric.juicy_mem_ops]
JuicyMemOps.juicy_mem_alloc_level [lemma, in veric.juicy_mem_ops]
JuicyMemOps.juicy_mem_alloc_at [lemma, in veric.juicy_mem_ops]
JuicyMemOps.juicy_mem_alloc [definition, in veric.juicy_mem_ops]
JuicyMemOps.juicy_mem_alloc_aux1 [lemma, in veric.juicy_mem_ops]
JuicyMemOps.juicy_mem_storebytes_succeeds [lemma, in veric.juicy_mem_ops]
JuicyMemOps.juicy_mem_storebytes [definition, in veric.juicy_mem_ops]
JuicyMemOps.juicy_mem_store_succeeds [lemma, in veric.juicy_mem_ops]
JuicyMemOps.juicy_mem_store [definition, in veric.juicy_mem_ops]
JuicyMemOps.pshare_sh_bot [lemma, in veric.juicy_mem_ops]
JUICY_MEM_OPS.juicy_mem_free_succeeds [axiom, in veric.juicy_mem_ops]
JUICY_MEM_OPS.juicy_mem_alloc_succeeds [axiom, in veric.juicy_mem_ops]
JUICY_MEM_OPS.juicy_mem_store_succeeds [axiom, in veric.juicy_mem_ops]
JUICY_MEM_OPS.juicy_mem_free [axiom, in veric.juicy_mem_ops]
JUICY_MEM_OPS.juicy_mem_alloc [axiom, in veric.juicy_mem_ops]
JUICY_MEM_OPS.juicy_mem_storebytes [axiom, in veric.juicy_mem_ops]
JUICY_MEM_OPS.juicy_mem_store [axiom, in veric.juicy_mem_ops]
JUICY_MEM_OPS [module, in veric.juicy_mem_ops]
juicy_mem_alloc_core [lemma, in veric.semax_call]
juicy_store_nodecay [lemma, in veric.juicy_mem]
juicy_mem_level [definition, in veric.juicy_mem]
juicy_mem_ext [lemma, in veric.juicy_mem]
juicy_mem_ageable [instance, in veric.juicy_mem]
juicy_mem_ageable_facts [lemma, in veric.juicy_mem]
juicy_mem_alloc_cohere [lemma, in veric.juicy_mem]
juicy_mem_max_access [lemma, in veric.juicy_mem]
juicy_mem_access [lemma, in veric.juicy_mem]
juicy_mem_contents [lemma, in veric.juicy_mem]
juicy_mem [inductive, in veric.juicy_mem]
juicy_mem_op [definition, in veric.juicy_extspec]
juicy_core_sem [definition, in veric.juicy_extspec]
juicy_ext_spec [record, in veric.juicy_extspec]
juicy_free_lemma [lemma, in veric.juicy_mem_lemmas]
juicy_mem_core [definition, in veric.juicy_mem_lemmas]
juicy_mem_pred [definition, in veric.semax]
juicy_fs_extension [library]
juicy_linking_extension [library]
juicy_mem [library]
juicy_mem_ops [library]
juicy_mem_lemmas [library]
juicy_extspec [library]
j_after_at_external_excl [lemma, in veric.juicy_extspec]
j_at_external_halted_excl [lemma, in veric.juicy_extspec]
j_safely_halted [definition, in veric.juicy_extspec]
K
Kcall [constructor, in veric.Clight_new]kind [inductive, in veric.compcert_rmaps]
kind_at [definition, in veric.res_predicates]
Kloop1 [constructor, in veric.Clight_new]
Kloop2 [constructor, in veric.Clight_new]
Kseq [constructor, in veric.Clight_new]
Kseq [constructor, in veric.local]
Kstop [constructor, in veric.local]
Kswitch [constructor, in veric.Clight_new]
L
laterR_level [lemma, in veric.semax_prog]later_strengthen_safe1 [lemma, in veric.semax_lemmas]
later_twin [lemma, in veric.semax_call]
later_twin' [lemma, in veric.semax_call]
later_sepcon2 [lemma, in veric.semax_straight]
level_storebytes_juicy_mem [lemma, in veric.juicy_mem]
level_store_juicy_mem [lemma, in veric.juicy_mem]
level_remake_rmap [lemma, in veric.juicy_mem]
level_make_rmap [lemma, in veric.juicy_mem]
level_juice_level_phi [lemma, in veric.juicy_mem]
level_only_blocks [lemma, in veric.initialize]
level_later [lemma, in veric.res_predicates]
level1_juicy_mem [lemma, in veric.juicy_mem]
level2_juicy_mem [lemma, in veric.juicy_mem]
lift [definition, in veric.lift]
Lift [record, in veric.lift]
lift [library]
LiftClassicalSep' [instance, in veric.SeparationLogic]
lifted [projection, in veric.lift]
LiftEnviron [definition, in veric.expr]
LiftIndir' [instance, in veric.SeparationLogic]
LiftNatDed' [instance, in veric.SeparationLogic]
LiftSepIndir' [instance, in veric.SeparationLogic]
LiftSepLog' [instance, in veric.SeparationLogic]
liftx [definition, in veric.lift]
liftx' [definition, in veric.lift]
lift_uncurry_open [projection, in veric.lift]
lift_curry [projection, in veric.lift]
lift_last [projection, in veric.lift]
lift_prod [projection, in veric.lift]
lift_T [projection, in veric.lift]
lift_S [projection, in veric.lift]
lift0 [definition, in veric.expr]
lift1 [definition, in veric.expr]
lift2 [definition, in veric.expr]
lift3 [definition, in veric.expr]
lift4 [definition, in veric.expr]
link_ext [library]
listprod [definition, in veric.rmaps]
list_drop [definition, in veric.semax_lemmas]
list_norepet_rev [lemma, in veric.expr]
list_disjoint_rev2 [lemma, in veric.initial_world]
list2opt [definition, in veric.semax]
LK [constructor, in veric.compcert_rmaps]
LKspec [definition, in veric.res_predicates]
LKspec_splittable [lemma, in veric.res_predicates]
LKspec_parametric [lemma, in veric.res_predicates]
LK_at [definition, in veric.res_predicates]
loadpath [library]
load_core_load [lemma, in veric.juicy_mem_lemmas]
load_store_init_data_lem1 [lemma, in veric.initialize]
load_store_zeros [lemma, in veric.initialize]
load_store_init_data1 [definition, in veric.initialize]
load_cast [lemma, in veric.semax_straight]
local [definition, in veric.SeparationLogic]
local [library]
lock_size [definition, in veric.res_predicates]
loeb [lemma, in veric.semax_lemmas]
loop1_ret_assert [definition, in veric.seplog]
loop1_ret_assert [definition, in veric.SeparationLogic]
loop2_ret_assert [definition, in veric.seplog]
loop2_ret_assert [definition, in veric.SeparationLogic]
lvalue_block [definition, in veric.seplog]
lvalue_closed_wrt_vars [definition, in veric.expr]
M
main_function [axiom, in veric.Clight_sim]main_params [definition, in veric.semax_prog]
main_post [definition, in veric.semax_prog]
main_pre [definition, in veric.semax_prog]
main_post [definition, in veric.SeparationLogic]
main_pre [definition, in veric.SeparationLogic]
make_args [definition, in veric.seplog]
make_ghostp [lemma, in veric.ghost]
make_GHOSTspec [definition, in veric.ghost]
make_ext_rval [definition, in veric.semax]
make_ext_args [definition, in veric.semax]
make_tycontext [definition, in veric.expr]
make_tycontext_g [definition, in veric.expr]
make_tycontext_v [definition, in veric.expr]
make_tycontext_t [definition, in veric.expr]
make_venv [definition, in veric.expr]
make_tenv [definition, in veric.expr]
make_tycontext_g_denote [lemma, in veric.semax_prog]
make_args' [definition, in veric.SeparationLogic]
make_args [definition, in veric.SeparationLogic]
Map [module, in veric.expr]
mapsto [definition, in veric.seplog]
mapsto [definition, in veric.SeparationLogic]
mapsto_core_load [lemma, in veric.assert_lemmas]
mapsto_zeros [definition, in veric.seplog]
mapsto_ [definition, in veric.seplog]
mapsto_can_store [lemma, in veric.juicy_mem_lemmas]
mapsto_valid_access_wr [lemma, in veric.juicy_mem_lemmas]
mapsto_valid_access [lemma, in veric.juicy_mem_lemmas]
mapsto_is_pointer [lemma, in veric.semax_straight]
mapsto_valid_pointer [lemma, in veric.semax_straight]
mapsto_zeros [definition, in veric.SeparationLogic]
mapsto_ [definition, in veric.SeparationLogic]
map_compose_approx_succ_e [lemma, in veric.res_predicates]
map_ptree_rel [lemma, in veric.expr_lemmas]
Map.empty [definition, in veric.expr]
Map.ext [lemma, in veric.expr]
Map.get [definition, in veric.expr]
Map.gro [lemma, in veric.expr]
Map.grs [lemma, in veric.expr]
Map.gso [lemma, in veric.expr]
Map.gss [lemma, in veric.expr]
Map.gsspec [lemma, in veric.expr]
Map.map [section, in veric.expr]
Map.map.B [variable, in veric.expr]
Map.override [lemma, in veric.expr]
Map.override_same [lemma, in veric.expr]
Map.remove [definition, in veric.expr]
Map.set [definition, in veric.expr]
Map.t [definition, in veric.expr]
match_states_ext [constructor, in veric.Clight_sim]
match_states_seq [constructor, in veric.Clight_sim]
match_states [inductive, in veric.Clight_sim]
match_find_label_ls [lemma, in veric.Clight_sim]
match_find_label [lemma, in veric.Clight_sim]
match_find_ls_None [lemma, in veric.Clight_sim]
match_find_label_None [lemma, in veric.Clight_sim]
match_cont_strip1 [lemma, in veric.Clight_sim]
match_cont_call_strip [lemma, in veric.Clight_sim]
match_cont_strip [lemma, in veric.Clight_sim]
match_cont_call [constructor, in veric.Clight_sim]
match_cont_switch [constructor, in veric.Clight_sim]
match_cont_loop2 [constructor, in veric.Clight_sim]
match_cont_loop1 [constructor, in veric.Clight_sim]
match_cont_seq [constructor, in veric.Clight_sim]
match_cont_nil [constructor, in veric.Clight_sim]
match_cont [inductive, in veric.Clight_sim]
match_fdecs_rev [lemma, in veric.initialize]
match_fsig_e [lemma, in veric.expr]
match_fsig [definition, in veric.expr]
match_fsig_aux [definition, in veric.expr]
match_fdecs_exists_Gfun [lemma, in veric.initial_world]
match_fdecs [definition, in veric.initial_world]
match_globvars [definition, in veric.semax_prog]
match_globvars [definition, in veric.SeparationLogic]
max_access_cohere [definition, in veric.juicy_mem]
max_access_at [definition, in veric.juicy_mem]
max_unsigned_modulus [lemma, in veric.initialize]
max_unsigned_eq [lemma, in veric.initialize]
MemoryPushouts [library]
memory_block [definition, in veric.seplog]
memory_block'_eq [lemma, in veric.seplog]
memory_block'_alt [definition, in veric.seplog]
memory_block' [definition, in veric.seplog]
memory_block'_split [lemma, in veric.SeparationLogic]
memory_block [definition, in veric.SeparationLogic]
memory_block' [definition, in veric.SeparationLogic]
mem_access_perm [lemma, in veric.juicy_mem]
mem_alloc_juicy [lemma, in veric.initial_world]
mismatch_context_type [constructor, in veric.expr]
mkAfterExtCore [axiom, in veric.Clight_sim]
mkEnviron [constructor, in veric.expr]
mkGenericSem [constructor, in veric.local]
mkJuicyMem [constructor, in veric.juicy_mem]
mkLift [constructor, in veric.lift]
mkStratifiedSemantics [constructor, in veric.local]
mk_pshare [definition, in veric.compcert_rmaps]
mk_step' [constructor, in veric.Clight_sim]
mk_funspec [constructor, in veric.expr]
modifiedvars [definition, in veric.expr]
modifiedvars_ls_union [lemma, in veric.expr]
modifiedvars_ls [definition, in veric.expr]
modifiedvars' [definition, in veric.expr]
modifiedvars'_union [lemma, in veric.expr]
mod_after_alloc [definition, in veric.juicy_mem]
mod_after_alloc'_ok [lemma, in veric.juicy_mem]
mod_after_alloc'_valid [lemma, in veric.juicy_mem]
mod_after_alloc' [definition, in veric.juicy_mem]
mpred [definition, in veric.expr]
MS [definition, in veric.Clight_sim]
myStatement [axiom, in veric.Clight_sim]
m_phi [definition, in veric.juicy_mem]
m_dry [definition, in veric.juicy_mem]
N
nat_of_Z_minus_le [lemma, in veric.semax_lemmas]nat_ind2 [lemma, in veric.Clight_lemmas]
nat_ind2_Type [lemma, in veric.Clight_lemmas]
nat_of_Z_lem2 [lemma, in veric.juicy_mem_lemmas]
nat_of_Z_lem1 [lemma, in veric.juicy_mem_lemmas]
nat_of_Z_eq [lemma, in veric.res_predicates]
necR_core [lemma, in veric.semax_call]
necR_m_dry [lemma, in veric.juicy_mem_lemmas]
necR_level [lemma, in veric.semax_prog]
neg_val_valid [lemma, in veric.Clight_coop]
neutral_cast_typecheck_val [lemma, in veric.expr_lemmas]
nextblock_access_empty [lemma, in veric.juicy_mem]
noat [definition, in veric.res_predicates]
nofunc_tycontext [definition, in veric.expr]
nonunit_join [lemma, in veric.res_predicates]
normal_ret_assert_FF [lemma, in veric.seplog]
normal_ret_assert_derives [lemma, in veric.seplog]
normal_ret_assert [definition, in veric.seplog]
normal_ret_assert [definition, in veric.SeparationLogic]
notbool_val_valid [lemma, in veric.Clight_coop]
notint_val_valid [lemma, in veric.Clight_coop]
not_dec [definition, in veric.initialize]
no_dups_swap [lemma, in veric.semax_lemmas]
no_dups_inv [lemma, in veric.Clight_lemmas]
no_dups [definition, in veric.Clight_lemmas]
no_VALs [definition, in veric.juicy_mem_lemmas]
nreadable_inv [lemma, in veric.juicy_mem]
nthbyte [definition, in veric.res_predicates]
nth_eq_nth_error_eq [lemma, in veric.assert_lemmas]
nth_error_in_bounds [lemma, in veric.assert_lemmas]
nth_getN [lemma, in veric.juicy_mem_lemmas]
nth_error_length [lemma, in veric.res_predicates]
nth_error_rev [lemma, in veric.initial_world]
nth_error_app1 [lemma, in veric.initial_world]
nth_error_app [lemma, in veric.initial_world]
NullExtension [library]
Nveric [instance, in veric.SeparationLogic]
O
offset_val [definition, in veric.expr]of_bool_Int_eq_e [lemma, in veric.Clight_lemmas]
OK_spec [projection, in veric.juicy_extspec]
OK_ty [projection, in veric.juicy_extspec]
only_blocks_at [lemma, in veric.initialize]
only_blocks [definition, in veric.initialize]
opt2list [definition, in veric.expr]
opt2list_inj [lemma, in veric.semax_call]
opt2list2opt [lemma, in veric.semax_lemmas]
op_result_type [constructor, in veric.expr]
op_to_cmp [definition, in veric.expr]
op_to_cmp [definition, in veric.SeparationLogic]
OracleKind [record, in veric.juicy_extspec]
oracle_unage [lemma, in veric.juicy_mem_lemmas]
orb_if [lemma, in veric.expr]
or_pred_ext [lemma, in veric.semax]
or_True [lemma, in veric.binop_lemmas]
or_False [lemma, in veric.binop_lemmas]
overridePost [definition, in veric.seplog]
overridePost [definition, in veric.SeparationLogic]
overridePost_normal [lemma, in veric.seplog]
P
packPQ [definition, in veric.res_predicates]pass_params_ni [lemma, in veric.semax_call]
perm_mem_access [lemma, in veric.juicy_mem]
perm_of_empty [lemma, in veric.juicy_mem]
perm_of_nonempty [lemma, in veric.juicy_mem]
perm_of_readable [lemma, in veric.juicy_mem]
perm_of_writable [lemma, in veric.juicy_mem]
perm_of_freeable [lemma, in veric.juicy_mem]
perm_of_sh_Freeable_top [lemma, in veric.juicy_mem]
perm_of_sh_fullshare [lemma, in veric.juicy_mem]
perm_of_sh_pshare [lemma, in veric.juicy_mem]
perm_of_res [definition, in veric.juicy_mem]
perm_of_sh [definition, in veric.juicy_mem]
perm_order'_trans [lemma, in veric.juicy_mem_lemmas]
perm_of_sh_join_sub [lemma, in veric.juicy_mem_lemmas]
pfunc [definition, in veric.local]
phi_valid [lemma, in veric.juicy_mem]
pjoinable_None_emp [lemma, in veric.semax_lemmas]
pjoinable_emp_None [lemma, in veric.semax_lemmas]
plus_star_trans [lemma, in veric.Clight_sim]
plus_trans [lemma, in veric.Clight_sim]
pointer_cmp_no_mem_bool_type [lemma, in veric.semax_straight]
pointer_cmp_eval [lemma, in veric.semax_straight]
pp_compare_size_0 [constructor, in veric.expr]
prebreak_cont_is [lemma, in veric.semax_lemmas]
prebreak_cont [definition, in veric.semax_lemmas]
precontinue_cont [definition, in veric.Clight_new]
preds_fmap_NoneP_approx [lemma, in veric.juicy_mem_lemmas]
pred_sub_later' [lemma, in veric.semax_lemmas]
PrimcomErasure [lemma, in veric.juicy_mem_ops]
PrimcomSafety [lemma, in veric.juicy_mem_ops]
primcom_safety [lemma, in veric.local]
primcom_erasure [lemma, in veric.local]
PrimexprErasure [lemma, in veric.juicy_mem_ops]
PrimexprSafety [lemma, in veric.juicy_mem_ops]
primexpr_safety [lemma, in veric.local]
primexpr_erasure [lemma, in veric.local]
prog_var_block [definition, in veric.initialize]
prog_vars [definition, in veric.initial_world]
prog_vars' [definition, in veric.initial_world]
prog_funct [definition, in veric.initial_world]
prog_funct' [definition, in veric.initial_world]
prog_contains_prog_funct [lemma, in veric.semax_prog]
prog_contains [definition, in veric.semax_prog]
prog_vars [definition, in veric.SeparationLogic]
prog_vars' [definition, in veric.SeparationLogic]
prog_funct [definition, in veric.SeparationLogic]
prog_funct' [definition, in veric.SeparationLogic]
prop_imp_derives [lemma, in veric.semax_lemmas]
prop_unext [lemma, in veric.semax_call]
prop_derives [lemma, in veric.assert_lemmas]
prop_imp_i [lemma, in veric.assert_lemmas]
ptr_compare_no_binop_tc [lemma, in veric.expr_lemmas]
pureat [definition, in veric.res_predicates]
pure_expr_dec [lemma, in veric.local]
pure_expr_safe [lemma, in veric.local]
pure_exprEval [lemma, in veric.local]
pure_expr [definition, in veric.local]
R
R [module, in veric.compcert_rmaps]range_inv [lemma, in veric.juicy_mem]
range_inv0 [lemma, in veric.juicy_mem]
range_dec [lemma, in veric.res_predicates]
readable [definition, in veric.compcert_rmaps]
readable_dec [lemma, in veric.compcert_rmaps]
readable_e [lemma, in veric.compcert_rmaps]
readable_writable_join [lemma, in veric.compcert_rmaps]
readable_join [lemma, in veric.compcert_rmaps]
readable_inv [lemma, in veric.juicy_mem]
readable_eq_after_alloc' [lemma, in veric.juicy_mem_lemmas]
readonly2share [definition, in veric.initialize]
readonly2share [definition, in veric.SeparationLogic]
read_sh [definition, in veric.juicy_mem]
read_sh_readonly [lemma, in veric.initialize]
resource_decay_funassert [lemma, in veric.semax_call]
resource_at_slice [lemma, in veric.slice]
resource_decay_trans [lemma, in veric.juicy_mem]
resource_decay_refl [lemma, in veric.juicy_mem]
resource_nodecay_decay [lemma, in veric.juicy_mem]
resource_nodecay [definition, in veric.juicy_mem]
resource_decay [definition, in veric.juicy_mem]
resource_at_remake_rmap [lemma, in veric.juicy_mem]
resource_at_make_rmap [lemma, in veric.juicy_mem]
resource_fmap_core [lemma, in veric.seplog]
resource_identity_dec [lemma, in veric.initialize]
res_retain' [definition, in veric.juicy_mem]
res_option_core [lemma, in veric.semax_straight]
res_predicates [library]
ret_assert [definition, in veric.seplog]
ret_temp [definition, in veric.seplog]
ret_type [definition, in veric.expr]
ret_type_update_dist [lemma, in veric.expr_lemmas]
ret_type_exit_tycon [lemma, in veric.semax_loop]
ret_type_join_tycon_labeled [lemma, in veric.semax_loop]
ret_type_update_tycon [lemma, in veric.semax_loop]
ret_type_join_tycon [lemma, in veric.semax_loop]
ret_temp [definition, in veric.SeparationLogic]
ret_assert [definition, in veric.SeparationLogic]
rev_if_be_singleton [lemma, in veric.seplog]
rev_prog_funct' [lemma, in veric.initialize]
rev_if_be_1 [lemma, in veric.initialize]
rev_prog_vars' [lemma, in veric.initialize]
rev_prog_vars' [lemma, in veric.semax_prog]
rguard [definition, in veric.semax]
rguard_adj [lemma, in veric.semax_lemmas]
RmapPrimexpr [inductive, in veric.juicy_mem_ops]
Rmaps [module, in veric.rmaps]
RMAPS [module, in veric.rmaps]
rmaps [library]
Rmaps_Lemmas.resource_at_empty2 [lemma, in veric.rmaps_lemmas]
Rmaps_Lemmas.core_not_YES [lemma, in veric.rmaps_lemmas]
Rmaps_Lemmas.core_PURE [lemma, in veric.rmaps_lemmas]
Rmaps_Lemmas.core_NO [lemma, in veric.rmaps_lemmas]
Rmaps_Lemmas.core_YES [lemma, in veric.rmaps_lemmas]
Rmaps_Lemmas.resource_at_identity [lemma, in veric.rmaps_lemmas]
Rmaps_Lemmas.core_resource_at [lemma, in veric.rmaps_lemmas]
Rmaps_Lemmas.PURE_inj [lemma, in veric.rmaps_lemmas]
Rmaps_Lemmas.SomeP_inj [lemma, in veric.rmaps_lemmas]
Rmaps_Lemmas.SomeP_inj2 [lemma, in veric.rmaps_lemmas]
Rmaps_Lemmas.SomeP_inj1 [lemma, in veric.rmaps_lemmas]
Rmaps_Lemmas.YES_inj [lemma, in veric.rmaps_lemmas]
Rmaps_Lemmas.resource_at_core_identity [lemma, in veric.rmaps_lemmas]
Rmaps_Lemmas.identity_resource [lemma, in veric.rmaps_lemmas]
Rmaps_Lemmas.Cross_rmap_simple [lemma, in veric.rmaps_lemmas]
Rmaps_Lemmas.Cross_rmap [instance, in veric.rmaps_lemmas]
Rmaps_Lemmas.join_res_retain [lemma, in veric.rmaps_lemmas]
Rmaps_Lemmas.fixup_trace_rmap [lemma, in veric.rmaps_lemmas]
Rmaps_Lemmas.fixup_trace_valid [lemma, in veric.rmaps_lemmas]
Rmaps_Lemmas.fixup_trace [definition, in veric.rmaps_lemmas]
Rmaps_Lemmas.res_retain [definition, in veric.rmaps_lemmas]
Rmaps_Lemmas.Cross_resource [lemma, in veric.rmaps_lemmas]
Rmaps_Lemmas.res_option_join [lemma, in veric.rmaps_lemmas]
Rmaps_Lemmas.Join_trace [instance, in veric.rmaps_lemmas]
Rmaps_Lemmas.level_make_rmap [lemma, in veric.rmaps_lemmas]
Rmaps_Lemmas.resource_at_make_rmap [lemma, in veric.rmaps_lemmas]
Rmaps_Lemmas.approx_FF [lemma, in veric.rmaps_lemmas]
Rmaps_Lemmas.empty_rmap_level [lemma, in veric.rmaps_lemmas]
Rmaps_Lemmas.emp_empty_rmap [lemma, in veric.rmaps_lemmas]
Rmaps_Lemmas.empty_rmap [definition, in veric.rmaps_lemmas]
Rmaps_Lemmas.empty_rmap' [definition, in veric.rmaps_lemmas]
Rmaps_Lemmas.join_YES_pfullshare2 [lemma, in veric.rmaps_lemmas]
Rmaps_Lemmas.join_YES_pfullshare1 [lemma, in veric.rmaps_lemmas]
Rmaps_Lemmas.ageN_resource_at_eq [lemma, in veric.rmaps_lemmas]
Rmaps_Lemmas.rmap_unage_age [lemma, in veric.rmaps_lemmas]
Rmaps_Lemmas.remake_rmap [lemma, in veric.rmaps_lemmas]
Rmaps_Lemmas.no_preds [definition, in veric.rmaps_lemmas]
Rmaps_Lemmas.resource_at_joins2 [lemma, in veric.rmaps_lemmas]
Rmaps_Lemmas.resource_at_constructive_joins2 [lemma, in veric.rmaps_lemmas]
Rmaps_Lemmas.level_later_fash [lemma, in veric.rmaps_lemmas]
Rmaps_Lemmas.level_age_fash [lemma, in veric.rmaps_lemmas]
Rmaps_Lemmas.empty_NO [lemma, in veric.rmaps_lemmas]
Rmaps_Lemmas.age1_YES [lemma, in veric.rmaps_lemmas]
Rmaps_Lemmas.age1_resource_at [lemma, in veric.rmaps_lemmas]
Rmaps_Lemmas.necR_res_option [lemma, in veric.rmaps_lemmas]
Rmaps_Lemmas.age1_res_option [lemma, in veric.rmaps_lemmas]
Rmaps_Lemmas.resource_at_join_sub [lemma, in veric.rmaps_lemmas]
Rmaps_Lemmas.necR_YES'' [lemma, in veric.rmaps_lemmas]
Rmaps_Lemmas.necR_YES' [lemma, in veric.rmaps_lemmas]
Rmaps_Lemmas.preds_fmap_NoneP [lemma, in veric.rmaps_lemmas]
Rmaps_Lemmas.rmap_valid [lemma, in veric.rmaps_lemmas]
Rmaps_Lemmas.resource_at_empty [lemma, in veric.rmaps_lemmas]
Rmaps_Lemmas.necR_NO [lemma, in veric.rmaps_lemmas]
Rmaps_Lemmas.necR_PURE [lemma, in veric.rmaps_lemmas]
Rmaps_Lemmas.necR_YES [lemma, in veric.rmaps_lemmas]
Rmaps_Lemmas.necR_resource_at [lemma, in veric.rmaps_lemmas]
Rmaps_Lemmas.resource_at_approx [lemma, in veric.rmaps_lemmas]
Rmaps_Lemmas.resource_fmap_fmap [lemma, in veric.rmaps_lemmas]
Rmaps_Lemmas.preds_fmap_fmap [lemma, in veric.rmaps_lemmas]
Rmaps_Lemmas.necR_NOx [lemma, in veric.rmaps_lemmas]
Rmaps_Lemmas.YES_overlap [lemma, in veric.rmaps_lemmas]
Rmaps_Lemmas.YES_not_identity [lemma, in veric.rmaps_lemmas]
Rmaps_Lemmas.YES_join_full [lemma, in veric.rmaps_lemmas]
Rmaps_Lemmas.unageN [lemma, in veric.rmaps_lemmas]
Rmaps_Lemmas.ageN_squash [lemma, in veric.rmaps_lemmas]
Rmaps_Lemmas.all_resource_at_identity [lemma, in veric.rmaps_lemmas]
Rmaps_Lemmas.resource_at_join2 [lemma, in veric.rmaps_lemmas]
Rmaps_Lemmas.resource_at_join [lemma, in veric.rmaps_lemmas]
Rmaps_Lemmas.rmap_ext [lemma, in veric.rmaps_lemmas]
Rmaps_Lemmas.unsquash_inj [lemma, in veric.rmaps_lemmas]
Rmaps_Lemmas.allocate [lemma, in veric.rmaps_lemmas]
Rmaps_Lemmas.deallocate [lemma, in veric.rmaps_lemmas]
Rmaps_Lemmas.resources_same_level [lemma, in veric.rmaps_lemmas]
Rmaps_Lemmas.approx_oo_approx [lemma, in veric.rmaps_lemmas]
Rmaps_Lemmas.approx_oo_approx' [lemma, in veric.rmaps_lemmas]
Rmaps_Lemmas.make_rmap'' [lemma, in veric.rmaps_lemmas]
Rmaps_Lemmas.make_rmap [lemma, in veric.rmaps_lemmas]
Rmaps_Lemmas.make_rmap' [lemma, in veric.rmaps_lemmas]
Rmaps_Lemmas.necR_resource_at_identity [lemma, in veric.rmaps_lemmas]
Rmaps_Lemmas.age1_resource_at_identity [lemma, in veric.rmaps_lemmas]
Rmaps_Lemmas.identity_NO [lemma, in veric.rmaps_lemmas]
Rmaps_Lemmas.PURE_identity [lemma, in veric.rmaps_lemmas]
Rmaps_Lemmas.NO_identity [lemma, in veric.rmaps_lemmas]
Rmaps_Lemmas.ageN_level [lemma, in veric.rmaps_lemmas]
Rmaps_Lemmas.approx_ge [lemma, in veric.rmaps_lemmas]
Rmaps_Lemmas.approx_lt [lemma, in veric.rmaps_lemmas]
Rmaps_Lemmas.approx_p [lemma, in veric.rmaps_lemmas]
Rmaps_Lemmas.R [module, in veric.rmaps_lemmas]
Rmaps_Lemmas [module, in veric.rmaps_lemmas]
rmaps_lemmas [library]
Rmaps.Age_rmap [instance, in veric.rmaps]
RMAPS.Age_rmap [axiom, in veric.rmaps]
Rmaps.ag_rmap [instance, in veric.rmaps]
RMAPS.ag_rmap [axiom, in veric.rmaps]
Rmaps.approx [definition, in veric.rmaps]
RMAPS.approx [definition, in veric.rmaps]
Rmaps.AV [module, in veric.rmaps]
RMAPS.AV [module, in veric.rmaps]
Rmaps.Canc_resource [instance, in veric.rmaps]
Rmaps.Canc_rmap [instance, in veric.rmaps]
RMAPS.Canc_resource [axiom, in veric.rmaps]
RMAPS.Canc_rmap [axiom, in veric.rmaps]
Rmaps.Disj_resource [instance, in veric.rmaps]
Rmaps.Disj_rmap [instance, in veric.rmaps]
RMAPS.Disj_resource [axiom, in veric.rmaps]
RMAPS.Disj_rmap [axiom, in veric.rmaps]
Rmaps.fmap_p2p'_inj [lemma, in veric.rmaps]
Rmaps.join_unsquash [lemma, in veric.rmaps]
Rmaps.Join_nat_rmap' [instance, in veric.rmaps]
Rmaps.Join_resource [instance, in veric.rmaps]
Rmaps.Join_rmap [instance, in veric.rmaps]
RMAPS.join_unsquash [axiom, in veric.rmaps]
RMAPS.Join_nat_rmap' [instance, in veric.rmaps]
RMAPS.Join_resource [instance, in veric.rmaps]
RMAPS.Join_rmap [axiom, in veric.rmaps]
Rmaps.K [module, in veric.rmaps]
Rmaps.KL [module, in veric.rmaps]
Rmaps.KSa [module, in veric.rmaps]
Rmaps.NO [constructor, in veric.rmaps]
RMAPS.NO [constructor, in veric.rmaps]
Rmaps.NoneP [definition, in veric.rmaps]
RMAPS.NoneP [definition, in veric.rmaps]
Rmaps.Perm_resource [instance, in veric.rmaps]
Rmaps.Perm_rmap [instance, in veric.rmaps]
RMAPS.Perm_resource [axiom, in veric.rmaps]
RMAPS.Perm_rmap [axiom, in veric.rmaps]
Rmaps.preds [inductive, in veric.rmaps]
RMAPS.preds [inductive, in veric.rmaps]
Rmaps.preds_fmap_comp [lemma, in veric.rmaps]
Rmaps.preds_fmap_id [lemma, in veric.rmaps]
Rmaps.preds_fmap [definition, in veric.rmaps]
RMAPS.preds_fmap_comp [axiom, in veric.rmaps]
RMAPS.preds_fmap_id [axiom, in veric.rmaps]
RMAPS.preds_fmap [definition, in veric.rmaps]
Rmaps.pred_ext' [lemma, in veric.rmaps]
Rmaps.pre_rmap2rmap'2pre_rmap [lemma, in veric.rmaps]
Rmaps.pre_rmap2rmap' [definition, in veric.rmaps]
Rmaps.PURE [constructor, in veric.rmaps]
RMAPS.PURE [constructor, in veric.rmaps]
Rmaps.p2p [definition, in veric.rmaps]
Rmaps.p2p' [definition, in veric.rmaps]
Rmaps.resource [inductive, in veric.rmaps]
RMAPS.resource [inductive, in veric.rmaps]
Rmaps.resource_at [definition, in veric.rmaps]
Rmaps.resource_fmap_comp [lemma, in veric.rmaps]
Rmaps.resource_fmap_id [lemma, in veric.rmaps]
Rmaps.resource_fmap [definition, in veric.rmaps]
RMAPS.resource_at [definition, in veric.rmaps]
RMAPS.resource_fmap_comp [axiom, in veric.rmaps]
RMAPS.resource_fmap_id [axiom, in veric.rmaps]
RMAPS.resource_fmap [definition, in veric.rmaps]
Rmaps.resource2res [definition, in veric.rmaps]
Rmaps.resource2res2resource [lemma, in veric.rmaps]
Rmaps.res_join_PURE [constructor, in veric.rmaps]
Rmaps.res_join_YES [constructor, in veric.rmaps]
Rmaps.res_join_NO3 [constructor, in veric.rmaps]
Rmaps.res_join_NO2 [constructor, in veric.rmaps]
Rmaps.res_join_NO1 [constructor, in veric.rmaps]
Rmaps.res_join [inductive, in veric.rmaps]
Rmaps.res_option_rewrite [lemma, in veric.rmaps]
Rmaps.res_option [definition, in veric.rmaps]
RMAPS.res_join_PURE [constructor, in veric.rmaps]
RMAPS.res_join_YES [constructor, in veric.rmaps]
RMAPS.res_join_NO3 [constructor, in veric.rmaps]
RMAPS.res_join_NO2 [constructor, in veric.rmaps]
RMAPS.res_join_NO1 [constructor, in veric.rmaps]
RMAPS.res_join [inductive, in veric.rmaps]
RMAPS.res_option [definition, in veric.rmaps]
Rmaps.res2resource [definition, in veric.rmaps]
Rmaps.res2resource2res [lemma, in veric.rmaps]
Rmaps.rmap [definition, in veric.rmaps]
RMAPS.rmap [axiom, in veric.rmaps]
Rmaps.rmapj_valid_join [lemma, in veric.rmaps]
Rmaps.rmapj_valid_core [lemma, in veric.rmaps]
RMAPS.rmapj_valid_core [axiom, in veric.rmaps]
RMAPS.rmapj_valid_join [axiom, in veric.rmaps]
Rmaps.rmap_level_eq [lemma, in veric.rmaps]
Rmaps.rmap_age1_eq [lemma, in veric.rmaps]
Rmaps.rmap_age1_knot_age1 [lemma, in veric.rmaps]
Rmaps.rmap_unage [definition, in veric.rmaps]
Rmaps.rmap_age1 [definition, in veric.rmaps]
Rmaps.rmap_level [definition, in veric.rmaps]
Rmaps.rmap_fmap_comp [lemma, in veric.rmaps]
Rmaps.rmap_fmap_id [lemma, in veric.rmaps]
Rmaps.rmap_fmap [definition, in veric.rmaps]
RMAPS.rmap_unage [definition, in veric.rmaps]
RMAPS.rmap_age1_eq [axiom, in veric.rmaps]
RMAPS.rmap_level_eq [axiom, in veric.rmaps]
RMAPS.rmap_fmap_comp [axiom, in veric.rmaps]
RMAPS.rmap_fmap_id [axiom, in veric.rmaps]
RMAPS.rmap_fmap [definition, in veric.rmaps]
Rmaps.rmap' [definition, in veric.rmaps]
RMAPS.rmap' [definition, in veric.rmaps]
Rmaps.rmap'2pre_rmap2rmap' [lemma, in veric.rmaps]
Rmaps.rmap'2pre_rmap [definition, in veric.rmaps]
Rmaps.same_valid [lemma, in veric.rmaps]
Rmaps.Sep_resource [instance, in veric.rmaps]
Rmaps.Sep_rmap [instance, in veric.rmaps]
RMAPS.Sep_resource [axiom, in veric.rmaps]
RMAPS.Sep_rmap [axiom, in veric.rmaps]
Rmaps.SM [module, in veric.rmaps]
Rmaps.SomeP [constructor, in veric.rmaps]
RMAPS.SomeP [constructor, in veric.rmaps]
Rmaps.squash [definition, in veric.rmaps]
RMAPS.squash [axiom, in veric.rmaps]
Rmaps.squash_unsquash [lemma, in veric.rmaps]
RMAPS.squash_unsquash [axiom, in veric.rmaps]
Rmaps.TyF [module, in veric.rmaps]
Rmaps.TyFSA [module, in veric.rmaps]
Rmaps.TyFSA.Canc_F [definition, in veric.rmaps]
Rmaps.TyFSA.Disj_F [definition, in veric.rmaps]
Rmaps.TyFSA.Join_F [instance, in veric.rmaps]
Rmaps.TyFSA.paf_F [definition, in veric.rmaps]
Rmaps.TyFSA.Perm_F [definition, in veric.rmaps]
Rmaps.TyFSA.Sep_F [definition, in veric.rmaps]
Rmaps.TyFSA.TF [module, in veric.rmaps]
Rmaps.TyF.F [definition, in veric.rmaps]
Rmaps.TyF.f_F [definition, in veric.rmaps]
Rmaps.TyF.other [definition, in veric.rmaps]
Rmaps.unevolve_identity_rmap [lemma, in veric.rmaps]
Rmaps.unsquash [definition, in veric.rmaps]
RMAPS.unsquash [axiom, in veric.rmaps]
Rmaps.unsquash_squash [lemma, in veric.rmaps]
RMAPS.unsquash_squash [axiom, in veric.rmaps]
Rmaps.valid [definition, in veric.rmaps]
RMAPS.valid [definition, in veric.rmaps]
Rmaps.valid_res_map [lemma, in veric.rmaps]
RMAPS.valid_res_map [axiom, in veric.rmaps]
Rmaps.YES [constructor, in veric.rmaps]
RMAPS.YES [constructor, in veric.rmaps]
_ @ _ [notation, in veric.rmaps]
_ @ _ [notation, in veric.rmaps]
rmap_valid_e2 [lemma, in veric.compcert_rmaps]
rmap_valid_e1 [lemma, in veric.compcert_rmaps]
rmap_join_sub_eq_level [lemma, in veric.juicy_mem]
rmap_join_eq_level [lemma, in veric.juicy_mem]
rmap_unage_age [lemma, in veric.assert_lemmas]
rmap_unage_YES [lemma, in veric.juicy_mem_lemmas]
RML [module, in veric.compcert_rmaps]
Rveric [instance, in veric.SeparationLogic]
r_update_tenv [definition, in veric.semax]
S
safe [definition, in veric.local]safeN_strip [lemma, in veric.semax_lemmas]
safe_step_forward [lemma, in veric.semax_lemmas]
safe_loop_skip [lemma, in veric.semax_lemmas]
safe_seq_assoc [lemma, in veric.local]
same_glob_funassert [lemma, in veric.semax_lemmas]
same_env [definition, in veric.expr]
same_base_type [definition, in veric.expr]
same_base_tc_val [lemma, in veric.expr_lemmas]
sa_R [projection, in veric.semax]
sa_c [projection, in veric.semax]
sa_P [projection, in veric.semax]
sa_Delta [projection, in veric.semax]
selectors [section, in veric.juicy_mem]
selectors.j [variable, in veric.juicy_mem]
semax [definition, in veric.semax]
semax [library]
semaxArg [record, in veric.semax]
SemaxArg [constructor, in veric.semax]
SemaxContext [section, in veric.semax_lemmas]
semax_extensionality_Delta [lemma, in veric.semax_lemmas]
semax_frame [lemma, in veric.semax_lemmas]
semax_extensionality1 [lemma, in veric.semax_lemmas]
semax_extensionality0 [lemma, in veric.semax_lemmas]
semax_skip [lemma, in veric.semax_lemmas]
semax_pre_post [lemma, in veric.semax_lemmas]
semax_pre [lemma, in veric.semax_lemmas]
semax_post [lemma, in veric.semax_lemmas]
semax_unfold [lemma, in veric.semax_lemmas]
semax_extract_prop [lemma, in veric.semax_lemmas]
semax_return [lemma, in veric.semax_call]
semax_call_ext [lemma, in veric.semax_call]
semax_call_alt [lemma, in veric.semax_call]
semax_call [lemma, in veric.semax_call]
semax_call_aux [lemma, in veric.semax_call]
semax_call_typecheck_environ [lemma, in veric.semax_call]
semax_fun_id_alt [lemma, in veric.semax_call]
semax_fun_id [lemma, in veric.semax_call]
semax_fold_unfold [lemma, in veric.semax]
semax_ [definition, in veric.semax]
semax_external [definition, in veric.semax]
semax_continue [lemma, in veric.semax_loop]
semax_break [lemma, in veric.semax_loop]
semax_loop [lemma, in veric.semax_loop]
semax_seq [lemma, in veric.semax_loop]
semax_ifthenelse [lemma, in veric.semax_loop]
semax_store [lemma, in veric.semax_straight]
semax_load [lemma, in veric.semax_straight]
semax_set [lemma, in veric.semax_straight]
semax_set_forward [lemma, in veric.semax_straight]
semax_ptr_compare [lemma, in veric.semax_straight]
semax_straight_simple [lemma, in veric.semax_straight]
semax_prog_rule [lemma, in veric.semax_prog]
semax_prog_typecheck_aux [lemma, in veric.semax_prog]
semax_func_cons_ext [lemma, in veric.semax_prog]
semax_func_cons [lemma, in veric.semax_prog]
semax_func_cons_aux [lemma, in veric.semax_prog]
semax_func_nil [lemma, in veric.semax_prog]
semax_prog [definition, in veric.semax_prog]
semax_func [definition, in veric.semax_prog]
semax_body [definition, in veric.semax_prog]
semax_body_params_ok [definition, in veric.semax_prog]
semax_prog [section, in veric.semax_prog]
semax_lemmas [library]
semax_call [library]
semax_prog [library]
semax_straight [library]
semax_loop [library]
semax' [definition, in veric.semax]
semax'_pre_post [lemma, in veric.semax_lemmas]
semax'_pre [lemma, in veric.semax_lemmas]
semax'_post [lemma, in veric.semax_lemmas]
sem_cast_eval_cast [lemma, in veric.expr_lemmas]
sem_cmp_val_valid [lemma, in veric.Clight_coop]
sem_shift_val_valid [lemma, in veric.Clight_coop]
sem_mod_val_valid [lemma, in veric.Clight_coop]
sem_div_val_valid [lemma, in veric.Clight_coop]
sem_mul_val_valid [lemma, in veric.Clight_coop]
sem_sub_val_valid [lemma, in veric.Clight_coop]
sem_add_val_valid [lemma, in veric.Clight_coop]
sem_binarith_val_valid [lemma, in veric.Clight_coop]
sem_cast_val_valid [lemma, in veric.Clight_coop]
SeparationLogic [library]
SeparationLogicSoundness [library]
SEPARATION_LOGIC_SOUNDNESS.semax_prog_rule [axiom, in veric.SeparationLogicSoundness]
SEPARATION_LOGIC_SOUNDNESS.CSL [module, in veric.SeparationLogicSoundness]
SEPARATION_LOGIC_SOUNDNESS [module, in veric.SeparationLogicSoundness]
sepcon_FF [lemma, in veric.semax_lemmas]
sepcon_list [definition, in veric.seplog]
SepErasureCorollaries [section, in veric.local]
seplog [library]
seplog_extension [library]
sep_expr_safety [lemma, in veric.local]
sep_expr_erasure [lemma, in veric.local]
sep_primexpr_safety [lemma, in veric.local]
sep_primexpr_erasure [lemma, in veric.local]
SequentialClight [library]
seq_assoc [lemma, in veric.semax_loop]
seq_assoc2 [lemma, in veric.semax_loop]
seq_assoc1 [lemma, in veric.semax_loop]
set_inside [lemma, in veric.expr_lemmas]
set_temp_ret [lemma, in veric.expr_lemmas]
set_temp_ge [lemma, in veric.expr_lemmas]
set_temp_ve [lemma, in veric.expr_lemmas]
share_of_Some [lemma, in veric.compcert_rmaps]
share_of [definition, in veric.compcert_rmaps]
share_oblivious [definition, in veric.res_predicates]
Sifte [constructor, in veric.local]
signed_zero [lemma, in veric.Clight_lemmas]
SimpleAdrVal [module, in veric.rmaps]
SimpleAdrVal.address [definition, in veric.rmaps]
SimpleAdrVal.kind [definition, in veric.rmaps]
SimpleAdrVal.some_address [definition, in veric.rmaps]
SimpleAdrVal.valid [definition, in veric.rmaps]
SimpleAdrVal.valid_join [lemma, in veric.rmaps]
SimpleAdrVal.valid_empty [lemma, in veric.rmaps]
SIveric [instance, in veric.SeparationLogic]
slice [library]
slice_rmap_join [lemma, in veric.slice]
slice_rmap_level [lemma, in veric.slice]
slice_rmap [definition, in veric.slice]
slice_rmap_ok [lemma, in veric.slice]
slice_rmap_valid [lemma, in veric.slice]
slice_resource_valid [lemma, in veric.slice]
slice_resource [definition, in veric.slice]
smaller_temps_exists [lemma, in veric.semax_call]
snd_split [lemma, in veric.semax_call]
someP_inj [lemma, in veric.semax_call]
some_pt_type [definition, in veric.expr_lemmas]
SoundSeparationLogic [module, in veric.SeparationLogicSoundness]
SoundSeparationLogic.CSL [module, in veric.SeparationLogicSoundness]
SoundSeparationLogic.CSL.corable_func_ptr [lemma, in veric.SeparationLogicSoundness]
SoundSeparationLogic.CSL.extract_exists [definition, in veric.SeparationLogicSoundness]
SoundSeparationLogic.CSL.func_ptr [definition, in veric.SeparationLogicSoundness]
SoundSeparationLogic.CSL.juicy_ext_spec [definition, in veric.SeparationLogicSoundness]
SoundSeparationLogic.CSL.semax [definition, in veric.SeparationLogicSoundness]
SoundSeparationLogic.CSL.semax_external_FF [lemma, in veric.SeparationLogicSoundness]
SoundSeparationLogic.CSL.semax_external [definition, in veric.SeparationLogicSoundness]
SoundSeparationLogic.CSL.semax_ptr_compare [definition, in veric.SeparationLogicSoundness]
SoundSeparationLogic.CSL.semax_extract_prop [definition, in veric.SeparationLogicSoundness]
SoundSeparationLogic.CSL.semax_extensionality_Delta [definition, in veric.SeparationLogicSoundness]
SoundSeparationLogic.CSL.semax_pre_post [definition, in veric.SeparationLogicSoundness]
SoundSeparationLogic.CSL.semax_frame [definition, in veric.SeparationLogicSoundness]
SoundSeparationLogic.CSL.semax_skip [definition, in veric.SeparationLogicSoundness]
SoundSeparationLogic.CSL.semax_load [definition, in veric.SeparationLogicSoundness]
SoundSeparationLogic.CSL.semax_store [definition, in veric.SeparationLogicSoundness]
SoundSeparationLogic.CSL.semax_return [definition, in veric.SeparationLogicSoundness]
SoundSeparationLogic.CSL.semax_ifthenelse [definition, in veric.SeparationLogicSoundness]
SoundSeparationLogic.CSL.semax_set_forward [definition, in veric.SeparationLogicSoundness]
SoundSeparationLogic.CSL.semax_set [definition, in veric.SeparationLogicSoundness]
SoundSeparationLogic.CSL.semax_call_ext [definition, in veric.SeparationLogicSoundness]
SoundSeparationLogic.CSL.semax_fun_id [definition, in veric.SeparationLogicSoundness]
SoundSeparationLogic.CSL.semax_call [definition, in veric.SeparationLogicSoundness]
SoundSeparationLogic.CSL.semax_loop [definition, in veric.SeparationLogicSoundness]
SoundSeparationLogic.CSL.semax_continue [definition, in veric.SeparationLogicSoundness]
SoundSeparationLogic.CSL.semax_break [definition, in veric.SeparationLogicSoundness]
SoundSeparationLogic.CSL.semax_seq [definition, in veric.SeparationLogicSoundness]
SoundSeparationLogic.CSL.semax_func_cons_ext [definition, in veric.SeparationLogicSoundness]
SoundSeparationLogic.CSL.semax_func_cons [definition, in veric.SeparationLogicSoundness]
SoundSeparationLogic.CSL.semax_func_nil [definition, in veric.SeparationLogicSoundness]
SoundSeparationLogic.CSL.semax_prog [definition, in veric.SeparationLogicSoundness]
SoundSeparationLogic.CSL.semax_func [definition, in veric.SeparationLogicSoundness]
SoundSeparationLogic.CSL.semax_body [definition, in veric.SeparationLogicSoundness]
SoundSeparationLogic.CSL.semax_body_params_ok [definition, in veric.SeparationLogicSoundness]
SoundSeparationLogic.CSL.seq_assoc [definition, in veric.SeparationLogicSoundness]
SoundSeparationLogic.semax_prog_rule [definition, in veric.SeparationLogicSoundness]
spec [definition, in veric.res_predicates]
spec_parametric [definition, in veric.res_predicates]
splittable [definition, in veric.res_predicates]
split_shareval [definition, in veric.slice]
split_rmap_at2 [lemma, in veric.slice]
split_rmap_at1 [lemma, in veric.slice]
split_rmap_join [lemma, in veric.slice]
split_resource_join [lemma, in veric.slice]
split_rmap [definition, in veric.slice]
split_rmap_ok2 [lemma, in veric.slice]
split_rmap_ok1 [lemma, in veric.slice]
split_rmap_valid2 [lemma, in veric.slice]
split_rmap_valid1 [lemma, in veric.slice]
split_resource [definition, in veric.slice]
split_range [lemma, in veric.initialize]
split_top_neq [lemma, in veric.initial_world]
Sprimcom [constructor, in veric.local]
SRveric [instance, in veric.SeparationLogic]
Sseq [constructor, in veric.local]
Sskip [constructor, in veric.local]
sss_primexpr_safety [projection, in veric.local]
sss_primexpr_erasure [projection, in veric.local]
sss_HG_wellformed [projection, in veric.local]
ss_primexpr_saftey [projection, in veric.local]
ss_primexpr_erasure [projection, in veric.local]
ss_primcom_safety [projection, in veric.local]
ss_primcom_erasure [projection, in veric.local]
ss_GF_wellformed [projection, in veric.local]
ss_VU_wellformed [projection, in veric.local]
stackframe_of_freeable_blocks [lemma, in veric.semax_call]
stackframe_of_eq [lemma, in veric.seplog]
stackframe_of [definition, in veric.seplog]
stackframe_of [definition, in veric.SeparationLogic]
star_trans [lemma, in veric.Clight_sim]
star_plus_trans [lemma, in veric.Clight_sim]
State [constructor, in veric.Clight_new]
step [inductive, in veric.local]
stepN [inductive, in veric.local]
stepN_S [constructor, in veric.local]
stepN_0 [constructor, in veric.local]
step_goto [constructor, in veric.Clight_new]
step_label [constructor, in veric.Clight_new]
step_switch [constructor, in veric.Clight_new]
step_return [constructor, in veric.Clight_new]
step_loop2 [constructor, in veric.Clight_new]
step_for [constructor, in veric.Clight_new]
step_ifthenelse [constructor, in veric.Clight_new]
step_break [constructor, in veric.Clight_new]
step_continue [constructor, in veric.Clight_new]
step_skip [constructor, in veric.Clight_new]
step_seq [constructor, in veric.Clight_new]
step_call_external [constructor, in veric.Clight_new]
step_call_internal [constructor, in veric.Clight_new]
step_set [constructor, in veric.Clight_new]
step_assign [constructor, in veric.Clight_new]
step_continue_switch_CC [lemma, in veric.Clight_sim]
step_continue_seq_CC [lemma, in veric.Clight_sim]
step_continue_strip_CC [lemma, in veric.Clight_sim]
step_to_CC_step [lemma, in veric.Clight_sim]
step_continue_strip [lemma, in veric.Clight_sim]
step_star_erasure [lemma, in veric.local]
step_safety [lemma, in veric.local]
step_erasure [lemma, in veric.local]
step_compatible [lemma, in veric.local]
step_safe' [lemma, in veric.local]
step_safe [lemma, in veric.local]
step_nprimcom_det [lemma, in veric.local]
step_star_stepN [lemma, in veric.local]
step_star_trans [lemma, in veric.local]
step_step_star [lemma, in veric.local]
step_starN [constructor, in veric.local]
step_star0 [constructor, in veric.local]
step_star [inductive, in veric.local]
step_Swhile [constructor, in veric.local]
step_Sifte_false [constructor, in veric.local]
step_Sifte_true [constructor, in veric.local]
step_Sseq [constructor, in veric.local]
step_Sskip [constructor, in veric.local]
step_Sprimcom [constructor, in veric.local]
step' [inductive, in veric.Clight_sim]
stmt [inductive, in veric.local]
stmt_erase [inductive, in veric.local]
store [section, in veric.juicy_mem]
storebytes [section, in veric.juicy_mem]
storebytes_juicy_mem [definition, in veric.juicy_mem]
storebytes_phi_elsewhere_eq [lemma, in veric.juicy_mem]
storebytes.b [variable, in veric.juicy_mem]
storebytes.bytes [variable, in veric.juicy_mem]
storebytes.jm [variable, in veric.juicy_mem]
storebytes.m' [variable, in veric.juicy_mem]
storebytes.ofs [variable, in veric.juicy_mem]
storebytes.STOREBYTES [variable, in veric.juicy_mem]
store_valid [lemma, in veric.compcert_rmaps]
store_juicy_mem [definition, in veric.juicy_mem]
store_phi_elsewhere_eq [lemma, in veric.juicy_mem]
store_outside' [lemma, in veric.juicy_mem_lemmas]
store_init_data_list_access [lemma, in veric.initialize]
store_zeros_contents1 [lemma, in veric.initial_world]
store_zeros_access [lemma, in veric.initial_world]
store_zeros_max_access [lemma, in veric.initial_world]
store_init_data_list_lem [lemma, in veric.initial_world]
store_init_data_list_outside' [lemma, in veric.initial_world]
store_init_data_outside' [lemma, in veric.initial_world]
store.b [variable, in veric.juicy_mem]
store.ch [variable, in veric.juicy_mem]
store.jm [variable, in veric.juicy_mem]
store.m' [variable, in veric.juicy_mem]
store.ofs [variable, in veric.juicy_mem]
store.STORE [variable, in veric.juicy_mem]
store.v [variable, in veric.juicy_mem]
straightline [definition, in veric.semax_lemmas]
straightline_assign [lemma, in veric.semax_lemmas]
StratifiedSemantics [record, in veric.local]
StratifiedSemanticsWithSeparation [record, in veric.local]
stratified_expr_safety [lemma, in veric.local]
stratified_expr_erasure [lemma, in veric.local]
StratModel [module, in veric.rmaps]
StratModel.AV [module, in veric.rmaps]
StratModel.Canc_pre_rmap [definition, in veric.rmaps]
StratModel.ca_rj [instance, in veric.rmaps]
StratModel.da_rj [instance, in veric.rmaps]
StratModel.Disj_pre_rmap [definition, in veric.rmaps]
StratModel.ff_res [lemma, in veric.rmaps]
StratModel.f_pre_rmap [definition, in veric.rmaps]
StratModel.f_res [definition, in veric.rmaps]
StratModel.f_preds [definition, in veric.rmaps]
StratModel.Join_pre_rmap [instance, in veric.rmaps]
StratModel.Join_res [instance, in veric.rmaps]
StratModel.Join_preds [instance, in veric.rmaps]
StratModel.NO' [constructor, in veric.rmaps]
StratModel.paf_pre_rmap [instance, in veric.rmaps]
StratModel.paf_res [instance, in veric.rmaps]
StratModel.pa_rj [instance, in veric.rmaps]
StratModel.Perm_pre_rmap [definition, in veric.rmaps]
StratModel.preds [definition, in veric.rmaps]
StratModel.pre_rmap_sa_valid_join [lemma, in veric.rmaps]
StratModel.pre_rmap_sa_valid_core [lemma, in veric.rmaps]
StratModel.pre_rmap [definition, in veric.rmaps]
StratModel.PURE' [constructor, in veric.rmaps]
StratModel.res [inductive, in veric.rmaps]
StratModel.res_option [definition, in veric.rmaps]
StratModel.res_join_PURE [constructor, in veric.rmaps]
StratModel.res_join_YES [constructor, in veric.rmaps]
StratModel.res_join_NO3 [constructor, in veric.rmaps]
StratModel.res_join_NO2 [constructor, in veric.rmaps]
StratModel.res_join_NO1 [constructor, in veric.rmaps]
StratModel.res_join [inductive, in veric.rmaps]
StratModel.res_fmap [definition, in veric.rmaps]
StratModel.same_valid [lemma, in veric.rmaps]
StratModel.sa_rj [instance, in veric.rmaps]
StratModel.Sep_pre_rmap [definition, in veric.rmaps]
StratModel.valid' [definition, in veric.rmaps]
StratModel.valid'_res_map2 [lemma, in veric.rmaps]
StratModel.valid'_res_map [lemma, in veric.rmaps]
StratModel.YES' [constructor, in veric.rmaps]
stratsem [instance, in veric.juicy_mem_ops]
stratsemsep [instance, in veric.juicy_mem_ops]
STRAT_MODEL.paf_pre_rmap [instance, in veric.rmaps]
STRAT_MODEL.Disj_pre_rmap [axiom, in veric.rmaps]
STRAT_MODEL.Canc_pre_rmap [axiom, in veric.rmaps]
STRAT_MODEL.Sep_pre_rmap [axiom, in veric.rmaps]
STRAT_MODEL.Perm_pre_rmap [axiom, in veric.rmaps]
STRAT_MODEL.Join_pre_rmap [instance, in veric.rmaps]
STRAT_MODEL.valid'_res_map2 [axiom, in veric.rmaps]
STRAT_MODEL.f_pre_rmap [definition, in veric.rmaps]
STRAT_MODEL.pre_rmap [definition, in veric.rmaps]
STRAT_MODEL.valid'_res_map [axiom, in veric.rmaps]
STRAT_MODEL.valid' [definition, in veric.rmaps]
STRAT_MODEL.res_option [definition, in veric.rmaps]
STRAT_MODEL.paf_res [axiom, in veric.rmaps]
STRAT_MODEL.da_rj [axiom, in veric.rmaps]
STRAT_MODEL.ca_rj [axiom, in veric.rmaps]
STRAT_MODEL.sa_rj [axiom, in veric.rmaps]
STRAT_MODEL.pa_rj [axiom, in veric.rmaps]
STRAT_MODEL.res_join_PURE [constructor, in veric.rmaps]
STRAT_MODEL.res_join_YES [constructor, in veric.rmaps]
STRAT_MODEL.res_join_NO3 [constructor, in veric.rmaps]
STRAT_MODEL.res_join_NO2 [constructor, in veric.rmaps]
STRAT_MODEL.res_join_NO1 [constructor, in veric.rmaps]
STRAT_MODEL.res_join [inductive, in veric.rmaps]
STRAT_MODEL.f_res [definition, in veric.rmaps]
STRAT_MODEL.ff_res [axiom, in veric.rmaps]
STRAT_MODEL.res_fmap [definition, in veric.rmaps]
STRAT_MODEL.PURE' [constructor, in veric.rmaps]
STRAT_MODEL.YES' [constructor, in veric.rmaps]
STRAT_MODEL.NO' [constructor, in veric.rmaps]
STRAT_MODEL.res [inductive, in veric.rmaps]
STRAT_MODEL.f_preds [definition, in veric.rmaps]
STRAT_MODEL.preds [definition, in veric.rmaps]
STRAT_MODEL.AV [module, in veric.rmaps]
STRAT_MODEL [module, in veric.rmaps]
strict_bool_val [definition, in veric.expr]
strict_bool_val_sub [lemma, in veric.semax_loop]
strip_skip_app_cons [lemma, in veric.semax_lemmas]
strip_strip [lemma, in veric.semax_lemmas]
strip_skip_app [lemma, in veric.semax_lemmas]
strip_step [lemma, in veric.semax_lemmas]
strip_skip [definition, in veric.Clight_new]
strip_skip'_loop2_CC [lemma, in veric.Clight_sim]
strip_skip'_call_CC [lemma, in veric.Clight_sim]
strip_skip'_loop1_CC [lemma, in veric.Clight_sim]
strip_skip'_call [lemma, in veric.Clight_sim]
strip_skip'_loop1 [lemma, in veric.Clight_sim]
strip_call' [lemma, in veric.Clight_sim]
strip_call [lemma, in veric.Clight_sim]
strip_skip'_loop2 [lemma, in veric.Clight_sim]
strip_step [lemma, in veric.Clight_sim]
strip_skip'_not [lemma, in veric.Clight_sim]
strip_skip_not [lemma, in veric.Clight_sim]
strip_skip' [definition, in veric.Clight_sim]
stupid_typeconv [definition, in veric.binop_lemmas]
subp_derives' [lemma, in veric.semax_lemmas]
subst [definition, in veric.seplog]
subst [definition, in veric.SeparationLogic]
substopt [definition, in veric.semax_call]
substopt [definition, in veric.SeparationLogic]
subst_extens [lemma, in veric.seplog]
subst_extens [lemma, in veric.SeparationLogic]
sub_option [definition, in veric.expr]
Sveric [instance, in veric.SeparationLogic]
Swhile [constructor, in veric.local]
T
Tarrow [definition, in veric.lift]tc_expropt [definition, in veric.semax_call]
tc_exprlist_sub [lemma, in veric.assert_lemmas]
tc_temp_id_load_sub [lemma, in veric.assert_lemmas]
tc_temp_id_sub [lemma, in veric.assert_lemmas]
tc_lvalue_sub [lemma, in veric.assert_lemmas]
tc_expr_sub [lemma, in veric.assert_lemmas]
tc_expr_lvalue_sub [lemma, in veric.assert_lemmas]
tc_temp_id_load [definition, in veric.seplog]
tc_temp_id [definition, in veric.seplog]
tc_value [definition, in veric.seplog]
tc_lvalue [definition, in veric.seplog]
tc_exprlist [definition, in veric.seplog]
tc_expr [definition, in veric.seplog]
tc_formals [definition, in veric.seplog]
tc_andp_sound [lemma, in veric.expr]
tc_always_true [definition, in veric.expr]
tc_might_be_true [definition, in veric.expr]
tc_bool [definition, in veric.expr]
tc_orp [definition, in veric.expr]
tc_andp [definition, in veric.expr]
tc_iszero [definition, in veric.expr]
tc_initialized [constructor, in veric.expr]
tc_nodivover [constructor, in veric.expr]
tc_samebase [constructor, in veric.expr]
tc_Zge [constructor, in veric.expr]
tc_Zle [constructor, in veric.expr]
tc_ilt [constructor, in veric.expr]
tc_isptr [constructor, in veric.expr]
tc_iszero' [constructor, in veric.expr]
tc_nonzero [constructor, in veric.expr]
tc_orp' [constructor, in veric.expr]
tc_andp' [constructor, in veric.expr]
tc_TT [constructor, in veric.expr]
tc_noproof [constructor, in veric.expr]
tc_FF [constructor, in veric.expr]
tc_assert [inductive, in veric.expr]
tc_error [inductive, in veric.expr]
tc_exprlist_length [lemma, in veric.expr_lemmas]
tc_lvalue_nonvol [lemma, in veric.expr_lemmas]
tc_binaryop_nomem [lemma, in veric.expr_lemmas]
tc_andp_TT1 [lemma, in veric.binop_lemmas]
tc_andp_TT2 [lemma, in veric.binop_lemmas]
tc_ge_denote_initial [lemma, in veric.semax_prog]
tc_expropt [definition, in veric.SeparationLogic]
tc_value [definition, in veric.SeparationLogic]
tc_lvalue [definition, in veric.SeparationLogic]
tc_exprlist [definition, in veric.SeparationLogic]
tc_expr [definition, in veric.SeparationLogic]
tc_temp_id_load [definition, in veric.SeparationLogic]
tc_temp_id [definition, in veric.SeparationLogic]
tc_environ [definition, in veric.SeparationLogic]
tc_val [definition, in veric.SeparationLogic]
temp_bindings [definition, in veric.Clight_new]
temp_types [definition, in veric.expr]
temp_types_same_type' [lemma, in veric.expr_lemmas]
temp_types_update_dist [lemma, in veric.expr_lemmas]
temp_types_same_type [lemma, in veric.expr_lemmas]
Tend [definition, in veric.lift]
tenviron [definition, in veric.expr]
test [definition, in veric.expr]
te_of [definition, in veric.expr]
te_one_denote [definition, in veric.expr_lemmas]
Tint32s [definition, in veric.Clight_new]
Tint32s [definition, in veric.semax_prog]
top_pfullshare [lemma, in veric.juicy_mem]
Trip_rmap [instance, in veric.compcert_rmaps]
Trip_resource [instance, in veric.compcert_rmaps]
true_expr [definition, in veric.semax_lemmas]
true_expr [definition, in veric.Clight_new]
True_and [lemma, in veric.expr]
True_or [lemma, in veric.binop_lemmas]
Tsh [definition, in veric.SeparationLogic]
TTat [definition, in veric.res_predicates]
tycontext [definition, in veric.expr]
tycontext_sub_trans [lemma, in veric.semax_lemmas]
tycontext_sub_update_l [lemma, in veric.semax_lemmas]
tycontext_sub_update_c [lemma, in veric.semax_lemmas]
tycontext_eqv_symm [lemma, in veric.expr]
tycontext_eqv [definition, in veric.expr]
tycontext_sub [definition, in veric.expr]
tycontext_sub_join [lemma, in veric.expr_lemmas]
tycontext_sub_refl [lemma, in veric.expr_lemmas]
tycontext_evolve_join_labeled [lemma, in veric.semax_loop]
tycontext_evolve_update_tycon [lemma, in veric.semax_loop]
tycontext_evolve_join [lemma, in veric.semax_loop]
tycontext_evolve_refl [lemma, in veric.semax_loop]
tycontext_evolve_trans [lemma, in veric.environ_lemmas]
tycontext_evolve [definition, in veric.environ_lemmas]
typecheck_tid_ptr_compare_sub [lemma, in veric.semax_lemmas]
typecheck_tid_ptr_compare [definition, in veric.semax_lemmas]
typecheck_environ_sub [lemma, in veric.semax_lemmas]
typecheck_store [definition, in veric.expr]
typecheck_environ [definition, in veric.expr]
typecheck_glob_environ [definition, in veric.expr]
typecheck_var_environ [definition, in veric.expr]
typecheck_temp_environ [definition, in veric.expr]
typecheck_vals [definition, in veric.expr]
typecheck_val [definition, in veric.expr]
typecheck_exprlist [definition, in veric.expr]
typecheck_pure_b [definition, in veric.expr]
typecheck_b [definition, in veric.expr]
typecheck_temp_id [definition, in veric.expr]
typecheck_lvalue [definition, in veric.expr]
typecheck_expr [definition, in veric.expr]
typecheck_tid_ptr_compare_sub [lemma, in veric.expr_lemmas]
typecheck_tid_ptr_compare [definition, in veric.expr_lemmas]
typecheck_val_eval_cast [lemma, in veric.expr_lemmas]
typecheck_bool_val [lemma, in veric.expr_lemmas]
typecheck_environ_update [lemma, in veric.expr_lemmas]
typecheck_environ_update_ge [lemma, in veric.expr_lemmas]
typecheck_environ_update_ve [lemma, in veric.expr_lemmas]
typecheck_ls_update_te [lemma, in veric.expr_lemmas]
typecheck_environ_update_te [lemma, in veric.expr_lemmas]
typecheck_binop_sound2 [lemma, in veric.expr_lemmas]
typecheck_force_Some [lemma, in veric.expr_lemmas]
typecheck_lvalue_sound [lemma, in veric.expr_lemmas]
typecheck_expr_sound [lemma, in veric.expr_lemmas]
typecheck_both_sound [lemma, in veric.expr_lemmas]
typecheck_deref_sound [lemma, in veric.expr_lemmas]
typecheck_temp_sound [lemma, in veric.expr_lemmas]
typecheck_cast_sound [lemma, in veric.expr_lemmas]
typecheck_unop_sound [lemma, in veric.expr_lemmas]
typecheck_expr_sound_Evar [lemma, in veric.expr_lemmas]
typecheck_lvalue_sound_Efield [lemma, in veric.expr_lemmas]
typecheck_expr_sound_Efield [lemma, in veric.expr_lemmas]
typecheck_lvalue_Evar [lemma, in veric.expr_lemmas]
typecheck_binop_sound [lemma, in veric.binop_lemmas]
typecheck_sem_mod_sound [lemma, in veric.binop_lemmas]
typecheck_sem_div_sound [lemma, in veric.binop_lemmas]
typecheck_val_cmp_eqne_pi [lemma, in veric.binop_lemmas]
typecheck_val_cmp_eqne_ip [lemma, in veric.binop_lemmas]
typecheck_val_sem_cmp [lemma, in veric.binop_lemmas]
typecheck_numeric_val [definition, in veric.binop_lemmas]
typecheck_val_void [lemma, in veric.binop_lemmas]
typecheck_environ_put_te' [lemma, in veric.environ_lemmas]
typecheck_environ_put_te [lemma, in veric.environ_lemmas]
typecheck_val_ptr_lemma [lemma, in veric.environ_lemmas]
typecheck_environ_join2 [lemma, in veric.environ_lemmas]
typecheck_environ_join1 [lemma, in veric.environ_lemmas]
typecheck_tid_ptr_compare [definition, in veric.SeparationLogic]
typed_params [definition, in veric.Clight_new]
typed_false [definition, in veric.seplog]
typed_true [definition, in veric.seplog]
typed_false [definition, in veric.SeparationLogic]
typed_true [definition, in veric.SeparationLogic]
typelist2list [definition, in veric.expr]
type_of_funspec [definition, in veric.expr]
type_eq_true [lemma, in veric.expr_lemmas]
type_eq_true [lemma, in veric.environ_lemmas]
type_of_funsig [definition, in veric.SeparationLogic]
U
umapsto [definition, in veric.seplog]umapsto [definition, in veric.SeparationLogic]
unage_umapsto [lemma, in veric.semax_lemmas]
unage_readable [lemma, in veric.juicy_mem]
unage_writable [lemma, in veric.juicy_mem]
unage_juicy_mem [lemma, in veric.juicy_mem]
unary_operation_val_valid [lemma, in veric.Clight_coop]
UNeg [constructor, in veric.local]
unitT [definition, in veric.res_predicates]
universal_imp_unfold [lemma, in veric.semax_lemmas]
unlater_writable [lemma, in veric.semax_call]
unop [inductive, in veric.local]
unopDenote [definition, in veric.local]
unOp_result_type [definition, in veric.expr]
UnpackStratifiedSemantics [section, in veric.local]
UnpackStratifiedSemanticsWithSeparation [section, in veric.local]
update_tycontext_eqv [lemma, in veric.semax_lemmas]
update_tycon [definition, in veric.expr]
update_tycon_sub [lemma, in veric.expr_lemmas]
update_le_same_ge [lemma, in veric.expr_lemmas]
update_tycon_same_ge [lemma, in veric.expr_lemmas]
update_le_eqv_ge [lemma, in veric.expr_lemmas]
update_tycon_eqv_ge [lemma, in veric.expr_lemmas]
update_le_same_ve [lemma, in veric.expr_lemmas]
update_tycon_same_ve [lemma, in veric.expr_lemmas]
update_le_eqv_ret [lemma, in veric.expr_lemmas]
update_tycon_eqv_ret [lemma, in veric.expr_lemmas]
update_le_eqv_ve [lemma, in veric.expr_lemmas]
update_tycon_eqv_ve [lemma, in veric.expr_lemmas]
update_labeled_te_same [lemma, in veric.expr_lemmas]
update_tycon_te_same [lemma, in veric.expr_lemmas]
upto_block [definition, in veric.initialize]
V
VAL [constructor, in veric.compcert_rmaps]val [inductive, in veric.local]
valid_access_None [lemma, in veric.juicy_mem_lemmas]
valid_corestate [definition, in veric.Clight_coop]
valid_tempenv [definition, in veric.Clight_coop]
valid_env [definition, in veric.Clight_coop]
valshare [definition, in veric.juicy_mem]
VALspec [definition, in veric.res_predicates]
VALspec_range_VALspec [lemma, in veric.res_predicates]
VALspec_range_split2 [lemma, in veric.res_predicates]
VALspec_range_0 [lemma, in veric.res_predicates]
VALspec_range_precise [lemma, in veric.res_predicates]
VALspec_range_bytes_writable [lemma, in veric.res_predicates]
VALspec_range_bytes_readable [lemma, in veric.res_predicates]
VALspec_range_splittable [lemma, in veric.res_predicates]
VALspec_readable [lemma, in veric.res_predicates]
VALspec_splittable [lemma, in veric.res_predicates]
VALspec_parametric [lemma, in veric.res_predicates]
VALspec_range [definition, in veric.res_predicates]
VALspec_range_e [lemma, in veric.initial_world]
VALspec1 [lemma, in veric.res_predicates]
VAL_valid [lemma, in veric.compcert_rmaps]
VAL_inj [lemma, in veric.compcert_rmaps]
VAL_valid [lemma, in veric.juicy_mem]
val_to_bool [definition, in veric.Clight_lemmas]
val2address [definition, in veric.res_predicates]
varspecs [definition, in veric.expr]
var_block [definition, in veric.seplog]
var_name [definition, in veric.Clight_lemmas]
var_not_in_tycontext [constructor, in veric.expr]
var_types [definition, in veric.expr]
var_types_join_labeled [lemma, in veric.expr_lemmas]
var_types_update_tycon [lemma, in veric.expr_lemmas]
var_types_update_dist [lemma, in veric.expr_lemmas]
var_block [definition, in veric.SeparationLogic]
venviron [definition, in veric.expr]
ve_of [definition, in veric.expr]
Vint [constructor, in veric.local]
volatile_load [constructor, in veric.expr]
Vptr [constructor, in veric.local]
vret2v [definition, in veric.Clight_new]
VU [inductive, in veric.juicy_mem_ops]
Vundef [constructor, in veric.local]
VU_free [constructor, in veric.juicy_mem_ops]
VU_alloc [constructor, in veric.juicy_mem_ops]
VU_store [constructor, in veric.juicy_mem_ops]
VU_wellformed [lemma, in veric.local]
W
weak_mapsto_ [definition, in veric.semax_straight]whole_program_sequential_safety [lemma, in veric.SequentialClight]
with_ge [definition, in veric.seplog]
with_ge [definition, in veric.SeparationLogic]
writable [definition, in veric.compcert_rmaps]
writable_dec [lemma, in veric.compcert_rmaps]
writable_e [lemma, in veric.compcert_rmaps]
writable_readable [lemma, in veric.compcert_rmaps]
writable_join [lemma, in veric.compcert_rmaps]
writable_inv [lemma, in veric.juicy_mem]
writable_join_sub [lemma, in veric.juicy_mem]
writable_blocks [definition, in veric.seplog]
writable_block [definition, in veric.seplog]
writable_share_right [lemma, in veric.seplog]
writable_share [definition, in veric.seplog]
writable_writable_after_alloc' [lemma, in veric.juicy_mem_lemmas]
writable_perm [lemma, in veric.juicy_mem_lemmas]
writable_blocks_rev [lemma, in veric.initialize]
writable_blocks_app [lemma, in veric.initial_world]
writable_share [definition, in veric.SeparationLogic]
wrong_signature [constructor, in veric.expr]
Y
yesat [definition, in veric.res_predicates]yesat_join_sub [lemma, in veric.res_predicates]
yesat_join [lemma, in veric.res_predicates]
yesat_raw_join [lemma, in veric.res_predicates]
yesat_join_diff [lemma, in veric.res_predicates]
yesat_eq [lemma, in veric.res_predicates]
yesat_eq_aux [lemma, in veric.res_predicates]
yesat_raw_eq [lemma, in veric.res_predicates]
yesat_raw_eq_aux [lemma, in veric.res_predicates]
yesat_raw [definition, in veric.res_predicates]
Z
zap_fn_return [definition, in veric.semax]zero_ext_inj [lemma, in veric.initialize]
Zlength_map [lemma, in veric.initial_world]
Zlength_rev [lemma, in veric.initial_world]
Zlength_app [lemma, in veric.initial_world]
Zle_bool_rev [lemma, in veric.expr_lemmas]
Zmax_of_nat [lemma, in veric.initialize]
Zmax_Z_of_nat [lemma, in veric.initialize]
Zminus_lem [lemma, in veric.juicy_mem_lemmas]
Z_of_nat_ge_O [lemma, in veric.seplog]
other
` _ [notation, in veric.lift]`( _ ) [notation, in veric.lift]
Instance Index
A
abstract [in veric.juicy_mem_ops]C
concrete [in veric.juicy_mem_ops]Cross_rmap_aux [in veric.compcert_rmaps]
Cveric [in veric.SeparationLogic]
E
EqDec_kind [in veric.compcert_rmaps]EqDec_memval [in veric.base]
EqDec_type [in veric.base]
EqDec_byte [in veric.base]
EqDec_ident [in veric.base]
EqDec_exitkind [in veric.expr]
I
Iveric [in veric.SeparationLogic]J
juicy_mem_ageable [in veric.juicy_mem]L
LiftClassicalSep' [in veric.SeparationLogic]LiftIndir' [in veric.SeparationLogic]
LiftNatDed' [in veric.SeparationLogic]
LiftSepIndir' [in veric.SeparationLogic]
LiftSepLog' [in veric.SeparationLogic]
N
Nveric [in veric.SeparationLogic]R
Rmaps_Lemmas.Cross_rmap [in veric.rmaps_lemmas]Rmaps_Lemmas.Join_trace [in veric.rmaps_lemmas]
Rmaps.Age_rmap [in veric.rmaps]
Rmaps.ag_rmap [in veric.rmaps]
Rmaps.Canc_resource [in veric.rmaps]
Rmaps.Canc_rmap [in veric.rmaps]
Rmaps.Disj_resource [in veric.rmaps]
Rmaps.Disj_rmap [in veric.rmaps]
Rmaps.Join_nat_rmap' [in veric.rmaps]
Rmaps.Join_resource [in veric.rmaps]
Rmaps.Join_rmap [in veric.rmaps]
RMAPS.Join_nat_rmap' [in veric.rmaps]
RMAPS.Join_resource [in veric.rmaps]
Rmaps.Perm_resource [in veric.rmaps]
Rmaps.Perm_rmap [in veric.rmaps]
Rmaps.Sep_resource [in veric.rmaps]
Rmaps.Sep_rmap [in veric.rmaps]
Rmaps.TyFSA.Join_F [in veric.rmaps]
Rveric [in veric.SeparationLogic]
S
SIveric [in veric.SeparationLogic]SRveric [in veric.SeparationLogic]
StratModel.ca_rj [in veric.rmaps]
StratModel.da_rj [in veric.rmaps]
StratModel.Join_pre_rmap [in veric.rmaps]
StratModel.Join_res [in veric.rmaps]
StratModel.Join_preds [in veric.rmaps]
StratModel.paf_pre_rmap [in veric.rmaps]
StratModel.paf_res [in veric.rmaps]
StratModel.pa_rj [in veric.rmaps]
StratModel.sa_rj [in veric.rmaps]
stratsem [in veric.juicy_mem_ops]
stratsemsep [in veric.juicy_mem_ops]
STRAT_MODEL.paf_pre_rmap [in veric.rmaps]
STRAT_MODEL.Join_pre_rmap [in veric.rmaps]
Sveric [in veric.SeparationLogic]
T
Trip_rmap [in veric.compcert_rmaps]Trip_resource [in veric.compcert_rmaps]
Projection Index
J
JE_exit_hered [in veric.juicy_extspec]JE_post_hered [in veric.juicy_extspec]
JE_pre_hered [in veric.juicy_extspec]
JE_spec [in veric.juicy_extspec]
jminit_fdecs_match [in veric.juicy_extspec]
jminit_defs_no_dups [in veric.juicy_extspec]
jminit_init_mem [in veric.juicy_extspec]
jminit_lev [in veric.juicy_extspec]
jminit_G [in veric.juicy_extspec]
jminit_prog [in veric.juicy_extspec]
jminit_m [in veric.juicy_extspec]
L
lifted [in veric.lift]lift_uncurry_open [in veric.lift]
lift_curry [in veric.lift]
lift_last [in veric.lift]
lift_prod [in veric.lift]
lift_T [in veric.lift]
lift_S [in veric.lift]
O
OK_spec [in veric.juicy_extspec]OK_ty [in veric.juicy_extspec]
S
sa_R [in veric.semax]sa_c [in veric.semax]
sa_P [in veric.semax]
sa_Delta [in veric.semax]
sss_primexpr_safety [in veric.local]
sss_primexpr_erasure [in veric.local]
sss_HG_wellformed [in veric.local]
ss_primexpr_saftey [in veric.local]
ss_primexpr_erasure [in veric.local]
ss_primcom_safety [in veric.local]
ss_primcom_erasure [in veric.local]
ss_GF_wellformed [in veric.local]
ss_VU_wellformed [in veric.local]
Record Index
G
GenericSemantics [in veric.local]J
jm_init_package [in veric.juicy_extspec]juicy_ext_spec [in veric.juicy_extspec]
L
Lift [in veric.lift]O
OracleKind [in veric.juicy_extspec]S
semaxArg [in veric.semax]StratifiedSemantics [in veric.local]
StratifiedSemanticsWithSeparation [in veric.local]
Lemma Index
A
address_mapsto_zeros_eq [in veric.seplog]address_mapsto_VALspec_range [in veric.seplog]
address_mapsto_exists [in veric.seplog]
address_mapsto_exists' [in veric.juicy_mem_lemmas]
address_mapsto_overlap [in veric.res_predicates]
address_mapsto_precise [in veric.res_predicates]
address_mapsto_VALspec_range [in veric.res_predicates]
address_mapsto_exists [in veric.res_predicates]
address_mapsto_VALspec [in veric.res_predicates]
address_mapsto_splittable [in veric.res_predicates]
address_mapsto_old_parametric [in veric.res_predicates]
address_mapsto_fun [in veric.res_predicates]
address_mapsto'_mapsto [in veric.res_predicates]
address_mapsto_can_store [in veric.semax_straight]
add_variables_nextblock [in veric.initialize]
add_globals_hack [in veric.initial_world]
adr_range_zle_fact [in veric.juicy_mem]
adr_range_inv [in veric.juicy_mem]
adr_range_eq_block [in veric.juicy_mem]
adr_inv [in veric.juicy_mem]
adr_inv0 [in veric.juicy_mem]
adr_range_split_lem3 [in veric.assert_lemmas]
adr_range_split_lem2 [in veric.assert_lemmas]
adr_range_split_lem1 [in veric.assert_lemmas]
adr_range_zle_zlt [in veric.juicy_mem_lemmas]
adr_range_divide [in veric.initial_world]
after_alloc'_ok [in veric.juicy_mem]
after_alloc'_valid [in veric.juicy_mem]
age_laterR [in veric.semax_lemmas]
age_core [in veric.semax_call]
age_twin' [in veric.semax_call]
age_jm_phi [in veric.juicy_mem]
age_jm_dry [in veric.juicy_mem]
age_safe [in veric.juicy_extspec]
age_resource_decay [in veric.juicy_extspec]
age1_resource_decay [in veric.semax_lemmas]
age1_juicy_mem_Some [in veric.juicy_mem]
age1_juicy_mem_None2 [in veric.juicy_mem]
age1_juicy_mem_None1 [in veric.juicy_mem]
age1_juicy_mem_unpack'' [in veric.juicy_mem]
age1_juicy_mem_unpack' [in veric.juicy_mem]
age1_juicy_mem_unpack [in veric.juicy_mem]
age1_constructive_joins_eq [in veric.juicy_mem]
age1_joinx [in veric.juicy_mem]
alloc_vars_lemma [in veric.semax_call]
alloc_vars_lookup [in veric.semax_call]
alloc_juicy_variables_e [in veric.semax_call]
alloc_dry_updated_on [in veric.juicy_mem]
alloc_dry_unchanged_on [in veric.juicy_mem]
alloc_variables_fun [in veric.Clight_lemmas]
alloc_Gfun_inflate [in veric.initialize]
alloc_global_inflate_same [in veric.initialize]
alloc_global_access [in veric.initialize]
alloc_global_beyond2 [in veric.initialize]
alloc_global_old [in veric.initial_world]
alloc_globals_rev_nextblock [in veric.initial_world]
alloc_globals_rev_eq [in veric.initial_world]
alloc_globals_app [in veric.initial_world]
alloc_variables_mem_wd [in veric.Clight_coop]
alloc_variables_forward [in veric.Clight_coop]
allowed_val_cast_sound [in veric.expr]
allowed_val_cast_sound [in veric.expr_lemmas]
andb_if [in veric.expr]
and_FF [in veric.semax_lemmas]
and_True [in veric.expr]
and_False [in veric.expr]
another_hackfun_lemma [in veric.initialize]
approx_map_idem [in veric.juicy_mem]
approx_eq_i [in veric.res_predicates]
approx_oo_approx'' [in veric.semax_prog]
assert_safe_last' [in veric.semax_lemmas]
assert_safe_adj' [in veric.semax_lemmas]
assert_safe_adj [in veric.semax_lemmas]
assert_safe_last [in veric.semax_lemmas]
assert_truth [in veric.assert_lemmas]
assign_loc_fun [in veric.Clight_lemmas]
assign_loc_mem_wd [in veric.Clight_coop]
assign_loc_forward [in veric.Clight_coop]
B
binary_operation_val_valid [in veric.Clight_coop]bind_parameters_fun [in veric.Clight_lemmas]
blockwise_valid [in veric.compcert_rmaps]
bool_val_Cnot [in veric.semax_lemmas]
boxy_jam [in veric.res_predicates]
break_strip_CC [in veric.Clight_sim]
break_strip [in veric.Clight_sim]
break_cont_skip [in veric.Clight_sim]
build_call_temp_env [in veric.semax_call]
bytes_writable_readable [in veric.compcert_rmaps]
bytes_readable_dec [in veric.compcert_rmaps]
bytes_writable_dec [in veric.compcert_rmaps]
C
call_cont_app_cons [in veric.semax_lemmas]call_cont_app_nil [in veric.semax_lemmas]
call_cont_current_function [in veric.semax_call]
call_cont_idem [in veric.semax_call]
call_cont_nonnil [in veric.Clight_new]
call_strip' [in veric.Clight_sim]
call_strip [in veric.Clight_sim]
can_alloc_variables' [in veric.semax_call]
can_alloc_variables [in veric.semax_call]
can_age_jm [in veric.juicy_mem]
can_age1_juicy_mem [in veric.juicy_mem]
cast_no_change [in veric.expr_lemmas]
cast_exists [in veric.expr_lemmas]
cast_int_long_nonzero [in veric.binop_lemmas]
cat_prefix_empty [in veric.semax_lemmas]
CCstep_to_CC_step_1 [in veric.Clight_sim]
CC_step_fun [in veric.Clight_sim]
CC_step_to_step [in veric.Clight_sim]
CC_atExternal_isExternal [in veric.Clight_sim]
CC_step_to_CCstep [in veric.Clight_sim]
CC_at_external_halted_excl [in veric.Clight_sim]
CC_corestep_not_halted [in veric.Clight_sim]
CC_corestep_not_at_external [in veric.Clight_sim]
CC_core_to_CC_state_inj [in veric.Clight_sim]
CC_core_CC_state_4 [in veric.Clight_sim]
CC_core_CC_state_3 [in veric.Clight_sim]
CC_core_CC_state_2 [in veric.Clight_sim]
CC_core_CC_state_1 [in veric.Clight_sim]
cc_step_fun [in veric.Clight_sim]
classify_shift_eq [in veric.binop_lemmas]
classify_add_eq [in veric.binop_lemmas]
classify_cmp_eq [in veric.binop_lemmas]
classify_sub_eq [in veric.binop_lemmas]
Clightnew_Clight_sim [in veric.Clight_sim]
Clightnew_Clight_sim_eq [in veric.Clight_sim]
Clightnew_Clight_sim_eq_noOrder [in veric.Clight_sim]
Clightnew_Clight_sim_eq_noOrder_SSplusConclusion [in veric.Clight_sim]
cl_corestep_fun' [in veric.semax_lemmas]
cl_corestep_fun [in veric.Clight_new]
cl_after_at_external_excl [in veric.Clight_new]
cl_corestep_not_halted [in veric.Clight_new]
cl_corestep_not_at_external [in veric.Clight_new]
cl_coopstep_not_halted [in veric.Clight_coop]
cl_coopstep_not_at_external [in veric.Clight_coop]
cl_forward [in veric.Clight_coop]
CompCert_AV.valid_join [in veric.compcert_rmaps]
CompCert_AV.valid_empty [in veric.compcert_rmaps]
components_join_joins [in veric.juicy_mem_lemmas]
compute_list_norepet_e [in veric.expr]
constructive_age1_join [in veric.juicy_mem]
cons_app' [in veric.semax_lemmas]
cons_app [in veric.semax_lemmas]
contains_Lsh_e [in veric.semax_call]
contents_cohere_join_sub [in veric.juicy_mem_lemmas]
continue_cont_is [in veric.Clight_sim]
continue_cont_skip [in veric.Clight_sim]
control_suffix_safe [in veric.semax_lemmas]
control_as_safe_le [in veric.semax_lemmas]
coop_forward [in veric.Clight_coop]
coop_mem_wd [in veric.Clight_coop]
corable_fun_assert [in veric.assert_lemmas]
corable_jam [in veric.assert_lemmas]
corable_funassert [in veric.assert_lemmas]
corable_imp [in veric.assert_lemmas]
corable_prop [in veric.assert_lemmas]
corable_exp [in veric.assert_lemmas]
corable_allp [in veric.assert_lemmas]
corable_orp [in veric.assert_lemmas]
corable_andp [in veric.assert_lemmas]
corable_pureat [in veric.assert_lemmas]
corestep_preservation_lemma [in veric.semax_lemmas]
core_load_fun [in veric.assert_lemmas]
core_load_load [in veric.juicy_mem_lemmas]
core_load_load' [in veric.juicy_mem_lemmas]
core_load_valid [in veric.juicy_mem_lemmas]
core_load_getN [in veric.juicy_mem_lemmas]
core_inflate_initial_mem [in veric.semax_prog]
current_function_find_label_ls [in veric.Clight_sim]
current_function_find_label [in veric.Clight_sim]
current_function_call_cont [in veric.Clight_sim]
current_function_strip [in veric.Clight_sim]
D
decode_byte_val [in veric.seplog]decode_val_getN_lem1 [in veric.initialize]
dec_skip [in veric.semax_lemmas]
dec_continue [in veric.Clight_sim]
dec_skip [in veric.Clight_sim]
dec_pure [in veric.initial_world]
denote_tc_assert_andp [in veric.expr]
denote_tc_assert'_andp'_e [in veric.binop_lemmas]
denote_tc_assert_orp' [in veric.binop_lemmas]
denote_tc_assert_andp' [in veric.binop_lemmas]
denote_tc_assert_andp [in veric.binop_lemmas]
denote_tc_assert_orp'' [in veric.binop_lemmas]
denote_tc_assert_andp'' [in veric.binop_lemmas]
denote_tc_assert_iszero' [in veric.binop_lemmas]
denote_tc_assert_iszero [in veric.binop_lemmas]
denote_tc_assert_orp [in veric.binop_lemmas]
denote_tc_assert'_eq [in veric.binop_lemmas]
den_isBinOpR [in veric.binop_lemmas]
deref_loc_fun [in veric.Clight_lemmas]
deref_loc_val_valid [in veric.Clight_coop]
derives_skip [in veric.semax_lemmas]
dry_noperm_juicy_nonreadable [in veric.juicy_mem]
E
elements_remove [in veric.semax_call]empty_program_ok [in veric.semax_lemmas]
empty_rmap_valid [in veric.res_predicates]
eqb_type_refl [in veric.expr]
eqb_type_true [in veric.expr]
eqb_type_false [in veric.environ_lemmas]
eqb_type_eq [in veric.environ_lemmas]
equiv_e2 [in veric.Clight_lemmas]
equiv_e1 [in veric.Clight_lemmas]
eq_block_lem [in veric.Clight_lemmas]
eval_lvalue_fun [in veric.Clight_lemmas]
eval_exprlist_fun [in veric.Clight_lemmas]
eval_expr_fun [in veric.Clight_lemmas]
eval_expr_lvalue_fun [in veric.Clight_lemmas]
eval_id_other [in veric.expr]
eval_id_same [in veric.expr]
eval_cast_sem_cast [in veric.expr_lemmas]
eval_lvalue_relate [in veric.expr_lemmas]
eval_expr_relate [in veric.expr_lemmas]
eval_both_relate [in veric.expr_lemmas]
eval_binop_relate_fail [in veric.expr_lemmas]
eval_lvalue_ptr [in veric.expr_lemmas]
eval_deref_loc_val_valid [in veric.Clight_coop]
eval_lvalue_val_valid [in veric.Clight_coop]
eval_expr_val_valid [in veric.Clight_coop]
eval_expr_lvalue_valid_aux [in veric.Clight_coop]
eventval_list_match_fun [in veric.Clight_lemmas]
ewand_TT_emp [in veric.semax_lemmas]
exec_skips'_CC [in veric.Clight_sim]
exec_skips_CC [in veric.Clight_sim]
exec_skips' [in veric.Clight_sim]
exec_skips [in veric.Clight_sim]
Exists_dec [in veric.initialize]
exit_tycontext_eqv [in veric.semax_lemmas]
exit_tycon_sub [in veric.semax_lemmas]
exprlist_eval [in veric.semax_call]
expr_safety [in veric.local]
expr_erasure [in veric.local]
expr_erase_pure_expr [in veric.local]
extend_tc_value [in veric.seplog]
extend_tc_lvalue [in veric.seplog]
extend_tc_exprlist [in veric.seplog]
extend_tc_expr [in veric.seplog]
extend_tc_temp_id [in veric.seplog]
extend_tc_temp_id_load [in veric.seplog]
extend_prop [in veric.seplog]
extensible_core_load' [in veric.assert_lemmas]
extern_retainer_neq_top [in veric.juicy_mem]
extern_retainer_neq_bot [in veric.juicy_mem]
extract_exists_pre [in veric.semax_lemmas]
extract_exists [in veric.semax_lemmas]
F
False_and [in veric.expr]False_or [in veric.binop_lemmas]
filter_seq_call_cont [in veric.semax_lemmas]
filter_seq_current_function [in veric.semax_lemmas]
filter_genv_zero_ofs [in veric.expr_lemmas]
find_label_prefix2 [in veric.semax_lemmas]
find_label_ls_prefix2' [in veric.semax_lemmas]
find_label_prefix2' [in veric.semax_lemmas]
find_label_ls_None [in veric.semax_lemmas]
find_label_None [in veric.semax_lemmas]
find_label_ls_prefix [in veric.semax_lemmas]
find_label_prefix [in veric.semax_lemmas]
find_id_rev [in veric.initialize]
find_symbol_globalenv [in veric.initial_world]
find_symbol_add_globals [in veric.initial_world]
find_id_e [in veric.initial_world]
find_id_i [in veric.initial_world]
fixup_join [in veric.compcert_rmaps]
fixup_splitting_valid [in veric.compcert_rmaps]
fold_right_rev_left [in veric.initial_world]
forallb_rev [in veric.initialize]
frame_loop1 [in veric.seplog]
frame_for1 [in veric.seplog]
frame_normal [in veric.seplog]
free_list_juicy_mem_lem [in veric.semax_call]
free_list_juicy_mem_ext [in veric.semax_call]
free_juicy_mem_ext [in veric.semax_call]
free_list_free [in veric.semax_call]
free_not_freeable_eq [in veric.juicy_mem]
free_nadr_range_eq [in veric.juicy_mem]
free_smaller_None [in veric.juicy_mem]
fst_split [in veric.semax_call]
fst_split_fullshare_not_top [in veric.juicy_mem]
fst_split_fullshare_not_bot [in veric.juicy_mem]
fst_match_fdecs [in veric.semax_prog]
fullempty_after_alloc [in veric.juicy_mem]
funassert_update_tycon [in veric.semax_loop]
funassert_exit_tycon [in veric.semax_loop]
funassert_rho [in veric.semax_prog]
funassert_initial_core [in veric.semax_prog]
function_pointer_aux [in veric.semax_call]
func_tycontext'_eqv [in veric.semax_lemmas]
func_at_func_at' [in veric.semax_call]
func_tycontext_t_sound [in veric.expr_lemmas]
func_tycontext_v_sound [in veric.expr_lemmas]
FUNspec_parametric [in veric.res_predicates]
fun_assert_contractive [in veric.res_predicates]
G
getVAL [in veric.compcert_rmaps]get_typed_int [in veric.expr_lemmas]
GF_wellformed [in veric.local]
ghostp_unique_andp [in veric.ghost]
ghostp_unique_sepcon [in veric.ghost]
global_initializers [in veric.initialize]
globvars2pred_rev [in veric.initialize]
glob_types_join_labeled [in veric.expr_lemmas]
glob_types_update_tycon [in veric.expr_lemmas]
glob_types_update_dist [in veric.expr_lemmas]
guard_environ_sub [in veric.semax_lemmas]
guard_safe_adj [in veric.semax_lemmas]
guard_environ_eqv [in veric.semax_lemmas]
guard_environ_put_te' [in veric.semax_lemmas]
guard_environ_e1 [in veric.semax]
H
hackfun_beyond_block [in veric.initialize]hackfun_sep [in veric.initialize]
HG_wellformed [in veric.local]
HO_pred_eq_i1 [in veric.semax_prog]
I
id_in_list_false [in veric.expr]id_in_list_true [in veric.expr]
if_E_true [in veric.Clight_coop]
if_E_false [in veric.Clight_coop]
inflate_free_resource_decay [in veric.juicy_mem]
inflate_store_resource_nodecay [in veric.juicy_mem]
inflate_initial_mem_all_VALs [in veric.juicy_mem]
inflate_initial_mem_level [in veric.juicy_mem]
inflate_initial_mem'_valid [in veric.juicy_mem]
inflate_initial_mem'_fmap [in veric.juicy_mem]
inflate_initial_mem_empty [in veric.juicy_mem_lemmas]
initblocksize_name [in veric.initial_world]
initialized_tycontext_eqv [in veric.semax_lemmas]
initialized_sub [in veric.expr_lemmas]
initialized_ne [in veric.expr_lemmas]
initialized_tycontext_evolve [in veric.environ_lemmas]
initial_mem_all_VALs [in veric.juicy_mem]
initial_mem_level [in veric.juicy_mem]
initial_mem_core [in veric.juicy_mem_lemmas]
initial_core_rev [in veric.initialize]
initial_core_ok [in veric.initial_world]
init_datalist_hack [in veric.initialize]
init_data_list_lem [in veric.initialize]
init_data_list_size_app [in veric.initialize]
init_data_lem [in veric.initialize]
init_data_list_size_pos [in veric.initialize]
intersection_splittable [in veric.res_predicates]
int_eq_true [in veric.binop_lemmas]
inv_find_symbol_fun [in veric.Clight_lemmas]
in_map_fst [in veric.initial_world]
In_fst_split [in veric.environ_lemmas]
in_prog_vars_in_prog_defs [in veric.semax_prog]
in_prog_funct_in_prog_defs [in veric.semax_prog]
in_prog_funct'_in [in veric.semax_prog]
isCastR [in veric.expr_lemmas]
isVAL_dec [in veric.compcert_rmaps]
isVAL_i [in veric.compcert_rmaps]
is_true_false [in veric.binop_lemmas]
is_true_true [in veric.binop_lemmas]
is_true_dec [in veric.local]
J
jam_noat_splittable [in veric.res_predicates]jam_noat_splittable_aux [in veric.res_predicates]
jam_false [in veric.res_predicates]
jam_true [in veric.res_predicates]
join_tycon_labeled_eqv [in veric.semax_lemmas]
join_tycontext_eqv [in veric.semax_lemmas]
join_sub_share_top [in veric.semax_lemmas]
join_share_of [in veric.compcert_rmaps]
join_upto_beyond_block [in veric.initialize]
join_only_blocks [in veric.initialize]
join_tycon_same [in veric.expr]
join_te_denote2 [in veric.expr_lemmas]
join_te_eqv [in veric.expr_lemmas]
join_te_denote [in veric.environ_lemmas]
jstep_not_halted [in veric.juicy_extspec]
jstep_not_at_external [in veric.juicy_extspec]
JuicyMemOps.after_alloc_alloc_cohere [in veric.juicy_mem_ops]
JuicyMemOps.after_alloc_max_access_cohere [in veric.juicy_mem_ops]
JuicyMemOps.after_alloc_access_cohere [in veric.juicy_mem_ops]
JuicyMemOps.after_alloc_contents_cohere [in veric.juicy_mem_ops]
JuicyMemOps.juicy_mem_free_succeeds [in veric.juicy_mem_ops]
JuicyMemOps.juicy_mem_alloc_succeeds [in veric.juicy_mem_ops]
JuicyMemOps.juicy_mem_alloc_level [in veric.juicy_mem_ops]
JuicyMemOps.juicy_mem_alloc_at [in veric.juicy_mem_ops]
JuicyMemOps.juicy_mem_alloc_aux1 [in veric.juicy_mem_ops]
JuicyMemOps.juicy_mem_storebytes_succeeds [in veric.juicy_mem_ops]
JuicyMemOps.juicy_mem_store_succeeds [in veric.juicy_mem_ops]
JuicyMemOps.pshare_sh_bot [in veric.juicy_mem_ops]
juicy_mem_alloc_core [in veric.semax_call]
juicy_store_nodecay [in veric.juicy_mem]
juicy_mem_ext [in veric.juicy_mem]
juicy_mem_ageable_facts [in veric.juicy_mem]
juicy_mem_alloc_cohere [in veric.juicy_mem]
juicy_mem_max_access [in veric.juicy_mem]
juicy_mem_access [in veric.juicy_mem]
juicy_mem_contents [in veric.juicy_mem]
juicy_free_lemma [in veric.juicy_mem_lemmas]
j_after_at_external_excl [in veric.juicy_extspec]
j_at_external_halted_excl [in veric.juicy_extspec]
L
laterR_level [in veric.semax_prog]later_strengthen_safe1 [in veric.semax_lemmas]
later_twin [in veric.semax_call]
later_twin' [in veric.semax_call]
later_sepcon2 [in veric.semax_straight]
level_storebytes_juicy_mem [in veric.juicy_mem]
level_store_juicy_mem [in veric.juicy_mem]
level_remake_rmap [in veric.juicy_mem]
level_make_rmap [in veric.juicy_mem]
level_juice_level_phi [in veric.juicy_mem]
level_only_blocks [in veric.initialize]
level_later [in veric.res_predicates]
level1_juicy_mem [in veric.juicy_mem]
level2_juicy_mem [in veric.juicy_mem]
list_norepet_rev [in veric.expr]
list_disjoint_rev2 [in veric.initial_world]
LKspec_splittable [in veric.res_predicates]
LKspec_parametric [in veric.res_predicates]
load_core_load [in veric.juicy_mem_lemmas]
load_store_init_data_lem1 [in veric.initialize]
load_store_zeros [in veric.initialize]
load_cast [in veric.semax_straight]
loeb [in veric.semax_lemmas]
M
make_ghostp [in veric.ghost]make_tycontext_g_denote [in veric.semax_prog]
mapsto_core_load [in veric.assert_lemmas]
mapsto_can_store [in veric.juicy_mem_lemmas]
mapsto_valid_access_wr [in veric.juicy_mem_lemmas]
mapsto_valid_access [in veric.juicy_mem_lemmas]
mapsto_is_pointer [in veric.semax_straight]
mapsto_valid_pointer [in veric.semax_straight]
map_compose_approx_succ_e [in veric.res_predicates]
map_ptree_rel [in veric.expr_lemmas]
Map.ext [in veric.expr]
Map.gro [in veric.expr]
Map.grs [in veric.expr]
Map.gso [in veric.expr]
Map.gss [in veric.expr]
Map.gsspec [in veric.expr]
Map.override [in veric.expr]
Map.override_same [in veric.expr]
match_find_label_ls [in veric.Clight_sim]
match_find_label [in veric.Clight_sim]
match_find_ls_None [in veric.Clight_sim]
match_find_label_None [in veric.Clight_sim]
match_cont_strip1 [in veric.Clight_sim]
match_cont_call_strip [in veric.Clight_sim]
match_cont_strip [in veric.Clight_sim]
match_fdecs_rev [in veric.initialize]
match_fsig_e [in veric.expr]
match_fdecs_exists_Gfun [in veric.initial_world]
max_unsigned_modulus [in veric.initialize]
max_unsigned_eq [in veric.initialize]
memory_block'_eq [in veric.seplog]
memory_block'_split [in veric.SeparationLogic]
mem_access_perm [in veric.juicy_mem]
mem_alloc_juicy [in veric.initial_world]
modifiedvars_ls_union [in veric.expr]
modifiedvars'_union [in veric.expr]
mod_after_alloc'_ok [in veric.juicy_mem]
mod_after_alloc'_valid [in veric.juicy_mem]
N
nat_of_Z_minus_le [in veric.semax_lemmas]nat_ind2 [in veric.Clight_lemmas]
nat_ind2_Type [in veric.Clight_lemmas]
nat_of_Z_lem2 [in veric.juicy_mem_lemmas]
nat_of_Z_lem1 [in veric.juicy_mem_lemmas]
nat_of_Z_eq [in veric.res_predicates]
necR_core [in veric.semax_call]
necR_m_dry [in veric.juicy_mem_lemmas]
necR_level [in veric.semax_prog]
neg_val_valid [in veric.Clight_coop]
neutral_cast_typecheck_val [in veric.expr_lemmas]
nextblock_access_empty [in veric.juicy_mem]
nonunit_join [in veric.res_predicates]
normal_ret_assert_FF [in veric.seplog]
normal_ret_assert_derives [in veric.seplog]
notbool_val_valid [in veric.Clight_coop]
notint_val_valid [in veric.Clight_coop]
no_dups_swap [in veric.semax_lemmas]
no_dups_inv [in veric.Clight_lemmas]
nreadable_inv [in veric.juicy_mem]
nth_eq_nth_error_eq [in veric.assert_lemmas]
nth_error_in_bounds [in veric.assert_lemmas]
nth_getN [in veric.juicy_mem_lemmas]
nth_error_length [in veric.res_predicates]
nth_error_rev [in veric.initial_world]
nth_error_app1 [in veric.initial_world]
nth_error_app [in veric.initial_world]
O
of_bool_Int_eq_e [in veric.Clight_lemmas]only_blocks_at [in veric.initialize]
opt2list_inj [in veric.semax_call]
opt2list2opt [in veric.semax_lemmas]
oracle_unage [in veric.juicy_mem_lemmas]
orb_if [in veric.expr]
or_pred_ext [in veric.semax]
or_True [in veric.binop_lemmas]
or_False [in veric.binop_lemmas]
overridePost_normal [in veric.seplog]
P
pass_params_ni [in veric.semax_call]perm_mem_access [in veric.juicy_mem]
perm_of_empty [in veric.juicy_mem]
perm_of_nonempty [in veric.juicy_mem]
perm_of_readable [in veric.juicy_mem]
perm_of_writable [in veric.juicy_mem]
perm_of_freeable [in veric.juicy_mem]
perm_of_sh_Freeable_top [in veric.juicy_mem]
perm_of_sh_fullshare [in veric.juicy_mem]
perm_of_sh_pshare [in veric.juicy_mem]
perm_order'_trans [in veric.juicy_mem_lemmas]
perm_of_sh_join_sub [in veric.juicy_mem_lemmas]
phi_valid [in veric.juicy_mem]
pjoinable_None_emp [in veric.semax_lemmas]
pjoinable_emp_None [in veric.semax_lemmas]
plus_star_trans [in veric.Clight_sim]
plus_trans [in veric.Clight_sim]
pointer_cmp_no_mem_bool_type [in veric.semax_straight]
pointer_cmp_eval [in veric.semax_straight]
prebreak_cont_is [in veric.semax_lemmas]
preds_fmap_NoneP_approx [in veric.juicy_mem_lemmas]
pred_sub_later' [in veric.semax_lemmas]
PrimcomErasure [in veric.juicy_mem_ops]
PrimcomSafety [in veric.juicy_mem_ops]
primcom_safety [in veric.local]
primcom_erasure [in veric.local]
PrimexprErasure [in veric.juicy_mem_ops]
PrimexprSafety [in veric.juicy_mem_ops]
primexpr_safety [in veric.local]
primexpr_erasure [in veric.local]
prog_contains_prog_funct [in veric.semax_prog]
prop_imp_derives [in veric.semax_lemmas]
prop_unext [in veric.semax_call]
prop_derives [in veric.assert_lemmas]
prop_imp_i [in veric.assert_lemmas]
ptr_compare_no_binop_tc [in veric.expr_lemmas]
pure_expr_dec [in veric.local]
pure_expr_safe [in veric.local]
pure_exprEval [in veric.local]
R
range_inv [in veric.juicy_mem]range_inv0 [in veric.juicy_mem]
range_dec [in veric.res_predicates]
readable_dec [in veric.compcert_rmaps]
readable_e [in veric.compcert_rmaps]
readable_writable_join [in veric.compcert_rmaps]
readable_join [in veric.compcert_rmaps]
readable_inv [in veric.juicy_mem]
readable_eq_after_alloc' [in veric.juicy_mem_lemmas]
read_sh_readonly [in veric.initialize]
resource_decay_funassert [in veric.semax_call]
resource_at_slice [in veric.slice]
resource_decay_trans [in veric.juicy_mem]
resource_decay_refl [in veric.juicy_mem]
resource_nodecay_decay [in veric.juicy_mem]
resource_at_remake_rmap [in veric.juicy_mem]
resource_at_make_rmap [in veric.juicy_mem]
resource_fmap_core [in veric.seplog]
resource_identity_dec [in veric.initialize]
res_option_core [in veric.semax_straight]
ret_type_update_dist [in veric.expr_lemmas]
ret_type_exit_tycon [in veric.semax_loop]
ret_type_join_tycon_labeled [in veric.semax_loop]
ret_type_update_tycon [in veric.semax_loop]
ret_type_join_tycon [in veric.semax_loop]
rev_if_be_singleton [in veric.seplog]
rev_prog_funct' [in veric.initialize]
rev_if_be_1 [in veric.initialize]
rev_prog_vars' [in veric.initialize]
rev_prog_vars' [in veric.semax_prog]
rguard_adj [in veric.semax_lemmas]
Rmaps_Lemmas.resource_at_empty2 [in veric.rmaps_lemmas]
Rmaps_Lemmas.core_not_YES [in veric.rmaps_lemmas]
Rmaps_Lemmas.core_PURE [in veric.rmaps_lemmas]
Rmaps_Lemmas.core_NO [in veric.rmaps_lemmas]
Rmaps_Lemmas.core_YES [in veric.rmaps_lemmas]
Rmaps_Lemmas.resource_at_identity [in veric.rmaps_lemmas]
Rmaps_Lemmas.core_resource_at [in veric.rmaps_lemmas]
Rmaps_Lemmas.PURE_inj [in veric.rmaps_lemmas]
Rmaps_Lemmas.SomeP_inj [in veric.rmaps_lemmas]
Rmaps_Lemmas.SomeP_inj2 [in veric.rmaps_lemmas]
Rmaps_Lemmas.SomeP_inj1 [in veric.rmaps_lemmas]
Rmaps_Lemmas.YES_inj [in veric.rmaps_lemmas]
Rmaps_Lemmas.resource_at_core_identity [in veric.rmaps_lemmas]
Rmaps_Lemmas.identity_resource [in veric.rmaps_lemmas]
Rmaps_Lemmas.Cross_rmap_simple [in veric.rmaps_lemmas]
Rmaps_Lemmas.join_res_retain [in veric.rmaps_lemmas]
Rmaps_Lemmas.fixup_trace_rmap [in veric.rmaps_lemmas]
Rmaps_Lemmas.fixup_trace_valid [in veric.rmaps_lemmas]
Rmaps_Lemmas.Cross_resource [in veric.rmaps_lemmas]
Rmaps_Lemmas.res_option_join [in veric.rmaps_lemmas]
Rmaps_Lemmas.level_make_rmap [in veric.rmaps_lemmas]
Rmaps_Lemmas.resource_at_make_rmap [in veric.rmaps_lemmas]
Rmaps_Lemmas.approx_FF [in veric.rmaps_lemmas]
Rmaps_Lemmas.empty_rmap_level [in veric.rmaps_lemmas]
Rmaps_Lemmas.emp_empty_rmap [in veric.rmaps_lemmas]
Rmaps_Lemmas.join_YES_pfullshare2 [in veric.rmaps_lemmas]
Rmaps_Lemmas.join_YES_pfullshare1 [in veric.rmaps_lemmas]
Rmaps_Lemmas.ageN_resource_at_eq [in veric.rmaps_lemmas]
Rmaps_Lemmas.rmap_unage_age [in veric.rmaps_lemmas]
Rmaps_Lemmas.remake_rmap [in veric.rmaps_lemmas]
Rmaps_Lemmas.resource_at_joins2 [in veric.rmaps_lemmas]
Rmaps_Lemmas.resource_at_constructive_joins2 [in veric.rmaps_lemmas]
Rmaps_Lemmas.level_later_fash [in veric.rmaps_lemmas]
Rmaps_Lemmas.level_age_fash [in veric.rmaps_lemmas]
Rmaps_Lemmas.empty_NO [in veric.rmaps_lemmas]
Rmaps_Lemmas.age1_YES [in veric.rmaps_lemmas]
Rmaps_Lemmas.age1_resource_at [in veric.rmaps_lemmas]
Rmaps_Lemmas.necR_res_option [in veric.rmaps_lemmas]
Rmaps_Lemmas.age1_res_option [in veric.rmaps_lemmas]
Rmaps_Lemmas.resource_at_join_sub [in veric.rmaps_lemmas]
Rmaps_Lemmas.necR_YES'' [in veric.rmaps_lemmas]
Rmaps_Lemmas.necR_YES' [in veric.rmaps_lemmas]
Rmaps_Lemmas.preds_fmap_NoneP [in veric.rmaps_lemmas]
Rmaps_Lemmas.rmap_valid [in veric.rmaps_lemmas]
Rmaps_Lemmas.resource_at_empty [in veric.rmaps_lemmas]
Rmaps_Lemmas.necR_NO [in veric.rmaps_lemmas]
Rmaps_Lemmas.necR_PURE [in veric.rmaps_lemmas]
Rmaps_Lemmas.necR_YES [in veric.rmaps_lemmas]
Rmaps_Lemmas.necR_resource_at [in veric.rmaps_lemmas]
Rmaps_Lemmas.resource_at_approx [in veric.rmaps_lemmas]
Rmaps_Lemmas.resource_fmap_fmap [in veric.rmaps_lemmas]
Rmaps_Lemmas.preds_fmap_fmap [in veric.rmaps_lemmas]
Rmaps_Lemmas.necR_NOx [in veric.rmaps_lemmas]
Rmaps_Lemmas.YES_overlap [in veric.rmaps_lemmas]
Rmaps_Lemmas.YES_not_identity [in veric.rmaps_lemmas]
Rmaps_Lemmas.YES_join_full [in veric.rmaps_lemmas]
Rmaps_Lemmas.unageN [in veric.rmaps_lemmas]
Rmaps_Lemmas.ageN_squash [in veric.rmaps_lemmas]
Rmaps_Lemmas.all_resource_at_identity [in veric.rmaps_lemmas]
Rmaps_Lemmas.resource_at_join2 [in veric.rmaps_lemmas]
Rmaps_Lemmas.resource_at_join [in veric.rmaps_lemmas]
Rmaps_Lemmas.rmap_ext [in veric.rmaps_lemmas]
Rmaps_Lemmas.unsquash_inj [in veric.rmaps_lemmas]
Rmaps_Lemmas.allocate [in veric.rmaps_lemmas]
Rmaps_Lemmas.deallocate [in veric.rmaps_lemmas]
Rmaps_Lemmas.resources_same_level [in veric.rmaps_lemmas]
Rmaps_Lemmas.approx_oo_approx [in veric.rmaps_lemmas]
Rmaps_Lemmas.approx_oo_approx' [in veric.rmaps_lemmas]
Rmaps_Lemmas.make_rmap'' [in veric.rmaps_lemmas]
Rmaps_Lemmas.make_rmap [in veric.rmaps_lemmas]
Rmaps_Lemmas.make_rmap' [in veric.rmaps_lemmas]
Rmaps_Lemmas.necR_resource_at_identity [in veric.rmaps_lemmas]
Rmaps_Lemmas.age1_resource_at_identity [in veric.rmaps_lemmas]
Rmaps_Lemmas.identity_NO [in veric.rmaps_lemmas]
Rmaps_Lemmas.PURE_identity [in veric.rmaps_lemmas]
Rmaps_Lemmas.NO_identity [in veric.rmaps_lemmas]
Rmaps_Lemmas.ageN_level [in veric.rmaps_lemmas]
Rmaps_Lemmas.approx_ge [in veric.rmaps_lemmas]
Rmaps_Lemmas.approx_lt [in veric.rmaps_lemmas]
Rmaps_Lemmas.approx_p [in veric.rmaps_lemmas]
Rmaps.fmap_p2p'_inj [in veric.rmaps]
Rmaps.join_unsquash [in veric.rmaps]
Rmaps.preds_fmap_comp [in veric.rmaps]
Rmaps.preds_fmap_id [in veric.rmaps]
Rmaps.pred_ext' [in veric.rmaps]
Rmaps.pre_rmap2rmap'2pre_rmap [in veric.rmaps]
Rmaps.resource_fmap_comp [in veric.rmaps]
Rmaps.resource_fmap_id [in veric.rmaps]
Rmaps.resource2res2resource [in veric.rmaps]
Rmaps.res_option_rewrite [in veric.rmaps]
Rmaps.res2resource2res [in veric.rmaps]
Rmaps.rmapj_valid_join [in veric.rmaps]
Rmaps.rmapj_valid_core [in veric.rmaps]
Rmaps.rmap_level_eq [in veric.rmaps]
Rmaps.rmap_age1_eq [in veric.rmaps]
Rmaps.rmap_age1_knot_age1 [in veric.rmaps]
Rmaps.rmap_fmap_comp [in veric.rmaps]
Rmaps.rmap_fmap_id [in veric.rmaps]
Rmaps.rmap'2pre_rmap2rmap' [in veric.rmaps]
Rmaps.same_valid [in veric.rmaps]
Rmaps.squash_unsquash [in veric.rmaps]
Rmaps.unevolve_identity_rmap [in veric.rmaps]
Rmaps.unsquash_squash [in veric.rmaps]
Rmaps.valid_res_map [in veric.rmaps]
rmap_valid_e2 [in veric.compcert_rmaps]
rmap_valid_e1 [in veric.compcert_rmaps]
rmap_join_sub_eq_level [in veric.juicy_mem]
rmap_join_eq_level [in veric.juicy_mem]
rmap_unage_age [in veric.assert_lemmas]
rmap_unage_YES [in veric.juicy_mem_lemmas]
S
safeN_strip [in veric.semax_lemmas]safe_step_forward [in veric.semax_lemmas]
safe_loop_skip [in veric.semax_lemmas]
safe_seq_assoc [in veric.local]
same_glob_funassert [in veric.semax_lemmas]
same_base_tc_val [in veric.expr_lemmas]
semax_extensionality_Delta [in veric.semax_lemmas]
semax_frame [in veric.semax_lemmas]
semax_extensionality1 [in veric.semax_lemmas]
semax_extensionality0 [in veric.semax_lemmas]
semax_skip [in veric.semax_lemmas]
semax_pre_post [in veric.semax_lemmas]
semax_pre [in veric.semax_lemmas]
semax_post [in veric.semax_lemmas]
semax_unfold [in veric.semax_lemmas]
semax_extract_prop [in veric.semax_lemmas]
semax_return [in veric.semax_call]
semax_call_ext [in veric.semax_call]
semax_call_alt [in veric.semax_call]
semax_call [in veric.semax_call]
semax_call_aux [in veric.semax_call]
semax_call_typecheck_environ [in veric.semax_call]
semax_fun_id_alt [in veric.semax_call]
semax_fun_id [in veric.semax_call]
semax_fold_unfold [in veric.semax]
semax_continue [in veric.semax_loop]
semax_break [in veric.semax_loop]
semax_loop [in veric.semax_loop]
semax_seq [in veric.semax_loop]
semax_ifthenelse [in veric.semax_loop]
semax_store [in veric.semax_straight]
semax_load [in veric.semax_straight]
semax_set [in veric.semax_straight]
semax_set_forward [in veric.semax_straight]
semax_ptr_compare [in veric.semax_straight]
semax_straight_simple [in veric.semax_straight]
semax_prog_rule [in veric.semax_prog]
semax_prog_typecheck_aux [in veric.semax_prog]
semax_func_cons_ext [in veric.semax_prog]
semax_func_cons [in veric.semax_prog]
semax_func_cons_aux [in veric.semax_prog]
semax_func_nil [in veric.semax_prog]
semax'_pre_post [in veric.semax_lemmas]
semax'_pre [in veric.semax_lemmas]
semax'_post [in veric.semax_lemmas]
sem_cast_eval_cast [in veric.expr_lemmas]
sem_cmp_val_valid [in veric.Clight_coop]
sem_shift_val_valid [in veric.Clight_coop]
sem_mod_val_valid [in veric.Clight_coop]
sem_div_val_valid [in veric.Clight_coop]
sem_mul_val_valid [in veric.Clight_coop]
sem_sub_val_valid [in veric.Clight_coop]
sem_add_val_valid [in veric.Clight_coop]
sem_binarith_val_valid [in veric.Clight_coop]
sem_cast_val_valid [in veric.Clight_coop]
sepcon_FF [in veric.semax_lemmas]
sep_expr_safety [in veric.local]
sep_expr_erasure [in veric.local]
sep_primexpr_safety [in veric.local]
sep_primexpr_erasure [in veric.local]
seq_assoc [in veric.semax_loop]
seq_assoc2 [in veric.semax_loop]
seq_assoc1 [in veric.semax_loop]
set_inside [in veric.expr_lemmas]
set_temp_ret [in veric.expr_lemmas]
set_temp_ge [in veric.expr_lemmas]
set_temp_ve [in veric.expr_lemmas]
share_of_Some [in veric.compcert_rmaps]
signed_zero [in veric.Clight_lemmas]
SimpleAdrVal.valid_join [in veric.rmaps]
SimpleAdrVal.valid_empty [in veric.rmaps]
slice_rmap_join [in veric.slice]
slice_rmap_level [in veric.slice]
slice_rmap_ok [in veric.slice]
slice_rmap_valid [in veric.slice]
slice_resource_valid [in veric.slice]
smaller_temps_exists [in veric.semax_call]
snd_split [in veric.semax_call]
someP_inj [in veric.semax_call]
SoundSeparationLogic.CSL.corable_func_ptr [in veric.SeparationLogicSoundness]
SoundSeparationLogic.CSL.semax_external_FF [in veric.SeparationLogicSoundness]
split_rmap_at2 [in veric.slice]
split_rmap_at1 [in veric.slice]
split_rmap_join [in veric.slice]
split_resource_join [in veric.slice]
split_rmap_ok2 [in veric.slice]
split_rmap_ok1 [in veric.slice]
split_rmap_valid2 [in veric.slice]
split_rmap_valid1 [in veric.slice]
split_range [in veric.initialize]
split_top_neq [in veric.initial_world]
stackframe_of_freeable_blocks [in veric.semax_call]
stackframe_of_eq [in veric.seplog]
star_trans [in veric.Clight_sim]
star_plus_trans [in veric.Clight_sim]
step_continue_switch_CC [in veric.Clight_sim]
step_continue_seq_CC [in veric.Clight_sim]
step_continue_strip_CC [in veric.Clight_sim]
step_to_CC_step [in veric.Clight_sim]
step_continue_strip [in veric.Clight_sim]
step_star_erasure [in veric.local]
step_safety [in veric.local]
step_erasure [in veric.local]
step_compatible [in veric.local]
step_safe' [in veric.local]
step_safe [in veric.local]
step_nprimcom_det [in veric.local]
step_star_stepN [in veric.local]
step_star_trans [in veric.local]
step_step_star [in veric.local]
storebytes_phi_elsewhere_eq [in veric.juicy_mem]
store_valid [in veric.compcert_rmaps]
store_phi_elsewhere_eq [in veric.juicy_mem]
store_outside' [in veric.juicy_mem_lemmas]
store_init_data_list_access [in veric.initialize]
store_zeros_contents1 [in veric.initial_world]
store_zeros_access [in veric.initial_world]
store_zeros_max_access [in veric.initial_world]
store_init_data_list_lem [in veric.initial_world]
store_init_data_list_outside' [in veric.initial_world]
store_init_data_outside' [in veric.initial_world]
straightline_assign [in veric.semax_lemmas]
stratified_expr_safety [in veric.local]
stratified_expr_erasure [in veric.local]
StratModel.ff_res [in veric.rmaps]
StratModel.pre_rmap_sa_valid_join [in veric.rmaps]
StratModel.pre_rmap_sa_valid_core [in veric.rmaps]
StratModel.same_valid [in veric.rmaps]
StratModel.valid'_res_map2 [in veric.rmaps]
StratModel.valid'_res_map [in veric.rmaps]
strict_bool_val_sub [in veric.semax_loop]
strip_skip_app_cons [in veric.semax_lemmas]
strip_strip [in veric.semax_lemmas]
strip_skip_app [in veric.semax_lemmas]
strip_step [in veric.semax_lemmas]
strip_skip'_loop2_CC [in veric.Clight_sim]
strip_skip'_call_CC [in veric.Clight_sim]
strip_skip'_loop1_CC [in veric.Clight_sim]
strip_skip'_call [in veric.Clight_sim]
strip_skip'_loop1 [in veric.Clight_sim]
strip_call' [in veric.Clight_sim]
strip_call [in veric.Clight_sim]
strip_skip'_loop2 [in veric.Clight_sim]
strip_step [in veric.Clight_sim]
strip_skip'_not [in veric.Clight_sim]
strip_skip_not [in veric.Clight_sim]
subp_derives' [in veric.semax_lemmas]
subst_extens [in veric.seplog]
subst_extens [in veric.SeparationLogic]
T
tc_exprlist_sub [in veric.assert_lemmas]tc_temp_id_load_sub [in veric.assert_lemmas]
tc_temp_id_sub [in veric.assert_lemmas]
tc_lvalue_sub [in veric.assert_lemmas]
tc_expr_sub [in veric.assert_lemmas]
tc_expr_lvalue_sub [in veric.assert_lemmas]
tc_andp_sound [in veric.expr]
tc_exprlist_length [in veric.expr_lemmas]
tc_lvalue_nonvol [in veric.expr_lemmas]
tc_binaryop_nomem [in veric.expr_lemmas]
tc_andp_TT1 [in veric.binop_lemmas]
tc_andp_TT2 [in veric.binop_lemmas]
tc_ge_denote_initial [in veric.semax_prog]
temp_types_same_type' [in veric.expr_lemmas]
temp_types_update_dist [in veric.expr_lemmas]
temp_types_same_type [in veric.expr_lemmas]
top_pfullshare [in veric.juicy_mem]
True_and [in veric.expr]
True_or [in veric.binop_lemmas]
tycontext_sub_trans [in veric.semax_lemmas]
tycontext_sub_update_l [in veric.semax_lemmas]
tycontext_sub_update_c [in veric.semax_lemmas]
tycontext_eqv_symm [in veric.expr]
tycontext_sub_join [in veric.expr_lemmas]
tycontext_sub_refl [in veric.expr_lemmas]
tycontext_evolve_join_labeled [in veric.semax_loop]
tycontext_evolve_update_tycon [in veric.semax_loop]
tycontext_evolve_join [in veric.semax_loop]
tycontext_evolve_refl [in veric.semax_loop]
tycontext_evolve_trans [in veric.environ_lemmas]
typecheck_tid_ptr_compare_sub [in veric.semax_lemmas]
typecheck_environ_sub [in veric.semax_lemmas]
typecheck_tid_ptr_compare_sub [in veric.expr_lemmas]
typecheck_val_eval_cast [in veric.expr_lemmas]
typecheck_bool_val [in veric.expr_lemmas]
typecheck_environ_update [in veric.expr_lemmas]
typecheck_environ_update_ge [in veric.expr_lemmas]
typecheck_environ_update_ve [in veric.expr_lemmas]
typecheck_ls_update_te [in veric.expr_lemmas]
typecheck_environ_update_te [in veric.expr_lemmas]
typecheck_binop_sound2 [in veric.expr_lemmas]
typecheck_force_Some [in veric.expr_lemmas]
typecheck_lvalue_sound [in veric.expr_lemmas]
typecheck_expr_sound [in veric.expr_lemmas]
typecheck_both_sound [in veric.expr_lemmas]
typecheck_deref_sound [in veric.expr_lemmas]
typecheck_temp_sound [in veric.expr_lemmas]
typecheck_cast_sound [in veric.expr_lemmas]
typecheck_unop_sound [in veric.expr_lemmas]
typecheck_expr_sound_Evar [in veric.expr_lemmas]
typecheck_lvalue_sound_Efield [in veric.expr_lemmas]
typecheck_expr_sound_Efield [in veric.expr_lemmas]
typecheck_lvalue_Evar [in veric.expr_lemmas]
typecheck_binop_sound [in veric.binop_lemmas]
typecheck_sem_mod_sound [in veric.binop_lemmas]
typecheck_sem_div_sound [in veric.binop_lemmas]
typecheck_val_cmp_eqne_pi [in veric.binop_lemmas]
typecheck_val_cmp_eqne_ip [in veric.binop_lemmas]
typecheck_val_sem_cmp [in veric.binop_lemmas]
typecheck_val_void [in veric.binop_lemmas]
typecheck_environ_put_te' [in veric.environ_lemmas]
typecheck_environ_put_te [in veric.environ_lemmas]
typecheck_val_ptr_lemma [in veric.environ_lemmas]
typecheck_environ_join2 [in veric.environ_lemmas]
typecheck_environ_join1 [in veric.environ_lemmas]
type_eq_true [in veric.expr_lemmas]
type_eq_true [in veric.environ_lemmas]
U
unage_umapsto [in veric.semax_lemmas]unage_readable [in veric.juicy_mem]
unage_writable [in veric.juicy_mem]
unage_juicy_mem [in veric.juicy_mem]
unary_operation_val_valid [in veric.Clight_coop]
universal_imp_unfold [in veric.semax_lemmas]
unlater_writable [in veric.semax_call]
update_tycontext_eqv [in veric.semax_lemmas]
update_tycon_sub [in veric.expr_lemmas]
update_le_same_ge [in veric.expr_lemmas]
update_tycon_same_ge [in veric.expr_lemmas]
update_le_eqv_ge [in veric.expr_lemmas]
update_tycon_eqv_ge [in veric.expr_lemmas]
update_le_same_ve [in veric.expr_lemmas]
update_tycon_same_ve [in veric.expr_lemmas]
update_le_eqv_ret [in veric.expr_lemmas]
update_tycon_eqv_ret [in veric.expr_lemmas]
update_le_eqv_ve [in veric.expr_lemmas]
update_tycon_eqv_ve [in veric.expr_lemmas]
update_labeled_te_same [in veric.expr_lemmas]
update_tycon_te_same [in veric.expr_lemmas]
V
valid_access_None [in veric.juicy_mem_lemmas]VALspec_range_VALspec [in veric.res_predicates]
VALspec_range_split2 [in veric.res_predicates]
VALspec_range_0 [in veric.res_predicates]
VALspec_range_precise [in veric.res_predicates]
VALspec_range_bytes_writable [in veric.res_predicates]
VALspec_range_bytes_readable [in veric.res_predicates]
VALspec_range_splittable [in veric.res_predicates]
VALspec_readable [in veric.res_predicates]
VALspec_splittable [in veric.res_predicates]
VALspec_parametric [in veric.res_predicates]
VALspec_range_e [in veric.initial_world]
VALspec1 [in veric.res_predicates]
VAL_valid [in veric.compcert_rmaps]
VAL_inj [in veric.compcert_rmaps]
VAL_valid [in veric.juicy_mem]
var_types_join_labeled [in veric.expr_lemmas]
var_types_update_tycon [in veric.expr_lemmas]
var_types_update_dist [in veric.expr_lemmas]
VU_wellformed [in veric.local]
W
whole_program_sequential_safety [in veric.SequentialClight]writable_dec [in veric.compcert_rmaps]
writable_e [in veric.compcert_rmaps]
writable_readable [in veric.compcert_rmaps]
writable_join [in veric.compcert_rmaps]
writable_inv [in veric.juicy_mem]
writable_join_sub [in veric.juicy_mem]
writable_share_right [in veric.seplog]
writable_writable_after_alloc' [in veric.juicy_mem_lemmas]
writable_perm [in veric.juicy_mem_lemmas]
writable_blocks_rev [in veric.initialize]
writable_blocks_app [in veric.initial_world]
Y
yesat_join_sub [in veric.res_predicates]yesat_join [in veric.res_predicates]
yesat_raw_join [in veric.res_predicates]
yesat_join_diff [in veric.res_predicates]
yesat_eq [in veric.res_predicates]
yesat_eq_aux [in veric.res_predicates]
yesat_raw_eq [in veric.res_predicates]
yesat_raw_eq_aux [in veric.res_predicates]
Z
zero_ext_inj [in veric.initialize]Zlength_map [in veric.initial_world]
Zlength_rev [in veric.initial_world]
Zlength_app [in veric.initial_world]
Zle_bool_rev [in veric.expr_lemmas]
Zmax_of_nat [in veric.initialize]
Zmax_Z_of_nat [in veric.initialize]
Zminus_lem [in veric.juicy_mem_lemmas]
Z_of_nat_ge_O [in veric.seplog]
Section Index
E
ErasureCorollaries [in veric.local]ExpressionErasure [in veric.local]
Expressions [in veric.local]
extensions [in veric.semax_lemmas]
extensions [in veric.semax_call]
extensions [in veric.semax_loop]
extensions [in veric.semax_straight]
F
free [in veric.juicy_mem]G
GenericSemanticsElaboration [in veric.local]I
inflate [in veric.juicy_mem]initial_mem [in veric.juicy_mem]
M
Map.map [in veric.expr]S
selectors [in veric.juicy_mem]SemaxContext [in veric.semax_lemmas]
semax_prog [in veric.semax_prog]
SepErasureCorollaries [in veric.local]
store [in veric.juicy_mem]
storebytes [in veric.juicy_mem]
U
UnpackStratifiedSemantics [in veric.local]UnpackStratifiedSemanticsWithSeparation [in veric.local]
Constructor Index
A
AbsPrimcom_free [in veric.juicy_mem_ops]AbsPrimcom_alloc [in veric.juicy_mem_ops]
AbsPrimcom_store [in veric.juicy_mem_ops]
arg_type [in veric.expr]
B
BAdd [in veric.local]C
CC_core_Returnstate [in veric.Clight_sim]CC_core_Callstate [in veric.Clight_sim]
CC_core_State [in veric.Clight_sim]
ConcPrimcom_free [in veric.juicy_mem_ops]
ConcPrimcom_alloc [in veric.juicy_mem_ops]
ConcPrimcom_store [in veric.juicy_mem_ops]
CT [in veric.compcert_rmaps]
D
deref_byvalue [in veric.expr]E
EBinop [in veric.local]EK_return [in veric.expr]
EK_continue [in veric.expr]
EK_break [in veric.expr]
EK_normal [in veric.expr]
EPrim [in veric.local]
erase_KSeq [in veric.local]
erase_KStop [in veric.local]
erase_SWhile [in veric.local]
erase_SIfte [in veric.local]
erase_SSeq [in veric.local]
erase_SSkip [in veric.local]
erase_SPrimcom [in veric.local]
erase_EPrim [in veric.local]
erase_EBinop [in veric.local]
erase_EUnop [in veric.local]
erase_EVal [in veric.local]
EUnop [in veric.local]
EVal [in veric.local]
ExtCall [in veric.Clight_new]
F
FUN [in veric.compcert_rmaps]G
Global_var [in veric.expr]Global_func [in veric.expr]
I
immed_safe1 [in veric.local]immed_safe0 [in veric.local]
invalid_lvalue [in veric.expr]
invalid_struct_field [in veric.expr]
invalid_field_access [in veric.expr]
invalid_expression [in veric.expr]
invalid_cast_result [in veric.expr]
invalid_cast [in veric.expr]
K
Kcall [in veric.Clight_new]Kloop1 [in veric.Clight_new]
Kloop2 [in veric.Clight_new]
Kseq [in veric.Clight_new]
Kseq [in veric.local]
Kstop [in veric.local]
Kswitch [in veric.Clight_new]
L
LK [in veric.compcert_rmaps]M
match_states_ext [in veric.Clight_sim]match_states_seq [in veric.Clight_sim]
match_cont_call [in veric.Clight_sim]
match_cont_switch [in veric.Clight_sim]
match_cont_loop2 [in veric.Clight_sim]
match_cont_loop1 [in veric.Clight_sim]
match_cont_seq [in veric.Clight_sim]
match_cont_nil [in veric.Clight_sim]
mismatch_context_type [in veric.expr]
mkEnviron [in veric.expr]
mkGenericSem [in veric.local]
mkJuicyMem [in veric.juicy_mem]
mkLift [in veric.lift]
mkStratifiedSemantics [in veric.local]
mk_step' [in veric.Clight_sim]
mk_funspec [in veric.expr]
O
op_result_type [in veric.expr]P
pp_compare_size_0 [in veric.expr]R
Rmaps.NO [in veric.rmaps]RMAPS.NO [in veric.rmaps]
Rmaps.PURE [in veric.rmaps]
RMAPS.PURE [in veric.rmaps]
Rmaps.res_join_PURE [in veric.rmaps]
Rmaps.res_join_YES [in veric.rmaps]
Rmaps.res_join_NO3 [in veric.rmaps]
Rmaps.res_join_NO2 [in veric.rmaps]
Rmaps.res_join_NO1 [in veric.rmaps]
RMAPS.res_join_PURE [in veric.rmaps]
RMAPS.res_join_YES [in veric.rmaps]
RMAPS.res_join_NO3 [in veric.rmaps]
RMAPS.res_join_NO2 [in veric.rmaps]
RMAPS.res_join_NO1 [in veric.rmaps]
Rmaps.SomeP [in veric.rmaps]
RMAPS.SomeP [in veric.rmaps]
Rmaps.YES [in veric.rmaps]
RMAPS.YES [in veric.rmaps]
S
SemaxArg [in veric.semax]Sifte [in veric.local]
Sprimcom [in veric.local]
Sseq [in veric.local]
Sskip [in veric.local]
State [in veric.Clight_new]
stepN_S [in veric.local]
stepN_0 [in veric.local]
step_goto [in veric.Clight_new]
step_label [in veric.Clight_new]
step_switch [in veric.Clight_new]
step_return [in veric.Clight_new]
step_loop2 [in veric.Clight_new]
step_for [in veric.Clight_new]
step_ifthenelse [in veric.Clight_new]
step_break [in veric.Clight_new]
step_continue [in veric.Clight_new]
step_skip [in veric.Clight_new]
step_seq [in veric.Clight_new]
step_call_external [in veric.Clight_new]
step_call_internal [in veric.Clight_new]
step_set [in veric.Clight_new]
step_assign [in veric.Clight_new]
step_starN [in veric.local]
step_star0 [in veric.local]
step_Swhile [in veric.local]
step_Sifte_false [in veric.local]
step_Sifte_true [in veric.local]
step_Sseq [in veric.local]
step_Sskip [in veric.local]
step_Sprimcom [in veric.local]
StratModel.NO' [in veric.rmaps]
StratModel.PURE' [in veric.rmaps]
StratModel.res_join_PURE [in veric.rmaps]
StratModel.res_join_YES [in veric.rmaps]
StratModel.res_join_NO3 [in veric.rmaps]
StratModel.res_join_NO2 [in veric.rmaps]
StratModel.res_join_NO1 [in veric.rmaps]
StratModel.YES' [in veric.rmaps]
STRAT_MODEL.res_join_PURE [in veric.rmaps]
STRAT_MODEL.res_join_YES [in veric.rmaps]
STRAT_MODEL.res_join_NO3 [in veric.rmaps]
STRAT_MODEL.res_join_NO2 [in veric.rmaps]
STRAT_MODEL.res_join_NO1 [in veric.rmaps]
STRAT_MODEL.PURE' [in veric.rmaps]
STRAT_MODEL.YES' [in veric.rmaps]
STRAT_MODEL.NO' [in veric.rmaps]
Swhile [in veric.local]
T
tc_initialized [in veric.expr]tc_nodivover [in veric.expr]
tc_samebase [in veric.expr]
tc_Zge [in veric.expr]
tc_Zle [in veric.expr]
tc_ilt [in veric.expr]
tc_isptr [in veric.expr]
tc_iszero' [in veric.expr]
tc_nonzero [in veric.expr]
tc_orp' [in veric.expr]
tc_andp' [in veric.expr]
tc_TT [in veric.expr]
tc_noproof [in veric.expr]
tc_FF [in veric.expr]
U
UNeg [in veric.local]V
VAL [in veric.compcert_rmaps]var_not_in_tycontext [in veric.expr]
Vint [in veric.local]
volatile_load [in veric.expr]
Vptr [in veric.local]
Vundef [in veric.local]
VU_free [in veric.juicy_mem_ops]
VU_alloc [in veric.juicy_mem_ops]
VU_store [in veric.juicy_mem_ops]
W
wrong_signature [in veric.expr]Notation Index
R
_ @ _ [in veric.rmaps]_ @ _ [in veric.rmaps]
other
` _ [in veric.lift]`( _ ) [in veric.lift]
Inductive Index
A
AbsPrimcom [in veric.juicy_mem_ops]AbsPrimexpr [in veric.juicy_mem_ops]
B
binop [in veric.local]C
CC_core [in veric.Clight_sim]cl_step [in veric.Clight_new]
ConcPrimcom [in veric.juicy_mem_ops]
ConcPrimexpr [in veric.juicy_mem_ops]
cont' [in veric.Clight_new]
corestate [in veric.Clight_new]
ctl [in veric.local]
ctl_erase [in veric.local]
E
environ [in veric.expr]exitkind [in veric.expr]
expr [in veric.local]
expr_erase [in veric.local]
F
final_state [in veric.Clight_sim]funspec [in veric.expr]
G
GF [in veric.juicy_mem_ops]global_spec [in veric.expr]
H
HG [in veric.juicy_mem_ops]I
immed_safe [in veric.local]initial_state [in veric.Clight_sim]
J
juicy_mem [in veric.juicy_mem]K
kind [in veric.compcert_rmaps]M
match_states [in veric.Clight_sim]match_cont [in veric.Clight_sim]
R
RmapPrimexpr [in veric.juicy_mem_ops]Rmaps.preds [in veric.rmaps]
RMAPS.preds [in veric.rmaps]
Rmaps.resource [in veric.rmaps]
RMAPS.resource [in veric.rmaps]
Rmaps.res_join [in veric.rmaps]
RMAPS.res_join [in veric.rmaps]
S
step [in veric.local]stepN [in veric.local]
step_star [in veric.local]
step' [in veric.Clight_sim]
stmt [in veric.local]
stmt_erase [in veric.local]
StratModel.res [in veric.rmaps]
StratModel.res_join [in veric.rmaps]
STRAT_MODEL.res_join [in veric.rmaps]
STRAT_MODEL.res [in veric.rmaps]
T
tc_assert [in veric.expr]tc_error [in veric.expr]
U
unop [in veric.local]V
val [in veric.local]VU [in veric.juicy_mem_ops]
Definition Index
A
access_cohere [in veric.juicy_mem]access_at [in veric.juicy_mem]
address [in veric.local]
address_mapsto_zeros' [in veric.seplog]
address_mapsto_zeros [in veric.seplog]
address_mapsto' [in veric.res_predicates]
address_mapsto [in veric.res_predicates]
address_mapsto_old [in veric.res_predicates]
address_mapsto_zeros [in veric.SeparationLogic]
address_mapsto [in veric.SeparationLogic]
after_alloc [in veric.juicy_mem]
after_alloc' [in veric.juicy_mem]
age1_juicy_mem [in veric.juicy_mem]
alloc_juicy_variables [in veric.semax_call]
alloc_cohere [in veric.juicy_mem]
alloc_globals_rev [in veric.initial_world]
allowedValCast [in veric.expr]
all_assertions_computable [in veric.semax_lemmas]
all_VALs [in veric.juicy_mem]
all_initializers_aligned [in veric.initialize]
all_initializers_aligned [in veric.SeparationLogic]
always [in veric.expr]
any_environ [in veric.expr]
arglist [in veric.semax]
arglist [in veric.SeparationLogic]
assert [in veric.seplog]
assert_safe [in veric.semax]
assoc_list_get [in veric.semax]
B
believe [in veric.semax]believepred [in veric.semax]
believe_internal [in veric.semax]
believe_internal_ [in veric.semax]
believe_external [in veric.semax]
beyond_block [in veric.initialize]
binarithType [in veric.expr]
bind_ret [in veric.seplog]
bind_args [in veric.seplog]
bind_ret [in veric.SeparationLogic]
binopDenote [in veric.local]
blockslice_mpred_rmap [in veric.initialize]
blockslice_mpred [in veric.initialize]
blockslice_rmap [in veric.initialize]
blocks_match [in veric.semax_straight]
blocks_match [in veric.SeparationLogic]
boolT [in veric.res_predicates]
bool_of_valf [in veric.Clight_lemmas]
bool_type [in veric.expr]
bool_type [in veric.SeparationLogic]
break_cont [in veric.Clight_new]
bytes_readable [in veric.compcert_rmaps]
bytes_writable [in veric.compcert_rmaps]
C
call_cont [in veric.Clight_new]cast_expropt [in veric.semax_call]
cast_no_val_change [in veric.expr_lemmas]
cast_expropt [in veric.SeparationLogic]
CCstep [in veric.Clight_sim]
CC_core_sem [in veric.Clight_sim]
CC_safely_halted [in veric.Clight_sim]
CC_step [in veric.Clight_sim]
CC_initial_core [in veric.Clight_sim]
CC_after_external [in veric.Clight_sim]
CC_at_external [in veric.Clight_sim]
CC_state_to_CC_core [in veric.Clight_sim]
CC_core_to_CC_state [in veric.Clight_sim]
check_pl_long [in veric.expr]
check_pp_int [in veric.expr]
check_pl_long' [in veric.binop_lemmas]
check_pp_int' [in veric.binop_lemmas]
claims [in veric.semax]
classify_shift' [in veric.binop_lemmas]
classify_add' [in veric.binop_lemmas]
classify_cmp' [in veric.binop_lemmas]
classify_sub' [in veric.binop_lemmas]
CLIGHT_SEPARATION_LOGIC.semax_body_params_ok [in veric.SeparationLogic]
CLIGHT_SEPARATION_LOGIC.semax_prog [in veric.SeparationLogic]
CLIGHT_SEPARATION_LOGIC.semax_body [in veric.SeparationLogic]
closed_wrt_vars [in veric.seplog]
closed_wrt_modvars [in veric.semax]
closed_wrt_modvars [in veric.SeparationLogic]
closed_wrt_vars [in veric.SeparationLogic]
cl_core_sem [in veric.Clight_new]
cl_initial_core [in veric.Clight_new]
cl_init_mem [in veric.Clight_new]
cl_safely_halted [in veric.Clight_new]
cl_after_external [in veric.Clight_new]
cl_at_external [in veric.Clight_new]
cl_coop_sem [in veric.Clight_coop]
cl_coop_core_sem [in veric.Clight_coop]
cmp_ptr_no_mem [in veric.expr]
cmp_ptr_no_mem [in veric.SeparationLogic]
Cnot [in veric.semax_lemmas]
CompCert_AV.valid [in veric.compcert_rmaps]
CompCert_AV.kind [in veric.compcert_rmaps]
CompCert_AV.some_address [in veric.compcert_rmaps]
CompCert_AV.address [in veric.compcert_rmaps]
compute_list_norepet [in veric.expr]
config_det [in veric.local]
construct_rho [in veric.expr]
cont [in veric.Clight_new]
contents_cohere [in veric.juicy_mem]
contents_at [in veric.juicy_mem]
continue_cont [in veric.Clight_new]
control_as_safe [in veric.semax_lemmas]
coopstep [in veric.Clight_coop]
core_load' [in veric.res_predicates]
core_load [in veric.res_predicates]
CTat [in veric.res_predicates]
ct_count [in veric.res_predicates]
current_function [in veric.Clight_new]
D
Dbool [in veric.assert_lemmas]Delta1 [in veric.expr_lemmas]
Delta1 [in veric.semax_prog]
denote_tc_assert [in veric.expr]
denote_tc_initialized [in veric.expr]
denote_tc_nodivover [in veric.expr]
denote_tc_samebase [in veric.expr]
denote_tc_Zle [in veric.expr]
denote_tc_Zge [in veric.expr]
denote_tc_igt [in veric.expr]
denote_tc_nonzero [in veric.expr]
denote_tc_iszero [in veric.expr]
denote_tc_assert' [in veric.binop_lemmas]
deref_noload [in veric.expr]
deterministic_rel [in veric.local]
dryspec [in veric.NullExtension]
dryspec [in veric.SequentialClight]
E
ef_exit [in veric.Clight_sim]empty_genv [in veric.semax_lemmas]
empty_function [in veric.Clight_new]
empty_retainer [in veric.juicy_mem]
empty_environ [in veric.semax]
empty_tycontext [in veric.expr]
empty_environ [in veric.expr]
empty_environ [in veric.expr_lemmas]
empty_tenv [in veric.expr_lemmas]
empty_genv [in veric.expr_lemmas]
entry_tempenv [in veric.semax_prog]
env_set [in veric.expr]
eqb_fieldlist [in veric.expr]
eqb_typelist [in veric.expr]
eqb_type [in veric.expr]
eqb_signedness [in veric.expr]
eqb_intsize [in veric.expr]
eqb_ident [in veric.expr]
eqb_floatsize [in veric.expr]
eqb_attr [in veric.expr]
eq_mod_blockslice [in veric.initialize]
Espec [in veric.NullExtension]
eval_expropt [in veric.expr]
eval_exprlist [in veric.expr]
eval_lvalue [in veric.expr]
eval_expr [in veric.expr]
eval_cast [in veric.expr]
eval_cast_struct [in veric.expr]
eval_cast_l2bool [in veric.expr]
eval_cast_f2l [in veric.expr]
eval_cast_l2f [in veric.expr]
eval_cast_l2i [in veric.expr]
eval_cast_i2l [in veric.expr]
eval_cast_p2bool [in veric.expr]
eval_cast_f2bool [in veric.expr]
eval_cast_f2i [in veric.expr]
eval_cast_i2f [in veric.expr]
eval_cast_f2f [in veric.expr]
eval_cast_l2l [in veric.expr]
eval_cast_i2i [in veric.expr]
eval_cast_neutral [in veric.expr]
eval_var [in veric.expr]
eval_field [in veric.expr]
eval_binop [in veric.expr]
eval_unop [in veric.expr]
eval_id [in veric.expr]
existential_ret_assert [in veric.seplog]
existential_ret_assert [in veric.SeparationLogic]
exit_syscall_number [in veric.Clight_new]
exit_tycon [in veric.semax]
exit_cont [in veric.semax]
exit_tycon [in veric.SeparationLogic]
exprEval [in veric.local]
exprEval' [in veric.local]
expr_false [in veric.seplog]
expr_true [in veric.seplog]
expr_closed_wrt_vars [in veric.expr]
expr_wellformed [in veric.local]
extensible_jam [in veric.res_predicates]
extern_retainer [in veric.juicy_mem]
extern_retainer [in veric.SeparationLogic]
ext_spec_post' [in veric.semax]
ext_spec_pre' [in veric.semax]
F
filter_seq [in veric.semax_lemmas]filter_genv [in veric.expr]
find_label_ls [in veric.Clight_new]
find_label [in veric.Clight_new]
find_id [in veric.initial_world]
fixup_splitting [in veric.compcert_rmaps]
fmap_option [in veric.juicy_mem]
fn_funsig [in veric.semax]
fn_funsig [in veric.SeparationLogic]
force_ptr [in veric.expr]
force_val [in veric.expr]
force_valid_pointers [in veric.semax_straight]
frame_ret_assert [in veric.seplog]
frame_ret_assert [in veric.SeparationLogic]
freeable_blocks [in veric.semax_call]
free_list_juicy_mem [in veric.semax_call]
free_juicy_mem [in veric.juicy_mem]
funassert [in veric.seplog]
function_body_ret_assert [in veric.seplog]
function_body_ret_assert [in veric.SeparationLogic]
func_ptr [in veric.semax_call]
func_at' [in veric.seplog]
func_at [in veric.seplog]
func_tycontext' [in veric.semax]
func_tycontext [in veric.expr]
func_tycontext_v_denote [in veric.expr_lemmas]
func_tycontext_t_denote [in veric.expr_lemmas]
funsig [in veric.base]
funsig [in veric.SeparationLogic]
FUNspec [in veric.res_predicates]
funspecs [in veric.expr]
fun_assert [in veric.seplog]
fun_assert [in veric.res_predicates]
G
genviron [in veric.expr]get_result [in veric.seplog]
get_result1 [in veric.seplog]
get_var_type [in veric.expr]
get_result [in veric.SeparationLogic]
get_result1 [in veric.SeparationLogic]
ge_of [in veric.expr]
ghostp [in veric.ghost]
GHOSTspec [in veric.ghost]
globals_only [in veric.seplog]
globals_only [in veric.SeparationLogic]
globtype [in veric.expr]
globvars2pred [in veric.initialize]
globvars2pred [in veric.SeparationLogic]
globvar2pred [in veric.initialize]
globvar2pred [in veric.SeparationLogic]
glob_types [in veric.expr]
guard [in veric.semax]
guard_environ [in veric.semax]
G0 [in veric.semax_lemmas]
H
hackfun [in veric.initialize]HO_pred_eq [in veric.semax_prog]
I
idset [in veric.expr]idset0 [in veric.expr]
idset1 [in veric.expr]
id_in_list [in veric.expr]
id_for_lift [in veric.lift]
inflate_free [in veric.juicy_mem]
inflate_store [in veric.juicy_mem]
inflate_alloc [in veric.juicy_mem]
inflate_initial_mem [in veric.juicy_mem]
inflate_initial_mem' [in veric.juicy_mem]
initblocksize [in veric.initial_world]
initblocksize [in veric.SeparationLogic]
initialized [in veric.expr]
initializers_aligned [in veric.initialize]
initializers_aligned [in veric.SeparationLogic]
initializer_aligned [in veric.initialize]
initializer_aligned [in veric.SeparationLogic]
initial_mem [in veric.juicy_mem]
initial_rmap_ok [in veric.juicy_mem]
initial_jm [in veric.initial_world]
initial_core [in veric.initial_world]
initial_core' [in veric.initial_world]
init_jmem [in veric.juicy_extspec]
init_data_list2pred [in veric.initialize]
init_data2pred [in veric.initialize]
init_data_list2pred [in veric.SeparationLogic]
init_data_list_size [in veric.SeparationLogic]
init_data_size [in veric.SeparationLogic]
init_data2pred [in veric.SeparationLogic]
insert_idset [in veric.expr]
isBinOpResultType [in veric.expr]
isCastResultType [in veric.expr]
isExternalCallState [in veric.Clight_sim]
isptr [in veric.expr]
isSome [in veric.expr]
isUnOpResultType [in veric.expr]
isVAL [in veric.compcert_rmaps]
is_neutral_cast [in veric.expr]
is_numeric_type [in veric.expr]
is_pointer_type [in veric.expr]
is_float_type [in veric.expr]
is_long_type [in veric.expr]
is_int_type [in veric.expr]
is_scalar_type [in veric.expr]
is_comparison [in veric.expr]
is_ptr_type [in veric.expr_lemmas]
is_true [in veric.local]
is_comparison [in veric.SeparationLogic]
J
jam [in veric.res_predicates]jam_vacuous [in veric.res_predicates]
Join_pk [in veric.compcert_rmaps]
join_tycon_labeled [in veric.expr]
join_tycon [in veric.expr]
join_te [in veric.expr]
join_te' [in veric.expr]
jsafeN [in veric.semax]
jstep [in veric.juicy_extspec]
JuicyMemOps.juicy_mem_free [in veric.juicy_mem_ops]
JuicyMemOps.juicy_mem_alloc [in veric.juicy_mem_ops]
JuicyMemOps.juicy_mem_storebytes [in veric.juicy_mem_ops]
JuicyMemOps.juicy_mem_store [in veric.juicy_mem_ops]
juicy_mem_level [in veric.juicy_mem]
juicy_mem_op [in veric.juicy_extspec]
juicy_core_sem [in veric.juicy_extspec]
juicy_mem_core [in veric.juicy_mem_lemmas]
juicy_mem_pred [in veric.semax]
j_safely_halted [in veric.juicy_extspec]
K
kind_at [in veric.res_predicates]L
lift [in veric.lift]LiftEnviron [in veric.expr]
liftx [in veric.lift]
liftx' [in veric.lift]
lift0 [in veric.expr]
lift1 [in veric.expr]
lift2 [in veric.expr]
lift3 [in veric.expr]
lift4 [in veric.expr]
listprod [in veric.rmaps]
list_drop [in veric.semax_lemmas]
list2opt [in veric.semax]
LKspec [in veric.res_predicates]
LK_at [in veric.res_predicates]
load_store_init_data1 [in veric.initialize]
local [in veric.SeparationLogic]
lock_size [in veric.res_predicates]
loop1_ret_assert [in veric.seplog]
loop1_ret_assert [in veric.SeparationLogic]
loop2_ret_assert [in veric.seplog]
loop2_ret_assert [in veric.SeparationLogic]
lvalue_block [in veric.seplog]
lvalue_closed_wrt_vars [in veric.expr]
M
main_params [in veric.semax_prog]main_post [in veric.semax_prog]
main_pre [in veric.semax_prog]
main_post [in veric.SeparationLogic]
main_pre [in veric.SeparationLogic]
make_args [in veric.seplog]
make_GHOSTspec [in veric.ghost]
make_ext_rval [in veric.semax]
make_ext_args [in veric.semax]
make_tycontext [in veric.expr]
make_tycontext_g [in veric.expr]
make_tycontext_v [in veric.expr]
make_tycontext_t [in veric.expr]
make_venv [in veric.expr]
make_tenv [in veric.expr]
make_args' [in veric.SeparationLogic]
make_args [in veric.SeparationLogic]
mapsto [in veric.seplog]
mapsto [in veric.SeparationLogic]
mapsto_zeros [in veric.seplog]
mapsto_ [in veric.seplog]
mapsto_zeros [in veric.SeparationLogic]
mapsto_ [in veric.SeparationLogic]
Map.empty [in veric.expr]
Map.get [in veric.expr]
Map.remove [in veric.expr]
Map.set [in veric.expr]
Map.t [in veric.expr]
match_fsig [in veric.expr]
match_fsig_aux [in veric.expr]
match_fdecs [in veric.initial_world]
match_globvars [in veric.semax_prog]
match_globvars [in veric.SeparationLogic]
max_access_cohere [in veric.juicy_mem]
max_access_at [in veric.juicy_mem]
memory_block [in veric.seplog]
memory_block'_alt [in veric.seplog]
memory_block' [in veric.seplog]
memory_block [in veric.SeparationLogic]
memory_block' [in veric.SeparationLogic]
mk_pshare [in veric.compcert_rmaps]
modifiedvars [in veric.expr]
modifiedvars_ls [in veric.expr]
modifiedvars' [in veric.expr]
mod_after_alloc [in veric.juicy_mem]
mod_after_alloc' [in veric.juicy_mem]
mpred [in veric.expr]
MS [in veric.Clight_sim]
m_phi [in veric.juicy_mem]
m_dry [in veric.juicy_mem]
N
noat [in veric.res_predicates]nofunc_tycontext [in veric.expr]
normal_ret_assert [in veric.seplog]
normal_ret_assert [in veric.SeparationLogic]
not_dec [in veric.initialize]
no_dups [in veric.Clight_lemmas]
no_VALs [in veric.juicy_mem_lemmas]
nthbyte [in veric.res_predicates]
O
offset_val [in veric.expr]only_blocks [in veric.initialize]
opt2list [in veric.expr]
op_to_cmp [in veric.expr]
op_to_cmp [in veric.SeparationLogic]
overridePost [in veric.seplog]
overridePost [in veric.SeparationLogic]
P
packPQ [in veric.res_predicates]perm_of_res [in veric.juicy_mem]
perm_of_sh [in veric.juicy_mem]
pfunc [in veric.local]
prebreak_cont [in veric.semax_lemmas]
precontinue_cont [in veric.Clight_new]
prog_var_block [in veric.initialize]
prog_vars [in veric.initial_world]
prog_vars' [in veric.initial_world]
prog_funct [in veric.initial_world]
prog_funct' [in veric.initial_world]
prog_contains [in veric.semax_prog]
prog_vars [in veric.SeparationLogic]
prog_vars' [in veric.SeparationLogic]
prog_funct [in veric.SeparationLogic]
prog_funct' [in veric.SeparationLogic]
pureat [in veric.res_predicates]
pure_expr [in veric.local]
R
readable [in veric.compcert_rmaps]readonly2share [in veric.initialize]
readonly2share [in veric.SeparationLogic]
read_sh [in veric.juicy_mem]
resource_nodecay [in veric.juicy_mem]
resource_decay [in veric.juicy_mem]
res_retain' [in veric.juicy_mem]
ret_assert [in veric.seplog]
ret_temp [in veric.seplog]
ret_type [in veric.expr]
ret_temp [in veric.SeparationLogic]
ret_assert [in veric.SeparationLogic]
rguard [in veric.semax]
Rmaps_Lemmas.fixup_trace [in veric.rmaps_lemmas]
Rmaps_Lemmas.res_retain [in veric.rmaps_lemmas]
Rmaps_Lemmas.empty_rmap [in veric.rmaps_lemmas]
Rmaps_Lemmas.empty_rmap' [in veric.rmaps_lemmas]
Rmaps_Lemmas.no_preds [in veric.rmaps_lemmas]
Rmaps.approx [in veric.rmaps]
RMAPS.approx [in veric.rmaps]
Rmaps.NoneP [in veric.rmaps]
RMAPS.NoneP [in veric.rmaps]
Rmaps.preds_fmap [in veric.rmaps]
RMAPS.preds_fmap [in veric.rmaps]
Rmaps.pre_rmap2rmap' [in veric.rmaps]
Rmaps.p2p [in veric.rmaps]
Rmaps.p2p' [in veric.rmaps]
Rmaps.resource_at [in veric.rmaps]
Rmaps.resource_fmap [in veric.rmaps]
RMAPS.resource_at [in veric.rmaps]
RMAPS.resource_fmap [in veric.rmaps]
Rmaps.resource2res [in veric.rmaps]
Rmaps.res_option [in veric.rmaps]
RMAPS.res_option [in veric.rmaps]
Rmaps.res2resource [in veric.rmaps]
Rmaps.rmap [in veric.rmaps]
Rmaps.rmap_unage [in veric.rmaps]
Rmaps.rmap_age1 [in veric.rmaps]
Rmaps.rmap_level [in veric.rmaps]
Rmaps.rmap_fmap [in veric.rmaps]
RMAPS.rmap_unage [in veric.rmaps]
RMAPS.rmap_fmap [in veric.rmaps]
Rmaps.rmap' [in veric.rmaps]
RMAPS.rmap' [in veric.rmaps]
Rmaps.rmap'2pre_rmap [in veric.rmaps]
Rmaps.squash [in veric.rmaps]
Rmaps.TyFSA.Canc_F [in veric.rmaps]
Rmaps.TyFSA.Disj_F [in veric.rmaps]
Rmaps.TyFSA.paf_F [in veric.rmaps]
Rmaps.TyFSA.Perm_F [in veric.rmaps]
Rmaps.TyFSA.Sep_F [in veric.rmaps]
Rmaps.TyF.F [in veric.rmaps]
Rmaps.TyF.f_F [in veric.rmaps]
Rmaps.TyF.other [in veric.rmaps]
Rmaps.unsquash [in veric.rmaps]
Rmaps.valid [in veric.rmaps]
RMAPS.valid [in veric.rmaps]
r_update_tenv [in veric.semax]
S
safe [in veric.local]same_env [in veric.expr]
same_base_type [in veric.expr]
semax [in veric.semax]
semax_ [in veric.semax]
semax_external [in veric.semax]
semax_prog [in veric.semax_prog]
semax_func [in veric.semax_prog]
semax_body [in veric.semax_prog]
semax_body_params_ok [in veric.semax_prog]
semax' [in veric.semax]
sepcon_list [in veric.seplog]
share_of [in veric.compcert_rmaps]
share_oblivious [in veric.res_predicates]
SimpleAdrVal.address [in veric.rmaps]
SimpleAdrVal.kind [in veric.rmaps]
SimpleAdrVal.some_address [in veric.rmaps]
SimpleAdrVal.valid [in veric.rmaps]
slice_rmap [in veric.slice]
slice_resource [in veric.slice]
some_pt_type [in veric.expr_lemmas]
SoundSeparationLogic.CSL.extract_exists [in veric.SeparationLogicSoundness]
SoundSeparationLogic.CSL.func_ptr [in veric.SeparationLogicSoundness]
SoundSeparationLogic.CSL.juicy_ext_spec [in veric.SeparationLogicSoundness]
SoundSeparationLogic.CSL.semax [in veric.SeparationLogicSoundness]
SoundSeparationLogic.CSL.semax_external [in veric.SeparationLogicSoundness]
SoundSeparationLogic.CSL.semax_ptr_compare [in veric.SeparationLogicSoundness]
SoundSeparationLogic.CSL.semax_extract_prop [in veric.SeparationLogicSoundness]
SoundSeparationLogic.CSL.semax_extensionality_Delta [in veric.SeparationLogicSoundness]
SoundSeparationLogic.CSL.semax_pre_post [in veric.SeparationLogicSoundness]
SoundSeparationLogic.CSL.semax_frame [in veric.SeparationLogicSoundness]
SoundSeparationLogic.CSL.semax_skip [in veric.SeparationLogicSoundness]
SoundSeparationLogic.CSL.semax_load [in veric.SeparationLogicSoundness]
SoundSeparationLogic.CSL.semax_store [in veric.SeparationLogicSoundness]
SoundSeparationLogic.CSL.semax_return [in veric.SeparationLogicSoundness]
SoundSeparationLogic.CSL.semax_ifthenelse [in veric.SeparationLogicSoundness]
SoundSeparationLogic.CSL.semax_set_forward [in veric.SeparationLogicSoundness]
SoundSeparationLogic.CSL.semax_set [in veric.SeparationLogicSoundness]
SoundSeparationLogic.CSL.semax_call_ext [in veric.SeparationLogicSoundness]
SoundSeparationLogic.CSL.semax_fun_id [in veric.SeparationLogicSoundness]
SoundSeparationLogic.CSL.semax_call [in veric.SeparationLogicSoundness]
SoundSeparationLogic.CSL.semax_loop [in veric.SeparationLogicSoundness]
SoundSeparationLogic.CSL.semax_continue [in veric.SeparationLogicSoundness]
SoundSeparationLogic.CSL.semax_break [in veric.SeparationLogicSoundness]
SoundSeparationLogic.CSL.semax_seq [in veric.SeparationLogicSoundness]
SoundSeparationLogic.CSL.semax_func_cons_ext [in veric.SeparationLogicSoundness]
SoundSeparationLogic.CSL.semax_func_cons [in veric.SeparationLogicSoundness]
SoundSeparationLogic.CSL.semax_func_nil [in veric.SeparationLogicSoundness]
SoundSeparationLogic.CSL.semax_prog [in veric.SeparationLogicSoundness]
SoundSeparationLogic.CSL.semax_func [in veric.SeparationLogicSoundness]
SoundSeparationLogic.CSL.semax_body [in veric.SeparationLogicSoundness]
SoundSeparationLogic.CSL.semax_body_params_ok [in veric.SeparationLogicSoundness]
SoundSeparationLogic.CSL.seq_assoc [in veric.SeparationLogicSoundness]
SoundSeparationLogic.semax_prog_rule [in veric.SeparationLogicSoundness]
spec [in veric.res_predicates]
spec_parametric [in veric.res_predicates]
splittable [in veric.res_predicates]
split_shareval [in veric.slice]
split_rmap [in veric.slice]
split_resource [in veric.slice]
stackframe_of [in veric.seplog]
stackframe_of [in veric.SeparationLogic]
storebytes_juicy_mem [in veric.juicy_mem]
store_juicy_mem [in veric.juicy_mem]
straightline [in veric.semax_lemmas]
StratModel.Canc_pre_rmap [in veric.rmaps]
StratModel.Disj_pre_rmap [in veric.rmaps]
StratModel.f_pre_rmap [in veric.rmaps]
StratModel.f_res [in veric.rmaps]
StratModel.f_preds [in veric.rmaps]
StratModel.Perm_pre_rmap [in veric.rmaps]
StratModel.preds [in veric.rmaps]
StratModel.pre_rmap [in veric.rmaps]
StratModel.res_option [in veric.rmaps]
StratModel.res_fmap [in veric.rmaps]
StratModel.Sep_pre_rmap [in veric.rmaps]
StratModel.valid' [in veric.rmaps]
STRAT_MODEL.f_pre_rmap [in veric.rmaps]
STRAT_MODEL.pre_rmap [in veric.rmaps]
STRAT_MODEL.valid' [in veric.rmaps]
STRAT_MODEL.res_option [in veric.rmaps]
STRAT_MODEL.f_res [in veric.rmaps]
STRAT_MODEL.res_fmap [in veric.rmaps]
STRAT_MODEL.f_preds [in veric.rmaps]
STRAT_MODEL.preds [in veric.rmaps]
strict_bool_val [in veric.expr]
strip_skip [in veric.Clight_new]
strip_skip' [in veric.Clight_sim]
stupid_typeconv [in veric.binop_lemmas]
subst [in veric.seplog]
subst [in veric.SeparationLogic]
substopt [in veric.semax_call]
substopt [in veric.SeparationLogic]
sub_option [in veric.expr]
T
Tarrow [in veric.lift]tc_expropt [in veric.semax_call]
tc_temp_id_load [in veric.seplog]
tc_temp_id [in veric.seplog]
tc_value [in veric.seplog]
tc_lvalue [in veric.seplog]
tc_exprlist [in veric.seplog]
tc_expr [in veric.seplog]
tc_formals [in veric.seplog]
tc_always_true [in veric.expr]
tc_might_be_true [in veric.expr]
tc_bool [in veric.expr]
tc_orp [in veric.expr]
tc_andp [in veric.expr]
tc_iszero [in veric.expr]
tc_expropt [in veric.SeparationLogic]
tc_value [in veric.SeparationLogic]
tc_lvalue [in veric.SeparationLogic]
tc_exprlist [in veric.SeparationLogic]
tc_expr [in veric.SeparationLogic]
tc_temp_id_load [in veric.SeparationLogic]
tc_temp_id [in veric.SeparationLogic]
tc_environ [in veric.SeparationLogic]
tc_val [in veric.SeparationLogic]
temp_bindings [in veric.Clight_new]
temp_types [in veric.expr]
Tend [in veric.lift]
tenviron [in veric.expr]
test [in veric.expr]
te_of [in veric.expr]
te_one_denote [in veric.expr_lemmas]
Tint32s [in veric.Clight_new]
Tint32s [in veric.semax_prog]
true_expr [in veric.semax_lemmas]
true_expr [in veric.Clight_new]
Tsh [in veric.SeparationLogic]
TTat [in veric.res_predicates]
tycontext [in veric.expr]
tycontext_eqv [in veric.expr]
tycontext_sub [in veric.expr]
tycontext_evolve [in veric.environ_lemmas]
typecheck_tid_ptr_compare [in veric.semax_lemmas]
typecheck_store [in veric.expr]
typecheck_environ [in veric.expr]
typecheck_glob_environ [in veric.expr]
typecheck_var_environ [in veric.expr]
typecheck_temp_environ [in veric.expr]
typecheck_vals [in veric.expr]
typecheck_val [in veric.expr]
typecheck_exprlist [in veric.expr]
typecheck_pure_b [in veric.expr]
typecheck_b [in veric.expr]
typecheck_temp_id [in veric.expr]
typecheck_lvalue [in veric.expr]
typecheck_expr [in veric.expr]
typecheck_tid_ptr_compare [in veric.expr_lemmas]
typecheck_numeric_val [in veric.binop_lemmas]
typecheck_tid_ptr_compare [in veric.SeparationLogic]
typed_params [in veric.Clight_new]
typed_false [in veric.seplog]
typed_true [in veric.seplog]
typed_false [in veric.SeparationLogic]
typed_true [in veric.SeparationLogic]
typelist2list [in veric.expr]
type_of_funspec [in veric.expr]
type_of_funsig [in veric.SeparationLogic]
U
umapsto [in veric.seplog]umapsto [in veric.SeparationLogic]
unitT [in veric.res_predicates]
unopDenote [in veric.local]
unOp_result_type [in veric.expr]
update_tycon [in veric.expr]
upto_block [in veric.initialize]
V
valid_corestate [in veric.Clight_coop]valid_tempenv [in veric.Clight_coop]
valid_env [in veric.Clight_coop]
valshare [in veric.juicy_mem]
VALspec [in veric.res_predicates]
VALspec_range [in veric.res_predicates]
val_to_bool [in veric.Clight_lemmas]
val2address [in veric.res_predicates]
varspecs [in veric.expr]
var_block [in veric.seplog]
var_name [in veric.Clight_lemmas]
var_types [in veric.expr]
var_block [in veric.SeparationLogic]
venviron [in veric.expr]
ve_of [in veric.expr]
vret2v [in veric.Clight_new]
W
weak_mapsto_ [in veric.semax_straight]with_ge [in veric.seplog]
with_ge [in veric.SeparationLogic]
writable [in veric.compcert_rmaps]
writable_blocks [in veric.seplog]
writable_block [in veric.seplog]
writable_share [in veric.seplog]
writable_share [in veric.SeparationLogic]
Y
yesat [in veric.res_predicates]yesat_raw [in veric.res_predicates]
Z
zap_fn_return [in veric.semax]Module Index
A
Abs [in veric.juicy_mem_ops]ADR_VAL0 [in veric.rmaps]
ADR_VAL [in veric.rmaps]
C
CC [in veric.Clight_sim]CLIGHT_SEPARATION_LOGIC [in veric.SeparationLogic]
CompCert_AV [in veric.compcert_rmaps]
J
JuicyMemOps [in veric.juicy_mem_ops]JUICY_MEM_OPS [in veric.juicy_mem_ops]
M
Map [in veric.expr]R
R [in veric.compcert_rmaps]Rmaps [in veric.rmaps]
RMAPS [in veric.rmaps]
Rmaps_Lemmas.R [in veric.rmaps_lemmas]
Rmaps_Lemmas [in veric.rmaps_lemmas]
Rmaps.AV [in veric.rmaps]
RMAPS.AV [in veric.rmaps]
Rmaps.K [in veric.rmaps]
Rmaps.KL [in veric.rmaps]
Rmaps.KSa [in veric.rmaps]
Rmaps.SM [in veric.rmaps]
Rmaps.TyF [in veric.rmaps]
Rmaps.TyFSA [in veric.rmaps]
Rmaps.TyFSA.TF [in veric.rmaps]
RML [in veric.compcert_rmaps]
S
SEPARATION_LOGIC_SOUNDNESS.CSL [in veric.SeparationLogicSoundness]SEPARATION_LOGIC_SOUNDNESS [in veric.SeparationLogicSoundness]
SimpleAdrVal [in veric.rmaps]
SoundSeparationLogic [in veric.SeparationLogicSoundness]
SoundSeparationLogic.CSL [in veric.SeparationLogicSoundness]
StratModel [in veric.rmaps]
StratModel.AV [in veric.rmaps]
STRAT_MODEL.AV [in veric.rmaps]
STRAT_MODEL [in veric.rmaps]
Axiom Index
A
ADR_VAL0.kind [in veric.rmaps]ADR_VAL0.some_address [in veric.rmaps]
ADR_VAL0.address [in veric.rmaps]
ADR_VAL.valid_join [in veric.rmaps]
ADR_VAL.valid_empty [in veric.rmaps]
ADR_VAL.valid [in veric.rmaps]
ADR_VAL.kind [in veric.rmaps]
ADR_VAL.some_address [in veric.rmaps]
ADR_VAL.address [in veric.rmaps]
C
CLIGHT_SEPARATION_LOGIC.semax_extract_prop [in veric.SeparationLogic]CLIGHT_SEPARATION_LOGIC.semax_frame [in veric.SeparationLogic]
CLIGHT_SEPARATION_LOGIC.semax_pre_post [in veric.SeparationLogic]
CLIGHT_SEPARATION_LOGIC.semax_skip [in veric.SeparationLogic]
CLIGHT_SEPARATION_LOGIC.semax_store [in veric.SeparationLogic]
CLIGHT_SEPARATION_LOGIC.semax_load [in veric.SeparationLogic]
CLIGHT_SEPARATION_LOGIC.semax_ptr_compare [in veric.SeparationLogic]
CLIGHT_SEPARATION_LOGIC.semax_set_forward [in veric.SeparationLogic]
CLIGHT_SEPARATION_LOGIC.semax_set [in veric.SeparationLogic]
CLIGHT_SEPARATION_LOGIC.semax_call_ext [in veric.SeparationLogic]
CLIGHT_SEPARATION_LOGIC.semax_fun_id [in veric.SeparationLogic]
CLIGHT_SEPARATION_LOGIC.semax_return [in veric.SeparationLogic]
CLIGHT_SEPARATION_LOGIC.semax_call [in veric.SeparationLogic]
CLIGHT_SEPARATION_LOGIC.corable_func_ptr [in veric.SeparationLogic]
CLIGHT_SEPARATION_LOGIC.func_ptr [in veric.SeparationLogic]
CLIGHT_SEPARATION_LOGIC.semax_loop [in veric.SeparationLogic]
CLIGHT_SEPARATION_LOGIC.semax_continue [in veric.SeparationLogic]
CLIGHT_SEPARATION_LOGIC.semax_break [in veric.SeparationLogic]
CLIGHT_SEPARATION_LOGIC.seq_assoc [in veric.SeparationLogic]
CLIGHT_SEPARATION_LOGIC.semax_seq [in veric.SeparationLogic]
CLIGHT_SEPARATION_LOGIC.semax_ifthenelse [in veric.SeparationLogic]
CLIGHT_SEPARATION_LOGIC.semax_func_cons_ext [in veric.SeparationLogic]
CLIGHT_SEPARATION_LOGIC.semax_external_FF [in veric.SeparationLogic]
CLIGHT_SEPARATION_LOGIC.semax_external [in veric.SeparationLogic]
CLIGHT_SEPARATION_LOGIC.semax_func_cons [in veric.SeparationLogic]
CLIGHT_SEPARATION_LOGIC.semax_func_nil [in veric.SeparationLogic]
CLIGHT_SEPARATION_LOGIC.semax_func [in veric.SeparationLogic]
CLIGHT_SEPARATION_LOGIC.semax_extensionality_Delta [in veric.SeparationLogic]
CLIGHT_SEPARATION_LOGIC.extract_exists [in veric.SeparationLogic]
CLIGHT_SEPARATION_LOGIC.semax [in veric.SeparationLogic]
J
JUICY_MEM_OPS.juicy_mem_free_succeeds [in veric.juicy_mem_ops]JUICY_MEM_OPS.juicy_mem_alloc_succeeds [in veric.juicy_mem_ops]
JUICY_MEM_OPS.juicy_mem_store_succeeds [in veric.juicy_mem_ops]
JUICY_MEM_OPS.juicy_mem_free [in veric.juicy_mem_ops]
JUICY_MEM_OPS.juicy_mem_alloc [in veric.juicy_mem_ops]
JUICY_MEM_OPS.juicy_mem_storebytes [in veric.juicy_mem_ops]
JUICY_MEM_OPS.juicy_mem_store [in veric.juicy_mem_ops]
M
main_function [in veric.Clight_sim]mkAfterExtCore [in veric.Clight_sim]
myStatement [in veric.Clight_sim]
R
RMAPS.Age_rmap [in veric.rmaps]RMAPS.ag_rmap [in veric.rmaps]
RMAPS.Canc_resource [in veric.rmaps]
RMAPS.Canc_rmap [in veric.rmaps]
RMAPS.Disj_resource [in veric.rmaps]
RMAPS.Disj_rmap [in veric.rmaps]
RMAPS.join_unsquash [in veric.rmaps]
RMAPS.Join_rmap [in veric.rmaps]
RMAPS.Perm_resource [in veric.rmaps]
RMAPS.Perm_rmap [in veric.rmaps]
RMAPS.preds_fmap_comp [in veric.rmaps]
RMAPS.preds_fmap_id [in veric.rmaps]
RMAPS.resource_fmap_comp [in veric.rmaps]
RMAPS.resource_fmap_id [in veric.rmaps]
RMAPS.rmap [in veric.rmaps]
RMAPS.rmapj_valid_core [in veric.rmaps]
RMAPS.rmapj_valid_join [in veric.rmaps]
RMAPS.rmap_age1_eq [in veric.rmaps]
RMAPS.rmap_level_eq [in veric.rmaps]
RMAPS.rmap_fmap_comp [in veric.rmaps]
RMAPS.rmap_fmap_id [in veric.rmaps]
RMAPS.Sep_resource [in veric.rmaps]
RMAPS.Sep_rmap [in veric.rmaps]
RMAPS.squash [in veric.rmaps]
RMAPS.squash_unsquash [in veric.rmaps]
RMAPS.unsquash [in veric.rmaps]
RMAPS.unsquash_squash [in veric.rmaps]
RMAPS.valid_res_map [in veric.rmaps]
S
SEPARATION_LOGIC_SOUNDNESS.semax_prog_rule [in veric.SeparationLogicSoundness]STRAT_MODEL.Disj_pre_rmap [in veric.rmaps]
STRAT_MODEL.Canc_pre_rmap [in veric.rmaps]
STRAT_MODEL.Sep_pre_rmap [in veric.rmaps]
STRAT_MODEL.Perm_pre_rmap [in veric.rmaps]
STRAT_MODEL.valid'_res_map2 [in veric.rmaps]
STRAT_MODEL.valid'_res_map [in veric.rmaps]
STRAT_MODEL.paf_res [in veric.rmaps]
STRAT_MODEL.da_rj [in veric.rmaps]
STRAT_MODEL.ca_rj [in veric.rmaps]
STRAT_MODEL.sa_rj [in veric.rmaps]
STRAT_MODEL.pa_rj [in veric.rmaps]
STRAT_MODEL.ff_res [in veric.rmaps]
Variable Index
E
ExpressionErasure.F [in veric.local]ExpressionErasure.G [in veric.local]
ExpressionErasure.GF [in veric.local]
ExpressionErasure.primexpr_safety [in veric.local]
ExpressionErasure.primexpr_erasure [in veric.local]
ExpressionErasure.S' [in veric.local]
ExpressionErasure.W [in veric.local]
ExpressionErasure.world_erase [in veric.local]
Expressions.G [in veric.local]
Expressions.W [in veric.local]
F
free.b [in veric.juicy_mem]free.FREE [in veric.juicy_mem]
free.hi [in veric.juicy_mem]
free.jm [in veric.juicy_mem]
free.lo [in veric.juicy_mem]
free.m' [in veric.juicy_mem]
I
inflate.m [in veric.juicy_mem]inflate.phi [in veric.juicy_mem]
initial_mem.IOK [in veric.juicy_mem]
initial_mem.w [in veric.juicy_mem]
initial_mem.m [in veric.juicy_mem]
M
Map.map.B [in veric.expr]S
selectors.j [in veric.juicy_mem]storebytes.b [in veric.juicy_mem]
storebytes.bytes [in veric.juicy_mem]
storebytes.jm [in veric.juicy_mem]
storebytes.m' [in veric.juicy_mem]
storebytes.ofs [in veric.juicy_mem]
storebytes.STOREBYTES [in veric.juicy_mem]
store.b [in veric.juicy_mem]
store.ch [in veric.juicy_mem]
store.jm [in veric.juicy_mem]
store.m' [in veric.juicy_mem]
store.ofs [in veric.juicy_mem]
store.STORE [in veric.juicy_mem]
store.v [in veric.juicy_mem]
Library Index
A
assert_lemmasB
basebinop_lemmas
C
CC_transCC_implies_FW
Clight_sim
Clight_lemmas
Clight_coop
Clight_new
CminorgenproofSIM
Cminor_CompcertSemantics
compcert_rmaps
concurrency_extension
CSharpminor_CompcertSemantics
E
environ_lemmasEvents2
expr
expr_lemmas
G
ghostI
initializeinitial_world
J
juicy_fs_extensionjuicy_linking_extension
juicy_mem
juicy_mem_ops
juicy_mem_lemmas
juicy_extspec
L
liftlink_ext
loadpath
local
M
MemoryPushoutsN
NullExtensionR
res_predicatesrmaps
rmaps_lemmas
S
semaxsemax_lemmas
semax_call
semax_prog
semax_straight
semax_loop
SeparationLogic
SeparationLogicSoundness
seplog
seplog_extension
SequentialClight
slice
| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (2159 entries) |
| Instance Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (55 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (33 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (8 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (953 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (20 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (161 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (4 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (48 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (670 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (33 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (90 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (36 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (48 entries) |
This page has been generated by coqdoc