Newbie questions about Pliant

Newbie questions about Pliant

On debugging

I am trying to understand how Pliant's debugging instructions
work.
Message posted by maybe Marcus on 2003/03/27 14:59:36
When running the program below, I get no error messages:

function foo y -> z
  arg Int y z
  z := y
  ensure
    z<0

funfunction foo y -> z
  arg Int y z
  z := y
  ensure
    z<0

function test
  foo 1

test

But when I run this other one, I get the expected error message:

function foo y -> z
  arg Int y z
  require
    true
  z := y
  ensure
    z<0

function test
  foo 1

test

I wonder if the 'ensure' needs a 'require' to work. Because the program below 
also works as expected:

function foo y -> z
  arg Int y z
  require
    y < 0 
  z := y

function test
  foo 1

test

Message posted by maybe Marcus on 2003/03/27 15:08:24
Sorry for the typo in my previous posting. My mouse is pasting things
twice when I mark sth and they paste with the middle button...

Anyway, my first program is actually:

function foo y -> z
  arg Int y z
  z := y
  ensure
    z<0

function test
  foo 1

test
Message posted by hubert.tonneau on 2003/03/27 15:45:09
There is no need to specify 'require' in order to use 'ensure'.

The bug seems related to 
      gc insert_at_section_bottom section_terminate (a map Instruction)
in function 'optimize_incorporate_ensure' in module /pliant/language/debug/dbc.pli
and I'll try to finish tracking it as soon as possible.

Anyway, the bug in your code appends because your fonction is mostly empty.
In any significant fonction, it would work.