Description

This directory contains the LaTeX source files for the ACSL reference manual. ACSL stands for ANSI/ISO C Specification Language and is meant to formally specify the intended behavior of C programs, in particular through the usage of function contracts. ACSL is used in particular by the Frama-C platform (http://frama-c.com/) that gathers a set of C analysis tools.

Requirements

In order to generate a pdf version of the manual, you will need the following:

a TeX distribution (e.g. TeXlive), including metapost
latexmk
ocaml

then, typing make should produce the acsl.pdf document

Name		Name	Last commit message	Last commit date
Latest commit History 600 Commits
.gitignore		.gitignore
CONTRIBUTING.md		CONTRIBUTING.md
LICENSE		LICENSE
Makefile		Makefile
QUESTIONS		QUESTIONS
README.md		README.md
abrupt_termination.c		abrupt_termination.c
acsl-mini-tutorial.ctex		acsl-mini-tutorial.ctex
acsl-mini-tutorial.html		acsl-mini-tutorial.html
acsl_allocator.c		acsl_allocator.c
advancedloopinvariants.c		advancedloopinvariants.c
allocation.tex		allocation.tex
assertions.tex		assertions.tex
assigns.c		assigns.c
assigns_array.c		assigns_array.c
assigns_list.c		assigns_list.c
at.tex		at.tex
biblio.bib		biblio.bib
binders.tex		binders.tex
bsearch.c		bsearch.c
bsearch2.c		bsearch2.c
cealistlogo.eps		cealistlogo.eps
cealistlogo.pdf		cealistlogo.pdf
cfg.mp		cfg.mp
cfg.mps		cfg.mps
common.h		common.h
compjml_modern.tex		compjml_modern.tex
concl_modern.tex		concl_modern.tex
cond_assigns.c		cond_assigns.c
dangling.c		dangling.c
data_invariants.tex		data_invariants.tex
dependencies.tex		dependencies.tex
div_lemma.c		div_lemma.c
dowhile.c		dowhile.c
euclide.c		euclide.c
example-lt-modern.tex		example-lt-modern.tex
example-lt.tex		example-lt.tex
exit.c		exit.c
exitbehavior.tex		exitbehavior.tex
fact.c		fact.c
flag.c		flag.c
fn_behavior.tex		fn_behavior.tex
footprint.c		footprint.c
frama-c-book.cls		frama-c-book.cls
frama-c-cover.pdf		frama-c-cover.pdf
frama-c-left.pdf		frama-c-left.pdf
frama-c-right.pdf		frama-c-right.pdf
fwrite-malloc.c-old		fwrite-malloc.c-old
gen_code.c		gen_code.c
gen_spec_with_ghost.c		gen_spec_with_ghost.c
gen_spec_with_model.c		gen_spec_with_model.c
generalinvariants.tex		generalinvariants.tex
ghost.tex		ghost.tex
ghostcfg.c		ghostcfg.c
ghostpointer.c		ghostpointer.c
glob_var_masked.c		glob_var_masked.c
glob_var_masked_sol.c		glob_var_masked_sol.c
higherorder.tex		higherorder.tex
import.c		import.c
incrstar.c		incrstar.c
inductive.tex		inductive.tex
inductiveloopinvariants.tex		inductiveloopinvariants.tex
inductiveloopinvariants_modern.tex		inductiveloopinvariants_modern.tex
initialized.c		initialized.c
inria.eps		inria.eps
inria.pdf		inria.pdf
integer-cast-modern.tex		integer-cast-modern.tex
integer-cast.tex		integer-cast.tex
intlists.c		intlists.c
intro_modern.tex		intro_modern.tex
invariants.c		invariants.c
isgcd.c		isgcd.c
isqrt.c		isqrt.c
lexico.c		lexico.c
libraries_modern.tex		libraries_modern.tex
list-gram.tex		list-gram.tex
list-observer.c		list-observer.c
list.h		list.h
listdecl.c		listdecl.c
listdef.c		listdef.c
listlengthdef.c		listlengthdef.c
listmodule.c		listmodule.c
loc.tex		loc.tex
logic.tex		logic.tex
logicdecl.tex		logicdecl.tex
logiclabels.tex		logiclabels.tex
logicreads.tex		logicreads.tex
logictypedecl.tex		logictypedecl.tex
loop-frees.c		loop-frees.c
loop_current.c		loop_current.c
loops.tex		loops.tex
loopvariantnegative.c		loopvariantnegative.c
macros_modern.tex		macros_modern.tex
main.tex		main.tex
malloc-free2-fn.c		malloc-free2-fn.c
malloc_free_fn.c		malloc_free_fn.c
max.c		max.c
max_index.c		max_index.c
mayexit.c		mayexit.c
mean.c		mean.c

License

aogrcs/acsl

Folders and files

Latest commit

History