search

dynaroars / dig

DIG is a numerical invariant generation tool. It infers program invariants or properties over (i) program execution traces or (ii) program source code. DIG supports many forms of numerical invariants, including nonlinear equalities, octagonal and interval properties, min/max-plus relations, and congruence relations.
https://github.com/dynaroars/dig
MIT License
38 stars 6 forks source link

Some problems encountered while testing custom cases #50

Closed WindOctober closed 2 months ago

WindOctober commented 3 months ago

While testing the code from a previous issue #24, I used the command:

time ~/miniconda3/bin/python3 -O dig.py ../data/const_1-1.c -log 4 -maxdeg 2 -nominmax -nomp -nominmaxplus -seed 0

to test the following code:

#include <stdio.h>
#include <stdlib.h>

void vassume(int b){}
void vtrace1(int x, int y){} 

void mainQ( ){ 
  int x,y;
  x=1;
  y=0;
  vassume (x==1 && y==0);
  while(x<=100){// loop invariant:2x-y^2==y
    vtrace1(x,y);
    y=y+1;
    x=x+y;
   } 
}

void main(int argc, char **argv){
    mainQ();
}

However, I encountered the following error:

settings:INFO:2024-04-10 02:47:01.434439: dig.py ../data/const_1-1.c -log 4 -maxdeg 2 -nominmax -nomp -nominmaxplus -seed 0
alg:INFO:analyzing '../data/const_1-1.c'
alg:DEBUG:seed=0.0 (test 49)
Traceback (most recent call last):
  File "/dig/src/dig.py", line 271, in <module>
    dinvs = dig.start(seed=seed, maxdeg=args.maxdeg)
            ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/dig/src/alg.py", line 113, in start
    self.mysrc = self.mysrc_cls(self.filename, self.tmpdir_del)
                 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/dig/src/data/prog.py", line 357, in __init__
    typ = instrument(self.filename, self.tracefile, self.symexefile)
          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/dig/src/c_instrument.py", line 170, in instrument
    vis.visit(ast_civl)
  File "/root/miniconda3/lib/python3.12/site-packages/pycparser/c_ast.py", line 158, in visit
    return visitor(node)
           ^^^^^^^^^^^^^
  File "/root/miniconda3/lib/python3.12/site-packages/pycparser/c_ast.py", line 165, in generic_visit
    self.visit(c)
  File "/root/miniconda3/lib/python3.12/site-packages/pycparser/c_ast.py", line 158, in visit
    return visitor(node)
           ^^^^^^^^^^^^^
  File "/dig/src/c_instrument.py", line 101, in visit_FuncDef
    nts = [(p.name , p.type.type.names[0]) for p in node.decl.type.args.params]
                                                    ^^^^^^^^^^^^^^^^^^^^^^^^^^
AttributeError: 'NoneType' object has no attribute 'params'
WindOctober commented 3 months ago

Based on the error, it seems like it is required for the function to have parameters? When I tried to run my custom program that does not take any parameters and solve for invariants, I noticed that all the functions in the examples depend on some variables from external inputs. How can I test programs that do not depend on external inputs?

nguyenthanhvuh commented 3 months ago

Yes it appears so. Could you add a couple of "fake" params ? E.g., 

void mainQ(int fx, int fy){ 
  int x,y;
  x=1;
  y=0;
  vassume (x==1 && y==0);
  while(x<=100){// loop invariant:2x-y^2==y
    vtrace1(x,y,fx,fy);
    y=y+1;
    x=x+y;
   } 
}

void main(int argc, char **argv){
    mainQ(atoi(argv[1]), atoi(argv[2]));
}
WindOctober commented 3 months ago

An odd thing is, when I tested another example, although vtrace1 inside the loop can calculate the results normally, as follows:

#include <stdio.h>
#include <stdlib.h>

void vassume(int b) {}
void vtrace1(int x, int y, int fx, int fy) {}
void vtrace2(int x, int y, int fx, int fy) {}
void mainQ(int fx, int fy)
{
  unsigned int x = 1;
  unsigned int y = 0;

  while (y < 1024)
  {
    vtrace1(x, y, fx, fy);
    x = 0;
    y++;
  }
  vtrace2(x, y, fx, fy);
  return;
}

void main(int argc, char **argv)
{
  mainQ(atoi(argv[1]), atoi(argv[2]));
}

