Commits · afp_devIsabelle_Clean_24 · Burkhart Wolff / Isabelle_C

Oct 14, 2024
- Sync with afp devel branch and Isabelle_09_Oct_2024 · 53e449d1
  Burkhart Wolff authored 5 months ago
  
  53e449d1
- dangling README. · e06575cf
  Burkhart Wolff authored 5 months ago
  
  e06575cf
Oct 13, 2024
- ... · 9e23320a
  Burkhart Wolff authored 5 months ago
  
  9e23320a
Oct 10, 2024
- merge. roughly funcioning again. pb with ROOTs in this branch · 4f8f5226
  Burkhart Wolff authored 5 months ago
  
  4f8f5226
- improved documentation. · 5c7fc698
  Burkhart Wolff authored 5 months ago
  
  5c7fc698
Oct 09, 2024
- ROOT in sync with the AFP - setup · 4a5c2e1d
  Burkhart Wolff authored 5 months ago
  
  4a5c2e1d
- some simpler proofs for more automatic symbexes · 6280450a
  Burkhart Wolff authored 5 months ago
  
  6280450a
- Bu's Symbolic execution rules for assertions · ea8ab81a
  Burkhart Wolff authored 5 months ago
  
  ea8ab81a
- Achims patch on recursive function return type · 65d8185b
  Burkhart Wolff authored 5 months ago
  
  65d8185b
Sep 27, 2024
- Minor corrections in the test suite. · 7653da1f
  Burkhart Wolff authored 6 months ago
  
  7653da1f
- final result of Lorenz Winkler · 82eef46e
  Burkhart Wolff authored 6 months ago
  
  82eef46e
- fix if · cc86cbe2
  Lorenz Winkler authored 6 months ago
  
  cc86cbe2
- fix unary operations (in C_Ast!) · 4883379c
  Lorenz Winkler authored 6 months ago
  
  4883379c
Sep 26, 2024
- now propperly support all crazy combinations of init-exprs mixed with simple declarations · f34824af
  Lorenz Winkler authored 6 months ago
  
  f34824af
- add init-expressions · cc99b0eb
  Lorenz Winkler authored 6 months ago
  
  cc99b0eb
- now propperly support assignments to types mapped to nat · d48a5e94
  Lorenz Winkler authored 6 months ago
  
  d48a5e94
- fix bug in previous bugfix (forgot functions) · dad2559f
  Lorenz Winkler authored 6 months ago
  
  dad2559f
- fix a bug where local vars would not be defined · 257e522e
  Lorenz Winkler authored 6 months ago
  
  ... if they occured as params in a previous function in the same transl unit
  257e522e
- add documentation · b4ab78a3
  Lorenz Winkler authored 6 months ago
  
  b4ab78a3
Sep 25, 2024
- add documentation · fb6e81d2
  Lorenz Winkler authored 6 months ago
  
  fb6e81d2
- rename translation hook file · 4e61b8ee
  Lorenz Winkler authored 6 months ago
  
  4e61b8ee
- minor refactoring · 416b3bf6
  Lorenz Winkler authored 6 months ago
  
  416b3bf6
- move translation to another file, so it can be imported into the documentation files · 44312719
  Lorenz Winkler authored 6 months ago
  
  44312719
- refactor the assignment translation · b445ccca
  Lorenz Winkler authored 6 months ago
  
  b445ccca
Sep 24, 2024
- begin overworking the assignment part --broken (arrays very much, other parts maybe aswell) · 8d302277
  Lorenz Winkler authored 6 months ago
  
  8d302277
- commenting in generator, updating reasme_dev for start config · 28c2cef3
  Burkhart Wolff authored 6 months ago
  
  28c2cef3
- remove debug messages · 4f931f98
  Lorenz Winkler authored 6 months ago
  
  4f931f98
- fix coder_exprstmt · 67c0b9a6
  Lorenz Winkler authored 6 months ago
  
  67c0b9a6
Sep 23, 2024
- remove automatic nat conversion and correctly infer type before calling clean... · 0e069a2a
  Lorenz Winkler authored 6 months ago
  
  remove automatic nat conversion and correctly infer type before calling clean interface for annotation terms
  0e069a2a
- hide parameters when reading annotation terms, so that free terms with... · fa79a574
  Lorenz Winkler authored 6 months ago
  
  hide parameters when reading annotation terms, so that free terms with parameters wouldnt get substituted
  fa79a574
Sep 20, 2024
- implement storing invariant and measure · 59f764b1
  Lorenz Winkler authored 6 months ago
  
  59f764b1
Sep 19, 2024
- add a small demo · 2fb82d3c
  Lorenz Winkler authored 6 months ago
  
  2fb82d3c
Sep 18, 2024
- add hook for c_expr antiquotation --broken-- · e429ab26
  Lorenz Winkler authored 6 months ago
  
  e429ab26
- implement mechanism to find invariants corresponding to loop · a838ff46
  Lorenz Winkler authored 6 months ago
  
  a838ff46
Sep 17, 2024
- begin implementing recursion. parseNodeContent is broken! · 9ec6f95f
  Lorenz Winkler authored 6 months ago
  
  9ec6f95f
- fix scoping issue where local vars would override global vars · dad07389
  Lorenz Winkler authored 6 months ago
  
  dad07389
Sep 16, 2024
- implement storing of invariants, pre- and postconditions · 23807c0e
  Lorenz Winkler authored 6 months ago
  
  23807c0e
Sep 13, 2024
- adapt parseNodeContent for handling multi-dimensional arrays (list list T) · bc8eac94
  Lorenz Winkler authored 6 months ago
  
  bc8eac94
- fix ordering of function declarations · 7dd42602
  Lorenz Winkler authored 6 months ago
  
  7dd42602
- enable functions without parameters in clean · d651c5ee
  Lorenz Winkler authored 6 months ago
  
  d651c5ee