Commit Graph

7 Commits (2c5a2976365c67a08a5c9be04e3ae66a7617e31e)

Author SHA1 Message Date
Scott Owens ab7233c5b8 [sledge sem] Refactor the way LLVM sem. does phis 6 years ago
Scott Owens 30c301a3e8 [sledge sem] Add a more llair-like LLVM semantics 6 years ago
Scott Owens f298d728c5 [sledge sem] Start sketching translation correctness 6 years ago
Scott Owens 84883127af Add a skeleton of an approach to llvm->llair 6 years ago
Scott Owens 89c3da4510 Prove that Ret preserves the invariant 6 years ago
Scott Owens df5f20956f Define a simple initial state that inits the globals 6 years ago
Scott Owens 97eb280cb5 Add initial mini-LLVM semantics written in HOL4 6 years ago