source: extracted @ 2657

Name Size Rev Age Author Last Change
../
abstractStatus.ml 4.1 KB 2649   7 years sacerdot
abstractStatus.mli 1.3 KB 2649   7 years sacerdot
arithmetic.ml 27.1 KB 2649   7 years sacerdot
arithmetic.mli 8.1 KB 2649   7 years sacerdot
aSM.ml 198.5 KB 2649   7 years sacerdot
aSM.mli 49.9 KB 2649   7 years sacerdot
aSMCosts.ml 17.6 KB 2649   7 years sacerdot
aSMCosts.mli 2.0 KB 2649   7 years sacerdot
aSMCostsSplit.ml 3.7 KB 2649   7 years sacerdot
aSMCostsSplit.mli 1.4 KB 2649   7 years sacerdot
aST.ml 55.4 KB 2649   7 years sacerdot
aST.mli 19.4 KB 2649   7 years sacerdot
bitVector.ml 2.7 KB 2649   7 years sacerdot
bitVector.mli 1.2 KB 2649   7 years sacerdot
bitVectorTrie.ml 10.5 KB 2649   7 years sacerdot
bitVectorTrie.mli 3.5 KB 2649   7 years sacerdot
bitVectorZ.ml 2.6 KB 2649   7 years sacerdot
bitVectorZ.mli 694 bytes 2649   7 years sacerdot
bool.ml 2.5 KB 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
bool.mli 924 bytes 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
build 129 bytes 2620   7 years campbell Sufficient hacking to run the extracted Clight semantics.
byteValues.ml 31.6 KB 2649   7 years sacerdot
byteValues.mli 10.0 KB 2649   7 years sacerdot
casts.ml 882 bytes 2649   7 years sacerdot
casts.mli 736 bytes 2649   7 years sacerdot
cexec.ml 48.1 KB 2649   7 years sacerdot
cexec.mli 3.1 KB 2649   7 years sacerdot
cexecInd.ml 538 bytes 2649   7 years sacerdot
cexecInd.mli 538 bytes 2649   7 years sacerdot
cexecSound.ml 865 bytes 2649   7 years sacerdot
cexecSound.mli 865 bytes 2649   7 years sacerdot
classifyOp.ml 40.1 KB 2649   7 years sacerdot
classifyOp.mli 18.0 KB 2649   7 years sacerdot
cminor_semantics.ml 35.9 KB 2649   7 years sacerdot
cminor_semantics.mli 11.0 KB 2649   7 years sacerdot
cminor_syntax.ml 41.5 KB 2649   7 years sacerdot
cminor_syntax.mli 19.3 KB 2649   7 years sacerdot
compiler.ml 3.7 KB 2649   7 years sacerdot
compiler.mli 2.3 KB 2649   7 years sacerdot
coqlib.ml 363 bytes 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
coqlib.mli 238 bytes 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
core_notation.ml 15 bytes 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
core_notation.mli 15 bytes 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
costLabel.ml 670 bytes 2649   7 years sacerdot
costLabel.mli 584 bytes 2649   7 years sacerdot
csem.ml 50.2 KB 2649   7 years sacerdot
csem.mli 13.6 KB 2649   7 years sacerdot
csyntax.ml 56.6 KB 2649   7 years sacerdot
csyntax.mli 22.3 KB 2649   7 years sacerdot
deqsets.ml 4.0 KB 2649   7 years sacerdot
deqsets.mli 1.8 KB 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
div_and_mod.ml 3.4 KB 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
div_and_mod.mli 1.5 KB 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
division.ml 7.2 KB 2649   7 years sacerdot
division.mli 1.6 KB 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
errorMessages.ml 23.6 KB 2649   7 years sacerdot
errorMessages.mli 4.0 KB 2649   7 years sacerdot
errors.ml 8.9 KB 2649   7 years sacerdot
errors.mli 4.1 KB 2649   7 years sacerdot
events.ml 11.1 KB 2649   7 years sacerdot
events.mli 4.9 KB 2649   7 years sacerdot
extra_bool.ml 463 bytes 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
extra_bool.mli 271 bytes 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
extralib.ml 1.6 KB 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
extralib.mli 637 bytes 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
extranat.ml 5.1 KB 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
extranat.mli 2.3 KB 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
fetch.ml 83.6 KB 2649   7 years sacerdot
fetch.mli 1.9 KB 2649   7 years sacerdot
foldStuff.ml 1.6 KB 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
foldStuff.mli 741 bytes 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
fresh.ml 2.1 KB 2649   7 years sacerdot
fresh.mli 1.2 KB 2649   7 years sacerdot
frontend_misc.ml 4.5 KB 2649   7 years sacerdot
frontend_misc.mli 2.2 KB 2649   7 years sacerdot
frontEndMem.ml 3.0 KB 2649   7 years sacerdot
frontEndMem.mli 1.2 KB 2649   7 years sacerdot
frontEndOps.ml 56.8 KB 2649   7 years sacerdot
frontEndOps.mli 23.4 KB 2649   7 years sacerdot
frontEndVal.ml 4.4 KB 2649   7 years sacerdot
frontEndVal.mli 1.2 KB 2649   7 years sacerdot
genMem.ml 9.8 KB 2649   7 years sacerdot
genMem.mli 4.1 KB 2649   7 years sacerdot
globalenvs.ml 21.4 KB 2649   7 years sacerdot
globalenvs.mli 9.0 KB 2649   7 years sacerdot
graphs.ml 1.1 KB 2649   7 years sacerdot
graphs.mli 823 bytes 2649   7 years sacerdot
hide.ml 81 bytes 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
hide.mli 81 bytes 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
hints_declaration.ml 162 bytes 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
hints_declaration.mli 162 bytes 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
identifiers.ml 16.7 KB 2649   7 years sacerdot
identifiers.mli 8.2 KB 2649   7 years sacerdot
initialisation.ml 5.5 KB 2649   7 years sacerdot
initialisation.mli 1.8 KB 2649   7 years sacerdot
integers.ml 9.7 KB 2649   7 years sacerdot
integers.mli 2.9 KB 2649   7 years sacerdot
interpret.ml 242.2 KB 2649   7 years sacerdot
interpret.mli 2.4 KB 2649   7 years sacerdot
iO.ml 6.9 KB 2649   7 years sacerdot
iO.mli 2.7 KB 2649   7 years sacerdot
iOMonad.ml 8.4 KB 2649   7 years sacerdot
iOMonad.mli 3.6 KB 2649   7 years sacerdot
jmeq.ml 3.9 KB 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
jmeq.mli 1.7 KB 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
label.ml 26.1 KB 2649   7 years sacerdot
label.mli 2.7 KB 2649   7 years sacerdot
labelledObjects.ml 2.1 KB 2649   7 years sacerdot
labelledObjects.mli 1.1 KB 2649   7 years sacerdot
list.ml 9.1 KB 2649   7 years sacerdot
list.mli 3.9 KB 2649   7 years sacerdot
listb.ml 1.1 KB 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
listb.mli 478 bytes 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
lists.ml 2.4 KB 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
lists.mli 964 bytes 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
logic.ml 6.3 KB 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
logic.mli 2.6 KB 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
memoryInjections.ml 5.1 KB 2649   7 years sacerdot
memoryInjections.mli 2.9 KB 2649   7 years sacerdot
memProperties.ml 1.3 KB 2649   7 years sacerdot
memProperties.mli 1006 bytes 2649   7 years sacerdot
monad.ml 20.2 KB 2649   7 years sacerdot
monad.mli 9.5 KB 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
nat.ml 3.2 KB 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
nat.mli 1.2 KB 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
option.ml 1.0 KB 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
option.mli 367 bytes 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
order.ml 2.6 KB 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
order.mli 968 bytes 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
pointers.ml 11.0 KB 2649   7 years sacerdot
pointers.mli 4.5 KB 2649   7 years sacerdot
positive.ml 12.1 KB 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
positive.mli 3.8 KB 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
positiveMap.ml 12.7 KB 2649   7 years sacerdot
positiveMap.mli 4.0 KB 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
preamble.ml 64 bytes 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
preIdentifiers.ml 6.7 KB 2649   7 years sacerdot
preIdentifiers.mli 2.8 KB 2649   7 years sacerdot
PROBLEMS 1.0 KB 2602   7 years piccolo Dead code commented out.
proper.ml 97 bytes 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
proper.mli 97 bytes 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
pts.ml 35 bytes 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
pts.mli 35 bytes 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
registers.ml 645 bytes 2649   7 years sacerdot
registers.mli 564 bytes 2649   7 years sacerdot
relations.ml 324 bytes 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
relations.mli 286 bytes 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
rTLabs_semantics.ml 75.6 KB 2649   7 years sacerdot
rTLabs_semantics.mli 9.8 KB 2649   7 years sacerdot
rTLabs_syntax.ml 30.3 KB 2649   7 years sacerdot
rTLabs_syntax.mli 18.1 KB 2649   7 years sacerdot
russell.ml 104 bytes 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
russell.mli 104 bytes 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
setoids.ml 2.4 KB 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
setoids.mli 1.2 KB 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
sets.ml 81 bytes 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
sets.mli 81 bytes 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
simplifyCasts.ml 28.4 KB 2649   7 years sacerdot
simplifyCasts.mli 4.0 KB 2649   7 years sacerdot
smallstep.ml 16.8 KB 2649   7 years sacerdot
smallstep.mli 7.9 KB 2649   7 years sacerdot
smallstepExec.ml 19.7 KB 2649   7 years sacerdot
smallstepExec.mli 9.8 KB 2649   7 years sacerdot
star.ml 97 bytes 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
star.mli 97 bytes 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
status.ml 251.7 KB 2649   7 years sacerdot
status.mli 17.0 KB 2649   7 years sacerdot
statusProofs.ml 589 bytes 2649   7 years sacerdot
statusProofs.mli 589 bytes 2649   7 years sacerdot
string.ml 890 bytes 2649   7 years sacerdot
string.mli 350 bytes 2649   7 years sacerdot
structuredTraces.ml 61.3 KB 2649   7 years sacerdot
structuredTraces.mli 28.3 KB 2649   7 years sacerdot
switchRemoval.ml 23.3 KB 2649   7 years sacerdot
switchRemoval.mli 7.4 KB 2649   7 years sacerdot
toCminor.ml 92.0 KB 2649   7 years sacerdot
toCminor.mli 14.9 KB 2649   7 years sacerdot
toRTLabs.ml 54.6 KB 2649   7 years sacerdot
toRTLabs.mli 22.1 KB 2649   7 years sacerdot
typeComparison.ml 7.8 KB 2649   7 years sacerdot
typeComparison.mli 1.1 KB 2649   7 years sacerdot
types.ml 14.0 KB 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
types.mli 5.9 KB 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
util.ml 19.5 KB 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
util.mli 5.5 KB 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
utilBranch.ml 398 bytes 2649   7 years sacerdot
utilBranch.mli 313 bytes 2649   7 years sacerdot
values.ml 13.9 KB 2649   7 years sacerdot
values.mli 3.3 KB 2649   7 years sacerdot
vector.ml 14.9 KB 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
vector.mli 5.0 KB 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
z.ml 7.6 KB 2649   7 years sacerdot
z.mli 2.0 KB 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
Note: See TracBrowser for help on using the repository browser.