Merge branch 'ralf/wp-fupd-no-more' into 'master'
wp_finish: avoid making a goal unprovable See merge request iris/iris!593
Showing
- iris/program_logic/adequacy.v 1 addition, 1 deletioniris/program_logic/adequacy.v
- iris/program_logic/total_weakestpre.v 10 additions, 14 deletionsiris/program_logic/total_weakestpre.v
- iris/program_logic/weakestpre.v 9 additions, 14 deletionsiris/program_logic/weakestpre.v
- iris_heap_lang/lib/array.v 3 additions, 3 deletionsiris_heap_lang/lib/array.v
- iris_heap_lang/lib/clairvoyant_coin.v 3 additions, 3 deletionsiris_heap_lang/lib/clairvoyant_coin.v
- iris_heap_lang/lib/counter.v 3 additions, 3 deletionsiris_heap_lang/lib/counter.v
- iris_heap_lang/lib/lazy_coin.v 1 addition, 1 deletioniris_heap_lang/lib/lazy_coin.v
- iris_heap_lang/lib/spin_lock.v 2 additions, 2 deletionsiris_heap_lang/lib/spin_lock.v
- iris_heap_lang/lib/ticket_lock.v 1 addition, 1 deletioniris_heap_lang/lib/ticket_lock.v
- iris_heap_lang/proofmode.v 27 additions, 3 deletionsiris_heap_lang/proofmode.v
- tests/heap_lang.ref 42 additions, 4 deletionstests/heap_lang.ref
- tests/heap_lang.v 19 additions, 3 deletionstests/heap_lang.v
- tests/heap_lang_proph.v 4 additions, 4 deletionstests/heap_lang_proph.v
- tests/ipm_paper.ref 1 addition, 1 deletiontests/ipm_paper.ref
- tests/ipm_paper.v 5 additions, 5 deletionstests/ipm_paper.v
- tests/one_shot.v 2 additions, 2 deletionstests/one_shot.v
- tests/one_shot_once.v 2 additions, 2 deletionstests/one_shot_once.v
Loading
Please register or sign in to comment