and corresponding results are:

settings:INFO:2024-04-10 04:50:44.384414: dig.py ../data/const_1-1.c -log 4 -maxdeg 2 -nominmax -nomp -nominmaxplus -seed 0
alg:INFO:analyzing '../data/const_1-1.c'
alg:DEBUG:seed=0.0 (test 49)
data.symstates:DEBUG:/usr/bin/java -jar ../EXTERNAL_FILES/civl/lib/civl-1.22_5854.jar verify -maxdepth=20 /var/tmp/dig_0_2bz24ttp/delete_me/symexe/const_1-1.c
data.symstates:DEBUG:got 9 symstates at depth 20
data.symstates:DEBUG:/usr/bin/java -jar ../EXTERNAL_FILES/civl/lib/civl-1.22_5854.jar verify -maxdepth=21 /var/tmp/dig_0_2bz24ttp/delete_me/symexe/const_1-1.c
data.symstates:DEBUG:got 9 symstates at depth 21
data.symstates:DEBUG:/usr/bin/java -jar ../EXTERNAL_FILES/civl/lib/civl-1.22_5854.jar verify -maxdepth=22 /var/tmp/dig_0_2bz24ttp/delete_me/symexe/const_1-1.c
data.symstates:DEBUG:got 10 symstates at depth 22
data.symstates:DEBUG:/usr/bin/java -jar ../EXTERNAL_FILES/civl/lib/civl-1.22_5854.jar verify -maxdepth=23 /var/tmp/dig_0_2bz24ttp/delete_me/symexe/const_1-1.c
data.symstates:DEBUG:got 10 symstates at depth 23
data.symstates:DEBUG:/usr/bin/java -jar ../EXTERNAL_FILES/civl/lib/civl-1.22_5854.jar verify -maxdepth=24 /var/tmp/dig_0_2bz24ttp/delete_me/symexe/const_1-1.c
data.symstates:DEBUG:got 11 symstates at depth 24
data.symstates:DEBUG:/usr/bin/java -jar ../EXTERNAL_FILES/civl/lib/civl-1.22_5854.jar verify -maxdepth=25 /var/tmp/dig_0_2bz24ttp/delete_me/symexe/const_1-1.c
data.symstates:DEBUG:got 11 symstates at depth 25
data.symstates:DEBUG:/usr/bin/java -jar ../EXTERNAL_FILES/civl/lib/civl-1.22_5854.jar verify -maxdepth=26 /var/tmp/dig_0_2bz24ttp/delete_me/symexe/const_1-1.c
data.symstates:DEBUG:got 12 symstates at depth 26
data.symstates:DEBUG:/usr/bin/java -jar ../EXTERNAL_FILES/civl/lib/civl-1.22_5854.jar verify -maxdepth=27 /var/tmp/dig_0_2bz24ttp/delete_me/symexe/const_1-1.c
data.symstates:DEBUG:got 12 symstates at depth 27
data.symstates:DEBUG:/usr/bin/java -jar ../EXTERNAL_FILES/civl/lib/civl-1.22_5854.jar verify -maxdepth=28 /var/tmp/dig_0_2bz24ttp/delete_me/symexe/const_1-1.c
data.symstates:DEBUG:got 13 symstates at depth 28
data.symstates:DEBUG:/usr/bin/java -jar ../EXTERNAL_FILES/civl/lib/civl-1.22_5854.jar verify -maxdepth=29 /var/tmp/dig_0_2bz24ttp/delete_me/symexe/const_1-1.c
data.symstates:DEBUG:got 13 symstates at depth 29
data.symstates:DEBUG:/usr/bin/java -jar ../EXTERNAL_FILES/civl/lib/civl-1.22_5854.jar verify -maxdepth=30 /var/tmp/dig_0_2bz24ttp/delete_me/symexe/const_1-1.c
data.symstates:DEBUG:got 14 symstates at depth 30
data.symstates:DEBUG:vtrace1: no new symstates at depth 21
data.symstates:DEBUG:vtrace1: no new symstates at depth 23
data.symstates:DEBUG:vtrace1: no new symstates at depth 25
data.symstates:DEBUG:vtrace1: no new symstates at depth 27
data.symstates:DEBUG:vtrace1: no new symstates at depth 29
data.symstates:DEBUG:loc vtrace1 depth 20 has 9 uniq symstates
data.symstates:DEBUG:loc vtrace1 depth 22 has 1 uniq symstates
data.symstates:DEBUG:loc vtrace1 depth 24 has 1 uniq symstates
data.symstates:DEBUG:loc vtrace1 depth 26 has 1 uniq symstates
data.symstates:DEBUG:loc vtrace1 depth 28 has 1 uniq symstates
data.symstates:DEBUG:loc vtrace1 depth 30 has 1 uniq symstates
alg:INFO:got 14 symstates for 1 locs: ['vtrace1']
alg:WARNING:vtrace2: no symbolic states. Skip
alg:INFO:got symbolic states in 35.30s
alg:DEBUG:infer 'eqts' at 1 locs
helpers.miscs:DEBUG:using deg 2
infer.eqt:DEBUG:vtrace1: generate random initial inps (curr inps 0, traces 0)
infer.eqt:DEBUG:vtrace1: need more traces (0 eqts, need >= 22, inps 0)
data.prog:DEBUG:/var/tmp/dig_0_2bz24ttp/delete_me/traces/const_1-1.exe 24 28
data.prog:DEBUG:/var/tmp/dig_0_2bz24ttp/delete_me/traces/const_1-1.exe 14 3
data.prog:DEBUG:/var/tmp/dig_0_2bz24ttp/delete_me/traces/const_1-1.exe 296 4
data.prog:DEBUG:/var/tmp/dig_0_2bz24ttp/delete_me/traces/const_1-1.exe 7 11
data.prog:DEBUG:/var/tmp/dig_0_2bz24ttp/delete_me/traces/const_1-1.exe 9 298
data.prog:DEBUG:/var/tmp/dig_0_2bz24ttp/delete_me/traces/const_1-1.exe 8 8
data.prog:DEBUG:/var/tmp/dig_0_2bz24ttp/delete_me/traces/const_1-1.exe 299 295
data.prog:DEBUG:/var/tmp/dig_0_2bz24ttp/delete_me/traces/const_1-1.exe 13 271
data.prog:DEBUG:/var/tmp/dig_0_2bz24ttp/delete_me/traces/const_1-1.exe 285 12
infer.eqt:DEBUG:gen 27 random inps
data.prog:DEBUG:/var/tmp/dig_0_2bz24ttp/delete_me/traces/const_1-1.exe 19 295
data.prog:DEBUG:/var/tmp/dig_0_2bz24ttp/delete_me/traces/const_1-1.exe 24 1
data.prog:DEBUG:/var/tmp/dig_0_2bz24ttp/delete_me/traces/const_1-1.exe 14 6
data.prog:DEBUG:/var/tmp/dig_0_2bz24ttp/delete_me/traces/const_1-1.exe 4 14
data.prog:DEBUG:/var/tmp/dig_0_2bz24ttp/delete_me/traces/const_1-1.exe 25 19
data.prog:DEBUG:/var/tmp/dig_0_2bz24ttp/delete_me/traces/const_1-1.exe 1 5
data.prog:DEBUG:/var/tmp/dig_0_2bz24ttp/delete_me/traces/const_1-1.exe 286 4
data.prog:DEBUG:/var/tmp/dig_0_2bz24ttp/delete_me/traces/const_1-1.exe 8 285
data.prog:DEBUG:/var/tmp/dig_0_2bz24ttp/delete_me/traces/const_1-1.exe 19 20
data.prog:DEBUG:/var/tmp/dig_0_2bz24ttp/delete_me/traces/const_1-1.exe 15 287
data.prog:DEBUG:/var/tmp/dig_0_2bz24ttp/delete_me/traces/const_1-1.exe 293 2
data.prog:DEBUG:/var/tmp/dig_0_2bz24ttp/delete_me/traces/const_1-1.exe 4 273
data.prog:DEBUG:/var/tmp/dig_0_2bz24ttp/delete_me/traces/const_1-1.exe 21 5
data.prog:DEBUG:/var/tmp/dig_0_2bz24ttp/delete_me/traces/const_1-1.exe 298 297
data.prog:DEBUG:/var/tmp/dig_0_2bz24ttp/delete_me/traces/const_1-1.exe 279 274
data.prog:DEBUG:/var/tmp/dig_0_2bz24ttp/delete_me/traces/const_1-1.exe 283 5
data.prog:DEBUG:/var/tmp/dig_0_2bz24ttp/delete_me/traces/const_1-1.exe 14 4
data.prog:DEBUG:/var/tmp/dig_0_2bz24ttp/delete_me/traces/const_1-1.exe 287 11
infer.eqt:DEBUG:got 27648 new traces
infer.eqt:DEBUG:vtrace1, iter 1 infer using 22 exprs
helpers.miscs:DEBUG:solving 15 uks using 22 eqts
helpers.miscs:DEBUG:got 5 eqts after instantiating
helpers.miscs:DEBUG:Grobner basis: from 5 to 1 ps
helpers.miscs:DEBUG:got 1 eqts after refinement
infer.eqt:DEBUG:vtrace1: 1 candidates: x == 0
infer.eqt:DEBUG:vtrace1: check 1 unchecked (1 candidates)
data.symstates:DEBUG:checking 1 invs:
vtrace1 (1 invs):
1. x == 0
infer.eqt:DEBUG:vtrace1: 1 new cex exprs
infer.eqt:DEBUG:vtrace1, iter 2 infer using 23 exprs
helpers.miscs:DEBUG:solving 15 uks using 23 eqts
helpers.miscs:DEBUG:got 4 eqts after instantiating
helpers.miscs:DEBUG:Grobner basis: from 4 to 4 ps
helpers.miscs:DEBUG:got 4 eqts after refinement
infer.eqt:DEBUG:vtrace1: 4 candidates: x**2 - x == 0; fx*x == 0; x*y == 0; fy*x == 0
infer.eqt:DEBUG:vtrace1: check 4 unchecked (4 candidates)
data.symstates:DEBUG:checking 4 invs:
vtrace1 (4 invs):
1. x*y == 0
2. fx*x == 0
3. fy*x == 0
4. x**2 - x == 0
infer.eqt:DEBUG:vtrace1: 2 new cex exprs
infer.eqt:DEBUG:vtrace1, iter 3 infer using 25 exprs
helpers.miscs:DEBUG:solving 15 uks using 25 eqts
helpers.miscs:DEBUG:got 2 eqts after instantiating
helpers.miscs:DEBUG:Grobner basis: from 2 to 2 ps
helpers.miscs:DEBUG:got 2 eqts after refinement
infer.eqt:DEBUG:vtrace1: no new results -- break
infer.eqt:DEBUG:vtrace1: got 2 eqts
infer.eqt:DEBUG:x**2 - x == 0
x*y == 0
alg:INFO:got 2 eqts in 1.35s
alg:DEBUG:vtrace1 (2 invs):
1. x*y == 0 p
2. x**2 - x == 0 p
alg:DEBUG:infer 'ieqs' at 1 locs
infer.infer:DEBUG:32 terms for Infer
helpers.miscs:DEBUG:filter terms: removed 4 invs in 0.00s (orig 32, new 28)
infer.infer:DEBUG:checking upperbounds for 28 terms at 1 locs
data.symstates:DEBUG:checking 28 invs:
vtrace1 (28 invs):
1. x <= 20
2. y <= 20
3. -y <= 20
4. -x <= 20
5. fx <= 20
6. fy <= 20
7. -fx <= 20
8. -fy <= 20
9. x + y <= 20
10. x - y <= 20
11. -x + y <= 20
12. fx - x <= 20
13. fx + y <= 20
14. fy - y <= 20
15. fy - x <= 20
16. -x - y <= 20
17. fx - y <= 20
18. fy + y <= 20
19. fx + x <= 20
20. fy + x <= 20
21. ...
infer.infer:DEBUG:inferring upperbounds for 8 terms at 1 locs
data.symstates:DEBUG:max depth diff -1*x + y: 8 sat @depth 20, 9 sat @depth 22
data.symstates:DEBUG:max depth diff -1*x + y: 9 sat @depth 22, 10 sat @depth 24
data.symstates:DEBUG:max depth diff -1*x + y: 10 sat @depth 24, 11 sat @depth 26
data.symstates:DEBUG:max depth diff -1*x + y: 11 sat @depth 26, 12 sat @depth 28
data.symstates:DEBUG:value of -1*x + y changes frequently, skip
data.symstates:DEBUG:max depth diff x + y: 8 sat @depth 20, 9 sat @depth 22
data.symstates:DEBUG:max depth diff x + y: 9 sat @depth 22, 10 sat @depth 24
data.symstates:DEBUG:max depth diff x + y: 10 sat @depth 24, 11 sat @depth 26
data.symstates:DEBUG:max depth diff x + y: 11 sat @depth 26, 12 sat @depth 28
data.symstates:DEBUG:value of x + y changes frequently, skip
data.symstates:DEBUG:max depth diff y: 8 sat @depth 20, 9 sat @depth 22
data.symstates:DEBUG:max depth diff y: 9 sat @depth 22, 10 sat @depth 24
data.symstates:DEBUG:max depth diff y: 10 sat @depth 24, 11 sat @depth 26
data.symstates:DEBUG:max depth diff y: 11 sat @depth 26, 12 sat @depth 28
data.symstates:DEBUG:value of y changes frequently, skip
alg:INFO:got 5 ieqs in 2.28s
alg:DEBUG:vtrace1 (5 invs):
1. x <= 1 p
2. -x <= 0 p
3. -y <= 0 p
4. x - y <= 1 p
5. -x - y <= -1 p
alg:DEBUG:check 7 invs using 27648 traces
helpers.miscs:DEBUG:test_dinvs: removed 0 invs in 28.39s (orig 7, new 7)
alg:INFO:check 7 invs using 27648 traces (28.39s)
alg:DEBUG:simplify 7 invs
alg:DEBUG:vtrace1 (7 invs):
1. x*y == 0
2. x**2 - x == 0
3. x <= 1
4. -x <= 0
5. -y <= 0
6. x - y <= 1
7. -x - y <= -1
helpers.miscs:DEBUG:_simplify_slow eqts: removed 0 invs in 0.05s (orig 2, new 2)
helpers.miscs:DEBUG:_simplify_fast octs: removed 2 invs in 0.10s (orig 3, new 1)
helpers.miscs:DEBUG:_simplify_slow octs_simple: removed 0 invs in 0.06s (orig 2, new 2)
infer.inv:DEBUG:done simplifying , time 0.20763182640075684
helpers.miscs:DEBUG:simplify: removed 2 invs in 0.21s (orig 7, new 5)
alg:INFO:simplify 7 invs (0.21s)
* prog const_1-1 locs 1; invs 5 (Eqt: 2, Oct: 3) V 2 T 2 D 2; NL 2 (2) ;
-> time symbolic_states 35.3s, eqts 1.4s, ieqs 2.3s, simplify 28.6s, total 67.7s
rand seed 0.0, test 56
tmpdir: /var/tmp/dig_0_2bz24ttp
vtrace1 (5 invs):
1. x*y == 0
2. x**2 - x == 0
3. -x <= 0
4. -y <= 0
5. -x - y <= -1

