c2lctrs: a converter of C programs to LCTRSs

Ver. 1.1.5

News

September 30th, 2016 (Version 1.1.5)

Fixed a bug to compute "LOGIC" for assignment of arrays, e.g., a[i] = ...;.

Adapted to the lack of "return" statements.

Improved WUI and added a button for the execution of ctrl.

September 21st, 2016 (Version 1.1.4)

Revised the combination of logics: NIA and QF_INTARRAY are combined as QF_INTARRAY.

Revised an error message for the existence of undeclared variables and functions.

Adapted to both ITE operator ( ? : ) and conversion of formulas in arithmetic expressions, e.g., (x > 1 + 2 is converted to (x > 1 ? 1 : 0) + 2.

September 16th, 2016 (Version 1.1.3)

The option for memory safety test of "main" funciton was introduced.

Improved WUI by adding the option for memory safety test to execution of c2lctrs.

September 15th, 2016

Improved WUI by adding some options to execution of c2lctrs.

Show compiler-specific behaviours in detail.

August 9th, 2016

Improved WUI.

Added comments on compiler-specific fragments.

January 5th, 2016

Started to provide a downloaded version.

Contents

• Web interface
• Downloads
• Input files
• Third party libraries
• References
• Contact

Please click here. WUI is now provided via another windows.

• c2lctrs 1.1.5 (source)

C programs which are successfully compiled are converted to LCTRSs (see [KN13]), while C programs are limited to a subclass and the implementation has not been completely adapted to the formalization in the document yet (see [KNF15] and [KN15]).

Example

int sum(int x){
  int i = 0;
  int z = 0;
  while( i <= x ){
    z = z + i;
    i = i + 1;
  }
  return z;
}

The current transformation does not admit compiler-specific fragment, e.g., (x++)+2. For this reason, the current tool does not allow us to write any expression with side effect, that cannot be transformed into any assignment without side effect, and nests of function calls. Such fragments can be avoided by transforming them into corresponding ones by hand. For example, x = (x++)+2 can be replaced by { int tmp; tmp = x; x++; x = tmp+2; } and x = f(f(x)); by { int tmp; tmp = f(x); x = f(tmp); }. We will adapt the tool to such fragments by specifying a compiler (and its options) in the future. New!

c2lctrs interfaces the following tools:

FrontC (version 3.4.2) for parsing C

cparser.mly was modified to accept e.g., for(int i=0 ; i<n ; i++) ... since version 1.1.0 (the detail can be seen in the downloadable sources).

Ctrl (WUI only) for simplifying LCTRSs.

[KNF15]

Cynthia Kop, Naoki Nishida, and Carsten Fuhs,
Verifying Procedural Programs via Constrained Rewriting Induction,
will be submitted to a journal soon (and the pre-submission version will be available soon).

[KN15]

Cynthia Kop and Naoki Nishida,
Converting C to LCTRSs,
[PDF]

[KN14]

Cynthia Kop and Naoki Nishida,
Automatic Constrained Rewriting Induction towards Verifying Procedural Programs,
In Proceedings of the 12th Asian Symposium on Programming Languages and Systems (APLAS 2014),
Lecture Notes in Computer Science, vol. 8858, pp. 334-353, November 2014.
Available from Springer or Ctrl's website.

[KN13]

Cynthia Kop and Naoki Nishida,
Term Rewriting with Logical Constraints,
In Proceedings of the 9th International Symposium on Frontiers of Combining Systems (FroCoS 2013),
Lecture Notes in Artificial Intelligence, vol. 8152, pp. 343-358, September 2013.
Available from Springer or Ctrl's website.

Naoki Nishida (Nagoya University)

nishida @ is.nagoya-u.ac.jp