C Semantics in K Framework

[Derek M Jones <derek AT knosof.co.uk>]

Chucky,

> The tmpSearchResults.txt is the raw search graph.  This has to get
> generated for me to create the summaries, like the one I print to the
> screen just showing final states.  However, I might be able to process

A lot of this information appears to be present right at the start of
the tmp... file, it looks like it just needs some reformatting.

I have tried (not very hard) to switch off graph production.
Using GRAPH=0 did not have the desired effect.
graphviv is installed on my machine, but I have not configured
c-semantics to use it and so get lots of error messages.

> it on the fly so there is no file generated.  Is that an option you'd
> be interested in?

It would enable me to try larger values of fib.  Not a particularly
good reason, but others might have filesize problems with more
realistic programs.

> -Chucky
>
> On Thu, Jun 16, 2011 at 9:43 PM, Derek M 
> Jones<derek AT knosof.co.uk>
>   wrote:
> > Chucky,
> >
> >   >>  Did you specify the '-n' option when you compiled?
> >
> > No, but I was thinking very hard that I wanted a complete search :-O
> >
> > > I should add, it really helps to use the -s option as well.  There is
> > > still some nondeterminism kicking around when in linking in the
> > > standard library.  Using the -s option brings the search time down
> > > from 50s to 20 seconds for me.
> >
> > The -s option also reduced the 1.1G tmpSearchResults.txt file by around
> > 70%, obtained when incrementing x to the next 'fib' number.
> >
> > Is there a way to summarise the contents of tmpSearchResults.txt
> > without having to generate it?
> >
> > > I'll have to look in to it to see if that nondeterminism is necessary
> > > or if it's just slowing things down.
> > >
> > > When the tests finish running and the version gets tagged, r826 should
> > > contain fixes to any spurious "you need to run with -n option"
> > > warnings that were being generated, even if you used the -n option.
> > >
> > > -Chucky
> > >
> > > On Thu, Jun 16, 2011 at 9:02 PM, Chucky 
> > > Ellison<celliso2 AT illinois.edu>
> > >     wrote:
> > > > Unless I'm missing something more subtle, it seems to work for me.
> > > > Did you specify the '-n' option when you compiled?  This is the only
> > > > way SEARCH will return a complete search.  I've attached the .pdf
> > > > graph it generates as well.
> > > >
> > > > $ kcc -n fib.c
> > > > $ ./a.out
> > > > fib = 4
> > > > $ SEARCH=1 GRAPH=1 ./a.out
> > > > Performing the search...
> > > > Generated tmpSearchResults.txt
> > > > Examining the output...
> > > > ========================================================================
> > > > 7 solutions found
> > > > ------------------------------------------------------------------------
> > > > Solution 1
> > > > Program completed successfully
> > > > Return value: 0
> > > > Output:
> > > > fib = 4
> > > > ------------------------------------------------------------------------
> > > > Solution 2
> > > > Program completed successfully
> > > > Return value: 0
> > > > Output:
> > > > fib = 5
> > > > ------------------------------------------------------------------------
> > > > Solution 3
> > > > Program completed successfully
> > > > Return value: 0
> > > > Output:
> > > > fib = 6
> > > > ------------------------------------------------------------------------
> > > > Solution 4
> > > > Program completed successfully
> > > > Return value: 0
> > > > Output:
> > > > fib = 7
> > > > ------------------------------------------------------------------------
> > > > Solution 5
> > > > Program completed successfully
> > > > Return value: 0
> > > > Output:
> > > > fib = 8
> > > > ------------------------------------------------------------------------
> > > > Solution 6
> > > > Program completed successfully
> > > > Return value: 0
> > > > Output:
> > > > fib = 9
> > > > ------------------------------------------------------------------------
> > > > Solution 7
> > > > Program completed successfully
> > > > Return value: 0
> > > > Output:
> > > > fib = 10
> > > > ========================================================================
> > > > 7 solutions found
> > > >
> > > > Generated tmpSearchResults.dot.
> > > > Generating graph...
> > > > Generated tmpSearchResults.ps.
> > > > Generated tmpSearchResults.pdf
> > > >
> > > >
> > > > -Chucky
> > > >
> > > > On Thu, Jun 16, 2011 at 7:26 PM, Derek M 
> > > > Jones<derek AT knosof.co.uk>
> > > >     wrote:
> > > > > Chucky,
> > > > >
> > > > > No programming system is complete without being able
> > > > > to generate the Fibonacci sequence.
> > > > >
> > > > > I was expecting some different orders of evaluation in the
> > > > > following, even if the number of orders is not yet the Fibonacci
> > > > > sequence.
> > > > >
> > > > > #include<stdio.h>
> > > > > int x;
> > > > >
> > > > > int fib(void)
> > > > > {
> > > > > x--;
> > > > > if (x<= 1)
> > > > >      return 1;
> > > > > else
> > > > >      return x + fib();
> > > > > }
> > > > >
> > > > > int main(void)
> > > > > {
> > > > > x=4+1;
> > > > > printf("fib = %dn", fib());
> > > > > }
> > > > >
> > > > >
> > > > > --
> > > > > Derek M. Jones                         tel: +44 (0) 1252 520 667
> > > > > Knowledge Software Ltd                 
> > > > > mailto:derek AT knosof.co.uk
> > > > > Source code analysis                   http://www.knosof.co.uk
> > > > > _______________________________________________
> > > > > c-semantics mailing list
> > > > > c-semantics AT cs.illinois.edu
> > > > > http://lists.cs.uiuc.edu/mailman/listinfo/c-semantics
> >
> > --
> > Derek M. Jones                         tel: +44 (0) 1252 520 667
> > Knowledge Software Ltd                 
> > mailto:derek AT knosof.co.uk
> > Source code analysis                   http://www.knosof.co.uk
> > _______________________________________________
> > c-semantics mailing list
> > c-semantics AT cs.illinois.edu
> > http://lists.cs.uiuc.edu/mailman/listinfo/c-semantics

--
Derek M. Jones                         tel: +44 (0) 1252 520 667
Knowledge Software Ltd                 
mailto:derek AT knosof.co.uk
Source code analysis                   http://www.knosof.co.uk