 |
C++Talk.NET
C++ language newsgroups
|
| View previous topic :: View next topic |
| Author |
Message |
rramanujam@gmail.com
Guest
|
 Posted: Thu Nov 24, 2005 5:14 pm Post subject: Equivalence Checing Tool for C/C++ |
 |
|
Is anybody aware of a tool that can check whether 2 C/C++ codes are
equivalent by doing static checks
[ See http://www.gotw.ca/resources/clcm.htm for info about ]
[ comp.lang.c++.moderated. First time posters: Do this! ]
|
|
| Back to top |
|
 |
Ira Baxter
Guest
|
| Posted: Sun Nov 27, 2005 5:50 pm Post subject: Re: Equivalence Checing Tool for C/C++ |
|
|
<rramanujam (AT) gmail (DOT) com> wrote
| Quote: |
Is anybody aware of a tool that can check whether 2 C/C++ codes are
equivalent by doing static checks
|
There's a theorem that says you can't do this in general.
I suspect it is pretty hard in practice, and you'd need
one hell of a theorem prover.
What you can do is to verify that one code is probably
a cut-n-paste copy of another, by matching program
parses of program source codes.
See http://www.semdesigns.com/Products/Clone/index.html
--
Ira D. Baxter, Ph.D., CTO 512-250-1018
Semantic Designs, Inc. www.semdesigns.com
[ See http://www.gotw.ca/resources/clcm.htm for info about ]
[ comp.lang.c++.moderated. First time posters: Do this! ]
|
|
| Back to top |
|
|
Gene Bushuyev
Guest
|
| Posted: Sun Nov 27, 2005 9:53 pm Post subject: Re: Equivalence Checing Tool for C/C++ |
|
|
<rramanujam (AT) gmail (DOT) com> wrote
| Quote: |
Is anybody aware of a tool that can check whether 2 C/C++ codes are
equivalent by doing static checks
|
There is no such tool. Though theoretically it's possible to check equivalence
of any two FSMs, in practice it only works when the number of collapsed states
(e.g. BDD nodes) is relatively small. Look for the papers on reachability
analysis for explanation of the theory.
Relatively simple FSMs, like event-driven transaction models can be verified.
It's an interesting exercise to write an equivalence checker for two parser
implementations. But general software applications have too many states for any
general purpose tool to be viable.
-- Gene Bushuyev
----------------------------------------------------------------
There is no greatness where there is no simplicity, goodness and truth. ~ Leo
Tolstoy
[ See http://www.gotw.ca/resources/clcm.htm for info about ]
[ comp.lang.c++.moderated. First time posters: Do this! ]
|
|
| Back to top |
|
|
ben
Guest
|
| Posted: Mon Nov 28, 2005 4:28 pm Post subject: Re: Equivalence Checing Tool for C/C++ |
|
|
[email]rramanujam (AT) gmail (DOT) com[/email] wrote:
| Quote: | Is anybody aware of a tool that can check whether 2 C/C++ codes are
equivalent by doing static checks
|
No general tool I know of can perform this equivalence check.
In order to prove that two pieces of code are equivalent you need to
feed them with all possible inputs and compare their outputs. This, of
course, is specific to the code itself. Given the complexity of today's
commercial software, it is nearly impossible to do that because there
are simply too many combinations of inputs.
Ben
[ See http://www.gotw.ca/resources/clcm.htm for info about ]
[ comp.lang.c++.moderated. First time posters: Do this! ]
|
|
| Back to top |
|
|
Jeffrey Schwab
Guest
|
| Posted: Mon Nov 28, 2005 9:07 pm Post subject: Re: Equivalence Checing Tool for C/C++ |
|
|
ben wrote:
| Quote: | rramanujam (AT) gmail (DOT) com wrote:
Is anybody aware of a tool that can check whether 2 C/C++ codes are
equivalent by doing static checks
No general tool I know of can perform this equivalence check.
In order to prove that two pieces of code are equivalent you need to
feed them with all possible inputs and compare their outputs.
|
Not quite true. What you have described would not, by definition, be a
"static check." In the processor design industry, it is common to use
symbolic logic to establish the formal equivalency of different
"models." Synopsys is probably the most popular vendor of formal
equivalency tools:
http://synopsys.com/products/solutions/discovery/func_checking/func_checking.html
These techniques are all about mapping state points between different
models. Usually, the models are written in Verilog or VHDL, which are
very special-purpose languages. However, Mentor Graphics (who are
competitive with Synopsys) seem to be pushing the use of C++ as an
alternative to traditional hardware design languages, at least for
synthesis tools:
http://www.mentor.com/products/c-based_design/catapult_c_synthesis/index.cfm
[ See http://www.gotw.ca/resources/clcm.htm for info about ]
[ comp.lang.c++.moderated. First time posters: Do this! ]
|
|
| Back to top |
|
|
|
|
You cannot post new topics in this forum
You cannot reply to topics in this forum
You cannot edit your posts in this forum
You cannot delete your posts in this forum
You cannot vote in polls in this forum
|
|
FAQ
Search
Memberlist
Usergroups
Register
Profile
Log in to check your private messages
Log in
