source: driver

Name Size Rev Age Author Last Change
../
tests 3073   6 years sacerdot New extraction, all tests pass.
extracted 3106   6 years sacerdot New extraction.
rTLabsPrinter.mli 205 bytes 3000   6 years tranquil added RTLabs printer
rTLabsPrinter.ml 9.9 KB 3014   6 years tranquil ERTL to ERTLptr pass suppressed (it introduced a bug in the later …
printer.mli 87 bytes 2993   6 years sacerdot 1. performance improved: the type inference was inferring …
printer.ml 10.8 KB 3079   6 years tranquil added printing of ERTL, LTL and LIN's ext_seq's.
optionsParsing.ml 356 bytes 3005   6 years sacerdot Beginning of making it fully compatible with untrusted one.
options.mli 2.1 KB 3020   6 years sacerdot - Options not used removed from the help/interface. - More compliance …
options.ml 5.4 KB 3020   6 years sacerdot - Options not used removed from the help/interface. - More compliance …
Makefile 960 bytes 3094   6 years sacerdot Makefile with targets: byte opt clean
IntelHex.mli 267 bytes 2856   7 years sacerdot Pretty printing of LTL almost finished.
IntelHex.ml 9.7 KB 2780   7 years sacerdot Bug fixed: in BitVector?.ma the functions bv_to_nat and nat_to_bv were …
error.ml 3.0 KB 2960   6 years sacerdot New extraction, it diverges in RTL execution now.
dist 159 bytes 3090   6 years tassi dist: take into account symlink
cparser 39 bytes 3089   6 years sacerdot Symbolic link to the cparser
clightPrinter.mli 929 bytes 3091   6 years sacerdot
clightPrinter.ml 22.4 KB 3083   6 years sacerdot The cost and stack* variables are now initialized with the cost of …
clightParser.mli 373 bytes 2620   7 years campbell Sufficient hacking to run the extracted Clight semantics.
clightParser.ml 1.7 KB 3013   6 years sacerdot Temporary parsing files removed.
clightFromC.ml 31.8 KB 2790   7 years campbell Some null handling in conversion from CIL.
ASMPrinter.mli 131 bytes 2999   6 years sacerdot code_memory added to labelled_object_code to avoid recomputing it …
ASMPrinter.ml 223 bytes 2999   6 years sacerdot code_memory added to labelled_object_code to avoid recomputing it …
acc.ml 3.6 KB 3083   6 years sacerdot The cost and stack* variables are now initialized with the cost of …
Note: See TracBrowser for help on using the repository browser.