menu

Return to entry

aligned
arithmetic_right_shift
asm_stmt
array_of_ptr
arrays
attributes
basic_char
bigstruct
breakcontinue
bug20060707
bug_mvt20110302
bugzilla180
bugzilla181
bugzilla182
builtins
charlit
codetests
dc_20081211
dc_embbug
decl_only
dont_translate
dupthms
empty
emptystmt
extern_builtin
extern_dups
exit
MachineWords
factorial
fncall
fnptr0
fnptr_enum
gcc_attribs
goto0
ghoststate1
ghoststate2
globals_fn
globals_in_record
globinits
guard_while
guardedsignedoverflow
hexliteral
init_static
initialised_decls
inner_fncalls
int_promotion
isa2014
jiraver039
jiraver092
jiraver105
jiraver110
jiraver150
jiraver224
jiraver253
jiraver254
jiraver307
jiraver310
jiraver313
jiraver315
jiraver332
jiraver336
jiraver337
jiraver344
jiraver345
jiraver384
jiraver400
jiraver422
jiraver426
jiraver429
jiraver432
jiraver434
jiraver439
jiraver440
jiraver443
jiraver443a
jiraver456
jiraver464
jiraver473
jiraver54
jiraver550
jiraver808
jiraver881
jiraver1241
kmalloc0
list_reverse
list_reverse_norm
locvarfncall
longlong
memcopy
modifies_assumptions
modifies_pointer_to_local
modifies_speed
multi_deref
multidim_arrays
mutrec_modifies
nested
padding_free
parse_addr
parse_c99block
parse_complit
parse_dowhile
parse_enum
parse_fncall
parse_forloop
parse_include
parse_protos
parse_retfncall
parse_sizeof
parse_someops
parse_struct
parse_struct_array
parse_switch
parse_typecast
parse_voidfn
Plus0
phantom_mstate
pointers_to_locals0
populate_globals
postfixOps
protoparamshadow
ptr_auxupd
ptr_diff
ptr_modifies
really_simple
relspec
retprefix
selection_sort
shortcircuit
sideeffects_reject
signed_div
signedoverflow
simple_annotated_fn
simple_constexpr_sizeof
simple_fn
sizeof_typedef
Skip_Asm
spec_annotated_fn
spec_annotated_voidfn
static
struct_init0
struct_names
swap0
switch_unsigned_signed
test_locality
test_shifts
ummbug20100217
union
untouched_globals
variable_munge
varinit
void_ptr_init
volatile_asm
CParserTest
basic
basic_recursion
big_bit_ops
bodyless_function
explosion
heap_infer
heap_lift_array
l2_opt_invariant
loop_test
loop_test2
mutual_recursion
mutual_recursion2
nested_break_cont
read_global_array
signed_ptr_ptr
simple1
single_auxupd
struct1
struct_init
unliftable_call
voidptrptr
while_loop_no_vars
word_abs_exn
write_to_global_array
anonymous_nested_struct
Asm_Labels
CustomWordAbs
SignedWordAbsHeap
Test_Spec_Translation
WhileLoopVarsPreserved
WordAbsFnCall
array_indirect_update
badnames
bitint
buffer
flexible_array_member
function_decay
function_pointer_array_decay
globals
global_array_update
Global_Structs
Guard_Simp
heap_lift_force_prevent
In_Out_Parameters_Slow
io_for_break
io_memcmp
io_global_array
int128
init_globals
nested_array
Nested_Field_Update
nested_struct
open_nested
open_nested_array
option_exploration
partial_open_nested
pointers_to_locals_skip_hl
pointers_to_locals_skip_hl_wa
prototyped_functions
side_effect_assignment
skip_heap_abs
skip_in_out_parameters
statement_expression
struct
struct2
struct3
ternary_conditional_operator
try
word_abs_cases
word_abs_options
struct_consecutive_init
profile_conversion
mmio
mmio_assume
EvaluationOrder
unfold_bind_options
bit_shuffle
fnptr_enum0
fnptr_groups
fnptr_io
fnptr_nested
fnptr_no_heap_abs
fnptr_proto
fnptr_skip_heap_abs
fnptr_skip_heap_abs_skip_word_abs
fnptr_large_array
underscore_funs
AC_Rename
Alloc_Ex
DataStructures
BinarySearch
CList
CompoundCTypesEx
CompoundCTypesExNew
ConditionGuard
Exception_Rewriting
FactorialTest
FibProof
final_autocorres
FunctionInfoDemo
goto
HeapWrap
Incremental
IsPrime_Ex
Kmalloc
ListRev
Match_Cterm_Ex
Memcpy
Memset
MultByAdd
Plus_Ex
Quicksort_Ex
SchorrWaite_Ex
Simple
Str2Long
Suzuki
Swap_Ex
TraceDemo
WordAbs
type_strengthen_tricks
Mutual_Fixed_Points
AutoCorresTest

AutoCorres2_Test.WhileLoopVarsPreserved

HTML Presentation