AutoCorres2: NEWS and flexible array members
Showing
- thys/AutoCorres2/NEWS 17 additions, 2 deletionsthys/AutoCorres2/NEWS
- thys/AutoCorres2/autocorres.ML 1 addition, 1 deletionthys/AutoCorres2/autocorres.ML
- thys/AutoCorres2/c-parser/Absyn-CType.ML 7 additions, 1 deletionthys/AutoCorres2/c-parser/Absyn-CType.ML
- thys/AutoCorres2/c-parser/Absyn-Expr.ML 26 additions, 0 deletionsthys/AutoCorres2/c-parser/Absyn-Expr.ML
- thys/AutoCorres2/c-parser/CTranslationInfrastructure.thy 0 additions, 1 deletionthys/AutoCorres2/c-parser/CTranslationInfrastructure.thy
- thys/AutoCorres2/c-parser/RegionExtras.ML 3 additions, 1 deletionthys/AutoCorres2/c-parser/RegionExtras.ML
- thys/AutoCorres2/c-parser/UMM_Proofs.ML 6 additions, 3 deletionsthys/AutoCorres2/c-parser/UMM_Proofs.ML
- thys/AutoCorres2/c-parser/calculate_state.ML 28 additions, 18 deletionsthys/AutoCorres2/c-parser/calculate_state.ML
- thys/AutoCorres2/c-parser/ex.c 1 addition, 1 deletionthys/AutoCorres2/c-parser/ex.c
- thys/AutoCorres2/c-parser/expression_translation.ML 28 additions, 4 deletionsthys/AutoCorres2/c-parser/expression_translation.ML
- thys/AutoCorres2/c-parser/program_analysis.ML 17 additions, 2 deletionsthys/AutoCorres2/c-parser/program_analysis.ML
- thys/AutoCorres2/heap_lift_base.ML 4 additions, 2 deletionsthys/AutoCorres2/heap_lift_base.ML
- thys/AutoCorres2/tests/AutoCorresTest.thy 1 addition, 0 deletionsthys/AutoCorres2/tests/AutoCorresTest.thy
- thys/AutoCorres2/tests/proof-tests/flexible_array_member.c 21 additions, 0 deletionsthys/AutoCorres2/tests/proof-tests/flexible_array_member.c
- thys/AutoCorres2/tests/proof-tests/flexible_array_member.thy 29 additions, 0 deletionsthys/AutoCorres2/tests/proof-tests/flexible_array_member.thy
Loading
Please register or sign in to comment