Commits · d535ef4bc8b6e71fe81c75856fbe4a3b58584793 · Iris / RefinedC

12 Feb, 2021 9 commits
- Progress on the verification of [early_alloc.c]. · d535ef4b
  Rodolphe Lepigre authored Feb 11, 2021
  
  d535ef4b
- maybe fix CI · ab8e25f5
  Michael Sammler authored Feb 12, 2021
  
  ab8e25f5
- start with GUIDE · c4ece0aa
  Michael Sammler authored Feb 12, 2021
  
  c4ece0aa
- page_alloc · ef26b9b0
  Michael Sammler authored Feb 04, 2021
  
  ef26b9b0
- no timing for ci branches · 7729ba88
  Michael Sammler authored Feb 12, 2021
  
  7729ba88
- Refactor rule for arithmetic operators. · a181453a
  Rodolphe Lepigre authored Feb 10, 2021
  
  a181453a
- Add a [no_build] option to the TOML file. · d7a647cf
  Rodolphe Lepigre authored Feb 11, 2021
  
  d7a647cf
- Update some code generation. · 2112f69f
  Rodolphe Lepigre authored Feb 11, 2021
  
  2112f69f
- try new version of unification · 3a0000a9
  Michael Sammler authored Feb 12, 2021
  
  3a0000a9
11 Feb, 2021 2 commits
- Add a size to the [ptr] type. · d055d375
  Rodolphe Lepigre authored Feb 11, 2021
  
  d055d375
- refactor mpool · 223a33ac
  Michael Sammler authored Feb 11, 2021
  
  223a33ac
10 Feb, 2021 4 commits
- More [loc_in_bounds] infrastructure. · 6407a1c9
  Rodolphe Lepigre authored Feb 10, 2021
  
  6407a1c9
- small tweaks to container of examples · c286acff
  Michael Sammler authored Feb 10, 2021
  
  c286acff
- simplify option fmap none · a889efa0
  Michael Sammler authored Feb 10, 2021
  
  a889efa0
- new makefile that is hopefully MacOS compliant · c94fb809
  Michael Sammler authored Feb 10, 2021
  
  c94fb809
08 Feb, 2021 7 commits
- Make more functions simpl never · 1e648f6a
  Michael Sammler authored Feb 08, 2021
  
  1e648f6a
- comment · 6b8accc2
  Michael Sammler authored Feb 08, 2021
  
  6b8accc2
- Use Z in early_alloc. · b0a28e4a
  Rodolphe Lepigre authored Feb 08, 2021
  
  b0a28e4a
- add ElimModal Instances for typed_stmt and WPs · cb702f79
  Michael Sammler authored Feb 08, 2021
  
  cb702f79
- fix typo · ff84926a
  Michael Sammler authored Feb 08, 2021
  
  ff84926a
- more docs · 84b09b90
  Michael Sammler authored Feb 08, 2021
  
  84b09b90
- improve docs · e2dad8cd
  Michael Sammler authored Feb 08, 2021
  
  e2dad8cd
05 Feb, 2021 2 commits
- fix evar instantiation · 5a80357c
  Michael Sammler authored Feb 05, 2021
  
  5a80357c
- Fix spec in [flags.c] example (reported by Paul). · 8d836361
  Rodolphe Lepigre authored Feb 05, 2021
  
  8d836361
04 Feb, 2021 6 commits
- Cleanup related to the ticket lock example. · f57064b3
  Rodolphe Lepigre authored Feb 04, 2021
  
  f57064b3
- small steps towards improving subsume_list · 224962d1
  Michael Sammler authored Feb 04, 2021
  
  224962d1
- refactor spinlock · 889a2dec
  Michael Sammler authored Feb 04, 2021
  
  889a2dec
- fix generate_all · 48998a09
  Michael Sammler authored Feb 04, 2021
  
  48998a09
- change dir structure · 78aff991
  Michael Sammler authored Feb 04, 2021
  
  78aff991
- Start verifying a new version of [early_alloc.c]. · 42414135
  Rodolphe Lepigre authored Jan 28, 2021
  
  42414135
03 Feb, 2021 5 commits
- Hand verification of a ticket lock. · 2e18054e
  Rodolphe Lepigre authored Jan 27, 2021
  
  2e18054e
- Improve Coq generation. · dd16dd70
  Rodolphe Lepigre authored Feb 03, 2021
  
  dd16dd70
- Enable the [rc::immovable] annotation. · 72c2d2bf
  Rodolphe Lepigre authored Feb 03, 2021
  
  72c2d2bf
- add new version of buddy allocator · 580d80ed
  Michael Sammler authored Feb 03, 2021
  
  580d80ed
- Unfold more definitions in the side condition solver. · 1aff2246
  Rodolphe Lepigre authored Feb 02, 2021 and Michael Sammler committed Feb 03, 2021
  
  1aff2246
02 Feb, 2021 2 commits
- Add the [rc::let] annotation. · 65a898ae
  Rodolphe Lepigre authored Feb 02, 2021
  
  65a898ae
- Strengthen the [LocInBounds] infrastructure. · df9ee0eb
  Rodolphe Lepigre authored Feb 02, 2021
  
  df9ee0eb
01 Feb, 2021 1 commit
- Infrastructure for [SimpleSubsumeVal]. · 345ff19c
  Rodolphe Lepigre authored Jan 29, 2021 and Michael Sammler committed Feb 01, 2021
  
  345ff19c
29 Jan, 2021 2 commits
- try different rule for introducing global with type · 30da83cd
  Michael Sammler authored Jan 29, 2021
  
  30da83cd
- update iris · a5314052
  Michael Sammler authored Jan 29, 2021
  
  a5314052