Previous week Up Next week

Hello

Here is the latest Caml Weekly News, for the week of September 19 to 26, 2006.

  1. Module dependencies of bytecode executables
  2. BrainScan - A source-code model checker for BrainF*ck

Module dependencies of bytecode executables

Archive: http://groups.google.com/group/fa.caml/browse_thread/thread/b296635c88b2ef87/87bd46a60b5d4d51#87bd46a60b5d4d51

Samuel Mimram asked and Xavier Leroy answered:
> Is it somehow possible to extract the list of modules used by a bytecode 
> executable? "ocamldumpobj a.out | grep SETGLOBAL" seems to be a good 
> starting point but I don't know if it's reliable. 

It is reliable. 
> Are the md5sums of the imported interfaces still available? 

Yes, these are saved in the bytecode executable, section "CRCS", 
but there are no tools in the distrib that will list this info for you. 
> Also, how can I determine which *.so will be dlopened by the executable? 

Run the executable with OCAMLRUNPARAM=v=256, this will print debug 
messages during shared library loading, including names and 
locations of these libraries.
			

BrainScan - A source-code model checker for BrainF*ck

Archive: http://groups.google.com/group/fa.caml/browse_thread/thread/9a34dc863f286c55/1cb9483c0fda7f08#1cb9483c0fda7f08

Yoriyuki Yamagata announced:
BrainScan is a simple source-code model checker for BrainF*ck.  It 
uses depth-first search with states in the buffer cells represented as 
sets of integer intervals. 
To compile, you need OCaml, findlib, and extlib. 
$ make 
This create a binary called brainscan.  Then you can give BrainF*ck 
program as the argument. 

$ ./brainscan '+[]!' 
$ 

BrainScan checks the following condition and prints the command trace 
if such conditions could arise. 

1. Underflow of the pointer 
2. Overflow (> 255) and Underflow (<0) of a buffer-cell value.  (Only 
with -R or --range option.) 
3. Reach the positions marked by ! 

In the case above, the program infinitely loops between [ and ]. 
Hence it never reaches !.  BrainScan understands this, and terminates 
without error messages.  On the other hand, 

$ ./brainscan ',[]!' 
! reached. 
        0: , 
        1: [ 
        3: ! 

this program may reach ! depending on the input at the ",". 

Enjoy!
			
Yoriyuki Yamagata then added:
I forgot the URL.  You can obtain BrainScan from 
http://www15.ocn.ne.jp/~rodinia/brainscan.tar.gz
			

Using folding to read the cwn in vim 6+

Here is a quick trick to help you read this CWN if you are viewing it using vim (version 6 or greater).

:set foldmethod=expr
:set foldexpr=getline(v:lnum)=~'^=\\{78}$'?'&lt;1':1
zM

If you know of a better way, please let me know.


Old cwn

If you happen to miss a CWN, you can send me a message and I'll mail it to you, or go take a look at the archive or the RSS feed of the archives.

If you also wish to receive it every week by mail, you may subscribe online.


Alan Schmitt