Skip to content
Snippets Groups Projects

Repository graph

You can move around the graph by using the arrow keys.
Select Git revision
  • C default protected
  • C_2019
  • C_2020
  • C_2021
  • C_2021-1
  • C_2022
  • C_AFP
  • C_AFP_draft
  • C_AFP_readme
  • C_devel_AFP
  • C_devel_AFP_readme
  • Clean_AFP
  • Isa2024
  • LorenzWinkler
  • LorenzWinkler2
  • afp_devIsabelle_C_24
  • afp_devIsabelle_Clean_24
  • main
18 results
Created with Raphaël 2.2.014Oct1310927Sep2625242320191817161312111096543229Aug286Sep429Aug2825242330Jun2928265218May178Feb26Jan242221194Nov26Oct251220Sep17Aug54328Jul27241513121186130Jun27May262519186Mar518Feb17932111Jan228Dec27262523222196329Nov1716151210331Oct5130Sep282225Aug18161412631Jul242216151413128529Jun272625217320May18171321Apr13430Mar2423191812115223Feb191817129Jan2825242220191813823Dec199230Nov26242317169228Oct27Sync with afp devel branch and Isabelle_09_Oct_2024afp_devIsabelle…afp_devIsabelle_Clean_24dangling README.Isa2024Isa2024tracking afp Isabelle_C Frontend developmentafp_devIsabelle…afp_devIsabelle_C_24...merge. roughly funcioning again. pb with ROOTs in this branchimproved documentation.LorenzWinklerLorenzWinklerROOT in sync with the AFP - setupsome simpler proofs for more automatic symbexesBu's Symbolic execution rules for assertionsAchims patch on recursive function return typeMinor corrections in the test suite.corrected callC_2021-1C_2021-1final result of Lorenz Winklerfix ifLorenzWinkler2LorenzWinkler2fix unary operations (in C_Ast!)now propperly support all crazy combinations of init-exprs mixed with simple declarationsadd init-expressionsnow propperly support assignments to types mapped to natfix bug in previous bugfix (forgot functions)fix a bug where local vars would not be definedadd documentationadd documentationrename translation hook fileminor refactoringmove translation to another file, so it can be imported into the documentation filesrefactor the assignment translationbegin overworking the assignment part --broken (arrays very much, other parts maybe aswell)commenting in generator, updating reasme_dev for start configremove debug messagesfix coder_exprstmtremove automatic nat conversion and correctly infer type before calling clean interface for annotation termshide parameters when reading annotation terms, so that free terms with parameters wouldnt get substitutedimplement storing invariant and measureadd a small demoadd hook for c_expr antiquotation --broken--implement mechanism to find invariants corresponding to loopbegin implementing recursion. parseNodeContent is broken!fix scoping issue where local vars would override global varsimplement storing of invariants, pre- and postconditionsadapt parseNodeContent for handling multi-dimensional arrays (list list T)