Issue 54 in teyjus: A trailing "true" in a clause cause a segmentation fault.

[tey...@googlecode.com]

Status: Accepted
Owner: dale.a.m...@gmail.com

New issue 54 by dale.a.m...@gmail.com: A trailing "true" in a clause cause
a segmentation fault.
http://code.google.com/p/teyjus/issues/detail?id=54

It seems that compiling a clause of the form

r :- 1 = 1, true.

yields code that produces a segmentation fault when one attempts to prove
r. Removing the trailing "true" fixes the problem. I attach a simple mod
and sig file for illustrating this problem. Specifics of my system are
below. -Dale

$ tjcc -v
Teyjus version 2.0-b1
$ uname -a
Linux alonzo 2.6.32-34-generic #77-Ubuntu SMP Tue Sep 13 19:40:53 UTC 2011
i686 GNU/Linux
$

Attachments:
bug.mod 273 bytes
bug.sig 40 bytes

[tey...@googlecode.com]

Comment #1 on issue 54 by fafou...@gmail.com: A trailing "true" in a clause

cause a segmentation fault.
http://code.google.com/p/teyjus/issues/detail?id=54

The following patch seems to do the job (adding a last proceed is what was
done in Teyjus 1):

svn diff source/compiler/clausegen.ml
@@ -1830,9 +1848,10 @@
let (inst, size) =
if (last) then
if (Absyn.getClauseHasEnv cl) then
- ([Instr.Ins_deallocate], Instr.getSize_deallocate)
+ ([Instr.Ins_deallocate ; Instr.Ins_proceed],
+ Instr.getSize_deallocate + Instr.getSize_proceed)

The number of tests checked remains the same.

Fabien

[tey...@googlecode.com]

Updates:
Owner: fafo...@gmail.com
Cc: gopalan....@gmail.com

Comment #2 on issue 54 by fafo...@gmail.com: A trailing "true" in a clause

cause a segmentation fault.
http://code.google.com/p/teyjus/issues/detail?id=54

Gopalan, do you agree that a "proceed" should follow the deallocate as in
Teyjus 1?

--
You received this message because this project is configured to send all
issue notifications to this address.
You may adjust your notification preferences at:
https://code.google.com/hosting/settings