Commit graph

6 commits

Author SHA1 Message Date
Leonardo de Moura
04b67f8b14 refactor(kernel/object): remove 'null' object, and operator bool for kernel objects
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-08 14:37:38 -08:00
Leonardo de Moura
74dfdd02de feat(util): add primitives for checking the amount of available stack space
Recursive functions that may go very deep should invoke the function check_stack. It throws an exception if the amount of stack space is limited.

The function check_system() is syntax sugar for
    check_interrupted();
    check_stack();

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-01 17:19:27 -08:00
Leonardo de Moura
b41789d085 feat(kernel): add is_bool predicate
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-26 11:34:50 -08:00
Leonardo de Moura
2141ee12f4 refactor(frontends/lean): use extension objects to store lean default frontend data in the environment
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-07 10:00:12 -08:00
Leonardo de Moura
d843d432d3 refactor(kernel): move printer and formatter objects to the kernel
The printer and formatter objects are not trusted code.
We moved them to the kernel to be able to provide them as an argument to the trace objects.
Another motivation is to eliminate the kernel_exception_formatter hack.
With the formatter in the kernel, we can implement the pretty printer for kernel exceptions as a virtual method.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-22 08:15:36 -07:00
Leonardo de Moura
6fc177056e refactor(tests/frontends/lean): use consistent name convention for file names
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-27 09:59:50 -07:00
Renamed from src/tests/frontends/lean/lean_frontend.cpp (Browse further)