real    1m9.422s
user    3m38.481s
sys     0m19.901s

However, vtrace2 after exiting the loop gets ignored. When I comment out vtrace1 and only keep vtrace2 for calculation, the following error occurs:

settings:INFO:2024-04-10 04:52:54.231654: dig.py ../data/const_1-1.c -log 4 -maxdeg 2 -nominmax -nomp -nominmaxplus -seed 0
alg:INFO:analyzing '../data/const_1-1.c'
alg:DEBUG:seed=0.0 (test 49)
data.symstates:DEBUG:/usr/bin/java -jar ../EXTERNAL_FILES/civl/lib/civl-1.22_5854.jar verify -maxdepth=20 /var/tmp/dig_0_poypiaxa/delete_me/symexe/const_1-1.c
data.symstates:DEBUG:/usr/bin/java -jar ../EXTERNAL_FILES/civl/lib/civl-1.22_5854.jar verify -maxdepth=21 /var/tmp/dig_0_poypiaxa/delete_me/symexe/const_1-1.c
data.symstates:DEBUG:/usr/bin/java -jar ../EXTERNAL_FILES/civl/lib/civl-1.22_5854.jar verify -maxdepth=22 /var/tmp/dig_0_poypiaxa/delete_me/symexe/const_1-1.c
data.symstates:DEBUG:/usr/bin/java -jar ../EXTERNAL_FILES/civl/lib/civl-1.22_5854.jar verify -maxdepth=23 /var/tmp/dig_0_poypiaxa/delete_me/symexe/const_1-1.c
data.symstates:DEBUG:/usr/bin/java -jar ../EXTERNAL_FILES/civl/lib/civl-1.22_5854.jar verify -maxdepth=24 /var/tmp/dig_0_poypiaxa/delete_me/symexe/const_1-1.c
data.symstates:DEBUG:/usr/bin/java -jar ../EXTERNAL_FILES/civl/lib/civl-1.22_5854.jar verify -maxdepth=25 /var/tmp/dig_0_poypiaxa/delete_me/symexe/const_1-1.c
data.symstates:DEBUG:/usr/bin/java -jar ../EXTERNAL_FILES/civl/lib/civl-1.22_5854.jar verify -maxdepth=26 /var/tmp/dig_0_poypiaxa/delete_me/symexe/const_1-1.c
data.symstates:DEBUG:/usr/bin/java -jar ../EXTERNAL_FILES/civl/lib/civl-1.22_5854.jar verify -maxdepth=27 /var/tmp/dig_0_poypiaxa/delete_me/symexe/const_1-1.c
data.symstates:DEBUG:/usr/bin/java -jar ../EXTERNAL_FILES/civl/lib/civl-1.22_5854.jar verify -maxdepth=28 /var/tmp/dig_0_poypiaxa/delete_me/symexe/const_1-1.c
data.symstates:DEBUG:/usr/bin/java -jar ../EXTERNAL_FILES/civl/lib/civl-1.22_5854.jar verify -maxdepth=29 /var/tmp/dig_0_poypiaxa/delete_me/symexe/const_1-1.c
data.symstates:DEBUG:/usr/bin/java -jar ../EXTERNAL_FILES/civl/lib/civl-1.22_5854.jar verify -maxdepth=30 /var/tmp/dig_0_poypiaxa/delete_me/symexe/const_1-1.c
data.symstates:WARNING:cannot obtain symstates, unreachable locs?

