SMT solvers write the weirdest programs. Wanna Jump? Simple: Just set the interrupt vector and then execute an illegal instruction.
-
-
Replying to @oe1cxw @whitequark
I understand what an SMT solver is, but in what context do they generate code?
2 replies 0 retweets 1 like -
in this case I believe it's formal verification of a CPU core
1 reply 0 retweets 6 likes -
Replying to @whitequark
do you have insider information? if you don't and this is a guess, please register me as betting on “superoptimizer” please
2 replies 0 retweets 1 like -
Replying to @rep_stosq_void
I've never heard of optimizers understanding ISRs and I've never seen Clifford work on non-HDL compilers
1 reply 0 retweets 1 like -
Replying to @whitequark
Some non-HLD compilers I wrote: http://www.clifford.at/spl/ http://www.clifford.at/bfcpu/bfcomp.html … http://www.openscad.org/ http://www.clifford.at/embedvm/
2 replies 0 retweets 1 like -
Replying to @oe1cxw @whitequark
The embedvm tutorial video you have is really cool, especially the end where A Certain Song plays...
1 reply 0 retweets 1 like
Of all web videos with bad lighting this one is the worst! :) And that beard that I had for a short time in 2011..
Like my evil twin..
-
-
Replying to @oe1cxw
I was looking to port embedvm to msp430 for fun in early August, but it fell by the wayside when trying to balance projects :P
0 replies 0 retweets 1 likeThanks. Twitter will use this to make your timeline better. UndoUndo
-
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.