tis-interpreter
c-semantics
| tis-interpreter | c-semantics | |
|---|---|---|
| 2 | 4 | |
| 561 | 301 | |
| 0.0% | 0.7% | |
| 10.0 | 1.8 | |
| over 7 years ago | over 2 years ago | |
| OCaml | C | |
| - | GNU General Public License v3.0 or later |
Stars - the number of stars that a project has on GitHub. Growth - month over month growth in stars.
Activity is a relative number indicating how actively a project is being developed. Recent commits have higher weight than older ones.
For example, an activity of 9.0 indicates that a project is amongst the top 10% of the most actively developed projects that we are tracking.
tis-interpreter
- The C Bounded Model Checker: Criminally Underused
-
GCC always assumes aligned pointer accesses
What makes you think they don't understand it? They acknowledge that it is UB. I read them as realistic, since they know that people rely on C compilers work in a certain way. They even wrote an interpreter that detects UB: https://github.com/TrustInSoft/tis-interpreter
I understand why people like the compiler being able to leverage UB. I suspect this philosophy actually makes Trust-In-Soft more money: You could argue that if there was no UB, there would be no need for the tis-interpreter.
So isn't it in fact quite self-less that they encourage the world to optimize a bit less (spending more money on 'compute'), while standing to profit from the unintended behaviour they'd otherwise be contracted to help debug?
c-semantics
- The C Bounded Model Checker: Criminally Underused
-
Soufflé: A Datalog Synthesis Tool for Static Analysis
https://github.com/kframework/c-semantics while you can do static analysis with this the dynamic instrumentation of UB isnfar more thorough than ubsan
-
Mildly Interesting Quirks of C
> "Who Says C is Simple?"
People who don't know what "simple" means and confuse it with "easy".
https://www.entropywins.wtf/blog/2017/01/02/simple-is-not-ea...
https://www.infoq.com/presentations/Simple-Made-Easy/
"Easy" things almost always lead to astonishing complexity.
Also it's easy to see just how complex C is: Have a look at a formal description of it! (And compare to a truly simple language like e.g. LISP).
https://github.com/kframework/c-semantics/tree/master/semant...
In contrast some basic Lambda calculus language semantics fit 0.5 of a pages in K.
https://www.youtube.com/watch?v=eSaIKHQOo4c
https://www.youtube.com/watch?v=y5Tf1EZVj8E
-
Programming language for high performance simulations. Is there anything like this already?
I stopped working on it in 2012, but people have continued working on it since then. The current repository is at https://github.com/kframework/c-semantics, but it includes stuff in addition to C; people have started adding C++ semantics as well.
What are some alternatives?
chibicc - A small C compiler
cclyzerpp - cclyzer++ is a precise and scalable pointer analysis for LLVM code.
cbmc - C Bounded Model Checker
taichi - Productive, portable, and performant GPU programming in Python.
coreHTTP - Client implementation of a subset of HTTP 1.1 protocol designed for embedded devices.
bakeware - Compile Elixir applications into single, easily distributed executable binaries
dmd - dmd D Programming Language compiler
kani - Kani Rust Verifier
percival - 📝 Web-based, reactive Datalog notebooks for data analysis and visualization
Halide - a language for fast, portable data-parallel computation
terra - Terra is a low-level system programming language that is embedded in and meta-programmed by the Lua programming language.