C program (input)

QUERY (see also Ctrl page)
memory safety test for "main" (--pre )
./c2lctrs -symshared -char2int <above textarea>
simplification (./ctrl <resulting LCTRS>)


Please don't write the following fragments in input programs.

  • expressions with side effects, e.g., (x++)+2, i = i++;, x++ < 0.
  • nests of function calles
One of the reason to extract above is to avoid compiler-specific semantics, e.g, i = i++;. A student has written i = i++; that behaves as i++; in his/her environment, but in a teacher's environment, the code behaves as { int j = i; j = i; i++; i = j; } (i.e., i = i;).


  • normal form  term
    e.g., normal form sum(10)
  • reduce constrained term  term  [constraint]
    e.g., sum(x) [x < 10]
  • confluence
  • termination
  • equivalence  term1  -><-  term2  [constraint]
    e.g., sum1(x) -><- sum(x) [x > 10]
  • user-equivalence  term1  -><-  term2  [constraint]
    e.g., sum1(x) -><- sum(x) [x > 10]
  • print-simplification [list] or simplification [list]
    e.g., print-simplification [sum]
  • do-simplify  [list] and  action
    e.g., do_simplify [sum] and termination

Memory Safety Test

By selecting memory safety test, a program is translated into an LCTRS with rules for errortest and a query for memory safety test equivalence errortest(main(...)) -><- true [precondition]. A precondition for the test can be specified.

When selecting memory safety test, the generated LCTRS is not simplified while it is shown in Generated LCTRS (simplified version).

Generated LCTRS

./ctrl <above textarea> timeout:  

Result of Ctrl


  • The current web interface doesn't work for the execution of ctrl, which takes a few seconds, e.g., a query with equivalence. In such a case, it is recommended to run Ctrl on a local environment.