program_logic · 2d44c0ef7cfa41be6f2884576f9f12c2023d0857 · Ike Mulder / Iris

Forked from Iris / Iris

6393 commits behind the upstream repository.

Solve atomic also using reification/vm_compute.

Robbert Krebbers authored 8 years ago

I also reverted 7952bca4 since there is no need for atomic to be a
boolean predicate anymore. Moreover, I introduced a hint database
fsaV for solving side-conditions related to FSAs, in particular,
side-conditions related to expressions being atomic.

2966b4da

History

2966b4da 8 years ago

History

Name	Last commit	Last update
..
adequacy.v
auth.v
boxes.v
ectx_language.v
ectx_lifting.v
ectxi_language.v
ghost_ownership.v
global_functor.v
hoare.v
hoare_lifting.v
invariants.v
language.v
lifting.v
model.v
namespaces.v
ownership.v
pviewshifts.v
resources.v
saved_prop.v
sts.v
viewshifts.v
weakestpre.v
weakestpre_fix.v
wsat.v