The Coq mailing list

[Georgi Guninski <guninski AT guninski.com>]

hi,

what do you mean by "stack overflow" - too much recursion resulting in
stack exhaustion or smashing the stack due to overflow?

on latest coqtop your testcase would apear to corrupt the stack
 if gdb is correct:

gdb coqtop
<your code
Program received signal SIGSEGV, Segmentation fault.
0x00007ffff68886ab in camlCcalgo__find_aux_1050 ()
   from /home/blah/local/lib/coq/plugins/cc/cc_plugin.cmxs
   (gdb) bt
   #0  0x00007ffff68886ab in camlCcalgo__find_aux_1050 ()
      from /home/blah/local/lib/coq/plugins/cc/cc_plugin.cmxs
      Cannot access memory at address 0x7fffff5feff0


if the last message is real it is hacker's dream (not counting the plugin
feature of coq) :)

On Wed, May 25, 2011 at 05:33:21PM +0200, David Baelde wrote:
> OCaml applications compiled to native code may cause segmentation
> faults as a result of stack overflows. I have experienced this,
> including with Coq, for which I have a file that causes sigsegv or
> stack overflow depending on the coq/ocaml versions:
> 
> Require Export Bvector.
> Notation BVfalse := (Vconst bool false).
> Goal forall n (a b : bool) (v : Bvector n),
>       Vcons _ a n v = Vcons _ b n (BVfalse n) -> v = BVfalse n.
> Proof.
>   intros.
>   assert (v = BVfalse n) by congruence.
> 
> Cheers,
> -- 
> David