Name | Date | Size | ||
---|---|---|---|---|
.. | 25-Jul-2019 | 10 | ||
.gitignore | H A D | 25-Jul-2019 | 318 | |
Absyn-CType.ML | H A D | 25-Jul-2019 | 11.7 KiB | |
Absyn-Expr.ML | H A D | 25-Jul-2019 | 17.1 KiB | |
Absyn-Serial.ML | H A D | 25-Jul-2019 | 6.8 KiB | |
Absyn-StmtDecl.ML | H A D | 25-Jul-2019 | 8.2 KiB | |
Absyn.ML | H A D | 25-Jul-2019 | 497 | |
basics.ML | H A D | 25-Jul-2019 | 1.8 KiB | |
Binaryset.ML | H A D | 25-Jul-2019 | 16.4 KiB | |
calculate_state.ML | H A D | 25-Jul-2019 | 26.8 KiB | |
CLanguage.thy | H A D | 25-Jul-2019 | 1.7 KiB | |
complit.ML | H A D | 25-Jul-2019 | 5.2 KiB | |
CProof.thy | H A D | 25-Jul-2019 | 18.2 KiB | |
CTranslation.thy | H A D | 25-Jul-2019 | 6.2 KiB | |
doc/ | H | 25-Jul-2019 | 6 | |
expression_translation.ML | H A D | 25-Jul-2019 | 47.5 KiB | |
expression_typing.ML | H A D | 25-Jul-2019 | 7.9 KiB | |
Feedback.ML | H A D | 25-Jul-2019 | 1.8 KiB | |
FunctionalRecordUpdate.ML | H A D | 25-Jul-2019 | 3.1 KiB | |
General.ML | H A D | 25-Jul-2019 | 365 | |
globalmakevars | H A D | 25-Jul-2019 | 1.4 KiB | |
heapstatetype.ML | H A D | 25-Jul-2019 | 3.2 KiB | |
hp_termstypes.ML | H A D | 25-Jul-2019 | 8.9 KiB | |
HPInter.ML | H A D | 25-Jul-2019 | 18.9 KiB | |
IndirectCalls.thy | H A D | 25-Jul-2019 | 2.4 KiB | |
INSTALL | H A D | 25-Jul-2019 | 1.6 KiB | |
isa_termstypes.ML | H A D | 25-Jul-2019 | 18.6 KiB | |
isar_install.ML | H A D | 25-Jul-2019 | 20.7 KiB | |
Makefile | H A D | 25-Jul-2019 | 2.4 KiB | |
MANIFEST | H A D | 25-Jul-2019 | 12.8 KiB | |
MemoryModelExtras-sig.ML | H A D | 25-Jul-2019 | 4.8 KiB | |
MemoryModelExtras.ML | H A D | 25-Jul-2019 | 1.8 KiB | |
mkrelease | H A D | 25-Jul-2019 | 5.8 KiB | |
MLton-LICENSE | H A D | 25-Jul-2019 | 1.2 KiB | |
modifies_proofs.ML | H A D | 25-Jul-2019 | 17 KiB | |
ModifiesProofs.thy | H A D | 25-Jul-2019 | 7.6 KiB | |
MString.ML | H A D | 25-Jul-2019 | 1.1 KiB | |
name_generation.ML | H A D | 25-Jul-2019 | 8.2 KiB | |
openUnsynch.ML | H A D | 25-Jul-2019 | 256 | |
PackedTypes.thy | H A D | 25-Jul-2019 | 38.3 KiB | |
PrettyProgs.thy | H A D | 25-Jul-2019 | 1.1 KiB | |
program_analysis.ML | H A D | 25-Jul-2019 | 83.7 KiB | |
README | H A D | 25-Jul-2019 | 1.6 KiB | |
recursive_records/ | H | 25-Jul-2019 | 4 | |
Region.ML | H A D | 25-Jul-2019 | 2.7 KiB | |
RegionExtras.ML | H A D | 25-Jul-2019 | 1 KiB | |
RELEASES | H A D | 25-Jul-2019 | 3.5 KiB | |
ROOT | H A D | 25-Jul-2019 | 454 | |
Simpl/ | H | 25-Jul-2019 | 33 | |
smlnj-license.html | H A D | 25-Jul-2019 | 1.2 KiB | |
SourceFile.ML | H A D | 25-Jul-2019 | 1.6 KiB | |
SourcePos.ML | H A D | 25-Jul-2019 | 1.5 KiB | |
standalone-parser/ | H | 25-Jul-2019 | 18 | |
static-fun.ML | H A D | 25-Jul-2019 | 7.1 KiB | |
StaticFun.thy | H A D | 25-Jul-2019 | 6 KiB | |
stmt_translation.ML | H A D | 25-Jul-2019 | 33.1 KiB | |
StrictC.grm | H A D | 25-Jul-2019 | 69.7 KiB | |
StrictC.lex | H A D | 25-Jul-2019 | 26.2 KiB | |
StrictCParser.ML | H A D | 25-Jul-2019 | 1.3 KiB | |
syntax_transforms.ML | H A D | 25-Jul-2019 | 16.3 KiB | |
Target-generic32.ML | H A D | 25-Jul-2019 | 1.5 KiB | |
TargetNumbers-sig.ML | H A D | 25-Jul-2019 | 1.6 KiB | |
termstypes-sig.ML | H A D | 25-Jul-2019 | 2.9 KiB | |
termstypes.ML | H A D | 25-Jul-2019 | 8.6 KiB | |
testfiles/ | H | 25-Jul-2019 | 294 | |
tools/ | H | 25-Jul-2019 | 4 | |
topo_sort.ML | H A D | 25-Jul-2019 | 3.2 KiB | |
umm_heap/ | H | 25-Jul-2019 | 28 | |
UMM_Proofs.ML | H A D | 25-Jul-2019 | 25.3 KiB | |
UMM_termstypes.ML | H A D | 25-Jul-2019 | 5.5 KiB | |
use.ML | H A D | 25-Jul-2019 | 356 |
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