From aff083950e663c3f23d63de9c4e2129bb03bacad Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Wed, 16 Dec 2020 16:07:03 +0100 Subject: update the doc for CompCert 3.8 --- doc/index-kvx.html | 18 ++++++++++++------ 1 file changed, 12 insertions(+), 6 deletions(-) (limited to 'doc') diff --git a/doc/index-kvx.html b/doc/index-kvx.html index b8850727..4e2e0b47 100644 --- a/doc/index-kvx.html +++ b/doc/index-kvx.html @@ -22,15 +22,17 @@ a:active {color : Red; text-decoration : underline; } -

The CompCert verified compiler

+ +

The CompCert verified compiler

Commented Coq development

-

Version 3.7, 2020-03-31

 +

Version 3.8, 2020-11-16

+

PATCHED for the Kalray MPPA-KVX VLIW CORE

Introduction

-

This web page is a patched version of the table of contents of the official CompCert documentation, - as given on the CompCert Web site. +

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. The unmodified parts of this table appear in gray.

@@ -40,7 +42,8 @@ a:active {color : Red; text-decoration : underline; } See also the README.md of our GitLab public repository.

-

Table of contents

+ +

Table of contents

General-purpose libraries, data structures and algorithms

@@ -85,6 +88,8 @@ See also: Memdata (in-memory rep
  • Determinism: determinism properties of small-step semantics.
  • Op: operators, addressing modes and their semantics. +
  • Builtins: semantics of built-in functions.
    +See also: Builtins0 (target-independent part), Builtins1 (target-dependent part).
  • Unityping: a solver for atomic unification constraints. @@ -172,7 +177,8 @@ This IR is generic over the processor, even if currently, only used for KVX. - Recognition of operators
    and addressing modes + Recognition of operators
    and addressing modes;
    + if-conversion Cminor to CminorSel Selection
    SelectOp
    -- cgit