GitHub - jtristan/CompCert-Extensions: Release of code written to experiment with formally verified translation validators for Compcert.

jtristan / CompCert-Extensions Public

Notifications You must be signed in to change notification settings
Fork 0
Star 3

Release of code written to experiment with formally verified translation validators for Compcert.

Notifications

Name		Name	Last commit message	Last commit date
Latest commit History 6 Commits
Trusted_Validators		Trusted_Validators
Untrusted_Transformations		Untrusted_Transformations
LICENSE		LICENSE
README		README

Repository files navigation

CompCert Extensions
===================

The directories 'Untrusted_Transformations' and 'Trusted_Validators' contain
respectively OCaml implementation of optimizations and Coq formally verified
translation validators that extend the Compcert compiler. 

These files are not maintained anymore and are meant to be used as a source
of code to extend Compcert. (It's a 'framework'.)