diff options
| author | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2018-05-29 16:23:01 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-05-29 16:23:01 +0200 |
| commit | 231899605cb48c695d898ebc68eef03bd27cd870 (patch) | |
| tree | f954443e7e124349905ebb9469541f864dfe302c /VERSION | |
| parent | a70741f8abc2e03346eed98e420f9a2e0c8531cc (diff) | |
| download | compcert-kvx-231899605cb48c695d898ebc68eef03bd27cd870.tar.gz compcert-kvx-231899605cb48c695d898ebc68eef03bd27cd870.zip | |
Simplify module Complements and add separate compilation (#121)
* Simplify the theorems about preservation of specifications (section 2)
There were three theorems, transf_c_program_preserves_spec, _safety_spec, and _liveness_spec) with the first being needlessly general and the last being hard to understand. Plus, the "liveness" and "safety" terminology wasn't very good.
Replaced by two theorems:
- transf_c_program_preserves_spec, which is the theorem previously named _safety_spec and talks about specifications that exclude going-wrong behaviors;
- transf_c_program_preserves_initial_trace, which is an instance of the theorem previously named _liveness_spec, and now talks about a single initial trace of interest rather than a set of such traces.
Added named definitions for properties of interest.
Added more explanations.
* Added theorems that talk about separate compilation (section 3)
These are the theorems from section 1 and 2 but reformulated in terms of multiple C source compilation units being separately compiled to Asm units then linked together.
Diffstat (limited to 'VERSION')
0 files changed, 0 insertions, 0 deletions