NameDateSize

..25-Jul-201910

.gitignoreH A D25-Jul-2019318

Absyn-CType.MLH A D25-Jul-201911.7 KiB

Absyn-Expr.MLH A D25-Jul-201917.1 KiB

Absyn-Serial.MLH A D25-Jul-20196.8 KiB

Absyn-StmtDecl.MLH A D25-Jul-20198.2 KiB

Absyn.MLH A D25-Jul-2019497

basics.MLH A D25-Jul-20191.8 KiB

Binaryset.MLH A D25-Jul-201916.4 KiB

calculate_state.MLH A D25-Jul-201926.8 KiB

CLanguage.thyH A D25-Jul-20191.7 KiB

complit.MLH A D25-Jul-20195.2 KiB

CProof.thyH A D25-Jul-201918.2 KiB

CTranslation.thyH A D25-Jul-20196.2 KiB

doc/H25-Jul-20196

expression_translation.MLH A D25-Jul-201947.5 KiB

expression_typing.MLH A D25-Jul-20197.9 KiB

Feedback.MLH A D25-Jul-20191.8 KiB

FunctionalRecordUpdate.MLH A D25-Jul-20193.1 KiB

General.MLH A D25-Jul-2019365

globalmakevarsH A D25-Jul-20191.4 KiB

heapstatetype.MLH A D25-Jul-20193.2 KiB

hp_termstypes.MLH A D25-Jul-20198.9 KiB

HPInter.MLH A D25-Jul-201918.9 KiB

IndirectCalls.thyH A D25-Jul-20192.4 KiB

INSTALLH A D25-Jul-20191.6 KiB

isa_termstypes.MLH A D25-Jul-201918.6 KiB

isar_install.MLH A D25-Jul-201920.7 KiB

MakefileH A D25-Jul-20192.4 KiB

MANIFESTH A D25-Jul-201912.8 KiB

MemoryModelExtras-sig.MLH A D25-Jul-20194.8 KiB

MemoryModelExtras.MLH A D25-Jul-20191.8 KiB

mkreleaseH A D25-Jul-20195.8 KiB

MLton-LICENSEH A D25-Jul-20191.2 KiB

modifies_proofs.MLH A D25-Jul-201917 KiB

ModifiesProofs.thyH A D25-Jul-20197.6 KiB

MString.MLH A D25-Jul-20191.1 KiB

name_generation.MLH A D25-Jul-20198.2 KiB

openUnsynch.MLH A D25-Jul-2019256

PackedTypes.thyH A D25-Jul-201938.3 KiB

PrettyProgs.thyH A D25-Jul-20191.1 KiB

program_analysis.MLH A D25-Jul-201983.7 KiB

READMEH A D25-Jul-20191.6 KiB

recursive_records/H25-Jul-20194

Region.MLH A D25-Jul-20192.7 KiB

RegionExtras.MLH A D25-Jul-20191 KiB

RELEASESH A D25-Jul-20193.5 KiB

ROOTH A D25-Jul-2019454

Simpl/H25-Jul-201933

smlnj-license.htmlH A D25-Jul-20191.2 KiB

SourceFile.MLH A D25-Jul-20191.6 KiB

SourcePos.MLH A D25-Jul-20191.5 KiB

standalone-parser/H25-Jul-201918

static-fun.MLH A D25-Jul-20197.1 KiB

StaticFun.thyH A D25-Jul-20196 KiB

stmt_translation.MLH A D25-Jul-201933.1 KiB

StrictC.grmH A D25-Jul-201969.7 KiB

StrictC.lexH A D25-Jul-201926.2 KiB

StrictCParser.MLH A D25-Jul-20191.3 KiB

syntax_transforms.MLH A D25-Jul-201916.3 KiB

Target-generic32.MLH A D25-Jul-20191.5 KiB

TargetNumbers-sig.MLH A D25-Jul-20191.6 KiB

termstypes-sig.MLH A D25-Jul-20192.9 KiB

termstypes.MLH A D25-Jul-20198.6 KiB

testfiles/H25-Jul-2019294

tools/H25-Jul-20194

topo_sort.MLH A D25-Jul-20193.2 KiB

umm_heap/H25-Jul-201928

UMM_Proofs.MLH A D25-Jul-201925.3 KiB

UMM_termstypes.MLH A D25-Jul-20195.5 KiB

use.MLH A D25-Jul-2019356

README

1#
2# Copyright 2014, NICTA
3#
4# This software may be distributed and modified according to the terms of
5# the BSD 2-Clause license. Note that NO WARRANTY is provided.
6# See "LICENSE_BSD2.txt" for details.
7#
8# @TAG(NICTA_BSD)
9#
10
11This is the NICTA StrictC translation tool.
12
13To install, see the file INSTALL in the src/c-parser directory.
14
15To use:
16
171. Use the heap CParser that is created by installation
182. Import the theory CTranslation
193. Load ('install') C files into your theories with the Isar command
20   install_C_file.
21
22See docs/ctranslation.pdf for more information about the options
23and C language semantics that this tool provides.
24
25See many examples in the testfiles directory.  For example,
26breakcontinue.thy is a fairly involved demonstration of doing things
27the hard way.
28
29----------------------------------------------------------------------
30The translation tool builds on various open source projects by others.
31
321. Norbert Schirmer's Simpl language and associated VCG tool.
33
34   Sources for this are found in the Simpl/ directory.  The
35   code is covered by an LGPL licence.
36
37   See http://afp.sourceforge.net/entries/Simpl.shtml
38
392. Code from SML/NJ:
40   - an implementation of binary sets (Binaryset.ML)
41   - the mllex and mlyacc tools (tools/{mllex,mlyacc})
42   - command-line option parsing (standalone-parser/GetOpt)
43
44   This code is covered by SML/NJ's BSD-ish licence.
45
46   See http://www.smlnj.org
47
483. Code from the mlton compiler:
49   - regions during lexing and parsing (Region.ML, SourceFile.ML and
50     SourcePos.ML)
51
52   This code is governed by a BSD licence.
53
54   See http://mlton.org
55