Repository navigation

RFC: stable memory block names for globals - #220

Open

jeremie-koenig wants to merge 26 commits into

AbsInt:masterfrom

CertiKOS:globmem

Open

RFC: stable memory block names for globals#220
jeremie-koenig wants to merge 26 commits into
AbsInt:masterfrom
CertiKOS:globmem

Commits on Jan 30, 2018
- Add set2 to the general MAP interface
  jeremie-koenig
  committed
  de3c418
- Improved namespace for memory block ids
  jeremie-koenig
  committed
  f93ca78
- BlockNames: Add a Block.le relation
  jeremie-koenig
  committed
  6274b59
Commits on Jan 31, 2018
- BlockNames: update some of Globalenvs.v
  Pierre Wilke
  committed
  4fd3c3f
- BlockNames: Progress on Globalenvs
  Pierre Wilke
  committed
  1284fb5
- BlockNames: finished Globalenvs and Memory
  Pierre WILKE
  committed
  4ec83f0
- BlockNames: update Events.v
  jeremie-koenig
  committed
  baf0ba3
Commits on Feb 1, 2018
- BlockNames: reintroduce find_symbol
  jeremie-koenig
  committed
  4696267
- BlockNames: add a Decidable instance Block.eq
  jeremie-koenig
  committed
  f69d799
- BlockNames: update Separation.v
  Pierre Wilke
  committed
  e53faa6
- BlockNames: update ValueDomain and ValueAnalysis
  Pierre Wilke
  committed
  4ef2be8
- BlockNames: Update Inlining + Unusedglob
  Pierre WILKE
  committed
  82dde56
- BlockNames: update Deadcode and Stacking
  Pierre WILKE
  committed
  ca0631f
- Add hints for Block.*
  Pierre WILKE
  committed
  8a204da
Commits on Feb 2, 2018
- BlockNames: encapsulate hints for Block.lt/le into a specific database and introduce blomega tactic
  Pierre Wilke
  committed
  616ec9e
- BlockNames: update frontend
  Pierre Wilke
  committed
  cb38d63
- BlockNames: add to_string and block_compare operations to BlockType. Update the interpreter
  Pierre WILKE
  committed
  2f152ed
- BlockNames: minor changes to minimize diff with CompCert.
  Pierre WILKE
  committed
  a5974d3
- BlockNames: cosmetic improvements to Initializers.v
  jeremie-koenig
  committed
  1a4dd43
Commits on Feb 16, 2018
- Make sure IMap satisfies the MAP interface
  jeremie-koenig
  committed
  8ab2cd3
- BlockNames: use an efficient IMap to implement BMap
  jeremie-koenig
  committed
  e268e60
- Merge remote-tracking branch 'absint/master' into globmem
  jeremie-koenig
  committed
  2f18434
Commits on Feb 19, 2018
- BlockNames: get rid of the BMapType interface
  jeremie-koenig
  committed
  f9a2754
- Cosmetic improvements to BlockNames.v
  jeremie-koenig
  committed
  74bb7e0
- Better compatibility with pull request #222
  jeremie-koenig
  committed
  7a0da56
Commits on Mar 11, 2019
- Merge remote-tracking branch 'absint/master' into globmem
  jeremie-koenig
  committed
  024b3bb

Commits

Commits on Jan 30, 2018

Commits on Jan 31, 2018

Commits on Feb 1, 2018

Commits on Feb 2, 2018

Commits on Feb 16, 2018

Commits on Feb 19, 2018

Commits on Mar 11, 2019