C Semantics in K Framework

[Chucky Ellison <celliso2 AT illinois.edu>]

Ok, I've added an issue so I don't forget.  I'll see what I can do.

Also, just leave out the GRAPH option and it should be disabled.  You
can also disable an option by setting it to nothing, e.g.,
SEARCH=1 GRAPH= ./a.out

the GRAPH option is just for the .pdf and .ps generation though.

Thanks Derek,
-Chucky

On Fri, Jun 17, 2011 at 7:18 AM, Derek M Jones 
<derek AT knosof.co.uk>
 wrote:
> 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
> _______________________________________________
> c-semantics mailing list
> c-semantics AT cs.illinois.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/c-semantics
>