lks9 / src-tracer

Other
0 stars 0 forks source link

Nested ghost code #37

Closed lks9 closed 1 year ago

lks9 commented 1 year ago

Currently, an exception "Nested ghosts are currently not supported" is raised in the retracer. The idea is to skip evaluation of nested ghost code.

We don't want to check assertions within another assertion check, outside of the trace. Assertions are currently translated into ghost code blocks.

Example:

int foo (void) {
    ASSERT( 1 == 1 );
    return 42;
}
void bar (void) {
    ASSERT( foo() == 42 );
}