real    0m36.562s
user    3m10.850s
sys     0m18.791s
WindOctober commented 3 months ago

I understand the reason, which is roughly similar to BMC, requiring loop unrolling? Within a limited number of unrollings, it is impossible to reach the postcondition here, so it would indicate unreachable locations? I further tested the situation with an indeterminate number of loop iterations, as follows:

#include <stdio.h>
#include <stdlib.h>

void vassume(int b) {}
void vtrace1(int x, int y, int fx, int fy) {}
void vtrace_post(int x, int y, int fx, int fy) {}
void mainQ(int fx, int fy)
{
  unsigned int x = 1;
  unsigned int y = 0;

  while (y < fx)
  {
    x = 0;
    y++;
    vtrace1(x, y, fx, fy);
  }
  vtrace_post(x, y, fx, fy);
  return;
}

void main(int argc, char **argv)
{
  mainQ(atoi(argv[1]), atoi(argv[2]));
}

But in this case, the code can normally output the invariant of vtrace_post(). It seems like this issue could be resolved at the code level.

nguyenthanhvuh commented 3 months ago

Yes, I think it's due to loop unrolling. DIG invokes CIVL, a symbolic execution tool for C, to obtain symbolic states. CIVL will perform symbolic execution up to specified depth and if it cannot reach the location by then DIG will report unreachable location. You can increase the depth by giving DIG the option --se_maxdepth SE_MAXDEPTH.

WindOctober commented 3 months ago

Thank you for your reply. Lastly, I would like to inquire about testing cases with uncertain inputs, such as a variable in a loop that is assigned a random value during each iteration. Does DIG offer a function that can express uncertain values (in non-constant loops)? For example, the __VERIFIER_nondet_uint() in SV-COMP. An illustrative example is as follows:

int main(void) {
  unsigned int s = 0;
  while (__VERIFIER_nondet_uint()) {
    if (s != 0) {
      ++s;
    }
    if (__VERIFIER_nondet_uint()) {
      __VERIFIER_assert(s == 0);
    }
  }
  return 0;
}
nguyenthanhvuh commented 2 months ago

I haven't tried this kind of programs. The dynamic inference part of DIG does not care about this as it just look at traces. But the symbolic execution tool CIVL might have problem analyzing nondet (it might have ways to deal with it, but I have never investigated).

WindOctober commented 2 months ago

Thank you for your response; I now understand the reasons behind the issue mentioned.