Le Saturday 06 Aug 2011 à 18:14:14 (+0300), ori bar a écrit :
> Hi, my name is Ori Bar. I've been thinking of the concept of a "more
> formal language with C semantics" for a while and was glad when I
> learned about your project. It is hard to discern from your webpage
> what is your progress (it says the webpage has not been updated since
> 2010?), so I wanted to ask how far have bitc progressed in the last
> year? Also, I wanted to know if you are looking for any assistance
> with BitC, as I would be glad to contribute my time to help with this
> project (I have been programming for several years, in functional
> languages as well, and was working for a while on a lisp-syntax
> C-semantics language). Finally, something that I was thinking of. In
> order to give this kind of a project more traction, I think it would
> be useful if anyone was working on a method to automatically convert
> existing C code (especially libraries) to BitC. Did anyone consider
> this? Possiibly with the conversion tools getting "hints" from a human
> to make the output code readable?
I cannot comment too much on BitC as I do not know it enough for that.
But you may also want to have a look at the ATS language.
http://www.ats-lang.org/
This language is a "more formal language with C semantics" or close to
it. You can almost do anything in C in it, you can keep track at
compile-time of information concerning where a pointer points to, and
it's a functional language that doesn't necessarily need a garbage
collector. Syntactic constructs are, however, not entirely friendly.
If people more knowledgeable could provide a cursory comparison of BitC
features with ATS features, I'd be most happy.
Concerning your question about "automatically converting C code", I've
udertaken a compiler project and this is on my to-do list. There are
tools to gather relevant C-level information, such as CIL or CLang.
http://cil.sourceforge.net/
http://clang-analyzer.llvm.org/
CIL is used in CPC (a tool that makes transformation to C code in order
to provide continuations and cooperative threading) or tools like Why
for annotating and proving stuff about C programs. CIL seems to
currently
live on in the Why and Frama-C projects, but it also seems that CLang
has more traction nowadays.
http://www.pps.jussieu.fr/~jch/software/cpc/
http://why3.lri.fr/
http://frama-c.com/
You also have Elsa for C++, but it's a bit more brittle as C++ is
quite a nightmare to parse and statically analyse.
http://www.scottmcpeak.com/elkhound/
Again, I do not know much about BitC, so I cannot comment, but ATS
provides constructs to import C code with 0 overhead. As it generates C
code, you can even import C macros and declare them as regular
functions. You still need to type it correctly.
So what you would need for your "conversion tool" would be a C parser,
and some type inference system specific to your target languages,
eventually with hints. This seems feasible to implement on top of ATS,
but I'm quite far from that yet.
--
Guillaume Yziquel
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
