Test/triggers/triggers-prevent-some-inlining.dfy


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26

// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t"
// RUN: %diff "%s.expect" "%t"

// This  file looks  at the  interactions  between inlining  and triggers.   The
// sum_is_sum predicate gets a {sum(a,  b)} trigger, which explicitly depends on
// one of the  variables being passed in. Since triggers  are generated prior to
// inlining  (inlining  happens  during  translation),  inlining  the  last  two
// instances of that call below would cause  b+1 (a trigger killer) to pop up in
// a trigger.   This would create  an invalid trigger,  so Dafny doesn't  let it
// happen.

function sum(a: int, b: int): int {
  a + b
}

predicate sum_is_sum(b: int, c: int) {
  forall a: int :: sum(a, b) + c == a + b + c
}

method can_we_inline(b: int, c: int)
  ensures sum_is_sum(0, 0)     // OK  to inline
  ensures sum_is_sum(b, c)     // OK  to inline
  ensures sum_is_sum(b, c+1)   // OK  to inline
  ensures sum_is_sum(b+1, c)   // NOK to inline
  ensures sum_is_sum(b+1, c+1) // NOK to inline
{ }