[Termtools] Complexity of C programs: some issues

[aeflores]

Dear all,

I noticed some of the benchmarks for the complexity of C programs have a 
single function with no parameters. Instead, the "parameters" are 
assigned with a call to the function __VERIFIER_nondet_int(). The 
simplest example of this is *test/C_Integer/Stroeder_15/WhileDecr.c:*

typedef enum {false,true} bool;

extern int __VERIFIER_nondet_int(void);

int main() {
     int i;
     i = __VERIFIER_nondet_int();

     while (i > 5) {
         i = i-1;
     }

     return 0;
}

I imagine that these examples come from the termination benchmarks where 
this is irrelevant, but I believe that the complexity of a function 
should be in terms of the input parameters, shouldn't it? As it is, the 
complexity of *WhileDecr.c *in terms of the input parameters is not defined.

Surprisingly, Loopus finds assigns a linear complexity to this example. 
I guess it assumes the return of __VERIFIER_nondet_int() as an input 
parameter...

We could adapt these examples for complexity by adding the relevant 
variables as parameters: "int main(int i)...". Other examples in which I 
noticed this  (there might be more) are:

AliasDarteFeautrierGonnord-SAS2010-wcet2_true-termination.c
CookSeeZuleger-TACAS2013-Fig8a-modified_true-termination.c
NoriSharma-FSE2013-Fig7_true-termination.c
svcomp_b.18.c

Best regards,


Antonio

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.lri.fr/pipermail/termtools/attachments/20160817/538f9e9d/attachment.html>