diff options
| author | Brian Campbell | 2019-04-17 18:30:40 +0100 |
|---|---|---|
| committer | Brian Campbell | 2019-04-17 18:30:49 +0100 |
| commit | 9e0f58f27966bf606bdc3ec06972bc294fbd362b (patch) | |
| tree | 1fbc86b26f9e948f8b462721c88677257c2fc8a0 /test | |
| parent | ba9894513af0c9b122be0af1afce37ef52d49116 (diff) | |
Coq: support pure loops with termination measures
Diffstat (limited to 'test')
| -rw-r--r-- | test/coq/pass/while_PP_terminating.sail | 2 | ||||
| -rw-r--r-- | test/coq/skip | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/test/coq/pass/while_PP_terminating.sail b/test/coq/pass/while_PP_terminating.sail index 00a4450b..80840ac9 100644 --- a/test/coq/pass/while_PP_terminating.sail +++ b/test/coq/pass/while_PP_terminating.sail @@ -11,3 +11,5 @@ function test n : int -> int = { }; j } + +termination_measure test while n - i diff --git a/test/coq/skip b/test/coq/skip index a4be9719..259df4b0 100644 --- a/test/coq/skip +++ b/test/coq/skip @@ -49,5 +49,3 @@ while_PM.sail while_PP.sail XXXXX Not yet - haven't decided whether to support register reads in measures while_MM_terminating.sail -XXXXX Not yet - haven't arranged for lifting pure loops into the monad (or proving termination outright) yet -while_PP_terminating.sail |