From f538b4dba3be5eb15b9e03de468ccb2b41a520dc Mon Sep 17 00:00:00 2001 From: rlar Date: Sat, 7 Nov 2015 20:22:42 +0100 Subject: [PATCH] frontend/define.c, ntharg(), #4/15 express some facts --- src/frontend/define.c | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/frontend/define.c b/src/frontend/define.c index a2f30e133..0a40ce7a8 100644 --- a/src/frontend/define.c +++ b/src/frontend/define.c @@ -407,8 +407,10 @@ trcopy(struct pnode *tree, char *args, struct pnode *nn) static struct pnode * ntharg(int num, struct pnode *args) { + // fact: num >= 1 for all known invocations of ntharg() while (--num > 0) { if (args && args->pn_op && (args->pn_op->op_num != PT_OP_COMMA)) { + // fact: num >= 1 because of `while' condition if (num == 1) break; return NULL;