aboutsummaryrefslogtreecommitdiffstats
path: root/driver/Interp.ml
Commit message (Expand)AuthorAgeFilesLines
* Add -main option to specify entrypoint function in interpreter mode (#374)Xavier Leroy2020-10-301-18/+37
* Cosmetic: in OCaml code, write "open! Module" instead of "open !Module"Xavier Leroy2020-02-211-2/+2
* Refine the type of function results in AST.signatureXavier Leroy2020-02-211-1/+1
* Compatibility with OCaml 4.08 (#302)Xavier Leroy2019-07-081-2/+2
* Remove overriding open in Interp.Bernhard Schommer2017-02-031-11/+11
* driver/Interp: updateXavier Leroy2016-10-241-8/+8
* Allow %lf type specifier in printf.Bernhard Schommer2016-09-221-1/+1
* Fixed issue with emulation of printfBernhard Schommer2016-08-171-2/+4
* Merge branch 'master' into cleanupBernhard Schommer2016-03-211-8/+8
|\
| * Print floating-point numbers with more digits in debug outputsXavier Leroy2016-03-151-2/+2
* | Deactivate warning 27 and added back removed code.Bernhard Schommer2016-03-151-34/+34
* | Code cleanup.Bernhard Schommer2016-03-101-46/+43
|/
* Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-201-6/+6
* Use Coq strings instead of idents to name external and builtin functions.Xavier Leroy2015-10-111-3/+3
* Represent external worlds by a coinductive type rather than an inductive type.Xavier Leroy2015-06-071-1/+1
* Experiment: support a subset of GCC's extended asm statements.Xavier Leroy2015-04-171-1/+1
* Interpreter produces more detailed trace, including name of semantic rules used.Xavier Leroy2015-02-081-95/+61
* Represent struct and union types by name instead of by structure.Xavier Leroy2014-12-221-10/+12
* Introduce symbol environments (type Senv.t) as a restricted view on global en...Xavier Leroy2014-11-261-1/+1
* Add Genv.public_symbol operation.Xavier Leroy2014-11-241-1/+21
* Record public global definitions via field "prog_public" in AST.program.Xavier Leroy2014-11-241-1/+2
* Revised translation of '&&' and '||' to Clight.Xavier Leroy2014-10-131-1/+1
* Merge of "newspilling" branch:xleroy2014-07-231-1/+1
* Error messages were not displayed correctly if the main() function is missing...xleroy2014-03-211-5/+5
* Add option -Os to optimize for code size rather than for execution speed.xleroy2014-02-191-0/+1
* Interp.ml: in the emulation of printf(), check formats against types of argum...xleroy2014-01-121-34/+51
* Better printing of integer literals: add U and LL suffixes when needed.xleroy2014-01-121-1/+1
* Simpler, more robust emulation of calls to variadic functions:xleroy2013-12-281-8/+5
* Revised semantics of external functions, continued:xleroy2013-11-181-22/+36
* Revised modeling of external functions and built-in functions: just axiomatizexleroy2013-11-171-20/+3
* Merge of the "princeton" branch:xleroy2013-06-161-4/+4
* More precise and faster recovery of function name from function or fundef value.xleroy2013-06-081-2/+8
* Merge of the float32 branch: xleroy2013-05-191-0/+1
* Fixes in PowerPC portxleroy2013-04-211-0/+1
* Interp.ml: support printf of long longxleroy2013-04-201-4/+8
* Big merge of the newregalloc-int64 branch. Lots of changes in two directions:xleroy2013-04-201-0/+1
* Improving the performance of exhaustive exploration (mode -all):xleroy2013-03-091-18/+112
* Typo in compare_mem causing merging of different states.xleroy2013-02-021-1/+1
* Ported to Coq 8.4pl1. Merge of branches/coq-8.4.xleroy2013-01-291-4/+2
* Better treatment of volatile accesses in the reference interpreter.xleroy2013-01-081-66/+83
* Update Cminor parser and printer so that the parser can parse the whole Cmino...xleroy2013-01-071-2/+2
* Globalenvs: allocate one-byte block with permissions Nonempty for eachxleroy2012-11-121-23/+32
* Make Clight independent of CompCert C.xleroy2012-10-081-0/+2
* - Revised non-overflow constraints on memory injections so that xleroy2012-07-231-1/+1
* Changelog: updatedxleroy2012-06-281-24/+1
* Use Flocq for floatsxleroy2012-06-281-5/+8
* Merge of the newmem branch:xleroy2012-05-211-0/+8
* Better printing of pointer values and of locations.xleroy2012-02-291-16/+38
* Interp: help debug stuck expressionsxleroy2012-02-101-2/+48
* Merge of the "volatile" branch:xleroy2012-02-041-16/+20
generated by cgit (git 2.34.1) at 2024-05-08 20:10:10 +0000