Abstract
AutoCorres2 is a tool to facilitate the verification of C programs within Isabelle.
It is a fork of AutoCorres.
License
Topics
- Computer science/Programming languages/Logics
- Computer science/Semantics and reasoning
- Tools
- Computer science/Programming languages/Language definitions
Session AutoCorres2
- Introduction_AutoCorres2
- More_Lib
- MkTermAntiquote
- MkTermAntiquote_Tests
- TermPatternAntiquote
- TermPatternAntiquote_Tests
- Print_Annotated
- ML_Fun_Cache
- AutoCorres_Utils
- Match_Cterm
- ML_Record_Antiquotation
- Misc_Antiquotation
- Tuple_Tools
- Subgoal_Methods
- Synthesize
- Rule_By_Method
- Option_Scanner
- Named_Rules
- Subgoals
- Tagging
- Basic_Runs_To_VCG
- Runs_To_VCG
- Eisbach_Methods
- Less_Monad_Syntax
- Reader_Monad
- Option_MonadND
- Apply_Trace
- Apply_Trace_Cmd
- Mutual_CCPO_Recursion
- Target_Architecture
- Word_Lemmas_Internal
- Word_Lemmas_32_Internal
- Word_Lemmas_64_Internal
- Distinct_Prop
- WordSetup
- Addr_Type_ARM
- Addr_Type_ARM64
- Addr_Type_ARM_HYP
- Addr_Type_RISCV64
- Addr_Type_X64
- Addr_Type
- CTypesBase
- CTypesDefs
- CTypes
- Vanilla32_Preliminaries
- Word_Mem_Encoding_ARM
- Word_Mem_Encoding_ARM64
- Word_Mem_Encoding_ARM_HYP
- Word_Mem_Encoding_RISCV64
- Word_Mem_Encoding_X64
- Word_Mem_Encoding
- Vanilla32
- Arrays
- Padding
- Lens
- CompoundCTypes
- ArraysMemInstance
- ArchArraysMemInstance
- HeapRawState
- MapExtra
- MapExtraTrans
- TypHeap
- Separation_UMM
- SepCode
- SepInv
- SepTactic
- SepFrame
- StructSupport
- ArrayAssertion
- ML_Infer_Instantiate
- CProof
- Padding_Equivalence
- CLanguage
- UMM
- PackedTypes
- PrettyProgs
- StaticFun
- IndirectCalls
- ModifiesProofs
- CLocals
- CTranslationSetup
- Array_Selectors
- CTranslation
- TypHeapLib
- LemmaBucket_C
- Cong_Tactic
- Spec_Monad
- Reaches
- Simp_Trace
- AutoCorres_Base
- SimplBucket
- CCorresE
- L1Defs
- L1Peephole
- SimplConv
- CorresXF
- L1Valid
- L2Defs
- LocalVarExtract
- AutoCorresSimpset
- ExceptionRewrite
- L2ExceptionRewrite
- L2Peephole
- TypHeapSimple
- Stack_Typing
- In_Out_Parameters
- Split_Heap
- AbstractArrays
- HeapLift
- NatBitwise
- WordAbstract
- WordPolish
- Refines_Spec
- TypeStrengthen
- Polish
- Runs_To_VCG_StackPointer
- AutoCorres
- Chapter1_MinMax
- Chapter2_HoareHeap
- Chapter3_HoareHeap
- AutoCorresInfrastructure
- pointers_to_locals
- In_Out_Parameters_Ex
- fnptr
- union_ac
- open_struct
- AutoCorres_Documentation
- CTranslationInfrastructure
Session AutoCorres2_Main
Session AutoCorres2_Test
- aligned
- analsignedoverflow
- 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
- 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
- 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
- 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
- Asm_Labels
- CustomWordAbs
- SignedWordAbsHeap
- Test_Spec_Translation
- WhileLoopVarsPreserved
- WordAbsFnCall
- array_indirect_update
- badnames
- buffer
- globals
- global_array_update
- Global_Structs
- Guard_Simp
- heap_lift_force_prevent
- In_Out_Parameters_Slow
- int128
- nested_array
- 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
- skip_heap_abs
- skip_in_out_parameters
- 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_skip_heap_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