From edc7505f0b1b617cda01648316ea02b58d268411 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Mon, 6 Dec 2021 23:15:51 +0100 Subject: improvement in html doc (not finished yet) --- doc/index-verimag.html | 167 ++++++++++++++++++++++++++++++++++++++++++------- 1 file changed, 145 insertions(+), 22 deletions(-) (limited to 'doc') diff --git a/doc/index-verimag.html b/doc/index-verimag.html index 242fa1cd..1eb857d9 100644 --- a/doc/index-verimag.html +++ b/doc/index-verimag.html @@ -26,7 +26,7 @@ a:active {color : Red; text-decoration : underline; }

Commented Coq development

Version 3.9, 2021-05-10

-

VERIMAG fork version 2021-29-10

+

VERIMAG fork version 2021-29-10

The CompCert Verimag's fork

This web page is a patched version of the table of contents of the official CompCert sources documentation, as given on the CompCert Web site. @@ -34,18 +34,37 @@ a:active {color : Red; text-decoration : underline; }

A high-level view of this CompCert backend is provided by the following documents: + +

+ +

The people responsible for this version are

+ + + + +

with contributions of:

+ +

Introduction

@@ -120,13 +139,15 @@ inequations by fixpoint iteration.
  • ImpPrelude: declares the data types exchanged with Impure oracles.
    • -

    The abstractbb library, introduced for Aarch64 and KVX cores

    +

    The abstractbb library, introduced for Aarch64 and KVX cores

    This library introduces a block intermediate representation used for postpass scheduling verification. It might be extended to others backends. + +

    Definitions and theorems used in many parts of the development