RFC: stable memory block names for globals#220

Open

jeremie-koenig wants to merge 26 commits intoAbsInt:masterfrom CertiKOS:globmem

+1,365-813

Commits on Jan 30, 2018

Commits on Jan 31, 2018

BlockNames: update some of Globalenvs.v
Pierre Wilke
committed
BlockNames: Progress on Globalenvs
Pierre Wilke
committed
BlockNames: finished Globalenvs and Memory
Pierre WILKE
committed
BlockNames: update Events.v
jeremie-koenig
committed

Commits on Feb 1, 2018

BlockNames: reintroduce find_symbol
jeremie-koenig
committed
BlockNames: add a Decidable instance Block.eq
jeremie-koenig
committed
BlockNames: update Separation.v
Pierre Wilke
committed
BlockNames: update ValueDomain and ValueAnalysis
Pierre Wilke
committed
BlockNames: Update Inlining + Unusedglob
Pierre WILKE
committed
BlockNames: update Deadcode and Stacking
Pierre WILKE
committed
Add hints for Block.*
Pierre WILKE
committed

Commits on Feb 2, 2018

BlockNames: encapsulate hints for Block.lt/le into a specific database and introduce blomega tactic
Pierre Wilke
committed
BlockNames: update frontend
Pierre Wilke
committed
BlockNames: add to_string and block_compare operations to BlockType. Update the interpreter
Pierre WILKE
committed
BlockNames: minor changes to minimize diff with CompCert.
Pierre WILKE
committed
BlockNames: cosmetic improvements to Initializers.v
jeremie-koenig
committed

Commits on Feb 16, 2018

Commits on Feb 19, 2018

Commits on Mar 11, 2019

Merge remote-tracking branch 'absint/master' into globmem
jeremie-koenig
committed