GitHub - epfl-systemf/sepviz-software-foundations-vc

Branches Tags

Name		Name	Last commit message	Last commit date
Latest commit History 5 Commits
common		common
.envrc		.envrc
.gitignore		.gitignore
Bib.html		Bib.html
Bib.v		Bib.v
Hashfun.html		Hashfun.html
Hashfun.v		Hashfun.v
LICENSE		LICENSE
Makefile		Makefile
Postscript.html		Postscript.html
Postscript.v		Postscript.v
Preface.html		Preface.html
Preface.v		Preface.v
README		README
Reverse-Slides.pdf		Reverse-Slides.pdf
SepvizNotations.v		SepvizNotations.v
Spec_stack.html		Spec_stack.html
Spec_stack.v		Spec_stack.v
Spec_stdlib.html		Spec_stdlib.html
Spec_stdlib.v		Spec_stdlib.v
Spec_triang.html		Spec_triang.html
Spec_triang.v		Spec_triang.v
VC.pdf		VC.pdf
VSU_intro.html		VSU_intro.html
VSU_intro.v		VSU_intro.v
VSU_main.html		VSU_main.html
VSU_main.v		VSU_main.v
VSU_main2.html		VSU_main2.html
VSU_main2.v		VSU_main2.v
VSU_stack.html		VSU_stack.html
VSU_stack.v		VSU_stack.v
VSU_stdlib.html		VSU_stdlib.html
VSU_stdlib.v		VSU_stdlib.v
VSU_stdlib2.html		VSU_stdlib2.html
VSU_stdlib2.v		VSU_stdlib2.v
VSU_triang.html		VSU_triang.html
VSU_triang.v		VSU_triang.v
Verif_append1.html		Verif_append1.html
Verif_append1.v		Verif_append1.v
Verif_append2.html		Verif_append2.html
Verif_append2.v		Verif_append2.v
Verif_hash.html		Verif_hash.html
Verif_hash.v		Verif_hash.v
Verif_reverse.html		Verif_reverse.html
Verif_reverse.v		Verif_reverse.v
Verif_stack.html		Verif_stack.html
Verif_stack.v		Verif_stack.v
Verif_strlib.html		Verif_strlib.html
Verif_strlib.v		Verif_strlib.v
Verif_sumarray.html		Verif_sumarray.html
Verif_sumarray.v		Verif_sumarray.v
Verif_triang.html		Verif_triang.html
Verif_triang.v		Verif_triang.v
_CoqProject		_CoqProject
append.c		append.c
append.v		append.v
append32.v		append32.v
append64.v		append64.v
cfiles-bitsize		cfiles-bitsize
chain.gif		chain.gif
coqindex.html		coqindex.html
flake.lock		flake.lock
flake.nix		flake.nix
hash.c		hash.c
hash.v		hash.v
hash32.v		hash32.v
hash64.v		hash64.v
hints.v		hints.v
index.html		index.html
main2.c		main2.c
main2.v		main2.v
main232.v		main232.v
main264.v		main264.v
reverse.c		reverse.c
reverse.v		reverse.v
reverse32.v		reverse32.v
reverse64.v		reverse64.v
sepviz.yaml		sepviz.yaml
stack.c		stack.c
stack.v		stack.v
stack2.c		stack2.c
stack2.h		stack2.h
stack2.v		stack2.v
stack232.v		stack232.v
stack264.v		stack264.v
stack32.v		stack32.v
stack64.v		stack64.v
stdlib.c		stdlib.c
stdlib.h		stdlib.h
stdlib.v		stdlib.v
stdlib2.c		stdlib2.c
stdlib2.v		stdlib2.v
stdlib232.v		stdlib232.v
stdlib264.v		stdlib264.v
stdlib32.v		stdlib32.v
stdlib64.v		stdlib64.v
strlib.c		strlib.c
strlib.v		strlib.v
strlib32.v		strlib32.v
strlib64.v		strlib64.v

Repository files navigation

#########################################################################
                           SOFTWARE FOUNDATIONS
#########################################################################

This directory contains both Coq scripts (.v files) and more readable
HTML files for Verifiable C, by Andrew W. Appel et al.,
volume [VC] of the Software Foundations series.

  - Preface.v or Preface.html
    The place to start reading, including details on how to install
    required software

  - index.html
    The book's cover page and navigation starting point

  - deps.html 
    Overview of the ordering of chapters

  - LICENSE
    Explanation of how these files may be redistributed

NOTE ABOUT VST VERSION:

Preface.v checks that you are using a version of VST that is well matched
to this textbook.   If you have installed VST by the standard Coq Platform
or by opam, then it will be found automatically in coq/lib/coq/user-contrib.
If that's the right version (as checked by Preface.v) then everything is easy.

TO USE THIS VOLUME BASED ON A CUSTOM-INSTALLED VST VERSION:
Otherwise, you may want to download a specific version from
https://github.com/PrincetonUniversity/VST   and build from sources.
In that case, your VST will not be found in user-contrib, and you should
follow these steps:

1. In this directory, "make clean" and remove Makefile.coq

2. Edit the first line of the Makefile to read,

COQMFFLAGS= -Q . VC -Q path/to/VST VST

where "path/to/VST" is whatever directory you've compiled VST in.

3. Edit the _CoqProject file to have the same -Q options.

4. If your compiled VST uses the special configuration COMPCERT=bundled,
then instead you should add one more -Q option to Makefile and _CoqProject:

COQMFFLAGS= -Q . VC -Q path/to/VST VST -Q path/to/VST/compcert compcert